An integrated environment for HDL verification

The functional verification of a digital design is an expensive step in the design process. As designs become more complex, simulation is challenged throughout the design and verification process, both at the low level (implementation verification), to show that a low level implementation implements a higher-level specification, and at the high level (design verification), to show that a design complies with some abstract specification. In both areas, formal methods can extend the reach of simulation: for implementation verification, equivalence checking is used to show that two circuits are functionally the same in some well defined sense. For design verification, model checking and other property checking techniques serve as a smart simulator. This paper describes Forte, a formal verification prototype that integrates formal verification and simulation. Forte fits into a standard top-down design flow using standard HDL's such as Verilog-HDL and VHDL, and works well with synthesis. Forte includes traditional and symbolic simulation, combinational and sequential equivalence, and CTL model checking. We discuss its design and implementation, and illustrate the utility of combining formal verification and simulation using an example. Moreover, Forte's object-oriented design makes it an ideal platform for rapidly evaluating new ideas in verification.