Applying Model-Checking to Post-Silicon-Verification: Bridging the Specification-Realisation Gap

We present a new methodology for Formal Verification of “Concrete” Digital Circuits. We apply Model checking to a Field Programmable Gate Array (FPGA)-based prototype of the circuit. We are able to establish or demonstrate a working bridge between circuit behaviors in the abstract world of specification, modelling and analysis, and the ones in the post-silicon domain. We suggest that, compared to conventional hardware design techniques, this approach 1) can operate at a much higher level of abstraction, 2) offers automated testing of the physical device in contrast to just a model, 3) reduces or eliminates laborious and time-consuming simulations, 4) is orders of magnitude faster than an HDL (Hardware Description Language) simulator, and, 5) is very suitable for Hardware/software co-design.