Open Computation Tree Logic for Formal Verification of Modules
Pallab Dasgupta, Arindam Chakrabarti, P. P. Chakrabarti · 2002
Modules of large VLSI circuits are often designed by dif-ferent designers spread across the globe. One of the main challenges of the designer is to guarantee that the module he/she designs will work correctly in the global design, the details of which, is often unknown to him/her. Modules are open systems whose behavior is subject to the inputs it re-ceives from its environment. It has been shown that veri-fication of open systems (modules) is computationally very hard (EXPTIME complete [7]) when we consider all pos-sible environments. On the other hand we show that in-tegrating the specification of the properties to be verified with the specification of only the valid input patterns (under which the module is expected to function correctly) gives us a powerful syntax which can be verified in polynomial time. We call the proposed logic Open-CTL (CTL for open systems). The convenience of being able to specify the prop-erty and the environment in a unified way in Open-CTL is demonstrated through a study of the PCI Bus properties. We present a symbolic BDD-based verification scheme for checking Open-CTL formulas, and present experimental re-sults on modules from the Texas-97 Verification Benchmark circuits [12]. 1