There has been a growing interest in applying formal methods for functional and performance verification of complex and safety critical designs. Model checking is one of the most common formal verification methodologies utilized in verifying sequential logic due to its automated decision procedures and its ability to provide "counter examples" for debugging. However, model checking hasn't found broad acceptance as a verification methodology due to its complexity. This arises because of the need to specify correctness properties in a temporal logic language and develop an environment around a partitioned model under test in a non deterministic HDL-type language. Generally, engineers are not trained in mathematical logic languages and becoming proficient in such a language requires a steep learning curve. Furthermore, defining a behavioral environment at the complex and undocumented microarchitectural interface level is a time consuming and error prone activity. As such, there is a strong motivation to bring the model checking technology to a level such that the designers may utilize this technology as a part of their design process without being burdened with the details that are generally only within the grasps of computer theoreticians. The paper outlines two tools which greatly assist in this goal: the first, Polly, automates the difficult and error prone task of developing the behavioral environment around the partitioned model under test; the second Oracle, obviates the need for learning temporal logic to enter specification.
展开▼
