Contradiction Analysis for Constraint-based Random Simulation∗

           Daniel Große¹     Robert Wille¹     Robert Siegmund²        Rolf Drechsler¹
                                                                1Institute of Computer Science, University of Bremen, 28359 Bremen, Germany
                                                                             {grosse,rwille,drechsle}@informatik.uni-bremen.de
                                                                  2AMD Saxony LLC & Co. KG, Dresden Design Center, 01330 Dresden, Germany
                                                                                          robert.siegmund@amd.com

               Abstract                                               A substantial time reduction for the creation of simula-
          Constraint-based random simulation is state-of-the-art   tion scenarios is achieved by constraint-based random sim-

in verification of multi-million gate industrial designs. This ulation (see e.g. [2, 22]). Here, the stimuli are generated method is based on stimulus generation by constraint solv- directly from specified constraints by means of a constraint ing. The resulting stimuli will particularly cover corner solver, i.e. stimulus patterns are selected by the solver which case test scenarios which are usually hard to identify manu- satisfy the constraints. The resulting stimuli will also cover ally by the verification engineer. Consequently, constraint- test scenarios for corner cases that may be difficult to gener- based random simulation will catch corner case bugs that ate manually. As a consequence, design bugs will be found would remain undetected otherwise. Therefore, the quality that might otherwise remain undetected, and the quality of of design verification is increased significantly. However, in design verification increases substantially. the process of constraint specification for a specific test sce- For constraint-based random simulation several ap- nario, the verification engineer is faced with the problem of proaches have been proposed (see e.g. [23, 4, 11, 21, 12]). over-constraining, i.e. the overall constraint specified for a However, a major problem that arises when stimuli are spec- test scenario has no solution. In this case the root cause of ified in form of constraints is over-constraining, i.e. the con- the contradiction has to be identified and resolved. Given straint solver is not able to find a valid solution for the given the complexity of constraints used to describe test scenar- set of constraints. Whenever such a contradiction occurs in ios, this can be a very time-consuming process. a constraint-based random simulation run, this run has to In this paper we propose a fully automated contradic- be terminated as no valid stimulus patterns can be applied. tion analysis method. Our method determines all “non rel- Note that over-constraining may not necessarily happen at evant” constraints and computes all reasons that lead to the very beginning of the simulation run, as modern test- the over-constraining. Thus, we pinpoint the verification bench languages such as SystemVerilog [9] allow the addi- engineer to exactly the sets of constraints that have to be tion of constraints dynamically during simulation. In any considered to resolve the over-constraining. Experiments case of over-constraining the verification engineer has to have been conducted in a real-life SystemC-based verifi- identify the root cause of the constraint contradiction. As cation environment at AMD Dresden Design Center. They this is usually done manually by either code inspection or demonstrate a significant reduction of the constraint con- trial-and-error debug, it is a tedious and time-consuming tradiction debug time. process. To the best of our knowledge in this work we pro-

1. Introduction pose the first non-trivial algorithm for contradiction anal- ysis in constraint-based random simulation. In the area The continued advance of circuit fabrication technology of constraint satisfaction problems methods for diagnos-

that persisted over the last 30 years now allows the integra- ing over-constrained problems have been introduced (see tion of more than 1 billion transistors in System-on-Chip e.g. [1, 16]). These methods aim to find a solution for the (SoC) designs. The development of SoCs of such complex- over-constrained problem by relaxing constraints according ity leads to enormous challenges in Computer-Aided De- to a given weight for each constraint. In the considered sign (CAD), especially in the area of design verification, problem no weights are available. Also, the approaches which needs to ensure the functional correctness of a de- do not determine all minimal reasons that cause the over- sign. Because the capacity of formal verification is limited, all contradiction. In contrast, Yuan et al. proposed an ap- simulation is still the most frequently used verification tech- proach to locate the source of a conflict using a kind of nique [22]. exhaustive enumeration [22]. But since a very large run- In directed simulation explicitly specified stimulus pat- time of this method is supposed – neither an implemen- terns (e.g. written by verification engineers) are applied to tation nor experiments are provided – they recommend to the design. Each of those patterns stimulates a very specific build an approximation. In the domain of Boolean Satis- design functionality (called a verification scenario) and the fiability (SAT) a somewhat similar problem can be found: response of the design is compared thereafter with the ex- computing an unsat core of an unsatisfiable formula, i.e. to pected result. Due to project time constraints, it is inherent identify an unsatisfiable sub-formula of the overall formula for directed simulation that only a limited number of such [5, 24]. However, to obtain a minimal reason the much more scenarios will be verified. complex problem of a minimal unsat core has to be consid- With random simulation these limitations are compen- ered [15, 7, 14]. Furthermore, all minimal unsat cores are sated. Random stimuli are generated as inputs for the de- required to determine all contradictions. In general this is sign. For example, to verify the communication over a bus, very time consuming (see e.g. [13]). random addresses, and random data are computed. In this paper we propose a fully automatic technique for analyzing contradictions in constraint-based random simu- ∗This research work was supported in part by the German Federal Min- lation. The basic idea is as follows: The overall constraint istry of Education and Research (BMBF) in the project URANOS under is reformulated such that (contradicting) constraints can be the contract number 01M3075. disabled by introducing new free variables. Next, an ab-

