Automata-based assertion-checker synthesis of PSL properties
Automata-based assertion-checker synthesis of PSL properties
复制标题
基于自动机的 PSL 属性断言检查器综合
DOI：
10.1145/1297666.1297670
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Z. Zilic
中科院分区：
文献类型：
--
作者：
M. Boule;Z. Zilic
使用PSL等语言的基于断言的验证越来越重要。从断言，可以生成硬件断言检查器，用于仿真，仿真加速和硅调试。我们提出的技术检查生成的完整的PSL属性，包括所有的变体的运营商，强和弱。基于全自动机的方法允许整个断言由单个自动机表示，因此允许在模块化方法中无法完成的优化，其中仅为单个运算符创建子电路。为此，自动机算法的基本情况下，和一套完整的重写规则推导出其他运营商。自动机分裂是为了有效地实现最终！操作符.
Assertion-based verification with languages such as PSL is gaining in importance. From assertions, one can generate hardware assertion checkers for use in emulation, simulation acceleration and silicon debug. We present techniques for checker generation of the complete set of PSL properties, including all variants of operators, both strong and weak. A full automata-based approach allows an entire assertion to be represented by a single automaton, hence allowing optimizations that can not be done in a modular approach where subcircuits are created only for individual operators. For this purpose, automata algorithms are developed for the base cases, and a complete set of rewrite rules is derived for other operators. Automata splitting is introduced for an efficient implementation of the eventually! operator.