Incremental ABV for functional validation of TL-to-RTL design refinement

ABSTRACT

Transaction-level modeling (TLM) has been proposed as the leading strategy to address the always increasing complexity of digital systems. However, its introduction arouses a new challenge for designers and verification engineers, since there are no mature tools to automatically synthesize an RTL implementation from a transaction-level (TL) design, thus manual refinements are mandatory. In this context, the paper presents an incremental assertion-based verification (ABV) methodology to check the correctness of the TL-to-RTL refinement. The methodology relies on reusing assertions and already checked code, and it is guided by an assertion coverage metrics.

REFERENCES

• 1: The Medea+ Design Automation Roadmap, 2002.
• 2: A. Rose, S. Swan, J. Pierce, and J.-M. Fernandez. Transaction Level Modeling in SystemC, 2004. White paper, www.systemc.org.
• 3: Synopsys Inc. Assertion-Based Verification, 2003. White paper. www.synopsys.com.
• 4: D. Brahme, S. Cox, J. Gallo, M. Glasser, W. Grundmann, C. N. Ip, W. Paulsen, J. Pierce, J. Rose, D. Shea, and K. Whiting. The Transaction-Based Verification Methodology. Tech. Rep. CDNL-TR-2000-0825, Cadence Berkeley Labs, 2000.
• 5: C. Norris Ip and S. Swan. A Tutorial Introduction on the New SystemC Verification Standard, 2003. White paper, www.systemc.org.
• 6: Anat Dahan , Daniel Geist , Leonid Gluhovsky , Dmitry Pidan , Gil Shapir , Yaron Wolfsthal , Lyes Benalycherif , Romain Kamdem , Younes Lahbib, Combining System Level Modeling with Assertion Based Verification, Proceedings of the 6th International Symposium on Quality of Electronic Design, p.310-315, March 21-23, 2005 [doi>10.1109/ISQED.2005.32]
• 7: Ali Habibi , Sofiene Tahar, Design for Verification of SystemC Transaction Level Models, Proceedings of the conference on Design, Automation and Test in Europe, p.560-565, March 07-11, 2005 [doi>10.1109/DATE.2005.112]
• 8: Doulos and Mentor Graphics. Verification Methodology in a Mixed Language Environment. In Solutions Workshop 3 at IEEE DATE. 2006.
• 9: Nicola Bombieri , Andrea Fedeli , Franco Fummi, On PSL Properties Re-use in SoC Design Flow Based on Transaction Level Modeling, Proceedings of the Sixth International Workshop on Microprocessor Test and Verification (MTV'05), p.127-132, November 03-05, 2005 [doi>10.1109/MTV.2005.15]
• 10: Martin Van Hulst, Verification of Transaction-Level SystemC models using RTL Testbenches, Proceedings of the First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE'03), p.199, June 24-26, 2003
• 11: Nicola Bombieri , Franco Fummi , Graziano Pravadelli, On the evaluation of transactor-based verification for reusing TLM assertions and testbenches at RTL, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
• 12: 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]
• 13: 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
• 14: 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
• 15: Nikhil Jayakumar , Mitra Purandare , Fabio Somenzi, Dos and don'ts of CTL state coverage estimation, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775908]
• 16: Franco Fummi , Graziano Pravadelli , Franco Toto, Coverage of Formal Properties Based on a High-Level Fault Model and Functional ATPG, Proceedings of the 10th IEEE European Symposium on Test, p.162-167, May 22-25, 2005 [doi>10.1109/ETS.2005.12]
• 17: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 18: Accellera. Property Specification Language Reference Manual, 2004.
• 19: Yael Abarbanel , Ilan Beer , Leonid Glushovsky , Sharon Keidar , Yaron Wolfsthal, FoCs: Automatic Generation of Simulation Checkers from Formal Specifications, Proceedings of the 12th International Conference on Computer Aided Verification, p.538-542, July 15-19, 2000
• 20: Pierre Wodey , Geoffrey Camarroque , Richard Hersemeule , Jean-Philippe Cousin, LOTOS Code Generation for Model Checking of STBus Based SoC: the STBus interconnect, Proceedings of the First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE'03), p.204, June 24-26, 2003
• 21: Synopsys. Magellan - Hybrid RTL Formal Verification, http://www.synopsys.com/products/magellan/, 2004.
• 22: Felice Balarin , Roberto Passerone, Functional verification methodology based on formal interface specification and transactor generation, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
• 23: M. Borgatti , A. Capello , U. Rossi , J.-L. Lambert , I. Moussa , F. Fummi , G. Pravadelli, An Integrated Design and Verification Methodology for Reconfigurable Multimedia Systems, Proceedings of the conference on Design, Automation and Test in Europe, p.266-271, March 07-11, 2005 [doi>10.1109/DATE.2005.61]
• 24: Hansu Cho , Samar Abdi , Daniel Gajski, Design and implementation of transducer for ARM-TMS communication, Proceedings of the 2006 conference on Asia South Pacific design automation, January 24-27, 2006, Yokohama, Japan [doi>10.1145/1118299.1118339]