s t r u c t c s t r : p u b l i c s c v c o n s t r a i n t b a s e { Usually a constraint consists of a conjunction of other s c v s m a r t p t r <s c u i n t <64> > a , b , a d d r ; constraints. We formalize the resulting overall constraint in SCV CONSTRAINT CTOR ( c s t r ) { the following definition. SCV CONSTRAINT ( a ( ) > 100 ) ; SCV CONSTRAINT ( b ( ) == 0 ) ; Definition 2. An overall constraint is defined as SCV CONSTRAINT ( a d d r ( ) >=0 && a d d r ( ) <=0x400 ) ; n∧ −1 } } ; Figure 1. Example constraint C = i=0 Ci straction is computed that forms the basis for the follow- where Ci are constraints according to Definition 1. ing steps. First, the self-contradicting constraints are iden- tified. Then, all “non relevant” constraints are determined. In practice, the conjunction is built by the explicit use of Finally, for the remaining constraints – typically only a very several SCV CONSTRAINT() macros or by applying in- small set – a detailed analysis is performed. In total our ap- heritance, i.e. parts of the constraints are defined in a base proach identifies all reasons of the over-constraining, i.e. all class and inherited in the actual constraint. Note that this minimal constraint combinations that lead to a contradic- is not specific to constraint-based random simulation using tion of the overall constraint. As shown by experiments in the SCV library. In fact, the same principles are found, for a verification environment of AMD Dresden Design Cen- example, in the random constraints of SystemVerilog [9]. ter (DDC), the debugging time is reduced significantly. The During the specification of complex non-trivial con- verification engineer completely understands what causes straints, the problem of over-constraining arises: the over-constraining and can resolve the contradictions in Definition 3. An overall constraint C is over-constrained one single step. or contradictory iff C is not satisfiable, i.e. C evaluates to 0 2. SystemC Verification Library for all assignments to the constraint variables. This section briefly reviews the SystemC Verification Typically, if C is over-constrained the verification en- (SCV) library that is used for constraint-based random sim- gineer has to manually identify the reason for the over- ulation in this work. The SCV library was introduced in constraining. This process can be very time-consuming be- 2002 as an open source C++ class library [20, 17, 10] on cause several cases are possible. For example, one of the top of SystemC [19, 8]. In the following we focus only on constraints Ci may have no solution. Another reason for the basic features of the SCV library for constraint-based a contradiction may be that the conjunction of some of the random simulation. constraints Ci leads to 0. In the following the term reason Using the SCV library, constraints are modeled in terms as used in the rest of this paper is defined. of C++ classes. That way constraints can be hierarchically Definition 4. A reason for a contradictory overall con- layered using C++ class inheritance. In detail a constraint is derived from the scv constraint base class. The data straint C is the set R = {Ci , Ci , . . . , C } C 1 2 ik ⊆ to be randomized is specified as scv smart ptr vari- { 0 , C , . . . , C 1 n−1} with the two properties: ables.An example of an SCV constraint is shown in Figure 1. 1. The constraints in R form a contradiction, i.e. the con- The name of the constraint is cstr. Here, the three 64 bit un- junction Ci ∧ C ∧ ∧ C 1 i2 . . . i always evaluates to 0. k C is contradictory. signed integer variables a, b, and addr are randomized. The Therefore the overall constraint conditions on the variables a, b, and addr are defined by ex- pressions in the respective SCV CONSTRAINT() macro. 2. Removing an arbitrary constraint from R resolves the Internally, a constraint in the SCV library is represented contradiction, i.e. minimality of R is required. by the corresponding characteristic function, i.e. the func- tion is true for all solutions of the constraint. This charac- Often the root of over-constraining results from more teristic function of a constraint is represented as a Binary than one contradiction, i.e. there is more than one reason. Decision Diagram (BDD), a canonical and compact data If in this case only one reason is identified by the verifi- structure for Boolean functions [3]. For stimuli generation cation engineer, the constraint solver has to solve the fixed a weighting algorithm is applied for the constraint BDD constraint again, but still there is no solution. to guarantee a uniform distribution of all constraint solu- Based on these observations, the following problem is tions and hence maximizing the chance for entering unex- considered in this paper: plored regions of the design state space. As BDD package CUDD [18] is used in the SCV library. How can we efficiently compute all minimal rea- sons for an over-constraining and thereby sup- 3. Contradiction Analysis port the verification engineer in constraint debug- ging? In this section first the considered problem, that is the contradiction of constraints, is formalized. Then, we Analyzing the contradictions in the overall constraint C present concepts for the contradiction analysis approach. and presenting all reasons is facilitated by our approach. In particular excluding all constraints which are not part of a 3.1. Problem Formulation contradiction reduces the debugging time significantly. Before the problem is formulated we define the type of 3.2. Concepts for Contradiction Analysis constraints that are considered in this paper. The general idea of the contradiction analysis approach Definition 1. A constraint is a Boolean function over vari- is as follows: The overall constraint C is reformulated such ables from the set of variables V . For the specification of that the conflicting constraints can be disabled by the con- a constraint, the typical HDL operators such as e.g. logic straint solver and C becomes satisfiable. By analyzing the AND, logic OR, arithmetic operators, and relational opera- logical dependencies of the disabled constraints, we can tors can be used. identify all reasons for the over-constraining.

