research-article

Concurrency-oriented verification and coverage of system-level designs

Author:

Alper SenAuthors Info & Claims

ACM Transactions on Design Automation of Electronic Systems (TODAES), Volume 16, Issue 4

Article No.: 37, Pages 1 - 25

https://doi.org/10.1145/2003695.2003697

Published: 27 October 2011 Publication History

Abstract

Correct concurrent System-on-Chips (SoCs) are very hard to design and reason about. In this work, we develop an automated framework complete with concurrency-oriented verification and coverage techniques for system-level designs. Our techniques are different from traditional simulation-based reliability techniques, since concurrency information is often lost in traditional techniques. We preserve concurrency information to obtain unique verification techniques that allow us to predict potential errors (formulated as transaction-level assertions) from error-free simulations. In order to do this, we exploit the inherent concurrency in the designs to generate and analyze novel partial-order simulation traces. Additionally, to evaluate the confidence on verification results and the gauge progress of verification, we develop novel mutation testing based on concurrent coverage metrics. Mutation testing is a fault insertion-based simulation technique that has been successfully applied in software testing. We present a comprehensive list of mutation operators for SystemC, similar to behavioral fault models, and show the effectiveness of these operators by relating them to actual bug patterns. We have successfully applied our verification and coverage techniques on industrial systems and demonstrated that current verification test suites need to be improved for concurrent designs, and we have found errors in systems that were tested previously.

References

[1]

Abramovici, M., Breuer, M. A., and Friedman, A. D. 1990. Digital Systems Testing and Testable Design. Computer Science Press, New York.

[2]

Andrews, J. H., Briand, L. C., and Labiche, Y. 2005. Is mutation an appropriate tool for testing experiments&quest; In Proceedings of the 27th International Conference on Software Engineering (ICSE). 402--411.

Digital Library

[3]

