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 "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.

AUTHOR
Mike Gordon

DOWNLOAD
[postscript | pdf ]

PUBLICATION
To be published in the special issue of the Formal Aspects of Computing Journal on Semantic Foundations of Engineering Design Languages (expected sometime in 2003).