C₀ ⇔ b()<3 && b()==7 Note that all variables a(), b(), c(), d() C₁ ⇔ a() + b() == c() are positive integers. Property 2. The value of variable si is don’t care for all solutions (i.e. for all rows of the table) iff the constraint C C₂ ⇔ a() < 6 s0₀ s−₁ s0₂ s0₃ s−₄ s0₅ s−₆ is never part of a contradiction of C. i C₃ ⇔ a() == 5 0 − 0 0 − 1 0 Proof. ⇒: This property is shown by contradiction. As- C₄ ⇔ a() == 10 00 − 0 1 0 0 − sume that si is don’t care for all solutions and Ci is part of a C₅ ⇔ d() == 8 0 − 0 1 0 1 0 − 1 − 0 0 − contradiction. Then, without loss of generality there has to C₆ ⇔ d() > 10 0 − 1 − 0 1 0 be another satisfiable constraint Cj such that Ci ∧ Cj = 0.2 (a) (b) If sj is set to 1 and all other constraints Ck with k = j are Figure 2. Contradictory constraint disabled by sk = 0, then C′ is 1. However, switching si to Definition 5. Let C be over-constrained. Then the reformu- 1 is not possible due to the conflict of Ci and Cj . But this lated constraint C′ is built by introducing a new free vari- contradicts the assumption that the value of si is don’t care able si for each constraint Ci and substituting each con- for all solutions. straint Ci with an implication from si to Ci. That is, ⇐: Because the constraint Ci is never part of a contra- n∧ diction, Ci can be enabled or can be disabled. In other of the overall constraint, which is equivalent to si is don’t C′ = −1(si → Ci). words, si can be set to 0 and also to 1 for each solution i=0 care. For the reformulated constraint C′ the following holds: Thus, each constraint Ci whose si variable is always

1. If si is set to 1, then the constraint Ci is enabled. don’t care, is not part of a reason for the contradictory over-
2. Ifcausesi is set to 0, then the constraint C i is disabled be- all constraint. Therefore these constraints are not presented C steps. i can evaluate to 0 or 1. to the verification engineer and can be left out in the next

