Shortening the verification cycle with synthesizable abstract models

Abstract modeling has been widely used, albeit independently, for both formal verification and high-level modeling of SoC designs. In this paper we show that proper selection of modeling language and abstraction level can make the same code useful for both formal and simulation-based techniques. The abstract model enables architecture exploration and the development of verification collateral pre-RTL, and can be used as a behavioral checker in simulation against the RTL and in hardware emulation. In parallel, it enables applying formal verification techniques to verify the specification and implementation of the design. We provide examples of the successful application of abstract models developed in SystemVerilog in the course of the verification of the newest Intel^reg Coretrade microprocessor.