Towards functional verifying a family of SystemC TLMs
Tun LI1,2(), Jun YE3, Qingping TAN1,2
1. College of Computer, National University of Defense Technology, Changsha 410073, China 2. Laboratory of Software Engineering for Complex Systems, Changsha 410073, China 3. Jiangnan Institute of Computing Technology, Wuxi 214083, China
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.
. [J]. Frontiers of Computer Science, 2020, 14(1): 53-66.
Tun LI, Jun YE, Qingping TAN. Towards functional verifying a family of SystemC TLMs. Front. Comput. Sci., 2020, 14(1): 53-66.
J Hu, T Li, S Li, Equivalence checking between SLM and TLM using coverage directed simulation. Frontiers of Computer Science, 2015, 9(6): 934–943 https://doi.org/10.1007/s11704-015-4257-0
2
T Li, Y Guo, W Liu, M Tang. 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 https://doi.org/10.1145/2483028.2483070
3
W Liu, R Wang, X Fu, J, Wang W Dong, X Mao. Counterexample-preserving reduction for symbolic model checking. Journal of Applied Mathematics, 2014, 2014: 1–13
4
L Zhang, W Qu, Y Huo, Y Guo, S Li. An SAT-based method to multithreaded program verification for mobile crowdsourcing networks. Wireless Communications and Mobile Computing, 2018, 2018: 59–66
5
J Ye, T Li, Q Tan. 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
J Ye, Q Tan, T Li. Feature-oriented refactoring proposal for transaction level models in SoCLib. In: Proceeding of 2010 Forum on Specification and Design Languages. 2010, 22–27
7
J Ye, Q Tan, T Li. 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
S Apel, T Leich, M Rosenmuller, G Saake. 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 https://doi.org/10.1007/11561347_10
9
T Ziadi, L Hélouët, J M Jézéquel. Towards a UML profile for software product lines. In: Proceedings of the International Workshop on Software Product-Family Engineering. 2003, 129–139
10
D Fischbein, S Uchitel, V A Braberman. 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 https://doi.org/10.1145/1147249.1147254
11
A Fantechi, S Gnesi. Formal modeling for product families engineering. In: Proceedings of the 12th IEEE International Conference on Software Product Lines. 2008, 193–202 https://doi.org/10.1109/SPLC.2008.45
12
P Asirelli, M H Beek, S Gnesi, A Fantechi. Deontic logics for modeling behavioural variability. In: Proceedings of the 3rd International Workshop on Variability Modeling of Software-Intensive Systems. 2009, 71–76
13
A Classen, P Heymans, P Y Schobbens, A Legay, J F Raskin. 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 https://doi.org/10.1145/1806799.1806850
14
K Fisler, S Krishnamurthi. 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 https://doi.org/10.1145/503209.503231
15
G J Holzmann. The SPIN Model Checker: Primer and Reference Manual. Boston: Addison-Wesley Professional, 2004
16
J Cornet. Separation of functional and non-functional aspects in transactional level models of systems-on-chip. Grenoble INP Group, 2008
17
P Clements, L Northrop. Software Product Lines: Practices and Patterns. 3rd ed. Boston: Addison-Wesley Professional, 2001
18
C Helmstetter, O Ponsini. 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 https://doi.org/10.1109/MEMCOD.2008.4547687
19
O Ponsini, W Serwe. 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 https://doi.org/10.1007/978-3-540-68237-0_20
20
M Moy. Techniques and tools for the verification of systems-on-a-chip at the transaction level. Institute National Polytechnigue de GrenobleINPG, 2005
21
M Moy, F Maraninchi, L Maillet-Contoz. 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 https://doi.org/10.1007/s10617-006-9044-6
22
D Karlsson, P Eles, Z Peng. 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 https://doi.org/10.1109/DATE.2006.244076
23
D Kroening, N Sharygina. 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 https://doi.org/10.1109/MEMCOD.2005.1487900
24
C Traulsen, J Cornet, M Moy, F Maraninchi. A SystemC/TLM semantics in Promela and its possible applications. In: Proceedings of the International SPIN Workshop on Model Checking Software. 2007, 204–222 https://doi.org/10.1007/978-3-540-73370-6_14
25
A Habibi, A Ahmed, O A Mohamed, S Tahar. 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
H D Patel, S K Shukla. Model-driven validation of SystemC designs. In: Proceedings of the 44th ACM/IEEE Annual Design Automation Conference. 2007, 29–34
27
D A Peled, T Wilke. Stutter-invariant temporal properties are expressible without the next-time operator. Information Processing Letters, 1997, 63(5): 243–246 https://doi.org/10.1016/S0020-0190(97)00133-6
28
H C Li, S Krishnamurthi, K Fisler. Verifying cross-cutting features as open systems. In: Proceedings of ACM Symposium on Foundations of Software Engineering. 2002, 89–98 https://doi.org/10.1145/587051.587066
29
H C Li, S Krishnamurthi, K Fisler. Modular Verification of open features using three-valued model checking. Automated Software Engineering, 2005, 12(3): 349–382 https://doi.org/10.1007/s10515-005-2643-9
30
C Blundell, K Fisler, S Krishnamurthi, P V Hentenryck. 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
N T Thang, T Katayama. Specification and verification of intercomponent constraints in CTL. ACM SIGSOFT Software Engineering Notes, 2006, 31(2): 81–88 https://doi.org/10.1145/1118537.1123067
32
F He, Y Gao, L Yin. Efficient software product-line model checking using induction and a SAT solver. Frontiers of Computer Science, 2018, 12(2): 264–279 https://doi.org/10.1007/s11704-016-6048-7
33
G D Michelli. Synthesis and Optimization of Digital Circuits. 1st ed. New York: McGraw-Hill Higher Education, 1994
