Interval Property Checking for Hardware Design Using Satisfiability Modulo Theories Solver ☆

We develop an open source formal verification framework for digital hardware designs based on the Interval Property Checking (IPC) methodology and the Satisfiability Modulo Theories (SMT) technique. The proposed framework formally verifies the Verilog design against interval properties specified in System Verilog Assertion (SVA). In the framework, the IPC problem is mapped into SMT problem which is handled by a SMT solver named Boolector. The framework were able to verify three open source hardware designs that can not be handled by SAT-based IPC. Several bugs in the designs are detected.