Reusing RTL Assertion Checkers for Verification of SystemC TLM Models

详细信息    查看全文

• 作者：Nicola Bombieri ; Franco Fummi ; Valerio Guarnieri…
• 关键词：Assertion ; based verification ; Transaction ; level modelling ; RTL abstraction
• 刊名：Journal of Electronic Testing
• 出版年：2015
• 出版时间：April 2015
• 年：2015
• 卷：31
• 期：2
• 页码：167-180
• 全文大小：2,118 KB
• 参考文献：1.Abarbanel Y, Beer I, Glushovsky L, Keidar S, Wolfsthal Y (2000) FoCs: automatic generation of simulation checkers from formal specifications. In: Proceedings of CAV, pp 538鈥?542
  2.Accellera (2004) Property specification language reference manual. http://鈥媤ww.鈥媋ccellera.鈥媜rg
  3.Bombieri N, Deganello N, Fummi F (2008) Integrating RTL IPs into TLM designs through automatic transactor generation. In: Proceedings of ACM/IEEE DATE, pp 15鈥?0
  4.Bombieri N, Fummi F, Pravadelli G (2006) On the evaluation of transactor-based verification for reusing TLM assertions and testbenches at RTL. In: Proceedings of ACM/IEEE DATE,pp 1鈥?
  5.Bombieri N, Fummi F, Pravadelli G (2007) Incremental ABV for functional validation of TL-to-RTL design refinement. In: Proceedings of ACM/IEEE DATE, pp 882鈥?887
  6.Bombieri N, Fummi F, Pravadelli G (2011) Automatic abstraction of RTL IPs into equivalent TLM descriptions. IEEE Trans Comput 60(12):1730鈥?743View Article MathSciNet
  7.Bombieri N, Fummi F, Pravadelli G, Fedeli A (2007) Hybrid, incremental assertion-based verification for TLM design flows. IEEE Design and Test 24(2):140鈥?52View Article
  8.Bombieri N, Fummi F, Pravadelli G, Marques-Silva J (2007) Towards Equivalence Checking Between TLM and RTL Models. In: Proceedings of ACM/IEEE MEMOCODE, pp 113鈥?122
  9.Boul茅 M, Zilic Z (2008) Generating hardware assertion checkers: for hardware verification, emulation, post-fabrication debugging and on-line monitoring. Springer
  10.Cai L, Gajski D (2003) Transaction Level Modelling: An Overview. In: IEEE/ACM CODES+ISSS, pp 19鈥?4
  11.Carbon Design Systems Carbon Model Studio. http://鈥媍arbondesignsyst鈥媏ms.鈥媍om/鈥?/span>
  12.Chen M, Mishra P (2013) Assertion-based functional consistency checking between TLM and RTL models. In: Proceedings of IEEE VLSID, pp 320鈥?25
  13.Clarke E M, Emerson E A, Sifakis J (2009) Model checking: algorithmic verification and debugging. Commun ACM 52(11)
  14.Das S, Roberts D, Lee S, Pant S, Blaauw D, Austin T, Flautner K, Mudge T (2006). A self-tuning DVS processor using delay-error detection and correction 41(4):792鈥?804
  15.Ecker W, Esen V, Hull M (2007) Implementation of a transaction level assertion framework in SystemC. In: Proceedings of IEEE/ACM DATE pp 894鈥?99
  16.Ecker W, Esen V, Hull M (2006) Execution semantics and formalism for multi-abstraction TLM assertions, pp 93鈥?02
  17.Ecker W, Esen V, Hull M (2006) Requirements and concepts for transaction level assertions. In: Proceedings of IEEE ICCD, pp 286鈥?93
  18.Ecker W, Esen V, Steininger T, Velten M, Hull M (2006) Specification Language for Transaction Level Assertions. In: Proceedings of IEEE HLDVT, pp 77鈥?4
  19.EDALab HIFSuite. http://鈥媤ww.鈥媓ifsuite.鈥媍om/鈥?/span>
  20.Ferro L, Pierre L, Ledru Y, du Bousquet L (2008) Generation of test programs for the assertion-based verification of TLM models. In: Proceedings of IEEE IDT, pp 237鈥?42
  21.Ferro L, Pierre L (2010) Formal semantics for PSL modelling layer and application to the verification of transactional models. In: Proceedings of ACM/IEEE DATE, pp 1207鈥?1212
  22.Ferro L, Laurence (2009) ISIS: runtime verification of TLM platforms. In: Proceedings of FDL, pp 1鈥?
  23.Fujita M (2005) Equivalence checking between behavioral and RTL descriptions with virtual controllers and datapaths. ACM TODAES 10(4):610鈥?26
  24.Ghofrani A, Javahery F, Navabi Z (2010) Assertion based verification in TLM. In: Proceedings of IEEE EWDTS, pp 509鈥?513
  25.Grosse D, Le H, Drechsler R (2010) Proving transaction and system-level properties of untimed SystemC TLM designs. In: Proceedings of IEEE/ACM MEMOCODE, pp 113鈥?122
  26.Habibi A, Tahar S (2006) Design and verification of SystemC transaction-level models. IEEE Trans VLSI Syst 14(1):57鈥?7View Article
  27.IBM FoCs property checkers generator. https://鈥媤ww.鈥媟esearch.鈥媔bm.鈥媍om/鈥媓aifa/鈥媝rojects/鈥媣erification/鈥媐ocs/鈥媠tart.鈥媓tml
  28.IEEE standard systemC language reference manual (2006). http://鈥媔eeexplore.鈥媔eee.鈥媜rg
  29.Kallel M, Lahbib Y, Tourki R, Baganne A (2009) Aspect-based ABV for SystemC transaction level models. In: Proceedings of IEEE ICM, pp 304鈥?07
  30.Kallel M, Lahbib Y, Tourki R, Baganne A (2010) Verification of SystemC transaction level models using an aspect-oriented and generic approach. In: Proceedings of IEEE DTIS, pp 1鈥?
  31.Kasuya A, Tesfaye T (2007) Verification methodologies in a TLM-to-RTL design flow. In: Proceedings of ACM/IEEE DAC, pp 199鈥?04
  32.Lahbib Y, Kamdem R, Benalycherif M-l, Tourki R (2005) An automatic ABV methodology enabling PSL assertions across SLD flow for SOCs modelled in SystemC. Comput Electr Eng 31(4-5):282鈥?02View Article
  33.Lahbib Y, Ghrab M-A, Hechkel M, Ghenassia F, Tourki R (2006) A new synchronization policy between PSL checkers and SystemC designs at transaction level. In: Proceedings of IEEE DTIS, pp 85鈥?0
  34.Mathur A, Krishnaswamy V (2007) Design for Verification in System-level Models and RTL. In: Proceedings of IEEE/ACM DAC, pp 193鈥?98
  35.Pierre L, Amor ZBH (2013) Automatic refinement of requirements for verification throughout the SoC design flow. In: Proceedings of ACM/IEEE CODES+ISSS, pp 1鈥?0
  36.Pierre L, Ferro L (2008) A Tractable and Fast Method for Monitoring SystemC TLM Specifications. IEEE Trans Comput 57(10):1346鈥?356View Article MathSciNet
  37.Pierre L, Ferro L (2010) Enhancing the assertion-based verification of TLM designs with reentrancy. In: Proceedings of ACM/IEEE MEMOCODE, pp 103鈥?12
  38.Pnueli A, Zaks A (2006) PSL model checking and run-time verification via testers. In: FM 2006: formal methods. Springer, pp 573鈥?86
  39.Smith DJ (1996) VHDL & Verilog compared & contrasted - plus modelled example written in VHDL, Verilog and C. In: Proceedings of ACM/IEEE DAC, pp 771鈥?776
  40.Xiong Z, Bian J, Zhao Y (2010) An assertion-based verification method for SystemC TLM. In: Proceedings of IEEE ICCCAS, pp 842鈥?46
  
