Towards functional verifying a family of SystemC TLMs

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 mutefeature-modules (MFM), which will avoid duplicated veri-fication. 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.

Keywords

system-on-a-chip / transaction level model / SystemC / feature-oriented / functional verification

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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[12] Asirelli P, Beek M H, 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

[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

[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

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

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

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

[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

[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

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

[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

[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

[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

[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

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

[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

[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

[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

[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

[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

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

[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

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

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature