Integrating formal verification methods with a conventional project design flow
ásgeir þór Eiríksson · 1996
We present a formal verification methodology that we have used on a computer system design project.The methodology integrates a temporal logic model checker with a conventional project design flow.The methodology has been used successfully to verify the protocols within a distributed shared memory machine.We consider the following to be the four main benefits to using the model checker.First, it ensures that there exists an accurate high-level machine readable system specification.Second, it allows high-level system verification early in the design phase.Third, it facilitates equivalence and refinement checking between the high-level specification, and the RTL implementation.Finally, and most importantly it uncovered many protocol specification and RTL implementation problems.