Validating the PSL/Sugar Semantics Using Automated Reasoning
Formal Asp. Comput.(2003)
摘要
. 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.
更多查看译文
关键词
Accellera,Formal verification,Higher-order logic,HOL,Model checking,Property language,PSL,Semantics,Sugar,Theorem proving
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络