Multi-clock SVA synthesis without re-writing

ABSTRACT

This paper presents a compilation procedure for synthesizing multiclock SVA properties for formal verification. The synthesis framework is built upon an existing compilation algorithm for single-clock SVA properties. While we could use the SVA rewriting rules to transform a multi-clock property into a single-clocked property and then apply existing techniques, instead we propose techniques to selectively model the multi-clock operators to produce a smaller checker logic. Through recursive construction and syntactic transformation, we are able demonstrate the efficiency of the technique and the generated checker logic is provably equivalent to the rewritten version.

REFERENCES

• 1: 1800: IEEE Standard for System Verilog -- Unified Hardware Design, Specification, and Verification Language. IEEE Computer Society, 2005.
• 2: Ilan Beer , Shoham Ben-David , Avner Landver, On-the-Fly Model Checking of RCTL Formulas, Proceedings of the 10th International Conference on Computer Aided Verification, p.184-194, June 28-July 02, 1998
• 3: P. Bjesse , J. Kukula, Automatic generalized phase abstraction for formal verification, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.1076-1082, November 06-10, 2005, San Jose, CA
• 4: Edmund Clarke , Armin Biere , Richard Raimi , Yunshan Zhu, Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, v.19 n.1, p.7-34, July 2001 [doi>10.1023/A:1011276507260]
• 5: Ambar A. Gadkari , S. Ramesh, Automated Synthesis of Assertion Monitors using Visual Specifications, Proceedings of the conference on Design, Automation and Test in Europe, p.390-395, March 07-11, 2005 [doi>10.1109/DATE.2005.74]
• 6: M. K. Ganai , A. Gupta, Efficient BMC for Multi-Clock Systems with Clocked Specifications, Proceedings of the 2007 conference on Asia South Pacific design automation, p.310-315, January 23-26, 2007 [doi>10.1109/ASPDAC.2007.358004]
• 7: M. Litteric. Pragmatic simulation-base verification of clock domain crossing signals and jitter using systemverilog assertions. In DVCon, 2006.
• 8: Jiang Long , Andrew Seawright, Synthesizing SVA local variables for formal verification, Proceedings of the 44th annual conference on Design automation, June 04-08, 2007, San Diego, California [doi>10.1145/1278480.1278500]
• 9: J. Long, A. Seawright, K. Larsen, B. Talukdar, and V. Viswanathan. Case study: Annotating ovl with sva assertions. In IP. Design and Reuse, December 2007.
• 10: A. Seawright and F. Brewer. Clairvoyant: A synthesis system for production-based specification. IEEE Transactions on Very Large Sacle Integration(VLSI) Systems, 2(2):172--185, June 1994.

INDEX TERMS

Keywords:
SVA, multi-clock SVA assertions