[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Towards functional verifying a family of systemC TLMs

  • Research Article
  • Published:
Frontiers of Computer Science Aims and scope Submit manuscript

Abstract

It is often the case that in the development of a system-on-a-chip (SoC) design, a family of SystemC transaction level models (TLM) is created. TLMs in the same family often share common functionalities but differ in their timing, implementation, configuration and performance in various SoC developing phases. In most cases, all the TLMs in a family must be verified for the follow-up design activities. In our previous work, we proposed to call such family TLM product line (TPL), and proposed feature-oriented (FO) design methodology for efficient TPL development. However, developers can only verify TLM in a family one by one, which causes large portion of duplicated verification overhead. Therefore, in our proposed methodology, functional verification of TPL has become a bottleneck. In this paper, we proposed a novel TPL verification method for FO designs. In our method, for the given property, we can exponentially reduce the number of TLMs to be verified by identifying mute-feature-modules (MFM), which will avoid duplicated verification. The proposed method is presented in informal and formal way, and the correctness of it is proved. The theoretical analysis and experimental results on a real design show the correctness and efficiency of the proposed method.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Hu J, Li T, Li S, Equivalence checking between SLM and TLM using coverage directed simulation. Frontiers of Computer Science, 2015, 9(6): 934–943

    Article  Google Scholar 

  2. Li T, Guo Y, Liu W, Tang M. Translation validation of scheduling in high level synthesis. In: Proceedings of the 23rd ACM International Conference on Great Lakes Symposium on VLSI. 2013, 101–106

    Chapter  Google Scholar 

  3. Liu W, Wang R, Fu X, Wang J, Dong W, Mao X. Counterexample-preserving reduction for symbolic model checking. Journal of Applied Mathematics, 2014, 2014: 1–13

    MATH  Google Scholar 

  4. Zhang L, Qu W, Huo Y, Guo Y, Li S. An SAT-based method to multithreaded program verification for mobile crowdsourcing networks. Wireless Communications and Mobile Computing, 2018, 2018: 59–66

    Google Scholar 

  5. Ye J, Li T, Tan Q. The application of aspectual feature module in the development and verification of SystemC models. In: Proceedings of the IEEE Forum on Specification and Design Languages. 2009, 1–6

    Google Scholar 

  6. Ye J, Tan Q, Li T. Feature-oriented refactoring proposal for transaction level models in SoCLib. In: Proceeding of 2010 Forum on Specification and Design Languages. 2010, 22–27

    Google Scholar 

  7. Ye J, Tan Q, Li T. Towards the Development of a Set of Transaction Level Models–a Feature-Oriented Approach. System Specification and Design Languages. New York: Springer, 2012, 143–156

    Google Scholar 

  8. Apel S, Leich T, Rosenmuller M, Saake G. FeatureC++: on the symbiosis of feature-oriented and aspect-oriented programming. In: Proceedings of the International Conference on Generative Programming and Component Engineering. 2005, 125–140

    Chapter  Google Scholar 

  9. Ziadi T, Hélouët L, Jézéquel J M. Towards a UML profile for software product lines. In: Proceedings of the International Workshop on Software Product-Family Engineering. 2003, 129–139

    Google Scholar 

  10. Fischbein D, Uchitel S, Braberman V A. A foundation for behavioural conformance in software product line architectures. In: Proceedings of the ISSTA 2006 Workshop on Role of Software Architecture for Testing and Analysis. 2006, 39–48

    Google Scholar 

  11. Fantechi A, Gnesi S. Formal modeling for product families engineering. In: Proceedings of the 12th IEEE International Conference on Software Product Lines. 2008, 193–202

    Google Scholar 

  12. Asirelli P, Beek MH, Gnesi S, Fantechi A. Deontic logics for modeling behavioural variability. In: Proceedings of the 3rd International Workshop on Variability Modeling of Software-Intensive Systems. 2009, 71–76

    Google Scholar 

  13. Classen A, Heymans P, Schobbens P Y, Legay A, Raskin J F. Model checking lots of systems: efficient verification of temporal properties in software product lines. In: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering. 2010, 335–344

    Google Scholar 

  14. Fisler K, Krishnamurthi S. Modular verification of collaboration-based software designs. In: Proceedings of European Software Engineering Conference and ACM International Symposium on Foundations of Software Engineering. 2001, 152–163

    Google Scholar 

  15. Holzmann G J. The SPIN Model Checker: Primer and Reference Manual. Boston: Addison-Wesley Professional, 2004

    Google Scholar 

  16. Cornet J. Separation of functional and non-functional aspects in transactional level models of systems-on-chip. Grenoble INP Group, 2008

    Google Scholar 

  17. Clements P, Northrop L. Software Product Lines: Practices and Patterns. 3rd ed. Boston: Addison-Wesley Professional, 2001

    Google Scholar 

  18. Helmstetter C, Ponsini O. A comparison of two SystemC/TLM semantics for formal verification. In: Proceedings of the 6th ACM/IEEE International Conference on Formal Methods and Models for Co-Design. 2008, 59–68

    Chapter  Google Scholar 

  19. Ponsini O, Serwe W. A schedulerless semantics of TLM models written in SystemC via translation into LOTOS. In: Proceedings of the International Symposium on Formal Methods. 2008, 278–293

    Google Scholar 

  20. Moy M. Techniques and tools for the verification of systems-on-a-chip at the transaction level. Institute National Polytechnigue de Grenoble-INPG, 2005

    Google Scholar 

  21. Moy M, Maraninchi F, Maillet-Contoz L. LusSy: an open tool for the analysis of systems-on-a-chip at the transaction level. Design Automation for Embedded Systems, 2005, 10(21): 73–104

    Article  Google Scholar 

  22. Karlsson D, Eles P, Peng Z. Formal verification of SystemC designs using a petri-net based representation. In: Proceedings of the IEEE Conference on Design, Automation and Test in Europe. 2006, 1228–1233

    Google Scholar 

  23. Kroening D, Sharygina N. 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. 2005, 101–110

    Google Scholar 

  24. Traulsen C, Cornet J, Moy M, Maraninchi F. A SystemC/TLM semantics in Promela and its possible applications. In: Proceedings of the International SPIN Workshop on Model Checking Software. 2007, 204–222

    Chapter  Google Scholar 

  25. Habibi A, Ahmed A, Mohamed O A, Tahar S. On the design and verification methodology of the look-aside interface. In: Proceedings of the Conference on Design, Automation and Test in Europe. 2004, 290–295

    Google Scholar 

  26. Patel H D, Shukla S K. Model-driven validation of SystemC designs. In: Proceedings of the 44th ACM/IEEE Annual Design Automation Conference. 2007, 29–34

    Google Scholar 

  27. Peled D A, Wilke T. Stutter-invariant temporal properties are expressible without the next-time operator. Information Processing Letters, 1997, 63(5): 243–246

    Article  MathSciNet  Google Scholar 

  28. Li H C, Krishnamurthi S, Fisler K. Verifying cross-cutting features as open systems. In: Proceedings of ACM Symposium on Foundations of Software Engineering. 2002, 89–98

    Google Scholar 

  29. Li H C, Krishnamurthi S, Fisler K. Modular Verification of open features using three-valued model checking. Automated Software Engineering, 2005, 12(3): 349–382

    Article  Google Scholar 

  30. Blundell C, Fisler K, Krishnamurthi S, Hentenryck P V. Parameterized interfaces for open system verification of product lines. In: Proceedings of the 19th IEEE International Conference on Automated Software Engineering. 2004, 258–267

    Google Scholar 

  31. Thang N T, Katayama T. Specification and verification of intercomponent constraints in CTL. ACM SIGSOFT Software Engineering Notes, 2006, 31(2): 81–88

    Article  Google Scholar 

  32. He F, Gao Y, Yin L. Efficient software product-line model checking using induction and a SAT solver. Frontiers of Computer Science, 2018, 12(2): 264–279

    Article  Google Scholar 

  33. Michelli G D. Synthesis and Optimization of Digital Circuits. 1st ed. New York: McGraw-Hill Higher Education, 1994

    Google Scholar 

Download references

Acknowledgements

The work was supported by the National Key R&D Program of China (2018YFB1004202) and by Laboratory of Software Engineering for Complex Systems.

Author information

Authors and Affiliations

  1. College of Computer, National University of Defense Technology, Changsha, 410073, China

    Tun Li & Qingping Tan

  2. Laboratory of Software Engineering for Complex Systems, Changsha, 410073, China

    Tun Li & Qingping Tan

  3. Jiangnan Institute of Computing Technology, Wuxi, 214083, China

    Jun Ye

Authors
  1. Tun Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jun Ye
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Qingping Tan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tun Li.

Additional information

Tun Li is a professor in the College of Computer, National University of Defense Technology, China. He received his PhD degree in Computer Science from National University of Defense Technology in 2003. His research interests include electronic design automation and SoC design verification.

Jun Ye received his PhD degree in Computer Science from National University of Defense Technology, China in 2011. His main research interests include formal verification verification of AOP/FOP, hardware and software co-design, adaptive dynamic compilation, garbage collection, Java Virtual Machine.

Qingping Tan is a professor and PhD supervisor in College of Computer at National University of Defense Technology, China. His research interests include intelligent software, distributed software engineering, and high dependable software.

Electronic supplementary material

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Li, T., Ye, J. & Tan, Q. Towards functional verifying a family of systemC TLMs. Front. Comput. Sci. 14, 53–66 (2020). https://doi.org/10.1007/s11704-018-8254-y

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11704-018-8254-y

Keywords

Search

Navigation