Note that the usage of an implication is crucial. If an equiv- alence is used instead of an implication, si = 0 would imply Example 2. Consider again Example 1. Because the value the negation of Ci. of s0 is 0 for all solutions, C0 is self-contradictory. Thus, R Example 1. Figure 2(a) shows a constraint C which is 0 = {C0} is a reason for C. Since the value of s1 is al- over-constrained. Reformulating C to C′ avoids the over- ways don’t care, C1 is never part of a contradiction. As a constraining because a constraint Ci may be disabled by result the first two constraints can be ignored in the further assigning si to 0. The table in Figure 2(b) gives all assign- analysis. ments to si such that the reformulated overall constraint C′ Note that the overall constraint of the example in Fig- evaluates to 1.1 That is, the table shows which constraints ure 2(a) has been specified to demonstrate the two proper- have to be disabled to get a valid solution. For example, ties. In practice, the number of constraints that are never from the first row it can be seen that disabling C0, C2, C3, part of a contradiction is considerably larger. Thus, apply- and C5 avoids the contradiction. ing Property 2 reduces the debugging effort significantly be- Based on the reformulation the verification engineer is cause each “non relevant” constraint does not have to con- able to avoid the over-constraining. But to understand what sidered anymore by the verification engineer. causes the over-constraining, i.e. to identify the reason of In fact, all remaining constraints (if there are any) are each contradiction, a more detailed analysis is required. part of at least one contradiction. Furthermore, since self- Here, two properties of the assignment table obtained from contradictory constraints have been filtered out by Prop- the reformulated overall constraint can be exploited. erty 1 only a conjunction of two or more constraints causes a Note that for simplicity we always refer to the assign- contradiction. Now the question is, how can we identify the ment table in the presentation. As shown later in the imple- minimal contradicting conjunctions of the remaining con- mentation the assignment table needs not to be build explic- straints, i.e. the reasons? itly. Example 3. Again Example 1 is considered. The con- Property 1. The value of variable si is 0 for all solutions straints C0 and C1 have been handled already according to (i.e. in each row of the table) iff the respective constraint C Property 1 and Property 2. Now, the conjunction of two or is self-contradictory (that is C causes a contradiction. Only identifying the product of all i has no solution). i more of the remaining constraints, C2, C3, C4, C5, and C6, Proof. ⇒: We show this by contraposition: If Ci has these constraints certainly does not help to resolve the con- at least one solution, then there is a row where s flict easily. In contrast, the over-constraining can only be i fixed if the different contradictions are understood. But this is 1. Obviously this solution (row) can be constructed by assigning 1 to si and 0 to sj for j = i, because requires the computation of all minimal reasons according (si → Ci) = si ∨ Ci = 0 ∨ Ci = Ci = 1 and to Definition 4. In the example, three reasons can be found (sj → Cj ) = sj ∨ Cj = 1 ∨ Cj = 1 for j = i. in total: R1 = {C2, C4} and R2 = {C3, C4} which over- ⇐: To satisfy C′ each element of the conjunction must lap as well as R3 = {C5, C6} which is independent of the evaluate to 1, so (si → Ci) = si ∨ Ci. Since Ci has no two before. solution (Ci is always 0) si must be 0. To find the minimal reason for each contradiction, all Thus, each constraint Ci whose si variable is always as- constraint combinations are tested for a contradiction start- signed to 0, is a reason for the contradictory overall con- ing with the smallest conjunction. For each tested com- straint C. bination the respective si variables are set to 1. Thus, if the conjunction Ci₁ ∧ . . . ∧ Ciₖ leads to a contradiction 1Here ‘−’ denotes a don’t care, i.e. the value of si can be either 0 or 1. 2 The table is derived from a symbolic BDD representation of all solutions for the si variables after abstraction of all other variables. solution.According to Property 1 both constraints Ci and Cj have at least one

