Design intent coverage revisited

ABSTRACT

Design intent coverage is a formal methodology for analyzing the gap between a formal architectural specification of a design and the formal functional specifications of the component RTL blocks of the design. In this article we extend the design intent coverage methodology to hybrid specifications containing both state-machines and formal properties. We demonstrate the benefits of this extension in two domains of considerable recent interest, namely (a) the use of auxiliary state-machines in formal specifications, and (b) the use of modest sized RTL blocks in the design intent coverage analysis.

REFERENCES

• 1: Basu, P., Das, S., Banerjee, A., P. Dasgupta, P. P. C., Mohan, C., Fix, L., and Armoni, R. 2006. Design intent coverage—a new paradigm for formal property verification. Comput.-Aid. Des. Int. Circ. Syst. 25, 10, 1922--1934.
• 2: Hana Chockler , Orna Kupferman , Robert P. Kurshan , Moshe Y. Vardi, A Practical Approach to Coverage in Model Checking, Proceedings of the 13th International Conference on Computer Aided Verification, p.66-78, July 18-22, 2001
• 3: Hana Chockler , Orna Kupferman , Moshe Y. Vardi, Coverage Metrics for Temporal Logic Model Checking, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.528-542, April 02-06, 2001
• 4: Chockler, H., Kupferman, O., and Vardi, Y. M. 2003. Coverage metrics for formal verification. In Proceedings of the 12^th Advanced Research Working Conference on Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science, vol. 2860, Springer, 111--125.
• 5: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 6: Sayantan Das , Prasenjit Basu , Pallab Dasgupta , P. P. Chakrabarti, What lies between design intent coverage and model checking?, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
• 7: Pallab Dasgupta, A Roadmap for Formal Property Verification, Springer-Verlag New York, Inc., Secaucus, NJ, 2006
• 8: Yatin Hoskote , Timothy Kam , Pei-Hsin Ho , Xudong Zhao, Coverage estimation for symbolic model checking, Proceedings of the 36th ACM/IEEE conference on Design automation, p.300-305, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309936]
• 9: Sagi Katz , Orna Grumberg , Daniel Geist, "Have I written enough Properties?" - A Method of Comparison between Specification and Implementation, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.280-297, September 27-29, 1999
• 10: Pnueli, A. 1977. The complexity of propositional linear temporal logics. In Proceedings of the Foundations of Computer Science. 46--57.
• 11: PSL. Property Specification Language (PSL). www.eda.org/vfv/docs/PSL-v1.1.pdf. PSL.
• 12: A. P. Sistla , E. M. Clarke, The complexity of propositional linear temporal logics, Journal of the ACM (JACM), v.32 n.3, p.733-749, July 1985 [doi>10.1145/3828.3837]
• 13: SVA. SystemVerilog 3.1a Language Reference Manual. www.eda.org/sv/SystemVerilog_3.1a.pdf. SVA.

INDEX TERMS

General Terms:
Verification

Keywords:
Design Intent Coverage