Efficient Automata-Based Assertion-Checker Synthesis of PSL Properties

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