Association for Computing Machinery
Abstract modeling has been widely used, albeit independently, for both formal verification and high-level modeling of SoC designs. In this paper, the authors 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.