Bailey, B. 2009. Can mutation analysis help fix our broken coverage metrics&quest; In Proceedings of the 4^th International Haifa Verification Conference (HVC '08). 5--5.

Digital Library

[4]

Blanc, N. and Kroening, D. 2010. Race analysis for systemc using model checking. ACM Trans. Des. Autom, Electron. Syst. 15, 3, 1--32.

Digital Library

[5]

Bombieri, N., Fummi, F., and Pravadelli, G. 2008. A mutation model for the SystemC TLM2.0 communication interfaces. In Proceedings of the Conference on Design Automation and Test in Europe (DATE). ACM, New York, 396--401.

Digital Library

[6]

Bombieri, N., Fummi, F., Pravadelli, G., Hampton, M., and Letombe, F. 2009. Functional qualification of TLM verification. In Proceedings of the Conference on Design Automation and Test in Europe (DATE). ACM, New York, 190--195.

Digital Library

[7]

Bradbury, J., Cordy, J., and Dingel, J. 2006. Mutation operators for Concurrent Java (J2SE 5.0). In Workshop on Mutation Analysis, 2006. 11.

Digital Library

[8]

Budd, T. A. 1981. Mutation analysis: Ideas, examples, problems and prospects. In Computer Program Testing, North-Holland, Amsterdam, 129--148.

[9]

Campenhout, D. V., Al-Asaad, H., Hayes, J. P., Mudge, T., and Brown, R. B. 1998. High-level design verification of microprocessors via error modeling. ACM Trans. Des. Autom. Electron. Syst, 3, 4, 581--599.

Digital Library

[10]

Certitude. 2010. Springsoft, Certitude website. http://www.springsoft.com/.

[11]

Ecker, W., Esen, V., Steininger, T., Velten, M., and Hull, M. 2007. Implementation of a transaction level assertion framework in SystemC. In Proceedings of the Conference on Design Automation and Test in Europe (DATE). ACM, New York, 1--6.

Digital Library

[12]

Fallah, F., Devadas, S., and Keutzer, K. 1998. OCCOM: Efficient computation of observability-based code coverage metrics for functional verification. In Proceedings of the Design Automation Conference (DAC). ACM, New York,152--157.

Digital Library

[13]

Farchi, E., Nir, Y., and Ur, S. 2003. Concurrent bug patterns and how to test them. In Proceedings of the International Parallel and Distributed Processing Symposium (IPDPS).

Digital Library

[14]

Foster, H. D., Krolnik, A. C., and Lacey, D. J. 2004. Assertion-Based Design 2nd Ed., Springer, Berlin.

Digital Library

[15]

Frankl, P. G., Weiss, S. N., and Hu, C. 1997. All-uses vs mutation testing: An experimental comparison of effectiveness. J. Syst. Softw. 38, 3, 235--253.

Digital Library

[16]

Fummi, F. and Pravadelli, G. 2007. Too few or too many properties&quest; Measure it by ATPG&excl; J. Electron. Testing 23, 5, 373--388.

Digital Library

[17]

Garg, V. K. 2002. Elements of Distributed Computing. Wiley, New York.

Digital Library

[18]

Ghenassia, F. 2005. Transaction-Level Modeling with SystemC. Springer, Berlin.

Digital Library

[19]

Grosse, D. and Drechsler, R. 2003. Formal verification of LTL formulas for SystemC designs. In Proceedings of the International Symposium on Circuits and Systems (ISCAS). 245--248.

[20]

Habibi, A. and Tahar, S. 2004. On the extension of SystemC by SystemVerilog assertions. In Proceedings of the Canadian Conference on Electrical and Computer Engineering. 1869--1872.

[21]

Hampton, M. and Petithomme, S. 2007. Leveraging a commercial mutation analysis tool for research. In Proceedings of Testing: Academic and Industrial Conference Practice and Research Techniques (MUTATION'07). 203--209.

Digital Library

[22]

Helmstetter, C., Maraninchi, F., and Maillet-Contoz, L. 2009. Full simulation coverage for SystemC transaction-level models of systems-on-a-chip. Formal Methods Syst, Des. 35, 2, 152--189.

Digital Library

[23]

Helmstetter, C., Maraninchi, F., Maillet-Contoz, L., and Moy, M. 2006. Automatic generation of schedulings for improving the test coverage of systems-on-a-chip. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD). 171--178.

Digital Library

[24]

Helmstetter, C. and Ponsini, O. 2008. A comparison of two SystemC/TLM semantics for formal verification. In Proceedings of the International Conference on Formal Methods and Models for Co-Design (MEMOCODE). 59--68.

[25]

Hsiao, M. S., Rudnick, E. M., and Patel, J. H. 2000. Dynamic state traversal for sequential circuit test generation. ACM Trans. Des. Autom. Electron. Syst. 5, 3, 548--565.

Digital Library

[26]

Kasuya, A. and Tesfaye, T. 2007. Verification methodologies in a TLM-to-RTL design flow. In Proceedings of the Design Automation Conference (DAC). 199--204.

Digital Library

[27]

Kundu, S., Ganai, M., and Gupta, R. 2008. Partial order reduction for scalable testing of SystemC TLM designs. In Proceedings of the 45th Annual Design Automation Conference (DAC'08). 936--941.

Digital Library

[28]

Kupferman, O., Li, W., and Seshia, S. A. 2008. A theory of mutations with applications to vacuity, coverage, and fault tolerance. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD). 1--9.

Digital Library

[29]

Lamport, L. 1978. Time, clocks, and the ordering of events in a distributed system. Comm. ACM 21, 7, 558--565.

Digital Library

[30]

Li, N., Praphamontripong, U., and Offutt, J. 2009. An experimental comparison of four unit test criteria: Mutation, edge-pair, all-uses and prime path coverage. In Proceedings of the IEEE International Conference on Software Testing Verification and Validation Workshop. IEEE, Los Alamitos, CA, 220--229.

Digital Library

[31]

Ma, Y.-S., Offutt, J., and Kwon, Y. R. 2005. MuJava: An automated class mutation system: Research articles. Softw. Test. Verification Reliability 15, 2, 97--133.

Digital Library

[32]

Mittal, N. and Garg, V. K. 2001. Computation slicing: Techniques and theory. In Proceedings of the Symposium on Distributed Computing (DISC). 78--92.

Digital Library

[33]

Offutt, J., Ammann, P., and Liu, L. 2006. Mutation testing implements grammar-based testing. In Proceedings of the 2nd Workshop on Mutation Analysis. 12.

Digital Library

[34]

Offutt, J. and Untch, R. H. 2001. Mutation 2000: Uniting the Orthogonal. Kluwer, Amsterdam.

[35]

OSCI 2010. Open SystemC initiative, http://www.systemc.org/.

[36]

Pinto Ferraz Fabbri, S. C., Delamaro, M., Maldonado, J., and Masiero, P. 1994. Mutation analysis testing for finite state machines. In Proceedings of the 5th International Symposium on Software Reliability Engineering. 220--229.

[37]

Pierre, L. and Ferro, L. 2008. A tractable and fast method for monitoring SystemC TLM specifications. IEEE Trans. Computers 57, 10, 1346--1356.

Digital Library

[38]

SCRV 2009. SystemC runtime verification toolbox (SCRV). http://mytrac.assembla.com/scrv/wiki.

[39]

Sen, A. and Garg, V. K. 2007. Formal verification of simulation traces using computation slicing. IEEE Trans. Computers 56, 4, 511--527.

Digital Library

[40]

Sen, A., Ogale, V., and Abadir, M. S. 2008. Predictive runtime verification of multi-processor SoCs in SystemC. In Proceedings of the Design Automation Conference (DAC). 948--953.

Digital Library

[41]

Sen, K., Rosu, G., and Agha, G. 2003. Runtime safety analysis of multithreaded programs. In Proceedings of the Symposium on the Foundations of Software Engineering (FSE).

Digital Library

[42]

Tabakov, D., Vardi, M. Y., Kamhi, G., and Singerman, E. 2008. A temporal language for SystemC. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD). 1--9.

