Validating the PSL/Sugar Semantics Using Automated Reasoning
- 1 December 2003
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 15 (4) , 406-421
- https://doi.org/10.1007/s00165-003-0014-5
Abstract
: The Accellera organisation selected Sugar, IBM’s formal specification language, as the basis for a standard to ‘drive assertion-based verification’ in the electronics industry. Sugar combines regular expressions, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) into a property language intended for both static verification (e.g. model checking) and dynamic verification (e.g. simulation). In 2003 Accellera decided to rename the evolving standard to ‘Accellera Property Specification Language’ (or ‘PSL’ for short). We motivate and describe a deep semantic embedding of PSL in the version of higher-order logic supported by the HOL 4 theorem-proving system. The main goal of this paper is to demonstrate that mechanised theorem proving can be a useful aid to the validation of the semantics of an industrial design language.Keywords
This publication has 4 references indexed in Scilit:
- A hardware semantics based on temporal intervalsPublished by Springer Nature ,2005
- Foundations of Software Science and Computation StructuresPublished by Springer Nature ,2003
- Isabelle/HOLPublished by Springer Nature ,2002
- An integration of model checking with automated proof checkingPublished by Springer Nature ,1995