Efficient Automata-Based Assertion-Checker Synthesis of SEREs for Hardware Emulation

In this paper, we present a method for generating checker circuits from sequential-extended regular expressions (SEREs). Such sequences form the core of increasingly-used assertion-based verification (ABV) languages. A checker generator capable of transforming assertions into efficient circuits allows the adoption of ABV in hardware emulation. Towards that goal, we introduce the algorithms for sequence fusion and length matching intersection, two SERE operators that are not typically used over regular expressions. We also develop an algorithm for generating failure detection automata, a concept critical to extending regular expressions for ABV, as well as present our efficient symbol encoding. Experiments with complex sequences show that our tool outperforms the best known checker generator.