Digital Library

[43]

Tasiran, S. and Keutzer, K. 2001. Coverage metrics for functional validation of hardware designs. IEEE Des. Test Comput. 18, 4, 36--45.

Digital Library

[44]

Tong, J. G., Boule, M., and Zilic, Z. 2010. Defining and providing coverage for assertion-based dynamic verification. J. Electron. Testing 26, 2, 211--225.

Digital Library

[45]

Vardi, M. Y. 2007. Formal techniques for SystemC verification; position paper. In Proceedings of the Design Automation Conference (DAC). 188--192.

Digital Library

[46]

Walsh, P. J. 1985. A measure of test case completeness (software, engineering). Ph.D. dissertation, State University of New York at Binghamton.

Digital Library

[47]

Weiser, M. 1982. Programmers use slices when debugging. Comm. ACM 25, 7, 446--452.

Digital Library

Cited By

Herdt VGroße DDrechsler RHerdt VGroße DDrechsler R(2023)Abdeckungsgesteuertes Testen für skalierbare Verifikation virtueller PrototypenVerbessertes virtuelles Prototyping10.1007/978-3-031-18174-0_5(127-152)Online publication date: 1-Jan-2023
https://doi.org/10.1007/978-3-031-18174-0_5
Hassan MGroße DDrechsler RHassan MGroße DDrechsler R(2022)AMS Enhanced Code Coverage Verification EnvironmentEnhanced Virtual Prototyping for Heterogeneous Systems10.1007/978-3-031-05574-4_4(45-86)Online publication date: 3-May-2022
https://doi.org/10.1007/978-3-031-05574-4_4
Lin BXie F(2020)A Systematic Investigation of State-of-the-Art SystemC VerificationJournal of Circuits, Systems and Computers10.1142/S021812662030013529:15(2030013)Online publication date: 18-Jul-2020
https://doi.org/10.1142/S0218126620300135
Show More Cited By

Index Terms

Recommendations

Verification and coverage of message passing multicore applications
Special section on verification challenges in the concurrent world

We describe verification and coverage methods for multicore software that uses message passing libraries for communication. Specifically, we provide techniques to improve reliability of software using the new industry standard MCAPI by the Multicore ...
State coverage: a structural test adequacy criterion for behavior checking
ESEC-FSE '07: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering

