|
|
|
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 |
|
|
|
|
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
|
|
Corresponding Author(s):
Tun LI
|
|
Just Accepted Date: 20 November 2018
Online First Date: 26 March 2019
Issue Date: 24 September 2019
|
|
| 1 |
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
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
| |
Shared |
|
|
|
|
| |
Discussed |
|
|
|
|