Symbolic model checking on SystemC designs
- Resource Type
- Conference
- Authors
- Chou, Chun-Nan; Ho, Yen-Sheng; Hsieh, Chiao; Huang, Chung-Yang
- Source
- DAC Design Automation Conference 2012 Design Automation Conference (DAC), 2012 49th ACM/EDAC/IEEE. :327-333 Jun, 2012
- Subject
- Components, Circuits, Devices and Systems
Communication, Networking and Broadcast Technologies
Computing and Processing
Engines
Cost accounting
Reachability analysis
Software
Semantics
Integrated circuit modeling
Hardware
Formal Verification
Symbolic Model Checking
SystemC
- Language
- ISSN
- 0738-100X
SystemC is a de-facto standard for modeling system-level designs in the early design stage. Verifying SystemC designs is critical in the design process since it can avoid error propagation down to the final implementation. Recent works exploit the software model checking techniques to tackle this important issue. But they abstract away relevant semantic aspects or show limited scalability. In this paper, we devise a symbolic model checking technique using bounded model checking and induction to formally verify SystemC designs. We introduce the notions of behavioral states and transitions to guarantee the soundness of our approach. The experiments show the scalability and the efficiency of our method.