SOURCE ARCHIVE
EXTRACTED CONTENT
44,001 chars Performance of a SystemVerilog
Sudoku Solver with VCSGame Board
Jeremy Ridgeway
Avago Technologies, Ltd.
Ph: +1 970-288-5211
Email: Jeremy.Ridgeway@avagotech.com
Abstract—Constrained random verification relies on efficient II. SUDOKU
generation of random values according to constraints provided.
As constraint solver metrics are not easily determined, usually Sudoku is an implementation of the Latin-square model.
solver efficiency can only be measured per-project and late in the A Latin-square is an n × n array of cells populated with n2 verification cycle. In this paper we dissect several SystemVerilog- based Sudoku puzzle solvers and compare their efficiency with the VCS constraint solver. Further, we compare efficiency be- tween constraints applied over object instance hierarchies (game board is object oriented) versus flat constraints (game board is fully contained within a single class). Finally, we compare both approaches with several optimizations in the Sudoku solver. The common Sudoku game board is a 9x9 grid yielding approximately 2,349 constraint clauses to solve. We show that VCS can solve grid sizes up to 49x49 with 357,749 clauses. While each clause is a (A) (B) (C) simple inequality, the size of the constraint formula to solve and its structure provides valuable feedback on the solvers efficiency. Fig. 1: Sudoku game model: (A) single cell, (B) Latin-square, and (C) full grid of rows (red), columns (green), squares (blue). I. INTRODUCTION different symbols each occurring exactly once in every row Constrained random verification is dependent on efficient and column [14]. The blue square in Fig. 1-(B) and again in Fig. 1-(C) is one Latin-square. The set of integer numbers generation of random values according to constraints provided. Small Game Board Poorly designed constraints or an inefficient constraint solver is commonly used as the symbols for cells. A Sudoku game can prove to be a bottleneck for simulation at the block level board is a n × n Latin-square of n × n Latin-squares, as in and, especially, at the sub-system or system-on-a-chip (SoC) Fig. 1-(C). Each of n2 different symbols occur exactly once level. Yet, solving constraints effectively is as much an art as in each row, column, and Latin-square of the board [15]. it is a science. Thus, constraint solvers can vary widely in their A. Sudoku Cell Constraints efficiency and performance even over successive iterations from the same supplier. In this paper we dissect the Sudoku game board as a non- c₀₀ c₀₁ c₀₂ c₀₃ proprietary approach for some measure of efficiency. Sudoku c₁₀ c₁₁ c₁₂ c₁₃ solving lends itself well to a constraint-based approach [8], c c c c [10]. The game board follows strict rules that are easy to 20 21 22 23 parameterize and scale. Large puzzles provide significant c₃₀ c₃₁ c₃₂ c₃₃ challenges for satisfiability (SAT) solvers [7], [9]. As the game Fig. 2: A 2 × 2 Latin-square Sudoku game board: 4 × 4 cells. board size increases the number of conjunctive normal form (CNF) clauses needing resolution explodes. As such, while Consider a 2 × 2 Latin-square Sudoku game. Each Latin- the game board is simple to visualize, reducing the formula square contains 4 cells total, while the entire game board to only necessary clauses is essential. contains 16 cells. Each cell in Fig. 2 is labelled accord- a We present Sudoku constraint solving in the context of ing to row and column position: C SystemVerilog test bench. We utilize the Sudoku SAT {C row col. The set of cells formula CNF clausal explosion to isolate small changes in 00, C01, C10, C11} is one Latin-square. the constraint composition and their effect on the solver. We There are four sets of constraints for the game board. First, show that the Synopsys VCS constraint solver is adept at each cell must constrain its value to the valid range. In general, handling all our constraint structures. This efficiency is against for an n × n Latin-square Sudoku game, the valid range for the norm, as we show with time metrics from three public any one cell is constrained to: domain SAT solvers, mathsat5 [2], yices [5], and Z3 [4]. val inside {[1 : n2]}. (1)
SystemVerilog specifies that all constraints on a given Listing 1: Sudoku row constraints.
random variable must be considered simultaneously in a con- 1 junctive fashion [6]. Therefore, when an instance of the cell is 2 for(int row=0; row < n2; row+=1) randomized, the constraint solver performs a composition and 3 for(int c=0; c < n2; c+=1) pre-processing step to construct a Boolean formula, simplifies 4 for(int i=0; i < n2; i+=1) that to conjunctive normal form (CNF), then employs SAT c != i -> crow_c.val != crow_i.val; and satisfiability modulo theory (SMT) techniques to solve. The general CNF structure is given in (2). Latin-square and Sudoku rules state that val must be unique ∧L ∨ within the row. In other words, a single cell’s val cannot be φ = Kj lji (2) equivalent to any other cell’s val in that row. Thus, a set of i=1 ji=1 inequalities must be built, as in Listing 1, to ensure the cell A predicate, p, is some Boolean term, a value. A literal, l, has a unique value in the row. represents a predicate in either its positive, p, or negative, Listing 1, line 1, considers one row at a time, the rowth !p, form. A literal is said to be negative when representing row. Line 2, considers one cell at a time, the cth cell within the !p, otherwise the literal is positive. In the equation above, lj row. The innermost loop, lines 3-4, compares the cell currently is a single Boolean literal. A disjunction of literals (logicalⁱ under examination, c, with the ith cell in the row. Either the OR), ci = ∨j l i current cell is the ith cell (c == i) or we constrain such that formula, i j is a single Boolean clause. A propositional the ith cell’s value is not the same as the current cell’s value. φ, is the conjunction (logical AND) of all its clauses, ∧ici. A CNF formula is essentially a formula in product-of- In general, the number of inequalities in a complete set per sums Boolean logic form. row is (n2 − 1) ∗ n2. An inequality should not be composed for the current cell versus the current cell in each row, thus TABLE I: Derivation of contiguous range term to literals. −1. The total number of inequalities in the complete set for all rows is: ((n2 − 1) ∗ n2) ∗ n2. For a Latin-square size of 2 × 2, val inside {[1:9]} ⇒ n = 2 and there are ((22 − 1) ∗ 22) ∗ 22) = 48 row inequalities ⇒ (1 <= val <= 9) in the complete set for all rows of the Sudoku game board. ⇒ ((1 <= val) && (val <= 9)) Distribution Ideally, each inequality would be a unit clause in the formula ⇒ !(!(1 <= val) || !(val <= 9)) De Morgan’s for the constraint solver to solve. However, according to the ⇒ !(1 > val) && !(val > 9) De Morgan’s constraint composition, Listing 1, line 4, some parasitic literals In the general CNF formula, clauses are the logical OR of are included due to the implication operator, as in Table II. multiple literals. It is possible for a clause to resolve to true TABLE II: Parasitic literals (i == j) in array constraints. when only a subset of literals are assigned a Boolean value. Conversely, when exactly one literal exists then that clause i ! = j → Crow i.val != Crow j.val ⇒ is considered a unit clause. The single literal must resolve to ⇒ !( i ! = j) || (Crow i.val != Crow j.val) true in order for the clause to resolve to true. ⇒ ( i == j) || (Crow i.val != Crow j.val) The Boolean formula for val from (1) and Table I consists of two clauses, φ = c0 && c1. Each clause contains a single At randomization time, each loop is unrolled to compose a negative literal, c0 ↔ !l0 and c1 ↔ !l1. The literals are related propositional CNF formula that is then presented to the con- to predicates and the Boolean quantities as: straint solver. Making the assumption that i and j are replaced !l0 ←→!p0 p0 ←→ (1 > val) with numeric constants during unrolling, their performance !l1 ←→!p1 p1 ←→ (val > 9). impact on the solver should be negligible. Thus, there are two literals per clause and 2 ∗ ((n2 − 1) ∗ n2) ∗ n2 (non-unique) To constrain all cells to a valid range for an n × n Sudoku literals in the formula. game n2 ∗ n2 = n4 constraints of the form (1) are required. In The set of column constraints are composed in the same way other words, 2∗n4 unit clauses must be solved simultaneously. as Listing 1, replacing row with the column index. However, For a 2×2 Latin-square Sudoku game, 32 clauses ensure each the composition of the set of Latin-square constraints must cell contains a valid value. track both current row and column, Listing 2. B. Sudoku Array Constraints Listing 2: Sudoku Latin-square constraints. In addition to the cell constraint, the cell’s value must be 1 for(int sq=0; sq < n2; sq+=1) unique in each of three arrays: row, column, and Latin-square. 2 for(int r = ((sq % n) * n); In a Sudoku game board, there are n2 rows. For each row, 3 r < (((sq % n) * n) + n); r++) there are n2 cells (i.e., the number of columns is equivalent 4 for(int c = ((sq / n) * n); to the number of rows). Assume each cell in the game board 5 c < (((sq / n) * n) + n); c++) is modelled as a class with randomized data member, val. 6 for(int i=0; i < n; i++) Then, in general, for an n × n Latin-square Sudoku game, the 7 for(int j=0; j < n; j++) { constraints for each cell within the row set of constraints is: int ri = (i%n) + ((sq % n) * n); 8
9 int cj = (j%n) + ((sq / n) * n); containing an array of cells, and a game board class. The
10 (r != ri || c != cj) -> cell class requires two members, a maximum range value and
11 cr_c.val != cri_ci.val; } current value.
Listing 3: Single cell in the Sudoku Game Board.
C. Testing Methodology 1 class scell;
We have composed two basic test benches. The object- 2 rand int val;
oriented (OOP) test bench constrains cell values separately 3 int max; // can optimize
from the row, column, and Latin-square inequality sets of the 4 constraint c {val inside {[1:max]};}
game board. The FLAT test bench simplifies the structure to 5 function new(int m); max=m; endfunction
a single class: all range constraints and inequality sets are 6 endclass
represented in the single class.1
For both OOP and FLAT, a single Sudoku game board was Given an n × n Latin-square Sudoku game board, each cell’s
instantiated (with no hints–no cell had an initial value) per maximum value is set at construction by the list class such that
simulation, and solved in a single randomize() step. The max = n2. In the scell class, above, the maximum value
size of the OOP game board was determined at compile time used in the constraint is a non-constant variable. Therefore, the
via macro definition. All game board sizes in the range n = constraint solver must perform at least one memory access to
{[2 : 7]}, resulting in Sudoku boards from 4 × 4 to 49 × 49, retrieve the value m_max during solving.
were simulated. However, at most, two 49×49 Sudoku boards The list class models each set of Sudoku array constraints:
were solved per test set. As such, their solving times have row, column, and Latin-square.
largely been omitted from the results in Table IV at the end
of this paper. Additionally, FLAT test benches were compared Listing 4: Single Sudoku array constraint.
against public SAT solvers mathsat5 [2], yices [5], and Z3 [4]. 1 class slist;
For these, the set of SystemVerilog constraints were written in 2 rand scell cel[];
the solvers’ input language, SMT2 [1], and only the random 3 constraint valid {
seed provided on the command-line (base options otherwise). 4 foreach(cel[i])
All tests were executed on a compute farm of identical 5 foreach(cel[j])
machines, each containing Intel Xenon processors with 64 6 i != j -> cel[i].val != cel[j].val;}
cores and 4096 GB of RAM. Jobs were limited to a CPU 7 endclass
execution time of 40 minutes and maximum 60 GB of memory
(RAM and/or swap space as designated by the scheduler). The same constraint may be applied over the array regardless
CPU times reported reflect only simulation time, compilation of the Sudoku constraint set. This is because the same goal
was performed separately. We assume the overhead for normal is always achieved: no cells in the cel array, line 2, may
SystemVerilog simulation is considered minimal and therefore have an equivalent value. The key, then, is to build the cel
not taken into account. array properly. We do so in Listing 5 by simultaneously
Finally, post-processing scripts, in Perl [13], verified cor- employing Listings 1 and 2 in the build function. The macro,
rectness on completed Sudoku game boards. Solutions be- NUM_ROWS, is set on the compile command-line. tween optimizations in the same test bench were compared (e.g., OOP Basic vs. Optimization 1), when feasible, for same- Listing 5: Sudoku game board. ness per game board size and seed. Thus, unless indicated, the 1 solutions found between optimizations using the same seed 2 class sgrid; were identical. Therefore, the metrics can accurately show 3 const int n2 = NUM_ROWS;
differences in constraint solving time. If a test experienced 4 rand slist row[n2], col[n2], box[n2];
time-out or memory-out, this was noted in the graphs but not 5 function void build();
incorporated into minimum, maximum, and average computed 6 for(int r=0; r<n2; r++) // row
solving times. 7 for(int c=0; c<n2; c++) // col
Question 1. Object-oriented or flat constraints? 8 begin// Row & column Latin-sq indexes
Our intuition states that constraints well within the single 9 int rs = ((r/n)*n)+(c/n);
class scope should be more efficient than crossing instance 10 int cs = ((r%n)*n)+(c%n);
boundaries. This is tested in the remainder of the paper. row[r].cel[c] = new(n2);
11 col[c].cel[r] = row[r].cel[c];
III. OBJECT ORIENTED GAME BOARD (OOP) 12 box[rs].cel[cs] = row[r].cel[c];
The architecture for the object oriented game board, refer 13 end
to Fig. 1, has three components: a cell class, a list class 14 endfunction
15 endclass
1The unique constraint was not employed because the OOP test bench
maintained an array of references, an invalid unique constraint construct.
The total number of clauses required to solve each Basic consistent in time as the formula grows.
OOP Sudoku board is given in Table IV. We compared
constraint solving performance between VCS-2011 [11] and
VCS-2014 [12]. Both axes in Fig. 3 represent CPU solving
time. For points above the center line, the x-axis performance - oo
was better; below the center line, the y-axis. It is clear that
VCS-2014 performs far better then VCS-2011 over the same wm JE
- rl
test bench in nearly every simulation. iiHi rdᵒ .
ail
amir
2
gm Ey
:LkH ue 53 a hy x 00 000
H FU Tine for 00F TB 2
Fig. 4: Solving Times for OOP Test Bench using if-else
Eos construct.
B. OOP optimization 2: constant vs. parameter in the cell
CPU Tine for 18 100 Question 3. Are constants more efficient than
Fig. 3: VCS-2014 outperforms VCS-2011 in nearly all cases. variables?
The range constraint in scell class in Listing 3, line 4,
sets the maximum range with a class variable. Depending on
A. OOP optimization 1: if-else vs. implication how the solver operates, each time the clause val <= max is
evaluated a memory access may be required on max. However,
Question 2. Is it better to use an implication or Latin-square and Sudoku rules dictate that the maximum
if-else constraint? cannot change for a single game board. Therefore, it is feasible
Referring to the row constraint in Listing 1, we showed to modify this constraint to use a constant value.
that parasitic literals are composed during the unrolling of the SystemVerilog provides two options for constant values
foreach loops. At line 4, an implication operator is used [6]. First, a constant class variable may be indicated using a when comparing loop indexes. From Table II, the implication keyword: const int max. Fig. 5 compares the Basic OOP composes two literals. During CNF formula composition, both test bench against Optimization 2 (constant). iterators, i and j, are replaced with integer values. An efficient L000 solver should be able to (a) maintain only unique copies of any (i == j) literal (e.g., 0 == 1 exists exactly once) and 3M hd x FEE (b) solve the literals immediately, with negligible impact on performance. We test this theory by replacing the implication & in Listing 4, line 6, with the if-else construction shown below. H . if(i != j) cel[i].val != cel[j].val; i P The SystemVerilog standard states that the “if-else style 9 constraint declarations are equivalent to implications” [6]. FH Therefore we suppose that an if-statement should be as ef- = ficient as the implication. Further, we make the assumption H that clauses are not composed when the if-statement, above, 3 is not satisfied, resulting in a reduction in the CNF formula. 01,5 Comparing test benches Basic OOP VCS-2014 against TinemOOF 18 2 “oo Optimization 1 in Fig. 4 and Table IV shows very little Fig. 5: Solving Times for OOP Test Bench with constant difference in solving time. As such, the if-else construct m_max class member. seems to have only a small effect. For VCS, neither implication nor if-else have significant benefit over the other. However, the const keyword may or may not im- Although, from Table IV, solving if-else appears to be more ply an immediate-type CPU instruction (value encoded
within the instruction). The implementation is simulator- previous loop iteration. Then for row 0, (3) becomes a reduced dependent. Therefore, for the second constant, we can set of inequalities: force the immediate-type by using a compile-time macro: val >= 0 && val <=`NUM_ROWS. Fig. 6 compares the ~~ C₀₀.val! = C₀₁.val && C₀₀.val! = C₀₂.val && Basic OOP test bench against Optimization 2 (parameter). C00.val! = C03.val && C01.val! = C02.val && (4) C01.val! = C03.val && C02.val! = C03.val. = hd x For this test, we used the if-construct in the constraint because . from Optimization 1 we noticed the VCS solver seems more H consistent in time. From Table IV, Optimization 3 should 5 oe compose half the number of clauses compared to the Basic 3 . OOP test bench. We compared all three storage types, local i . 4 I, variable, const variable (Fig. 7), and parameter in Table IV.2
as
; Fal
H 4
EY = ak
:
CPU tine for0 18 2 io Ei £7 .
Fig. 6: Solving Times for OOP Test Bench with parameter
m_max.
Comparing the metrics for Optimization 2 in both cases a A
from Table IV, we see that even though Fig. 6 varies wildly 2 =ᴮᵃ
on the larger game board sizes, the overall performance is very 0a
similar. As such, we suggest that the VCS constraint solver is hs Yn ww
about as efficient in either variable, constant, and parameter
accesses in constraints. Fig. 7: Solving Times for OOP Test Bench with reduced
inequalities, constant class variable.
C. OOP optimization 3: reduction of array duplicates Our intuition was that reducing the clausal explosion di-
Question 4. Does removing duplicates from the rectly in the constraint would have a significant effect on the
row/column/square constraint improve efficiency? solving time required. That does not appear to be true. In fact,
From Listing 1, we can see that duplicate constraint clauses all OOP Optimizations proved largely ineffectual for VCS.
will be composed. For a 2 × 2 Latin-square Sudoku game, the IV. FLAT GAME BOARD (FLAT)
following is a complete set of inequalities for row 0: We theorized that a flat constant game board would have the
C00.val! = C01.val && C00.val! = C02.val && best constraint solving performance. To that end, we wrote a
C00.val! = C03.val && Perl5 [13] script to generate four sets of flat game board tests.
Each test bench contained exactly one class definition per
C01.val! = C00.val && C01.val! = C02.val && (3) game board size. All random variables and constraints were C01.val! = C03.val && fully contained within the class. No cross-reference or inher- C02.val! = C00.val && C02.val! = C01.val && itance was employed. For example, a snippet of the Sudoku C02.val! = C03.val. game board for n = 2 is shown in Listing 6. Listing 6: Flat Sudoku Game Board 2 × 2. However, as the foreach loops are always incrementing 1 over the array (i.e., 0th cell before 1st cell before 2nd cell, 2 class sgrid_4x4; etc.), we can take advantage of this construct to reduce the 3 rand int c_1_1; // row 1, col 1 number of clauses generated by rewriting line 6 in Listing 4. ... 4 constraint cells_valid { if(j > i) cel[i].val != cel[j].val; 5 c_1_1 inside {[1:4]}; ... } In other words, if current cell under examination, j, is in 6 constraint rows_valid { a greater position than the ith cell for comparison, then no 2 inequality is necessary because it was already composed by a Figures for local variable and parameter are similar to Fig. 7, but have been omitted due to space considerations.
7 c_1_1 != c_1_2; ... } solvers are highly considered in the Boolean Satisfiability
8 constraint cols_valid { community and often compete in the SMT-COMP competition
9 c_1_1 != c_2_1; ... } [3]. Table III compares average solving time per game board
10 constraint sqrs_valid { size for each solver. Starting at the 16 × 16 game board, no 11 c_1_1 != c_1_2; ... TABLE III: Ave. Solving Time (s) VCS vs. SMT. 12 c_2_1 != c_1_1; ... } 13 endclass OOP SMT Grid Basic Opt 3. const MSAT4 Yices Z3 Generation of constraints for row and column, Listing 1, and 4x4 0.23 0.22 0.02 0.00 0.01 Latin-square, Listing 2, were handled in the script itself. The 9x9 0.26 0.24 21.99 7.70 174.64 testing methodology was the same as the OOP game board. 16x16 0.47 0.39 N/A N/A N/A 25x25 1.60 1.25 N/A N/A N/A The Full FLAT game board is similar to Basic OOP test bench with one difference: parasitic literals, as described in public domain solver was able complete within the given 40 section II-B, Table II, were not generated. As such, the number minute time window. VCS outperformed all three SAT solvers. of clauses in Table IV in OOP Basic VCS-2014 and FLAT V. CONCLUSIONS Basic sections differ somewhat. However, the solving times required are very nearly the same in all cases. We set out to characterize the VCS constraint solver based The Re-ordered FLAT game board directly tests if the on a few typical situations. We took advantage of Sudoku’s constraint solver is able to re-order and strip out duplicate ability to saturate the solver with clauses due to its exponential clauses on its own. In this game board, we have re-ordered scalability. However, we were unable to find any compelling each clause so that it matches a duplicate clause if one reason that one constraint composition was more efficient exists. The solving metrics in Table IV indicate no significant than another. Our conclusion is that, for Synopsys VCS, the difference between the FLAT re-ordered test bench and the readability of the constraint block is overwhelmingly more OOP basic test bench. important than its structure for time-efficiency purposes. The Array Reduction FLAT game board extends clausal REFERENCES re-ordering by actually removing the duplicates within each [1] C. Barrett, P. Fontaine, and C. Tinelli. The SMT-LIB Standard: Version array (row, column, and Latin-square). The metrics in Table 2.5. Technical report, Department of Computer Science, The University IV show the number of clauses FLAT versus Basic have been [2] of Iowa, 2015. Available at www.SMT-LIB.org. reduced. Still, the solving efficiency has not changed much. A. Cimatti, A. Griggio, B. Schaafsma, and R. Sebastiani. The MathSAT5 SMT Solver. In N. Piterman and S. Smolka, editors, Proceedings of The Unique FLAT game board extends array reduction by Tools and Algorithms for the Construction and Analysis of Software removing duplicate clauses from any constraint block. Thus, (TACAS), volume 7795 of LNCS. Springer, 2013. only unique clauses exist. The metrics in Table IV show an [3] D. R. Cok, A. Griggio, R. Bruttomesso, and M. Deters. The 2012 SMT competition. In SMT at The International Joint Conference on even further reduction in the CNF clauses, but, again, no Automated Reasoning (IJCAR), pages 131–142, 2012. significant reduction in solving efficiency. In fact, we were [4] L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In unable to find a significant difference in solving time on Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis any FLAT versus OOP test bench; they both appear equally of Systems, TACAS’08/ETAPS’08, pages 337–340, Berlin, Heidelberg, efficient for VCS. 2008. Springer-Verlag. Finally, a flat game board has a nearly one-to-one mapping [5] B. Dutertre. Yices 2.2. In Computer Aided Verification, pages 737–744. Springer, 2014. to SMT2 constraint language, the common input to public [6] IEEE Computer Society. SystemVerilog–Unified Hardware Design, domain SAT solvers (refer to Listing 7 for a 2 × 2 board). Specification, and Verification Language, 1800-2012 edition, 2012. [7] G. Kwon and H. Jain. Optimized CNF encoding for sudoku puzzles. Listing 7: Flat Sudoku Game Board 2 × 2 in SMT2. In Proceedings of the 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR), pages 1– 1 (declare-fun c_1_1 () Int) ... [8] 5, 2006. I. Lynce and J. Ouaknine. Sudoku as a SAT problem. In International 2 ; cells valid Symposium on Artificial Intelligence and Mathematicsc (ISAIM), 2006. 3 (assert (>= c_1_1 1)) [9] U. Pfeiffer, T. Karnagel, and G. Scheffler. A sudoku-solver for large 4 (assert (<= c_1_1 4)) ... puzzles using SAT. In Logic for Programming Artificial Intelligence and Reasoning (LAPR) Short Papers, pages 52–57, 2010. 5 ; rows valid [10] H. Simonis. Sudoku as a constraint problem. In CP Workshop on Mod- 6 (assert (not (= c_1_1 c_1_2))) ... eling and Reformulating Constraint Satisfaction Problems, volume 12, 7 ; ... cols valid, sqrs valid ... [11] pages 13–27, 2005. Synopsys, Inc. VCS(R)MX/VCS MXi(TM) User Guide, E-2011.03 8 (check-sat) ; Satisfy? edition, 2011. 9 (get-model) ; Get cell values [12] Synopsys, Inc. VCS(R)MX/VCS MXi(TM) User Guide, J-2014.12 edi- tion, 2014. [13] L. Wall. The perl programming language, 2006. We employed public domain solvers mathsat5 [2], yices [5] [14] Wikipedia. Latin square — wikipedia, the free encyclopedia, 2015. and Z3 [4], executing on the same machine farm and under the [15] [Online; accessed 3-September-2015]. Wikipedia. Sudoku — wikipedia, the free encyclopedia, 2015. [Online; same constraints as the SystemVerilog simulators. All three accessed 3-September-2015].
FLAT FLAT FLAT FLAT OOP OOP OOP OOP OOP OOP OOP OOP Unique Array Re-ordered Basic Optimize 3 Optimize 3 Optimize 3 Optimize 2 Optimize 2 Optimize 1 Basic Basic Reduction Parameter Constant Variable Parameter Constant if-else VCS-2014 VCS-2011
TABLE IV: Clause count and metrics for OOP and FLAT Test Benches.
Number of Clauses Seeds VCS Solving Time (seconds)
Test Set Grid Cell Row Col Square Total Reduced Solved Min Ave Max
4x4 32 64 64 64 224 - 100 0.15 0.17 0.21
9x9 162 729 729 729 2,349 - 100 0.26 0.28 0.51
16x16 512 4,096 4,096 4,096 12,800 - 100 1.43 2.03 11.53
25x25 1,250 15,625 15,625 15,625 48,125 - 63 11.79 25.58 66.34
36x36 2,592 46,656 46,656 46,656 142,560 - 0 - - -
4x4 32 64 64 64 224 - 100 0.18 0.23 0.43
9x9 162 729 729 729 2,349 - 100 0.21 0.26 0.43
16x16 512 4,096 4,096 4,096 12,800 - 100 0.40 0.47 0.99
25x25 1,250 15,625 15,625 15,625 48,125 - 100 1.20 1.60 5.94
36x36 2,592 46,656 46,656 46,656 142,560 - 100 4.29 109.32 1,040.92
49x49 4,802 117,649 117,649 117,649 357,749 - 1 587.48 587.48 587.48
4x4 32 48 48 48 176 21.43% 100 0.17 0.21 0.39
9x9 162 648 648 648 2,106 10.34% 100 0.22 0.25 0.74
16x16 512 3,840 3,840 3,840 12,032 6.00% 100 0.41 0.50 2.42
25x25 1,250 15,000 15,000 15,000 46,250 3.90% 100 1.16 1.69 3.00
36x36 2,592 45,360 45,360 45,360 138,672 2.73% 100 4.32 108.74 1,548.41
4x4 32 64 64 64 224 - 100 0.18 0.22 0.36
9x9 162 729 729 729 2,349 - 100 0.21 0.26 0.61
16x16 512 4,096 4,096 4,096 12,800 - 100 0.40 0.48 1.23
25x25 1,250 15,625 15,625 15,625 48,125 - 100 1.16 1.86 7.86
36x36 2,592 46,656 46,656 46,656 142,560 - 100 3.93 104.48 986.74
4x4 32 64 64 64 224 - 100 0.17 0.23 0.53
9x9 162 729 729 729 2,349 - 100 0.21 0.25 0.40
16x16 512 4,096 4,096 4,096 12,800 - 100 0.39 0.52 2.21
25x25 1,250 15,625 15,625 15,625 48,125 - 100 1.13 1.55 3.00
36x36 2,592 46,656 46,656 46,656 142,560 - 100 4.12 108.94 1,070.65
4x4 32 24 24 24 104 53.57% 100 0.17 0.22 0.29
9x9 162 324 324 324 1,134 51.72% 100 0.20 0.24 0.55
16x16 512 1,920 1,920 1,920 6,272 51.00% 100 0.33 0.39 0.92
25x25 1,250 7,500 7,500 7,500 23,750 50.65% 100 0.79 1.27 4.63
36x36 2,592 22,480 22,480 22,480 70,632 50.45% 100 3.26 107.08 1,041.81
4x4 32 24 24 24 104 53.57% 100 0.17 0.22 0.40
9x9 162 324 324 324 1,134 51.72% 100 0.20 0.24 0.47
16x16 512 1,920 1,920 1,920 6,272 51.00% 100 0.32 0.39 0.91
25x25 1,250 7,500 7,500 7,500 23,750 50.65% 100 0.82 1.25 5.24
36x36 2,592 22,480 22,480 22,480 70,632 50.45% 100 3.12 104.32 1,060.59
4x4 32 24 24 24 104 53.57% 100 0.17 0.23 0.58
9x9 162 324 324 324 1,134 51.72% 100 0.21 0.28 1.55
16x16 512 1,920 1,920 1,920 6,272 51.00% 100 0.32 0.40 1.84
25x25 1,250 7,500 7,500 7,500 23,750 50.65% 100 0.76 1.27 6.58
36x36 2,592 22,480 22,480 22,480 70,632 50.45% 100 2.76 114.09 1,340.97
4x4 32 48 48 48 176 - 100 0.18 0.28 1.36
9x9 162 648 648 648 2,106 - 100 0.20 0.25 0.70
16x16 512 3,840 3,840 3,840 12,032 - 100 0.41 0.58 2.79
25x25 1,250 15,000 15,000 15,000 46,250 - 100 1.19 1.90 5.17
36x36 2,592 45,360 45,360 45,360 138,672 - 100 12.61 137.72 746.75
4x4 32 48 48 48 176 - 100 0.17 0.21 0.66
9x9 162 648 648 648 2,106 - 100 0.21 0.25 0.35
16x16 512 3,840 3,840 3,840 12,032 - 100 0.42 0.51 1.27
25x25 1,250 15,000 15,000 15,000 46,250 - 100 1.34 2.11 5.70
36x36 2,592 45,360 45,360 45,360 138,672 - 100 13.50 158.19 716.66
4x4 32 24 24 24 104 40.91% 100 0.18 0.26 1.47
9x9 162 324 324 324 1,134 46.15% 100 0.19 0.32 1.50
16x16 512 1,920 1,920 1,920 6,272 47.87% 100 0.33 0.38 0.64
25x25 1,250 7,500 7,500 7,500 23,750 48.65% 100 0.79 1.46 6.36
36x36 2,592 22,680 22,680 22,680 70,632 49.07% 100 8.22 127.85 716.66
4x4 32 24 24 8 88 50.00% 100 0.17 0.22 0.41
9x9 162 324 324 162 972 53.85% 100 0.19 0.22 0.51
16x16 512 1,920 1,920 1,152 5,504 54.26% 100 0.32 0.42 1.55
25x25 1,250 7,500 7,500 5,000 21,250 54.05% 100 0.80 1.61 7.58
36x36 2,592 22,680 22,680 16,200 64,152 53.74% 100 8.60 148.51 1,138.90