skip to main content
research-article

Reuse and optimization of testbenches and properties in a TLM-to-RTL design flow

Published: 25 July 2008 Publication History

Abstract

In transaction-level modeling (TLM), verification methodologies based on transactions allow testbenches, properties, and IP cores in mixed TL-RTL designs to be reused. However, no papers in the literature analyze the effectiveness of transaction-based verification (TBV) in comparison to the more traditional RTL approach. The first contribution of this article is the introduction of a functional-fault-model-based methodology for demonstrating the effectiveness of reuse through TBV. A second contribution is the introduction of a similar methodology for efficient property checking which identifies and removes redundant properties prior to assertion-based verification or model checking.

References

[1]
Abarbanel, Y., Beer, I., Gluhovsky, L., Keidar, S., and Wolfsthal, Y. 2000. Focs—automatic generation of simulation checkers from formal specifications. In Proceedings of the International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 1855. Springer, 538--542.]]
[2]
Asaf, S., Marcus, E., and Ziv, A. 2004. Defining coverage views to improve functional coverage analysis. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), 41--44.]]
[3]
Beer, I., Ben-David, S., Eisner, C., and Landver, A. 1996. Rulebase, an industry-oriented formal verification tool. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), 655--660.]]
[4]
Bombieri, N., Fedeli, A., and Fummi, F. 2005. On PSL properties re-use in SoC design flow based on transaction level modeling. In Proceedings of the IEEE International Workshop on Microprocessor Test Verification. 127--132.]]
[5]
Brahme, D., Cox, S., Gallo, J., Glasser, M., Grundmann, W., Norris Ip, C., Paulsen, W., Pierce, J., Rose, J., Shea, D., and Whiting, K. 2000. The transaction-based verification methodology. Tech. Rep. CDNL-TR-2000-0825, Cadence Berkeley Labs.]]
[6]
Breuer, M., Abramovici, M., and Friedman., A. 1990. Digital Systems Testing and Testable Design. IEEE Press.]]
[7]
Cai, L. and Gajski, D. 2003. Transaction level modeling: An overview. In Proceedings of the ACM/IEEE International Conference on Hardware-Software Codesign and System Synthesis (CODES + ISSS), 19--24.]]
[8]
Cheng, K.-T. and Jou, J.-Y. 1990. A single-state-transition fault model for sequential machines. In Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD), 226--229.]]
[9]
Chockler, H., Kupferman, O., Kurshan, R. P., and Vardi, M. Y. 2001. A practical approach to coverage in model checking. In Proceedigs of the International Conference on Computer-Aided Verification (CAV), 66--78.]]
[10]
Clarke, E., Grumberg, D., and Peled, D. 2000. Model Checking. MIT Press.]]
[11]
Clarke, E., Grumberg, O., McMillan, K., and Zhao, X. 1995. Efficient generation of counterexamples and witnesses in symbolic model checking. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), 427--432.]]
[12]
Emerson, E. and Halpen, J. 1985. Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci. 30, 1--24.]]
[13]
Fedeli, A., Fummi, F., Pravadelli, G., Rossi, U., and Toto, F. 2003. On the use of a high-level fault model to check properties incompleteness. In Proceedings of the ACM/IEEE International Conference on Formal Methods and Models for Codesign, (MEMOCODE). 145--152.]]
[14]
Ferrandi, F., Fummi, F., Gerli, L., and Sciuto, D. 1999. Symbolic functional vector generation for vhdl specifications. In Proceedings of the IEEE Design, Automation and Test in Europe (DATE), 442--446.]]
[15]
Ferrandi, F., Fummi, F., Pravadelli, G., and Sciuto, D. 2003. Identification of design erros through functional testing. IEEE Trans. Reliabil. 52, 4, 400--412.]]
[16]
Foster, H. D., Krolnik, A. C., and Lacey, D. J. 2004. Assertion-Based Design. Springer Academic, The Netherlands.]]
[17]
Fummi, F., Pravadelli, G., and Toto, F. 2005. Coverage of formal properties based on a high-level fault model and functional ATPG. In Proceedings of the IEEE European Test Symposium (ETS), 162--167.]]
[18]
Ghosh, S. and Chakraborty, T. 1991. On behavior fault modeling for digital designs. Int. J. Electron. Test. Theory Appl. 2, 2, 135--151.]]
[19]
Hachtel, G. D. and Somenzi, F. 1996. Logic Synthesis and Verification Algorithms. Kluwer Academic.]]
[20]
Hoskote, Y., Kam, T., Ho, P. H., and Zao, X. 1999. Coverage estimation for symbolic model checking. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), 300--305.]]
[21]
Jayakumar, N., Purandare, M., and Somenzi, F. 2003. Dos and don'ts of CTL state coverage estimation. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), 292--295.]]
[22]
Jindal, R. and Jain, K. 2003. Verification of transaction-level systemc models using RTL testbenches. In Proceedings of the IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE). 199--203.]]
[23]
Katz, S., Grumberg, O., and Geist, D. 1999. Have I written enough properties? A method of comparison between specification and implementation. In Proceedings of the IFIP Correct Hardware Design and Verification Methods (CHARME). 280--297.]]
[24]
Kwon, Y.-S., Kim, Y.-I., and Kyung, C.-M. 2004. Systematic functional coverage metric synthesis from hierarchical temporal event relation graph. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), 45--48.]]
[25]
Lee, T.-C. and Hsiung, P.-A. 2004. Mutation coverage estimation for model checking. In Proceedings of the International Symposium on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 3299. Springer, 534--368.]]
[26]
Lichtenstein, O. and Pnueli, A. 2000. Propositional temporal logics: Decidability and completeness. Logic J. Interest Group Pure Appl. Logic 8, 55--85.]]
[27]
McMillan, K. L. 1993. Symbolic Model Checking. Kluwer Academic, Norwell, MA.]]
[28]
Myers, G. 1979. The Art of Software Testing. Wiley Interscience, New York.]]
[29]
Norris Ip, C. and Swan, S. 2003. A tutorial introduction on the new systemc verification standard. White paper. www.systemc.org.]]
[30]
Politecnico di Torino. 1999. ITC-99 benchmarks. In http://www.cad.polito.it/tools/itc99.html.]]
[31]
Reynolds, M. 2001. An axiomatization of full computation tree logic. J. Symbol. Logic 66, 3, 1011--1057.]]
[32]
Rose, A., Swan, S., Pierce, J., and Fernandez, J.-M. 2004. Transaction level modeling in systemC. White paper. www.systemc.org.]]
[33]
Santos, M. B., Gonalves, F. M., Teixeira, I. C., and Teixeira, J. P. 2000. RTL-Based functional test generation for high defects coverage in digital SoCs. In Proceedings of the IEEE European Test Workshop (ETW), 99--104.]]
[34]
Su, M.-Y., Shih, C.-H., Huang, J.-D., and Jou, J.-Y. 2006. FSM-Based transaction-level functional coverage for interface compliance verification. In Proceedings of the ACM/IEEE Asia and South Pacific Design Automation Conference (ASP-DAC), 448--453.]]
[35]
Xu, X., Kimura, S., Horikawa, K., and Tsuchiya, T. 2006. Transition-Based coverage estimation for symbolic model checking. In Proceedings of the ACM/IEEE Asia and South Pacific Design Automation Conference (ASP-DAC). 1--6.]]
[36]
Zhong-hai, W. and Yi-zheng, Y. 2005. The improvement for transaction level verification functional coverage. In Proceedings of the IEEE International Symposium on Circuits and Systems (ISCAS). 5850--5853.]]

