TY - GEN
T1 - SMT-based stimuli generation in the SystemC verification library
AU - Wille, Robert
AU - Große, Daniel
AU - Haedicke, Finn
AU - Drechsler, Rolf
PY - 2010
Y1 - 2010
N2 - Modelling at the Electronic System Level (ESL) is the established approach of the major System-on-chip (SoC) companies. While in the past ESL design covered design methodologies only, today also verification and debugging is included. To improve the verification process, testbench automation has been introduced highlighted as constraint-based random simulation. In SystemC -the de facto standard modelling language for ESL- constraint-based random simulation is available through the SystemC Verification (SCV) library. However, the underlying constraint-solver is based on Binary Decision Diagrams (BDDs) and hence suffers from memory problems. In this chapter, we propose the integration of new techniques for stimuli generation based on Satisfiability Modulo Theories (SMT). Since SMT solvers are designed to determine a single satisfying solution only, several strategies are proposed forcing the solver to generate more than one stimuli from different parts of the search space. Experiments demonstrate the advantage of the proposed approach and the developed strategies in comparison to the original BDD-based method.
AB - Modelling at the Electronic System Level (ESL) is the established approach of the major System-on-chip (SoC) companies. While in the past ESL design covered design methodologies only, today also verification and debugging is included. To improve the verification process, testbench automation has been introduced highlighted as constraint-based random simulation. In SystemC -the de facto standard modelling language for ESL- constraint-based random simulation is available through the SystemC Verification (SCV) library. However, the underlying constraint-solver is based on Binary Decision Diagrams (BDDs) and hence suffers from memory problems. In this chapter, we propose the integration of new techniques for stimuli generation based on Satisfiability Modulo Theories (SMT). Since SMT solvers are designed to determine a single satisfying solution only, several strategies are proposed forcing the solver to generate more than one stimuli from different parts of the search space. Experiments demonstrate the advantage of the proposed approach and the developed strategies in comparison to the original BDD-based method.
KW - Constraint-based random simulation
KW - SAT modulo theories
KW - SystemC verification library
UR - http://www.scopus.com/inward/record.url?scp=78651548250&partnerID=8YFLogxK
U2 - 10.1007/978-90-481-9304-2_14
DO - 10.1007/978-90-481-9304-2_14
M3 - Conference contribution
AN - SCOPUS:78651548250
SN - 9789048193035
T3 - Lecture Notes in Electrical Engineering
SP - 227
EP - 244
BT - Advances in Design Methods from Modeling Languages for Embedded Systems and SoC's - Selected Contributions on Specification, Design, and Verification from FDL 2009
A2 - Borrione, Dominique
ER -