A Case for Multi-level Combination of Theorem Proving and Model Checking Tools

We are combining ACL2 theorem proving with an off-the-shelf commercial model checker to verify a functional unit that would have been hard to verify by just using either of the two approaches. It is essential that our combination of the two tools allows for results of either of the tools to be used for the other tool in both directions. The unit is a packed integer multiplier that can handle a variety of multiplication operations on signed and unsigned integer operands ranging from 8 bits to 32 bits. The implementation of the unit is targeting low-power operation and is described in production RTL. The combination of the two verification approaches builds on the strengths and works around the challenges of each of the two approaches. Communication between the two approaches is based on a standard Veriloginterface. In this manuscript we are describing the verification environment and explain details of the verification project.