Journal of Electronic Testing

, Volume 29, Issue 5, pp 669–684 | Cite as

Automatic Generation of System Level Assertions from Transaction Level Models



We automatically generate assertions from Transaction Level Model (TLM) simulation traces. The generated assertions express design specifications in the form of linear temporal logic with quantitative temporal constraints [4]. We first generate the assertions without regard to the quantitative time constraints. They are mined in the form of frequent patterns in the simulation traces. We mine simulation traces using episode mining to identify frequent episodes comprising function calls and events. We then annotate the episodes with real time parameters to express quantitative time constraints among the function calls or events in the episode. When mining such TLM assertions, we employ symbolic execution to generalize the parameters and return values of function calls in the traces to help the mining engine generate high quality assertions. We have constructed a realistic AXI-based interconnection network platform that we demonstrate experimental results on. We show that our technique efficiently generates high quality performance and functional assertions on the AXI-based platform as well as a transaction level AMBA-based DMA controller. We demonstrate that episode mining is more scalable and able to generate a more compact set of high quality TLM assertions than previous efforts using sequential pattern mining. The number of generated assertions using episode mining can be reduced by up to 228 times, and the time interval between two events/function calls in each assertion is smaller than 50 time units.


Transaction level models Assertion generation Episode mining Symbolic execution 


  1. 1.
    AMBA-PV extensions to OSCI TLM 2.0 developer guide.
  2. 2.
  3. 3.
    Ayres J, Flannick J, Gehrke J, Yiu T (2002) Sequential pattern mining using a bitmap representation. In: Proceedings of the eighth ACM SIGKDD international conference on knowledge discovery and data mining, pp 429–435Google Scholar
  4. 4.
    Bellini P, Mattolini R, Nesi P (2000) Temporal logics for real-time system specification. ACM Comput Surv 32(1):12–42CrossRefGoogle Scholar
  5. 5.
    Bombieri N, Fummi F, Pravadelli G, Fedeli A (2007) Hybrid, incremental assertion-based verification for tlm design flows, design & test of computers. IEEE 24(2)140–152Google Scholar
  6. 6.
    Cai L, Gajski D (2003) Transaction level modeling: an overview. In: First IEEE/ACM/IFIP international conference on hardware/software codesign and system synthesis, pp 19–24Google Scholar
  7. 7.
    Chang P-H, Wang L-C (2010) Automatic assertion extraction via sequential data mining of simulation traces. In: Design automation conference (ASP-DAC), 2010 15th Asia and South Pacific, pp 607–612Google Scholar
  8. 8.
    Chen X, Hsieh H, Balarin F, Watanabe Y (2004) Logic of constraints: a quantitative performance and functional constraint formalism. IEEE Trans. on CAD of Integrated Circuits and Systems 23(8):1243–1255CrossRefGoogle Scholar
  9. 9.
    Cheng X, Hsiao MS (2008) Simulation-directed invariant mining for software verification. In: Proceedings of DATE, pp 682–687Google Scholar
  10. 10.
    Ecker W, Esen V, Steininger T, Velten M, Hull M (2006) Specification language for transaction level assertions. In: High-level design, validation, and test workshop, IEEE international, pp 77–84Google Scholar
  11. 11.
    Ernst MD, Cockrell J, Griswold WG, Notkin D (1999) Dynamically discovering likely program invariants to support program evolution. In: Proceedings of the 21st international conference on software engineering, pp 213–224Google Scholar
  12. 12.
    Han J, Kamber M (2006) Data mining: conceptes and techniques. Morgan Kaufmann Publishers, San Francisco, CAGoogle Scholar
  13. 13.
    Hangal S, Chandra N, Narayanan S, Chakravorty S (2005) Iodine: a tool to automatically infer dynamic invariants for hardware designs. In: Proceedings of DAC, pp 775–778Google Scholar
  14. 14.
    IEEE standard for system verilog: unified hardware design, specification, and verification language (2005) IEEE Std 1800–2005, pp 0–648Google Scholar
  15. 15.
    King JC (1976) Symbolic execution and program testing. Commun ACM 19(7)385–394CrossRefMATHGoogle Scholar
  16. 16.
    Kroening D, Sharygina N (2005) Formal verification of systemc by automatic hardware/software partitioning. In: Proceedings of the 2nd ACM/IEEE international conference on formal methods and models for co-design, pp 101–110Google Scholar
  17. 17.
    Li W, Forin A, Seshia SA (2010) Scalable specification mining for verification and diagnosis. In: Proceedings of the 47th design automation conference, pp 755–760Google Scholar
  18. 18.
    Liu L, Vasudevan S (2010) STAR: generating input vectors for design validation by static analysis of rtl. In: IEEE international high level design validation and test workshopGoogle Scholar
  19. 19.
    Liu L, Sheridan D, Athavale V, Vasudevan S (2011) Automatic generation of assertions from system level design using data mining. In: ACM/IEEE conference on formal methods and models for codesignGoogle Scholar
  20. 20.
    Lo D, Khoo S-C (2006) Smartic: towards building an accurate, robust and scalable specification miner. In: Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, pp 265–275Google Scholar
  21. 21.
    Mannila H, Toivonen H, Inkeri Verkamo A (1997) Discovery of frequent episodes in event sequences. Data Min Knowl Discov 1(3):259–289CrossRefGoogle Scholar
  22. 22.
    Pei J, Han J, Mortazavi-asl B, Pinto H, Chen Q, Dayal U, chun Hsu M (2001) Prefixspan: mining sequential patterns efficiently by prefix-projected pattern growth. In: Proceedings of the 17th international conference on data engineeringGoogle Scholar
  23. 23.
    Pierre L, Ferro L (2008) A tractable and fast method for monitoring systemc tlm specifications. IEEE Trans Comput 57(10):1346–1356MathSciNetCrossRefGoogle Scholar
  24. 24.
    Pnueli A (1977) The temporal logic of programs. In: Proceedings of FOCS, pp 46–57Google Scholar
  25. 25.
    Srikant R, Agrawal R (1996) Mining sequential patterns: generalizations and performance improvements. In: Proceedings of the 5th international conference on extending database technology: advances in database technology, pp 3–17Google Scholar
  26. 26.
    SystemC web page:
  27. 27.
    Tabakov D, Vardi MY, Kamhi G, Singerman E (2008) A temporal language for systemc. In: Proceedings of the 2008 international conference on formal methods in computer-aided design, pp 22:1–22:9Google Scholar
  28. 28.
    Vasudevan S, Sheridan D, Tcheng D, Patel S, Tuohy W, Johnson D (2010) Goldmine: automatic assertion generation using data mining and static analysis. In: Proceedings of DATEGoogle Scholar
  29. 29.
    Zaki MJ (2001) Spade: an efficient algorithm for mining frequent sequences. Mach Learn 42(1–2)31–60CrossRefMATHGoogle Scholar

Copyright information

© Springer Science+Business Media New York 2013

Authors and Affiliations

  1. 1.Department of Electrical and Computer EngineeringUniversity of Illinois at Urbana-ChampaignChampaignUSA

Personalised recommendations