• 作者单位：Nicola Bombieri (1) (2)
  Franco Fummi (1) (2)
  Valerio Guarnieri (2)
  Graziano Pravadelli (1) (2)
  Francesco Stefanni (1)
  Tara Ghasempouri (2)
  Michele Lora (2)
  Giovanni Auditore (3)
  Mirella Negro Marcigaglia (3)
  
  1. EDALab s.r.l., Verona, Italy
  2. University of Verona, Verona, Italy
  3. STMicroelectronics s.r.l., Veroan, Italy
  
• 刊物类别：Engineering
• 刊物主题：Circuits and Systems
  Electronic and Computer Engineering
  Computer-Aided Engineering and Design
  
• 出版者：Springer Netherlands
• ISSN：1573-0727

文摘

The recent trend towards system-level design gives rise to new challenges for reusing existing (RTL) intellectual properties (IPs) and their verification environment in (TLM). While techniques and tools to abstract (RTL) IPs into TLM models have begun to appear, the problem of reusing, at TLM, a verification environment originally developed for an RTL IP is still under-explored, particularly when (ABV) is adopted. Some frameworks have been proposed to deal with ABV at TLM, but they assume a top-down design and verification flow, where assertions are defined ex-novo at TLM level. In contrast, the reuse of existing assertions in an RTL-to-TLM bottom-up design flow has not been analyzed yet, except by using transactors to create a mixed simulation between the TLM design and the RTL checkers corresponding to the assertions. However, the use of transactors may lead to longer verification time due to the need of developing and verifying the transactors themselves. Moreover, the simulation time is negatively affected by the presence of transactors, which slow down the simulation at the speed of the slowest parts (i.e., RTL checkers). This article proposes an alternative methodology that does not require transactors for reusing assertions, originally defined for a given RTL IP, in order to verify the corresponding TLM model. Experimental results have been conducted on benchmarks with different characteristics and complexity to show the applicability and the efficiency of the proposed methodology.