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.

• Type: Journal
• Year: 2008
• Where: TODAES
• Authors: Marc Boule, Zeljko Zilic
• Keywords: Automata-based Checker Generation, Automata-based Methods, PSL Hardware Assertion, TODAES 2008