AbstractA formal verification technique is presented which is suitable for the verification of standard components (cores) for programmable hardware (FPGAs). This technique can be viewed as a suitable complement to traditional techniques, such as simulation. We describe the modelling and verification of combinational and sequential components using the formal verification tool NP-Tools, and report successful verification of real cores.
Categories and Subject Descriptors: B.6.3 [Logic Design]: Design Aids; D.2.4 [Software Engineering]: Program Verification
Additional Key Words and Phrases: formal verification, cores, reconfigurable cores, core development methodology, intellectual property, FPGAs, equivalence checking, Stålmarck's Method
Selected references
- Randal E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293-318, September 1992.
- J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 10^{20} states and beyond. Information and Computation, 98(2):142-170, June 1992.
- Mike Gordon. The semantic challenge of verilog HDL. In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 136-145, San Diego, California, 26-29 June 1995. IEEE Computer Society Press.