(1) ContradictionAnalysis(BDD C′, set V ) si variables of a reason, not the constraints itself. The set S (2) // abstraction is used to save all s (3) C′′ = ∃v1, . . . , ∃v|V | C′ i variables that are passed to the detailed analysis later. So this set corresponds to the remaining con- (4) // initialization straints. Then, for each constraint C either self-contradictory (line 9) or never part of a contra- (5) R = ∅; // reasons of contradictions i it is checked if Ci is (6) S = ∅; // si variables for detailed anaysis diction (line 12) according to Property 1 and Property 2. In (7) // test properties the former case the respective si variable is added to the set (8) for (i = 0; i < n; i++) of reasons R (line 11). Both checks are conducted on the (9) if ((C′′ ∧ si = 1) ≡ 0) quantified representation C′′ of the reformulated constraint, (10) // Ci is self-contradictory that is:• To check if s (11) R = R ∪ {{si}}; the conjunctioni isC0′′ for all solutions (see Property 1) (12) else if ((C′′ ∧ si = 0) ≡ (C′′ ∧ si = 1)) ∧ si = 1 is carried out. If the (13) // Ci is not responsible for over-constr. result is the constant zero-function, si is never 1 in any (14) else solution, i.e. si is always zero. Thus, Ci becomes a (15) // Ci is selected for detailed analysis • reason. (16) S = S ∪ {si}; The check if si is don’t care in all solutions (see Prop- (17) // detailed analysis erty 2) is carried out by (C′′∧si = 0) ≡ (C′′∧si = 1). (18) for each (X ∈ P (S)) If the respective BDDs are equal, it has been shown the solutions are identical. Therefore, the constraint (19) // from the smallest to the largest thatsi si is don’t care, since regardless of the value of (20) if (∃X ′ ∈ R : X ′ ⊂ X ) Ci is not relevant for a contradiction and thus neither (21) // ensure minimality added to the set R nor to the set S. (22) continue;∧ If both properties cannot be applied (line 14), then the re- (23) if ((C′′ ∧ si = 1) ≡ 0)) spective constraint Ci is part of a contradiction caused by ∈X C the conjunction of Ci with one or more other constraints. (24) // subset over-constrainssⁱ Thus, Ci is passed to the detailed analysis by inserting the (25) R = R ∪ {X }; respective si into S (line 16). (26) return R; Finally, the detailed analysis for all elements in S – the Figure 3. Overall algorithm remaining constraints – is performed (line 18 to 25). First, the power set P(S) of S is created resulting in all subsets ((si = 1) ∧ . . . ∧ (s C′ ≡ 0 ), then this combina- (i.e. combinations) of constraints considered for detailed 1 Ci = 1) ∧ analysis. Note that we exclude the empty set as well as all tion is a reason for . The minimality is ensured by build- ing the constraint combinations in ascending order with re-ᵏ sets which only contain one element (this is already covered spect to their size and skipping each superset of a previ- by Property 1) from the power set. Furthermore, during the ously found reason. Since the overall problem has already construction the elements of the power set are ordered ac- been simplified by exploiting Property 1 and Property 2, the cording to their cardinality. Then, for each subset X (i.e. for combination based procedure has to be applied only for a each combination) the conjunction of the respective con- small set of constraints, i.e. the remaining ones. This is the straints is tested for a contradiction. Therefore, the conjunc- key to the efficiency of the overall contradiction analysis tion of the current combination X – represented as a cube of procedure. all variables si ∈ X – and C′′ is created, i.e. all respective The next section presents the details on the implementa- constraints Ci are enabled (line 23). If the conjunction leads tion of the overall contradiction analysis approach. to a contradiction, then X is a reason and thus, X is added to R (line 25). To ensure minimality each contradiction test of a subset X is only carried out if no reason X ′ ∈ R exists 4. Implementation such that X ′ ⊂ X (line 20-22), i.e. no subset of X has al- As already mentioned earlier, the SCV library uses ready been identified as reason for a contradiction (see also BDDs for the representation of constraints. More precisely Definition 4). the characteristic function of the overall constraint is rep- In summary, the presented contradiction analysis proce- resented as a BDD. This characteristic function is true for dure computes all minimal reasons R of a contradictory all solutions of the constraint, false otherwise. We imple- overall constraint C. First, the proposed reformulation of mented the contradiction analysis approach using the SCV the overall constraint allows a representation where all con- library. Therefore our implementation is “BDD driven”. tradictory constraints can be disabled. From this represen- The pseudo-code of the contradiction analysis approach tation a much more compact one is computed by quantifi- is shown in Figure 3. As input the approach starts with the cation. All following operations have to be carried out on this representation only. Then, the two properties are ap- BDD representation of the reformulated constraint C′ and plied which significantly reduces the problem size since the set of all constraint variables V . At first, all constraint only 2n−|Z−DC| instead of all 2n subsets have to be con- variables are existentially quantified from the reformulated sidered in the detailed analysis (Z denotes the set of self- constraint (line 3). Thus, the resulting function C′′ only contradictory constraints, and DC denotes the set of con- depends on the si variables. In other words, this function straints, which are not part of a contradiction). In practice, is the symbolic representation of the assignment table de- especially the number of “non relevant” constraints that be- scribed in the previous section. In general the quantified long to the set DC is very large, so the input for the detailed BDD is much more compact than the BDD for the reformu- analysis shrinks considerably. lated constraint. Thus, the following BDD operations can be executed very fast. 5. Experimental Evaluation After quantification the two sets R and S are initialized to the empty set. R stores all reasons that are found. Note This section provides experimental results for the contra- that for simplicity R contains the sets of the corresponding diction analysis. We show the efficiency of our approach by

