Automata-based assertion-checker synthesis of PSL properties

10 years 11 months ago
Automata-based assertion-checker synthesis of PSL properties
Abstract-- Automata-based methods for generating PSL hardware assertion checkers were primarily considered for use with temporal sequences, as opposed to full-scale properties. We present a technique for automata-based checker generation of PSL properties for dynamic verification. A full automata-based approach allows an entire assertion to be represented by a single automaton, hence allowing optimizations which can not be done in a modular approach where sub-circuits 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 developed and applied for all other operators. We show that the generated checkers are resource-efficient for use in hardware emulation, simulation acceleration and silicon debug.
Marc Boule, Zeljko Zilic
Added 29 Dec 2010
Updated 29 Dec 2010
Type Journal
Year 2008
Authors Marc Boule, Zeljko Zilic
Comments (0)