SOURCE ARCHIVE
EXTRACTED CONTENT
46,790 chars Minimal Stimuli Generation
in Simulation-based Verification
Shuo Yang∗ Robert Wille∗† Daniel Große‡ Rolf Drechsler∗†
∗Institute of Computer Science, University of Bremen, 28359 Bremen, Germany
†Cyber-Physical Systems, DFKI GmbH, 28359 Bremen, Germany
‡solvertec GmbH, 28359 Bremen, Germany
{shuo,rwille,drechsle}@informatik.uni-bremen.de grosse@solvertec.de
Abstract—Simulation-based verification is still the state-of-the- insufficiently considered cases. Commonly, the determination art when checking the correctness of complex Systems-on-Chips. of such stimuli is performed using constraint-based stimuli In particular, constraint-based simulation is popular, since here generation (see e.g. [21], [16], [18]). Considering the insuffi- dedicated stimuli are generated which trigger certain corner- case behavior. However, to the best of our knowledge, only ciently triggered cases only, constraints for stimuli generation heuristic methods have been introduced so far. In this paper, are formulated and, subsequently, solved by a constraint solver. we propose an approach that determines a minimal set of By this, stimuli result that directly trigger scenarios which have stimuli for the desired set of scenarios to be simulated. For not sufficiently been covered yet. this purpose, we are making use of solving techniques from Boolean satisfiability. Experimental evaluations demonstrate that Overall, this practice is a coverage-driven verification pro- the proposed approach can be applied to generate very compact cess. The successful adoption of this methodology continues stimuli sets. Furthermore, the proposed approach can be used to encouraging new research in this field. One trend intends to evaluate the quality of results obtained by heuristic methods. improve constraint-based stimuli generation by boosting the Keywords-Constraint-based Simulation; Simulation-based Ver- ability of constraint-stimuli generation (see e.g. [13], [20], ification; Coverage [19], [6]). In [13], [20], constraints are automatically generated I. INTRODUCTION either (1) for improving controllability of internal signals and Verification continues to be a major bottleneck in the current thereby achieving a high coverage [13] or (2) for reduc- design flow for embedded systems. In particular, functional ing the time-consuming and error-prone manual constraint verification, i.e. ensuring the functional correctness of a de- composition process [20]. In contrast, other work focus on sign, still dominates the overall costs in the development of manipulating existing constraints either to obtain a compact modern complex Systems-on-Chips (SoCs). set of stimuli (see e.g. [19]) or to increase the efficiency of Different approaches have thereby been developed to im- the respective solving process (see e.g. [6], [18]). prove functional verification. Formal methods, for instance However, to the best of our knowledge exact constraint- property checking (see e.g. [9], [4]) and completeness check- based stimuli generation, i.e. the determination of a minimal ing (see e.g. [8], [12], [7]), exploit the design’s behavior ex- number of stimuli satisfying the coverage requirement, has not haustively. However, they suffer inevitably from high compu- been considered so far. This is done in the paper at hand. For tational costs. Consequently, the much faster simulation-based this purpose, we propose: verification (see e.g. [3]) is still the dominating verification • An iterative work-flow: First, it is tried to sufficiently method in industry. cover the DUV with one stimulus only. If no such Here, a number of stimuli is either determined randomly stimulus exists, the number of stimuli to be generated considering the global functionality of a Design Under Ver- is increased by 1. This is iterated until a set of stimuli ification (DUV) or directed to verify certain behaviors, e.g. satisfying the coverage requirement can be determined. corner cases. Afterwards, the stimuli are applied to the DUV, • A dedicated SAT-based generation: In order to determine and their responses are checked, i.e. compared to the expected the desired stimuli or to prove that the coverage require- results. ments cannot be satisfied with the currently considered In order to evaluate the verification quality, coverage metrics number of stimuli, we encode the respective problem as have been introduced (see e.g. [10], [17]). They abstract certain an instance of Boolean satisfiability. Then, off-the-shelf functionality of the DUV (e.g. in terms of scenarios) which solvers are applied to solve the problem is supposed to be checked. With them, coverage analysis methods can efficiently eval- Experimental evaluations show the applicability of the pro- uate whether the DUV has sufficiently been checked or posed approach. On the one hand side, it is shown that very not (see e.g. [14], [15], [1], [2]). In the former case, the compact sets of stimuli can be generated. On the other hand, simulation-based verification process terminates. Otherwise, the proposed approach allows for an evaluation of the results further dedicated stimuli are generated aiming for covering the obtained by heuristic methods.
II. PROBLEM FORMULATION Definition 5. A set of stimuli is considered sufficient iff it
This section formally introduces the problem addressed in contains stimuli sufficiently covering all scenarios, i.e. each
this paper. scenario Si is triggered by at least tS different stimuli. In the
following, sufficient sets of stimuli are denoted by
In general, it is infeasible to exhaustively simulate a DUV i Ssuff .
with all its possible input assignments. Therefore, simulation- Due to various methods used for the stimuli generation, the
based verification is applied in order to explicitly cover certain size of the sufficient stimuli Ssuff may vary significantly. corner-case functionalities of the DUV. For this purpose, user- defined scenarios are formulated for which dedicated stimuli Example 2. Consider the DUV composed of a PC and an shall be generated. Such a scenario is defined as follows: ALU, where scenarios S0 and S1 for the PC are defined similar Definition 1. A scenario Si (0 ≤ i < n) is a Boolean to the one of Example 1. For the ALU, a scenario S2 = (op = function over variables from the set of DUV signals. For add) forcing an ALU addition is introduced (the op is the the specification of a scenario, a constraint is formulated select input to define the operation to be performed on the by using the typical HDL operators such as e.g. logic AND, data inputs of the ALU). Finally, assume that each scenario is logic OR, arithmetic operators, and relational operators. In supposed to be triggered at least 10 times, i.e. ∧2i=0(tS = 10). i A naive approach would individually generate stimuli for each the following, scenario and constraint is used interchangeably. scenario eventually leading to a total of 30 stimuli. However, The set of scenarios is denoted by S = {S0, . . . , Sn−1}. since an ALU addition (op = add) may be followed by an PC The goal of methods for constraint-based random simulation incrementation (load = 0), in fact, significant less stimuli are is to generate a stimulus which triggers at least one scenario. required in order to satisfy the coverage criteria. For this purpose, a proper constraint is constructed as input for the respective engines. In general, a sufficient stimuli set of minimal size is inter- Definition 2. A stimulus satisfying at least one scenario can esting. The term ”minimal” is thereby formalized as follows: be derived from a solution to the following constraint: Definition 6. Given a verification task and a sufficient n∨ set Ssuff of stimuli. The set Ssuff of stimuli is called −1 Si (1) minimal, iff no other sufficient set Ssuff′ of stimuli with i=0 |Ssuff | > |Ssuff′ | exists.
Example 1. Consider a program counter (PC), where the A minimal set of sufficient stimuli provides a lower-bound
inputs reset and load define the renewal strategy on the to the amount of stimuli that have to be applied to a DUV. current program address pc. Possible scenarios are for in- Commonly, in order to achieve such minimal stimuli set, one stance S0 = ((reset = 0)∧(load = 0)) (the pc is incremented stimulus must trigger multiple scenarios at the same time. by 1) and S1 = ((reset = 0) ∧ (load = 1)) (the pc is renewed This fact is important since bugs often occur when multiple with an arbitrary value according to the address input of behaviors of the DUV occur simultaneously [1]. Furthermore, the program counter). Then, the stimulus {pc = 0x00F F , a minimal set of stimuli is compact and, thus, suitable to form reset = 0, load = 0} triggers a scenario (here S0), a regression suit which can be run periodically or after major while {pc = 0x00F F , reset = 1, load = 0} does not. changes to the DUV. The amount of stimuli triggering a scenario is important. However, determining such a minimal Ssuff often is not So we define: trivial. Several methods that can reduce the size of a Ssuff Definition 3. Given the DUV and a set S of scenarios. For have been published in the past. In [20], a set of constraints each scenario Si ∈ S, the coverage status cS denotes the was generated for multiple coverage holes. As a consequence, i Si. the resulting stimuli could affect multiple coverage holes total amount of stimuli which have triggered the scenario simultaneously. However, no mechanism was used there to In simulation-based verification, stimuli are generated (and guarantee that the resulting stimuli set is minimal. In [19], a their responses are checked) so that all scenarios S are parallel simulation for multiple scenarios has been exploited. sufficiently covered. The term ”sufficiently” is thereby user- However, this has been conducted in a heuristic manner so defined via a threshold value such as: that also here minimality was not guaranteed. Motivated by this, we address the following research question in this paper: Definition 4. For each scenario Si (0 ≤ i < n), a thresh- old tS is defined by the verification engineer. A scenario i Si is triggered by at How can we efficiently determine a minimal set of is considered ”sufficiently” covered iff least tSi different stimuli, i.e. iff cSi ≥ tSi. stimuli Ssuff , so that each scenario Si is triggered by at least tSi different stimuli. The simulation-based verification terminates, when a suffi- cient set of stimuli has been generated. In the next section, solutions to this problem are proposed.
IV. ENDCODING AND IMPLEMENTATION
D, S, T
For clarity, how to determine a minimal stimuli set covering
each scenario Si at least one time, i.e. tS = 1, is first de-
i
scribed. Afterwards, extensions are introduced so that arbitrary
Problem Encoding c++ threshold values, i.e. tSi ≥ 1 can be supported.
Solving A. Minimal Stimuli Set with tSi = 1
SAT no As mentioned earlier, a sequence of decision problems is
formulated and solved based on SAT techniques. For this
yes purpose, an instance is created for each of the decision
Stimuli Extracting problems. In order to describe the respective encoding of the
instance smoothly, the applied vectors of variables are defined
first.
End
Definition 7. Let c ∈ N with c > 0 which corresponds to the
Fig. 1: Determination of Minimal Set Suff currently considered number of stimuli. Then, given the DUV
with m primary inputs, k states (FFs), as well as n scenarios
III. GENERAL IDEA AND MAIN FLOW (m, k, n ∈ N), we define:
1) −−−→
DU V = (DU V 0, DU V 1, . . . , DU V c−1) represents a
Given a DUV, a set S of scenarios, and a threshold value tS vector of DUV copies, i.e. DU V 0 denotes the first
for each scenario, the determination of a minimal S i
suff is copy, DU V 1 denotes the second one, etc. Apparently, all
formulated as a sequence of decision problems. The respective copies are functionally identical but allow for different
decision problems ask whether there is a set of c stimuli which assignments of their respective signals.
sufficiently triggers all scenarios of the considered DUV. When 2) For each copy DU V d with 0 ≤ d < c, the vector
→
this decision problem turns out to be satisfiable, a sufficient set −
of c stimuli can be derived. Otherwise, it has been proven that xd = (xd0, . . . , xdm−1) denotes the primary inputs of the
→
no S currently considered DUV-copy. Similarly, the FFs of
suff with c stimuli exists. The general idea of our approach the copy are denoted by −rd = (rd, . . . , rd ). Overall,
is to solve this kind of decision problems until a satisfying − − −→
→ → −−→ 0 −k−1
− →
−r = (r0, . . . , rc−1) represent
solution has been obtained. Minimality is thereby ensured by x = (x0, . . . , xc−1) and →
starting with c = 1 and iteratively incrementing c by one the primary inputs and the FFs of the c different DUV
−
→
whenever the decision problems turns out to be unsatisfiable. copies, respectively. Since the value assignments on xd
→
The respective decision problems are solved using solvers for and −rd together build up a stimulus on DU V d, the
− −r } compose a stimuli set.
x , →
Boolean satisfiability. assignments on {→ →
Based on these ideas, the overall method is formulated as 3) For each copy DU V d, −sd = (S0d, . . . , Sn−1d ) defines
− →
an iterative approach as shown in Fig. 1. The inputs are the one copy of all scenarios. Thereby, →
s = (− −−→
s0, . . . , sc−1)
DUV, a set S of scenarios, and a set T of corresponding represents c copies of them. Similarly, the copies of each
thresholds. The flow starts with encoding the problem as an scenario Si are functionally identical, but independent
instance of the satisfiability problem with a fix number c of with each other because of the renamed signals in all
stimuli. Afterwards, the resulting instance is solved using off- copies of Si.
the-shelf solvers. When the instance is satisfiable, c stimuli
composing a minimal Ssuff are extracted and the approach Based on these definitions we can formulate the following
terminates. Otherwise, c is incremented by one and the last theorem:
steps are repeated. Theorem 1. A scenario Si is considered to be sufficiently
In order to realize this approach, the respective problem needs to be encoded with respect to the dedicated solving (tSi = 1) covered iff at least one of its copies Sid is triggered engines, i.e. the applied SAT solvers in this case. Therefore, on the corresponding DU V d. the problem is formulated as a conjunction of the following With this theorem, the problem to determine a constraints: the proposed stimuli number c, the constraint of minimal Ssuff with tS = 1 is formalized as: Is there − i→ the DUV, the constraint of all scenarios S, the constraint of an assignment to {→ −r } such that for all scenarios, at x , − −r the threshold tS for each scenario, and, finally, the constraint least one of its copies is triggered and c for both → i S to be sufficiently triggered. In the next is minimal? x and → which enforces all section, the details on the encoding are presented.
x₀ s 0 ( 1 ) 1) Constraints for c copies of the DUV and the scenarios
0 s 0 ( 1 ) following the well known Tseitin transformation.
x 0
Copy 0 0
x¹₀ₘ₋₁ ... DUV⁰ ss...¹₀₂⁰ ( 0 ) 2) Constraints for the OR gates and the AND gate are
r⁰₀ FF. n-1 ( 0 ) ... or ( 1 ) added.
r⁰ₖ₋₁ FF.. 3) Since tSi = 1, no constraint for the threshold is needed.
x¹ s₁ ( 0 ) Finally, the complete instance for each decision problem is:
x ( 1 )
Copy 1 011 DUV¹ s¹⁰ ( 0 ) . or ( 1 ) −1 n∧
−1 c∨
x ... ( 0 ) ( 1 ) −1
1 s...¹₂¹¹ .. c∧
m-1 s¹
n-1 ... & DU V d ∧ Sid (2)
r10 FF ... or ( 1 ) d=0 i=0 d=0
r¹
k-1 FF... ..
... ( 1 ) i
xᶜ⁻¹ sᶜ⁻¹ ( 0 ) .. As mentioned earlier, a minimal Ssuff with tS = 1 can be
0 0 ( 0 ) .. or obtained by gradually incrementing c. The worst case is
x
Copy c-1 c-1 i.e. each scenario needs a new copy since no scenarios can be
x¹ₘ₋₁ᶜ⁻¹ ... DUVᶜ⁻¹ ssᶜ⁻¹c-1...₁₂ ( 0 ) . c = n,
sᶜ⁻¹ ( 1 )
r₀ᶜ⁻¹ FF. n-1 triggered simultaneously.
rᶜ⁻¹
k-1 FF.. In the following section, we consider the case with threshold
values greater than one.
Fig. 2: Structure of the Problem Encoding
B. Minimal Stimuli Sets with tSi ≥ 1
The general structure for the problem to be converted to To enable a threshold value greater than one, the problem
an instance is shown in Fig. 2. Besides the elements for c instance as introduced in the previous section can be refor- copies of the DUV and scenarios S, all different copies Sid mulated. Considering the problem instance as presented in of the scenario Si are connected via an OR gate as depicted. Formula 2, the second term in the formula ensures that each Furthermore, an AND gate constrains all the outputs of the OR the scenario is triggered since in at least one of the scenario’s gates. Apparently, the output of the AND gate must be fixed copies a 1 is required. This is expressed using the OR term. to 1 such that all scenarios are enforced to be sufficiently Now, a simple OR is not sufficient. Instead, we have to sum triggered (a 1 at the output of a scenario copy Sid ensures up the triggerings for each scenario Si and ensure that the − → → that the scenario Si is simulated by the input vectors {xd, −rd} user-defined threshold value is achieved. This results in the following new instance: on DU V d). −1 n∧ −1 ∑ −s is c∧ c−1 Example 3. As an example, a Boolean assignment on → − → → shown in Fig. 2. As can be seen, the stimulus {x0, −r0} triggers DU V d ∧ ( Sid ≥ tsi) (3) S0 and S0, i.e. S and S while S0 to S0 d=0 i=0 d=0 i.e.0 S2 and1 Sn−10 1 2 n−1 evaluate to 0, are not triggered in Copy 0. When the Based on this instance, the general procedure for minimal structure contains only one copy, i.e. c = 1, no Ssuff can be stimuli generation does not change. However, a satisfying determined. The scenarios S20 and Sn−10 evaluate to 0, which solution may require a large value for c since potentially many is invalid since the AND gate requires them to become 11. copies are required to meet the threshold condition of each As a consequence, the number c has to be incremented and scenario. Hence, we propose a different approach. Instead of thereby, further copies are gradually added in the structure. “blowing up” the instance, we perform several calls to the Example 4. Consider again Example 3. Further copies 1 constraint solver while blocking the previous solutions (hence to c − 1 have been added. As a consequence, the stimu- ensuring new stimuli to be found). − → → lus {x1, −r1} generated of Copy 1 triggers S1, i.e. S Example 5. Consider again Example 2. Assume that two −−→ −−→ 2 2, and {xc−1, rc−1} of Copy c − 1 triggers Sc−1 , i.e. S . Since S stimuli S n−1 − stim1 and Sstim2 have been determined. Sstim1 → → and S1 have already been triggered by {x0, −r0n−1} in Copy 0,0 triggers S0 and S2, while Sstim2 triggers S1. To generate − → → − − → → the stimuli set {{x0, r0}, {x1, −r1}, . . . , −−→ −−→ additional stimuli, we block the previous stimuli. As problem minimal c {xc−1, rc−1}} with instance we get: sufficiently triggers all scenarios. With the structure as shown in Fig. 2, the instance to be ∧1 DU V d ∧ (∧2 ∨1 Sd) ∧ S ∧ S solved can be obtained by directly encoding the elements into d=0 i=0 d=0 i stim1 stim2 (4) a SAT instance as follows: Now, we can call the constraint solver again to determine 1Please note for the case of one copy there is no OR level. additional stimuli meeting higher threshold values.
Algorithm 1: Minimal Stimuli Generation • An alternative CPU with a reduced ALU (denoted by
Input: DUV, Scenarios S, Thresholds T ALU reduced) implementing 8 ALU functions.
1 c = 1; Slog = ∅; cS = 0 foreach S ⊆ ; • A Memory Management Unit (MMU) which is used as an
∧1
c− i n∧ i S
−1 c∨
Instance = DU V d ∧ ( −1 Sid) ∧ ∨ Sstim ; interface between a CPU and an external memory. This
2 d=0 i=0 d=0 Stim log i unit manages the corresponding data transactions between
solving( ) ; i∈S these components.
3 result = Instance
4 if result = true then For each DUV, suitable scenarios have been considered,
5 extract c stimuli {Sstim , . . . , S } ; i.e. several scenarios for the respective components of the
Slog = Slog ∪ { stim 0 stimc−1}
6 S 0 , . . . , S stimc−1 ; CPU (e.g. 3 scenarios for the PC and 16 scenarios for the
c∑
7 cSi = cSi + −1 Sid foreach Si ∈ S ; CU, etc.), 8 scenarios for the reduced CPU, and 53 scenarios
d=0 for the MMU. The results generated by our approach have
8 if cSi ≥ tSi foreach Si ∈ S then also been compared to the results obtained by previously
9 return introduced approaches, namely the naive and the iterative
10 else stimuli generation scheme as proposed in [19]. Here, the
11 go to 2 ; maximal number of stimuli to be generated has been set
12 else to 1000. All experiments have been conducted using a 64-bit
13 ++c AMD Athlon Dual Core machine with 4 GB of memory
14 go to 2 running Linux.
Results of the evaluations assuming a threshold for each
scenario of tS = 1 and a threshold of t = 40
i Si are reported
in Table I and Table II, respectively. The first column denotes
Overall, we have devised Algorithm 1 to determine the the name of the DUV, while the second column gives the stimuli set Ssuff with tS ≥ 1. The number c is initialized number of the considered scenarios. The remaining columns to 1, and the log files recording the generated stimuli as wellⁱ provide both, the number of generated stimuli and the run-time as coverage status for each scenario are initialized in Line 1. to generate them (in CPU seconds) for each approach. Then, the instance is built and solved (Line 2-3). If the instance The results clearly show the benefits of the proposed is satisfiable (Line 4), the stimuli are extracted and recorded. approach. Of course, determining the minimal number of Furthermore, the coverage status is updated (Line 5-7). If stimuli is computationally more expensive than a heuristic ap- all scenarios are sufficiently covered (Line 8), the algorithm proach. However, particularly compared to the naive approach terminates. Otherwise, a new instance with the blocked stimuli from [19] the proposed solution gives very good results. In is created and the process is repeated (Line 11). Here, the fact, orders of magnitudes less stimuli are generated in a number c is not incremented. New stimuli are still generated reasonable time. Compared to the iterative approach from [19], based on the current instance. In case no more stimuli can be the proposed approach allows for rating the effectiveness of generated with the current value of c, c is incremented such the heuristic: In fact, we were able to show that for many that an additional DUV copy is included (Line 12-13). benchmarks the iterative approach already determines minimal The effectiveness of the proposed algorithm is demonstrated or close to minimal solutions (cf. PC, Stack, or ALU reduced). in the experimental evaluation in the next section. Considering all benchmarks, the iterative approach never gen- erates more than twice the number of stimuli than necessary. Overall, the proposed approach allows (1) for an efficient V. EXPERIMENTAL EVALUATION stimuli generation and (2) for an analysis how far heuristics are away from the optimum.
In this section the experimental evaluation is presented.
The proposed approach has been implemented in C++. As VI. CONCLUSIONS
constraint solver we used Boolector [5]. To illustrate the
applicability of our approach, experimental evaluations for In this work, we have presented a solution for the deter-
several benchmarks have been conducted. In the following, mination of a minimal set of stimuli for simulation-based
we summarize the results. verification. For this purpose, we formulated the problem as a
As benchmarks, the following DUVs have been considered: sequence of decision problems which, in turn, are solved using techniques of Boolean satisfiability. Experimental evaluations • The RISC processor from [11] has been used. Essentially, demonstrated the applicability of the proposed solution, i.e. the this is a Harvard architecture composed of typical com- approach can be applied to generate a very efficient set ponents such as a Control Unit (CU), a Program Counter of stimuli or to evaluate the quality of results obtained by (PC), an ALU, an external data memory (RAM), and heuristic methods. The methods presented in this paper can a stack pointer which represents a special register and further be adopted targeting on other research questions such enables standard stack operations on the RAM. as design learning, parallel simulation, or coverage analysis.
TABLE I: Minimal Suff with tS = 1
Maximal amount of generated stimuli: 1000 i
method naive approach [19] iterative approach [19] minimal approach
design # of scenarios # of stimuli run time(s) # of stimuli run time(s) # of stimuli run time(s)
PC 3 16 0.01 3 0.01 3 0.01
Stack 3 104 0.02 3 0.01 3 0.02
Data Memory 4 > 1000 - 3 0.28 2 0.34
ALU reduced 8 42 0.04 8 0.02 8 0.16
ALU 16 47 0.03 16 0.03 - time out
Control Unit 16 > 1000 - 5 0.01 3 0.02
RISC 40 > 1000 - 20 1.65 12 46.16
MMU 53 > 1000 - 20 0.06 11 6.11
TABLE II: Minimal Suff with tS = 40
Maximal amount of generated stimuli: 1000 i
method naive approach [19] iterative approach [19] minimal approach
design # of scenarios # of stimuli run time(s) # of stimuli run time(s) # of stimuli run time(s)
PC 3 404 0.08 120 0.03 120 0.05
Stack 3 143 0.03 120 0.03 120 0.03
Data Memory 4 > 1000 - 120 3.30 80 3.00
ALU reduced 8 428 0.08 320 0.10 320 0.21
ALU 16 989 0.36 640 0.29 - time out
Control Unit 16 > 1000 - 200 0.07 120 0.10
RISC 40 > 1000 - 800 49.85 480 92.18
MMU 53 > 1000 - 800 1.33 440 7.89
REFERENCES [11] D. Große, U. K¨uhne, and R. Drechsler. HW/SW Co-Verification of
Embedded Systems using Bounded Model Checking. In ACM Great
[1] S. Asaf, E. Marcus, and A. Ziv. Defining coverage views to improve Lakes Symposium on VLSI, pages 43–48, 2006. functional coverage analysis. In Design Automation Conf., pages 41–44, [12] D. Große, U. K¨uhne, and R. Drechsler. Analyzing functional coverage 2004. in bounded model checking. IEEE Trans. on CAD, 27(7):1305–1314, [2] H. Azatchi, L. Fournier, E. Marcus, S. Ur, A. Ziv, and K. Zohar. 2008. Advanced analysis techniques for cross-product coverage. IEEE Trans. [13] O. Guzey and L.-C. Wang. Coverage-directed test generation through on Comp., 55(11):1367–1379, 2006. automatic constraint extraction. In IEEE International Workshop on [3] J. Bergeron. Writing Testbenches Using SystemVerilog. Springer Verlag, High-Level Design Validation and Test, pages 151–158, 2007. 2006. [14] O. Lachish, E. Marcus, S. Ur, and A. Ziv. Hole analysis for functional [4] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model coverage data. In Design Automation Conf., pages 807–812, 2002. checking without BDDs. In Tools and Algorithms for the Construction [15] A. Piziali. Functional Verification Coverage Measurement and Analysis. and Analysis of Systems, pages 193–207, 1999. Springer, 2004. [5] R. Brummayer and A. Biere. Boolector: An efficient SMT solver for [16] S. M. Plaza, I. L. Markov, and V. Bertacco. Random stimulus generation bit-vectors and arrays. In Tools and Algorithms for the Construction using entropy and XOR constraints. In Design, Automation and Test in and Analysis of Systems, pages 174–177, 2009. Europe, pages 664–669, 2008. [6] A.-C. Cheng, C.-C. Yen, and J.-Y. Jou. A formal method to improve [17] S. Tasiran and K. Keutzer. Coverage metrics for functional validation of system verilog functional coverage. In IEEE International High Level hardware designs. IEEE Design & Test of Comp., 18(4):36 –45, 2001. Design Validation and Test Workshop, pages 56–64, 2012. [18] R. Wille, D. Große, F. Haedicke, and R. Drechsler. SMT-based stimuli [7] H. Chockler, D. Kroening, and M. Purandare. Coverage in interpolation- generation in the SystemC verification library. In Forum on Specification based model checking. In Design Automation Conf., pages 182–187, and Design Languages, pages 1–6, 2009. 2010. [19] S. Yang, R. Wille, D. Große, and R. Drechsler. Coverage-driven stimuli [8] K. Claessen. A coverage analysis for safety property lists. In Int’l Conf. generation. In EUROMICRO Symp. on Digital System Design, pages on Formal Methods in CAD, pages 139–145, 2007. 525–528, 2012. [9] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, [20] H.-H. Yeh and C.-Y. Huang. Automatic constraint generation for guided 1999. random simulation. In ASP Design Automation Conf., pages 613–618, [10] R. Grinwald, E. Harel, M. Orgad, S. Ur, and A. Ziv. User defined 2010. coverage-a tool supported methodology for design verification. In [21] J. Yuan, C. Pixley, and A. Aziz. Constraint-based Verification. Springer, Design Automation Conf., pages 158–165, 1998. 2006.