several testcases. Finally, the application of our approach in Table 1. Constraint characteristics an industrial setting is presented. # BOOL INT LONG BITS CONSTR. (n) In all examples the partitioning of the constraints is 1 10 8 - 328 15 given according to the specification in the constraint classes, 2 3 3 6 483 16 i.e. each Ci in the following corresponds to a separate 34 108 10 - 330 26 SCV CONSTRAINT() macro (see also Section 3.1). The 5 5 40 - 1,288 50 30 15 1,925 53 contradiction analysis is started by an additional command- line switch and runs fully automatic in the SCV library en- Table 2. Effect of using properties vironment. BDD W/O PROPERTIES WITH PROPERTIES # n R TIME 2n # √ TIME |Z DC| 2n′ #√ TIME 5.1. Effect of Property 1 and Property 2 1 15 1 5.48 32,768 24,577 4.12 0 13 4 4 0.06 Applying the two properties introduced in Section 3.2 2 16 3 14.90 65,536 26,883 11.25 1 8 128 107 0.04 3 26 1 22.30 67,108,864 – TO 0 21 32 32 0.30 significantly reduces the complexity of the contradiction 4 50 3 35.96 > 1.1 · 1015 – TO 0 42 256 190 2.10 analysis since each matched constraint can be excluded 5 53 2 238.07 > 9.0 · 1015 – TO 0 47 64 55 9.77 from further considerations. To show the increasing ef- ficiency we tested our approach for several examples the detailed signal wigglings on those buses. The abstract which contain some typical overconstraining errors (e.g. ty- bus transactions are generated by means of random genera- pos, contradicting implications, hierarchical contradictions, tors which are in turn controlled by constraints. Bus mon- etc.).For the considered constraints we give some statistics in itors observe the transactions sent into or from either inter- Table 1. In the first column a number to identify the test- face and send them to checkers which perform the end-to- case is given. Then, in the next columns information on the end transaction checking of the DUV. The verification envi- constraint variables and their respective sizes are provided. ronment is implemented in SystemC 2.1, the SCV library, Finally, the total number of constraints is given. The results and SystemVerilog, with a special co-simulation interface after application of our contradiction analysis are shown in synchronizing the SystemVerilog and SystemC simulation Table 2. The first four columns give some information about kernels. The constraint-random verification methodology the testcase, i.e. the number of constraints in total (n), the was chosen in order to both reduce effort in stimulus pattern number of contradictions/reasons (R), and the runtime in development and to get high coverage of stimulation corner CPU seconds needed to construct the BDD in the SCV li- cases. The PCIe and host bus protocol rules were captured brary (BDD TIME). The next columns provide the results in SCV constraint descriptions and are used to generate the for the trivial analysis approach without (W/O PROPERTIES) contents of the abstract bus transactions driving the BFMs. tion within the PCIe transaction generator is a layered con- and with the application of the properties (WITH PROPER- The PCIe constraint used to control stimulus genera- TIES), respectively. Here the number of checks in the worst straint. The lower level layer describes generic PCIe pro- case (2n or 2n′ , respectively), the number of checks actually tocol rules and is comprised of a number of 16 constraint executed by the approach (#√), and the runtime for the de- terms. They are shown in Figure 4(a) (denoted from C0 to tailed analysis (TIME) are given. Additionally the number C 15 )3. The meaning of the constraint variables is given in of “non relevant” constraints (|DC|) and self-contradictory the table (Figure 4(b)). The upper level layer imposes user- constraints (|Z|) obtained by the two properties are pro- specific constraints on the generic PCIe constraints (de- i vided. noted by CU ) in order to generate specific stimulus scenar- ios. Generic PCIe constraints and user-defined constraints The results clearly show, that identifying all reasons are usually developed by different verification engineers; without applying the properties leads to a large number of the former by the designer of the test environment and the checks in the worst case (e.g. 253 ≥ 9.0 · 1015 in exam- latter by the engineer who implements and runs the tests. ple #5). In contrast, when the properties are applied most The engineer writing the tests and hence the user-specific of the constraints can be excluded for the analysis since they constraints which are layered on top of the generic PCIe are “non relevant”. This significantly reduces the number of constraints is faced with the problem to resolve contradic- checks to be performed at detailed analysis. Instead of all tions which are generated by imposing the user-defined con- (only2n only 2n−|Z−DC| checks are needed in the worst case straints on the PCIe generic constraints. Given the com- 64 in example #5). As a result the runtime of the de- plexity of the constraints, this is usually a non-trivial task. tailed analysis is magnitudes faster when the properties are Two real-life examples of contradictions that are not easy applied. Moreover, for the last three testcases the reasons to resolve by manual constraint inspection are depicted in can be determined within the timeout of 7200 CPU seconds Figure 4(c). only when the properties are applied. In the first example the user sets the maximum transac- tion length to a value greater than 128 bytes (CU 1), thereby 5.2. Real-life Example causing a contradiction to constraint C 13, which states that The constraint contradiction analysis algorithm has been the total transaction length must not exceed 128 bytes. In evaluated using a real-life design example. the second example, the user independently constrains the The Design Under Verification (DUV) is a PCIe root transaction address to byte address 4000 (CU 2 ) and the complex design with an AMD-proprietary host bus inter- transaction length to 100 bytes (C U ). While both values, 3 face which is employed in a SoC recently developed by viewed independently, are each perfectly legal (the address AMD. The root complex supports a number of PCIe links. should be in 32 bit range and the transaction length is less The verification tasks are to show (1) that transactions are than 128), an over-constraining occurs. The reason identi- routed correctly from the host bus to one of the PCIe links fied by our approach is R1 = {C12, CU , C } 2 U3 . By manual and vice versa, (2) that the PCIe protocol is not violated constraint inspection it is not immediately obvious that a and (3) that no deadlocks occur when multiple PCIe links PCIe protocol rule is violated when combining constraints communicate to the host bus at the same time. CU 2 and C U3 . However, reason R1 found for the contra- Host bus and PCIe links are driven by Bus Functional Models (BFMs) which convert abstract bus transactions into 3 Bit operators are used as introduced in [6].

