Auxiliary state machines + context-triggered properties in verification

ABSTRACT

Formal specifications of interface protocols between a design-under-test and its environment mostly consist of two types of correctness requirements, namely (a) a set of invariants that applies throughout the protocol execution and (b) a set of context-triggered properties that applies only when the protocol state belongs to a specific set of contexts. To model such requirements, an increasingly popular design choice in the assertion IP design community has been the use of abstract context state machines and state-oriented properties. In this paper, we formalize this modeling style and present algorithms for verifying such specifications. Specifically, we present a purely formal approach and a semi-formal approach for verifying such specifications. We demonstrate the use of this design style in modeling some of the industry standard protocol descriptions and present encouraging results.

REFERENCES

• 1: E. Borger , Robert F. Stark, Abstract State Machines: A Method for High-Level System Design and Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 2003
• 2: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 3: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996
• 4: J. R. Burch , E. M. Clarke , D. E. Long, Representing circuits more efficiently in symbolic model checking, Proceedings of the 28th conference on ACM/IEEE design automation, p.403-407, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127702]
• 5: Chauhan, P., Clarke, E. M., Lu, Y., and Wang, D. 1999. Verifying Ip-core based system-on-chip designs. In Proceedings of the ASIC Conference. 27--31.
• 6: Hyunwoo Cho , Gary D. Hachtel , Enrico Macii , Bernard Plessier , Fabio Somenzi, Algorithms for approximate FSM traversal, Proceedings of the 30th international conference on Design automation, p.25-30, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164555]
• 7: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 8: Pallab Dasgupta, A Roadmap for Formal Property Verification, Springer-Verlag New York, Inc., Secaucus, NJ, 2006
• 9: Shankar G. Govindaraju , David L. Dill, Counterexample-guided choice of projections in approximate symbolic model checking, Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design, November 05-09, 2000, San Jose, California
• 10: Matt Kaufmann , Andrew Martin , Carl Pixley, Design Constraints in Symbolic Model Checking, Proceedings of the 10th International Conference on Computer Aided Verification, p.477-487, June 28-July 02, 1998
• 11: M. D. Nguyen , D. Stoffel , M. Wedler , W. Kunz, Transition-by-transition FSM traversal for reachability analysis in bounded model checking, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.1068-1075, November 06-10, 2005, San Jose, CA
• 12: Amir Pnueli, The temporal logic of programs, Proceedings of the 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), p.46-57, September 30-October 31, 1977
• 13: Roberto Sebastiani , Eli Singerman , Stefano Tonetta , Moshe Y. Vardi, GSTE is partitioned model checking, Formal Methods in System Design, v.31 n.2, p.177-196, October 2007 [doi>10.1007/s10703-007-0036-3]
• 14: Kanna Shimizu , David L. Dill , Ching-Tsun Chou, A Specification Methodology by a Collection of Compact Properties as Applied to the Intel® ItaniumTM Processor Bus Protocol, Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.340-354, September 04-07, 2001
• 15: Kanna Shimizu , David L. Dill , Alan J. Hu, Monitor-Based Formal Specification of PCI, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.335-353, November 01-03, 2000
• 16: Smitha Shyam , Valeria Bertacco, Distance-guided hybrid verification with GUIDO, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
• 17: Somenzi, F. 1998. Cudd: CU decision diagram package, release 2.3.0, User's Manual.
• 18: Jin Yang , Carl-Johan H. Seger, Introduction to generalized symbolic trajectory evaluation, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.11 n.3, p.345-353, June 2003 [doi>10.1109/TVLSI.2003.812320]

INDEX TERMS

Primary Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.2 Design Aids
          Subjects: Verification

General Terms:
Verification