Incorporating efficient assertion checkers into hardware emulation

Assertion-based verification (ABV) is emerging as a paramount technique for industrial-strength hardware verification, especially through the emerging property specification language (PSL). Since PSL introduces significant overhead to simulators, in this paper we present the infrastructure for hardware emulation capable of supporting ABV. We develop a tool that generates hardware assertion checkers for inclusion into efficient circuit emulation. The MBAC checker generator is outlined, together with the algorithms for optimized assertion-circuit generation. Experiments show that MBAC outperforms the best known checker-generator.