Cited By

View all
  • (2012)A systematic approach to configurable functional verification of HW IP blocks at transaction levelComputers and Electrical Engineering10.1016/j.compeleceng.2012.05.00638:6(1513-1523)Online publication date: 1-Nov-2012
  • (2010)Model checking on TLM-2.0 IPs through automatic TLM-to-RTL synthesis2010 18th IEEE/IFIP International Conference on VLSI and System-on-Chip10.1109/VLSISOC.2010.5642620(61-66)Online publication date: Sep-2010
  • (2010)Automatic synthesis of OSCI TLM-2.0 models into RTL bus-based IPs2010 IEEE International High Level Design Validation and Test Workshop (HLDVT)10.1109/HLDVT.2010.5496652(105-112)Online publication date: Jun-2010

Recommendations

Reviews

Paparao S Kavalipati

Transaction-based verification is a recent trend in hardware verification. The system is considered at higher levels of abstraction that model the data transfers and input/output (I/O) events between computational blocks, and functional verification is based on assertions that describe the expected behavior. In this paper, the authors attempt a comparison of transaction-level modeling (TLM) verification with a full register transfer level (RTL) verification methodology. They also present an approach for deriving logical consequences of properties that becomes important in detecting redundant properties. The technique presented in the paper is based on a functional fault model, and considers witness coverage that indicates the percentage of faults covered by fault-simulating witnesses of the property. The presentation of the methodology is lucid and the terminology is well defined. The fact that relevant background material is provided in detail makes the paper easy to read and understand. However, the theoretical contribution is somewhat weak, as the theorems and corollaries follow trivially from the definitions. The suggested property optimization methodology cannot fully eliminate the burden of theorem proving, as the mechanism based on fault simulation can only provide a necessary condition for property redundancy. However, the presented ideas can be explored further to enhance the performance of model-checking tools. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Design Automation of Electronic Systems
ACM Transactions on Design Automation of Electronic Systems  Volume 13, Issue 3
July 2008
370 pages
ISSN:1084-4309
EISSN:1557-7309
DOI:10.1145/1367045
Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

Publication History

Published: 25 July 2008
Accepted: 01 November 2007
Revised: 01 August 2006
Received: 01 November 2005
Published in TODAES Volume 13, Issue 3

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Model checking
  2. TBV
  3. TLM
  4. fault models
  5. functional verification

Qualifiers

  • Research-article
  • Research
  • Refereed

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)1
  • Downloads (Last 6 weeks)0
Reflects downloads up to 15 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2012)A systematic approach to configurable functional verification of HW IP blocks at transaction levelComputers and Electrical Engineering10.1016/j.compeleceng.2012.05.00638:6(1513-1523)Online publication date: 1-Nov-2012
  • (2010)Model checking on TLM-2.0 IPs through automatic TLM-to-RTL synthesis2010 18th IEEE/IFIP International Conference on VLSI and System-on-Chip10.1109/VLSISOC.2010.5642620(61-66)Online publication date: Sep-2010
  • (2010)Automatic synthesis of OSCI TLM-2.0 models into RTL bus-based IPs2010 IEEE International High Level Design Validation and Test Workshop (HLDVT)10.1109/HLDVT.2010.5496652(105-112)Online publication date: Jun-2010

View Options

Login options

Full Access

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media