C0 ⇔ (addr space != memory || ((mem addr base0 <= addr) && ((addr+length) <= mem addr base0 + mem size0))) || ((mem addr base1 <= addr) &&((addr+length) <= mem addr base1 + mem size1))) // address boundaries for memory C1 ⇔ (addr space != io || ((io addr base <= addr)&&((addr + length)<= io addr base + io size))) // address boundaries for io C2 ⇔ (addr space != config || ((cfg base addr <= addr)&&((addr+length) <= config base addr + config size))) // address boundaries for config C3 ⇔ be[] <= 0xf // valid byte enables are in 0x0..0xf C4 ⇔ be[].len == length // generate as many byte enables as we have dword data C5 ⇔ data[].len == length // set data length addr transaction address (64 bits) C 6 ⇔ cmd != read || posted == false // read transactions are always non−posted addr space transaction address space C7 ⇔ gen host trans.addr space == memory || (addr&3)+length <= 4 tkind (memory,io,config) transaction kind (request,response) // transactions to IO/config space are 1 dword (4bytes) only cmd transaction command (read,write) C8 ⇔ addr <= 0xFFFFFFFF // addresses are in 32 bit range msr transaction is targeted at MSR space C posted transaction is posted (yes/no) 9 ⇔ addr space==memory || addr space==config || addr space==io length transaction size in dwords // only generate transactions in memory/IO/config space be[] array of byte enables C10 ⇔ length > 0 // requests must have length > 0 (one per each dword data) C 11 ⇔ addr space == sr::mem || addr <= 0xFFFFFFFF data[] array of dword (32 bit) data // IO and config space are restricted to 32 bits be[].len length of byte enable array C12 ⇔ (addr&4095) + length <= 4096 // transactions must not cross 4k page boundary data[].len length of data array [io|mem|cfg] io, memory and config space C13 ⇔ (addr&3) + length <= 128 // keep transaction length to max. 128 bytes addr base0,1 window base addresses C14 ⇔ tkind == request // generate requests only (not responses) [io|mem|cfg] size0,1 io, memory and config C 15 ⇔ msr == false // do not generate MSR accesses space window sizes (a) (b) Example 1: CU₁ ⇔ length > 128 Example 2: CU₂ ⇔ addr == 4000 ∧ CU₃ ⇔ length == 100 (c)

       Figure 4. PCIe transaction generator constraint with examples