We propose a new language-independent, structural test adequacy criterion called state coverage. State coverage measures whether unit-level tests check the outputs and sideeffects of a program.

State coverage differs in several respects from existing ...
State coverage: a structural test adequacy criterion for behavior checking
ESEC-FSE companion '07: The 6th Joint Meeting on European software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering: companion papers

We propose a new language-independent, structural test adequacy criterion called state coverage. State coverage measures whether unit-level tests check the outputs and side effects of a program.

State coverage differs in several respects from existing ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Design Automation of Electronic Systems

ACM Transactions on Design Automation of Electronic Systems Volume 16, Issue 4

October 2011

326 pages

ISSN:1084-4309

EISSN:1557-7309

DOI:10.1145/2003695

Issue’s Table of Contents

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 27 October 2011

Accepted: 01 February 2011

Revised: 01 January 2011

Received: 01 July 2010

Published in TODAES Volume 16, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
422
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)3

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Herdt VGroße DDrechsler RHerdt VGroße DDrechsler R(2023)Abdeckungsgesteuertes Testen für skalierbare Verifikation virtueller PrototypenVerbessertes virtuelles Prototyping10.1007/978-3-031-18174-0_5(127-152)Online publication date: 1-Jan-2023
https://doi.org/10.1007/978-3-031-18174-0_5
Hassan MGroße DDrechsler RHassan MGroße DDrechsler R(2022)AMS Enhanced Code Coverage Verification EnvironmentEnhanced Virtual Prototyping for Heterogeneous Systems10.1007/978-3-031-05574-4_4(45-86)Online publication date: 3-May-2022
https://doi.org/10.1007/978-3-031-05574-4_4
Lin BXie F(2020)A Systematic Investigation of State-of-the-Art SystemC VerificationJournal of Circuits, Systems and Computers10.1142/S021812662030013529:15(2030013)Online publication date: 18-Jul-2020
https://doi.org/10.1142/S0218126620300135
Herdt VGroße DDrechsler RHerdt VGroße DDrechsler R(2020)Coverage-Guided Testing for Scalable Virtual Prototype VerificationEnhanced Virtual Prototyping10.1007/978-3-030-54828-5_5(119-142)Online publication date: 15-Oct-2020
https://doi.org/10.1007/978-3-030-54828-5_5
Hassan MGrose DLe HVortler TEinwich KDrechsler R(2018)Testbench qualification for SystemC-AMS timed data flow models2018 Design, Automation & Test in Europe Conference & Exhibition (DATE)10.23919/DATE.2018.8342125(857-860)Online publication date: Mar-2018
https://doi.org/10.23919/DATE.2018.8342125
Hassan MHerdt VLe HChen MGroße DDrechsler R(2017)Data flow testing for virtual prototypesProceedings of the Conference on Design, Automation & Test in Europe10.5555/3130379.3130469(380-385)Online publication date: 27-Mar-2017
https://dl.acm.org/doi/10.5555/3130379.3130469
Hassan MHerdt VLe HChen MGrose DDrechsler R(2017)Data flow testing for virtual prototypesDesign, Automation & Test in Europe Conference & Exhibition (DATE), 201710.23919/DATE.2017.7927020(380-385)Online publication date: Mar-2017
https://doi.org/10.23919/DATE.2017.7927020
Huo CClause J(2016)Interpreting Coverage Information Using Direct and Indirect Coverage2016 IEEE International Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST.2016.20(234-243)Online publication date: Apr-2016
https://doi.org/10.1109/ICST.2016.20
Grosse DLe HHassan MDrechsler R(2016)Guided lightweight Software test qualification for IP integration using Virtual Prototypes2016 IEEE 34th International Conference on Computer Design (ICCD)10.1109/ICCD.2016.7753347(606-613)Online publication date: Oct-2016
https://doi.org/10.1109/ICCD.2016.7753347
Sen AKalaci O(2014)Hybrid dynamic data race detection in systemCProceedings of the 2014 Forum on Specification and Design Languages (FDL)10.1109/FDL.2014.7119347(1-6)Online publication date: Oct-2014
https://doi.org/10.1109/FDL.2014.7119347
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents