Skip to main content
Erschienen in: Journal of Electronic Testing 2/2015

01.04.2015

Reusing RTL Assertion Checkers for Verification of SystemC TLM Models

verfasst von: Nicola Bombieri, Franco Fummi, Valerio Guarnieri, Graziano Pravadelli, Francesco Stefanni, Tara Ghasempouri, Michele Lora, Giovanni Auditore, Mirella Negro Marcigaglia

Erschienen in: Journal of Electronic Testing | Ausgabe 2/2015

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Weitere Produktempfehlungen anzeigen
Fußnoten
1
It is worth noting that the proposed methodology is independent from the checker generator employed in this step.
 
Literatur
1.
Zurück zum Zitat 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 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
3.
Zurück zum Zitat 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–20 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–20
4.
Zurück zum Zitat 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–6 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–6
5.
Zurück zum Zitat 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 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.
Zurück zum Zitat Bombieri N, Fummi F, Pravadelli G (2011) Automatic abstraction of RTL IPs into equivalent TLM descriptions. IEEE Trans Comput 60(12):1730–1743CrossRefMathSciNet Bombieri N, Fummi F, Pravadelli G (2011) Automatic abstraction of RTL IPs into equivalent TLM descriptions. IEEE Trans Comput 60(12):1730–1743CrossRefMathSciNet
7.
Zurück zum Zitat 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–152CrossRef 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–152CrossRef
8.
Zurück zum Zitat 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 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.
Zurück zum Zitat Boulé M, Zilic Z (2008) Generating hardware assertion checkers: for hardware verification, emulation, post-fabrication debugging and on-line monitoring. Springer Boulé M, Zilic Z (2008) Generating hardware assertion checkers: for hardware verification, emulation, post-fabrication debugging and on-line monitoring. Springer
10.
Zurück zum Zitat Cai L, Gajski D (2003) Transaction Level Modelling: An Overview. In: IEEE/ACM CODES+ISSS, pp 19–24 Cai L, Gajski D (2003) Transaction Level Modelling: An Overview. In: IEEE/ACM CODES+ISSS, pp 19–24
12.
Zurück zum Zitat Chen M, Mishra P (2013) Assertion-based functional consistency checking between TLM and RTL models. In: Proceedings of IEEE VLSID, pp 320–325 Chen M, Mishra P (2013) Assertion-based functional consistency checking between TLM and RTL models. In: Proceedings of IEEE VLSID, pp 320–325
13.
Zurück zum Zitat Clarke E M, Emerson E A, Sifakis J (2009) Model checking: algorithmic verification and debugging. Commun ACM 52(11) Clarke E M, Emerson E A, Sifakis J (2009) Model checking: algorithmic verification and debugging. Commun ACM 52(11)
14.
Zurück zum Zitat 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 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.
Zurück zum Zitat Ecker W, Esen V, Hull M (2007) Implementation of a transaction level assertion framework in SystemC. In: Proceedings of IEEE/ACM DATE pp 894–899 Ecker W, Esen V, Hull M (2007) Implementation of a transaction level assertion framework in SystemC. In: Proceedings of IEEE/ACM DATE pp 894–899
16.
Zurück zum Zitat Ecker W, Esen V, Hull M (2006) Execution semantics and formalism for multi-abstraction TLM assertions, pp 93–102 Ecker W, Esen V, Hull M (2006) Execution semantics and formalism for multi-abstraction TLM assertions, pp 93–102
17.
Zurück zum Zitat Ecker W, Esen V, Hull M (2006) Requirements and concepts for transaction level assertions. In: Proceedings of IEEE ICCD, pp 286–293 Ecker W, Esen V, Hull M (2006) Requirements and concepts for transaction level assertions. In: Proceedings of IEEE ICCD, pp 286–293
18.
Zurück zum Zitat Ecker W, Esen V, Steininger T, Velten M, Hull M (2006) Specification Language for Transaction Level Assertions. In: Proceedings of IEEE HLDVT, pp 77–84 Ecker W, Esen V, Steininger T, Velten M, Hull M (2006) Specification Language for Transaction Level Assertions. In: Proceedings of IEEE HLDVT, pp 77–84
20.
Zurück zum Zitat 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–242 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–242
21.
Zurück zum Zitat 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 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.
Zurück zum Zitat Ferro L, Laurence (2009) ISIS: runtime verification of TLM platforms. In: Proceedings of FDL, pp 1–6 Ferro L, Laurence (2009) ISIS: runtime verification of TLM platforms. In: Proceedings of FDL, pp 1–6
23.
Zurück zum Zitat Fujita M (2005) Equivalence checking between behavioral and RTL descriptions with virtual controllers and datapaths. ACM TODAES 10(4):610–626 Fujita M (2005) Equivalence checking between behavioral and RTL descriptions with virtual controllers and datapaths. ACM TODAES 10(4):610–626
24.
Zurück zum Zitat Ghofrani A, Javahery F, Navabi Z (2010) Assertion based verification in TLM. In: Proceedings of IEEE EWDTS, pp 509– 513 Ghofrani A, Javahery F, Navabi Z (2010) Assertion based verification in TLM. In: Proceedings of IEEE EWDTS, pp 509– 513
25.
Zurück zum Zitat 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 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.
Zurück zum Zitat Habibi A, Tahar S (2006) Design and verification of SystemC transaction-level models. IEEE Trans VLSI Syst 14(1):57–67CrossRef Habibi A, Tahar S (2006) Design and verification of SystemC transaction-level models. IEEE Trans VLSI Syst 14(1):57–67CrossRef
29.
Zurück zum Zitat Kallel M, Lahbib Y, Tourki R, Baganne A (2009) Aspect-based ABV for SystemC transaction level models. In: Proceedings of IEEE ICM, pp 304–307 Kallel M, Lahbib Y, Tourki R, Baganne A (2009) Aspect-based ABV for SystemC transaction level models. In: Proceedings of IEEE ICM, pp 304–307
30.
Zurück zum Zitat 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–6 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–6
31.
Zurück zum Zitat Kasuya A, Tesfaye T (2007) Verification methodologies in a TLM-to-RTL design flow. In: Proceedings of ACM/IEEE DAC, pp 199–204 Kasuya A, Tesfaye T (2007) Verification methodologies in a TLM-to-RTL design flow. In: Proceedings of ACM/IEEE DAC, pp 199–204
32.
Zurück zum Zitat 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–302CrossRef 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–302CrossRef
33.
Zurück zum Zitat 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–90 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–90
34.
Zurück zum Zitat Mathur A, Krishnaswamy V (2007) Design for Verification in System-level Models and RTL. In: Proceedings of IEEE/ACM DAC, pp 193–198 Mathur A, Krishnaswamy V (2007) Design for Verification in System-level Models and RTL. In: Proceedings of IEEE/ACM DAC, pp 193–198
35.
Zurück zum Zitat 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–10 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–10
36.
Zurück zum Zitat Pierre L, Ferro L (2008) A Tractable and Fast Method for Monitoring SystemC TLM Specifications. IEEE Trans Comput 57(10):1346–1356CrossRefMathSciNet Pierre L, Ferro L (2008) A Tractable and Fast Method for Monitoring SystemC TLM Specifications. IEEE Trans Comput 57(10):1346–1356CrossRefMathSciNet
37.
Zurück zum Zitat Pierre L, Ferro L (2010) Enhancing the assertion-based verification of TLM designs with reentrancy. In: Proceedings of ACM/IEEE MEMOCODE, pp 103–112 Pierre L, Ferro L (2010) Enhancing the assertion-based verification of TLM designs with reentrancy. In: Proceedings of ACM/IEEE MEMOCODE, pp 103–112
38.
Zurück zum Zitat Pnueli A, Zaks A (2006) PSL model checking and run-time verification via testers. In: FM 2006: formal methods. Springer, pp 573–586 Pnueli A, Zaks A (2006) PSL model checking and run-time verification via testers. In: FM 2006: formal methods. Springer, pp 573–586
39.
Zurück zum Zitat 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 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.
Zurück zum Zitat Xiong Z, Bian J, Zhao Y (2010) An assertion-based verification method for SystemC TLM. In: Proceedings of IEEE ICCCAS, pp 842–846 Xiong Z, Bian J, Zhao Y (2010) An assertion-based verification method for SystemC TLM. In: Proceedings of IEEE ICCCAS, pp 842–846
Metadaten
Titel
Reusing RTL Assertion Checkers for Verification of SystemC TLM Models
verfasst von
Nicola Bombieri
Franco Fummi
Valerio Guarnieri
Graziano Pravadelli
Francesco Stefanni
Tara Ghasempouri
Michele Lora
Giovanni Auditore
Mirella Negro Marcigaglia
Publikationsdatum
01.04.2015
Verlag
Springer US
Erschienen in
Journal of Electronic Testing / Ausgabe 2/2015
Print ISSN: 0923-8174
Elektronische ISSN: 1573-0727
DOI
https://doi.org/10.1007/s10836-015-5514-8

Weitere Artikel der Ausgabe 2/2015

Journal of Electronic Testing 2/2015 Zur Ausgabe

EditorialNotes

Editorial

Neuer Inhalt