diction by our algorithm shows that when combining con- [3] R. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE straints CU and CU , then PCIe protocol rule C is vi- 2 3 12 [4] Trans. on Comp., 35(8):677–691, 1986. olated: “A transaction must not cross a 4k page bound- R. Dechter, K. Kask, E. Bin, and R. Emek. Generating random solutions for ary”. Our user constraints of transaction start address set constraint satisfaction problems. In Eighteenth national conference on Artificial to 4000 and transaction length of 100 bytes would result [5] intelligence, pages 15–21, 2002. in addresses that cross a 4k page and therefore violate this E. Goldberg and Y. Novikov. Verification of proofs of unsatisfiability for CNF formulas. In Design, Automation and Test in Europe, pages 10886–10891, constraint. 2003. The algorithm described in this paper is able to identify [6] D. Große, R. Ebendt, and R. Drechsler. Improvements for constraint solving exactly the violating constraint expressions for both exam- in the SystemC verification library. In ACM Great Lakes Symposium on VLSI, pages 493–496, 2007. ples in about 30 seconds. The PCIe constraint to be ana- [7] J. Huang. Mup: a minimal unsatisfiability prover. In ASP Design Automation lyzed contained a total of 21 random variables to be solved Conf., pages 432–437, 2005. which are constrained by 17 and 18 constraint expressions [8] IEEE Std. 1666. IEEE Standard SystemC Language Reference Manual, 2005. for the respective examples. The total bit count for the ran- [9] IEEE Std. 1800. IEEE SystemVerilog, 2005. dom variables amounted to 781 bits. Without such an anal- [10] C. N. Ip and S. Swan. A tutorial introduction on the new SystemC verification standard. White paper, 2003. ysis capability, we would have had to spend several hours [11] M. A. Iyer. Race: A word-level ATPG-based constraints solver system for on manual constraint inspection in order to identify the root smart random simulation. Int’l Test Conf., pages 299–308, 2003. cause for the constraint contradiction. Thus, a significant [12] N. Kitchen and A. Kuehlmann. Stimulus generation for constrainted random speed up of the contradiction debug cycle was achieved. [13] simulation. In Int’l Conf. on CAD, pages 258–265, 2007. M. H. Liffiton and K. A. Sakallah. On finding all minimally unsatisfiable sub- formulas. In Theory and Applications of Satisfiability Testing, pages 173–186, 2005. 6. Conclusions [14] M. N. Mneimneh, I. Lynce, Z. S. Andraus, J. P. Marques-Silva, and K. A. Sakallah. A branch and bound algorithm for extracting smallest minimal un- In this paper we have presented a fully automatic ap- satisfiable formulas. In Theory and Applications of Satisfiability Testing, pages proach to analyze contradictory constraints that occur in [15] 467–474, 2005. Y. Oh, M. Mneimneh, Z. Andraus, K. Sakallah, and I. Markov. Amuse: A constraint-based random simulation. After reformulating minimally-unsatisfiable subformula extractor. In Design Automation Conf., the overall constraint and building an abstraction, the self- pages 518–523, 2004. contradictory constraints and all “non relevant” constraints [16] T. Petit, J.-C. R´egin, and C. Bessi`ere. Specific filtering algorithms for over- are determined in an initial step. Then for the small set of re- constrained problems. In International Conference on Principles and Practice of Constraint Programming, pages 451–463, 2001. maining constraints, all minimal reasons for a contradiction [17] J. Rose and S. Swan. SCV randomization version 1.0. 2003. are computed efficiently and presented to the verification [18] F. Somenzi. CUDD: CU Decision Diagram Package Release 2.3.0. University engineer. The minimality and completeness of the reasons [19] of Colorado at Boulder, 1998. Synopsys Inc., CoWare Inc., and Frontier Design Inc., http://www.systemc.org. allows to fully understand the over-constraining. Thus, the Functional Specification for SystemC 2.0. verification engineer is able to resolve the conflict in one [20] SystemC Verification Working Group, http://www.systemc.org. SystemC Veri- single step. In total, as shown by industrial experiments, fication Standard Specification Version 1.0e. the debugging time is reduced significantly. [21] J. Yuan, A. Aziz, C. Pixley, and K. Albin. Simplifying boolean constraint solv- ing for random simulation-vector generation. IEEE Trans. on CAD of Inte- grated Circuits and Systems, 23(3):412–420, 2004. [22] J. Yuan, C. Pixley, and A. Aziz. Constraint-based Verification. Springer, 2006. References [23] J. Yuan, K. Shultz, C. Pixley, H. Miller, and A. Aziz. Modeling design con- straints and biasing in simulation using BDDs. In Int’l Conf. on CAD, pages [1] R. R. Bakker, F. Dikker, F. Tempelman, and P. M. Wognum. Diagnosing and [24] 584–590, 1999. solving over-determined constraint satisfaction problems. In International Joint L. Zhang and S. Malik. Validating SAT solvers using an independent resolution- Conference on Artificial Intelligence, pages 276–281, 1993. based checker: Practical implementations and other applications. In Design, Automation and Test in Europe, pages 10880–10885, 2003. [2] J. Bergeron. Writing Testbenches Using SystemVerilog. Springer, 2006.