Verification is the art of modeling complex relationships and behaviors. Effective model creation requires that the verification engineer be driven by a curiosity to explore a design's functionality, anticipate how it ought to work, and understand what should be considered an error. The model must be focused and expressed as clearly as possible, as it transitions from a natural language to a machine-understandable artificial programming language. Ideally, the process should be aided by the modeling language itself.

In this article, we'll highlight such a modeling process - one that describes the structure and problem of the popular Sudoku puzzle. A Sudoku puzzle is a three-dimensional problem, accompanied by a set of rules that actually define its full solution space.

Defining the data structure is the first step in our modeling process. The playing field consists of a box of exactly N by N fields, whereas N may be an arbitrary integer.

The rules by which this game is played is that we look at lines, columns, and boxes which contain a set of symbols. The size of lines, columns, and boxes, respectively, is N; therefore, we need N different symbols which are shared across the playing field. We will have N lines, columns, and boxes.

The actual rules are that each line, column, and box contains every symbol once. Duplication and omissions are not allowed.

First, we want to create a configurable list of symbols. In ** e**, we do this by
creating a list and constraining that list properly:

symbols_l: **list of uint**(**bits**: 32);

**keep** SYMBOLS_L **is for each in** { **it** == **index** + 1; };

To represent a set of N lines with N elements, we declare a two-dimensional matrix and ensure that this matrix has lines with one of each of the defined elements:

matrix_lin: **list of list
of uint**(**bits**: 32);

**keep**
MATRIX_LINES_C **is for each in **matrix_lin
{ **it**.**is_a_permutation**( symbols_l ); };

Now we do the same thing for the columns:

matrix_col: **list of list
of uint**(**bits**: 32);

**keep** MATRIX_COLUMNS_C
**is for each in** matrix_col { **it**.**is_a_permutation**(
symbols_l ); };

And we'll do the same thing for the boxes.

matrix_box: **list of list
of uint**(**bits**: 32);

**keep**
MATRIX_BOX_C **is for each in**
matrix_box { **it**.**is_a_permutation**( symbols_l ); };

Now we constrain the first dimension of each matrix to ensure that we are generating the right number of lines, columns, and boxes:

**keep**
MATRIX_SIZES_C **is all of** {

matrix_lin.**size**() == symbols_l.**size**();

matrix_col.**size**() == symbols_l.**size**();

matrix_box.**size**() == symbols_l.**size**();

};

The only thing now left to do is to connect the three different fields together:

**keep** CONNECT_LINE_COLUMN_C
**is**

**for each** (line) **using index**
(i_y) **in** matrix_lin {

**for each** (x) **using index**
(i_x) **in** line {

matrix_lin[i_y][i_x] == matrix_col[i_x][i_y];

};

};

Connecting the boxes with the lines and columns requires some thinking. We already described and constrained all of the boxes; however, mapping the boxes to columns and lines requires some arithmetic. We must first determine the strides needed to identify the box boundaries within the line coordinates. This is done by calculating the square root of N, which we will call n_sqrt. In terms of mapping this to the line coordinates, this means that we will have a new box every n_sqrt elements:

n_sqrt: **uint**(**bits**: 32);

**keep**
FIELD_SIZE_C **is** symbols_l.**size**() == n_sqrt*n_sqrt;

Let's assume N := 9 and n_sqrt := 3

Line 0 |
Line 1 |
Line 2 |

line[0] == box[0][0] line[1] == box[0][1] line[2] == box[0][2] line[3] == box[1][0] line[4] == box[1][1] line[5] == box[1][2] line[6] == box[2][0] line[7] == box[2][1] line[8] == box[2][2] |
line[0] == box[0][3] line[1] == box[0][4] line[2] == box[0][5] line[3] == box[1][3] line[4] == box[1][4] line[5] == box[1][5] line[6] == box[2][3] line[7] == box[2][4] line[8] == box[2][5] |
line[0] == box[0][6] line[1] == box[0][7] line[2] == box[0][8] line[3] == box[1][6] line[4] == box[1][7] line[5] == box[1][8] line[6] == box[2][6] line[7] == box[2][7] line[8] == box[2][8] |

Line 3 |
Line 4 |
Line 5 |

line[0] == box[3][0] line[1] == box[3][1] line[2] == box[3][2] line[3] == box[4][0] line[4] == box[4][1] line[5] == box[4][2] line[6] == box[5][0] line[7] == box[5][1] line[8] == box[5][2] |
line[0] == box[3][3] line[1] == box[3][4] line[2] == box[3][5] line[3] == box[4][3] line[4] == box[4][4] line[5] == box[4][5] line[6] == box[5][3] line[7] == box[5][4] line[8] == box[5][5] |
line[0] == box[3][6] line[1] == box[3][7] line[2] == box[3][8] line[3] == box[4][6] line[4] == box[4][7] line[5] == box[4][8] line[6] == box[5][6] line[7] == box[5][7] line[8] == box[5][8] |

Line 6 |
Line 7 |
Line 8 |

line[0] == box[6][0] line[1] == box[6][1] line[2] == box[6][2] line[3] == box[7][0] line[4] == box[7][1] line[5] == box[7][2] line[6] == box[8][0] line[7] == box[8][1] line[8] == box[8][2] |
line[0] == box[6][3] line[1] == box[6][4] line[2] == box[6][5] line[3] == box[7][3] line[4] == box[7][4] line[5] == box[7][5] line[6] == box[8][3] line[7] == box[8][4] line[8] == box[8][5] |
line[0] == box[6][6] line[1] == box[6][7] line[2] == box[6][8] line[3] == box[7][6] line[4] == box[7][7] line[5] == box[7][8] line[6] == box[8][6] line[7] == box[8][7] line[8] == box[8][8] |

This reveals the pattern

line[i_x] == [((i_y/3)%3)*3 + (i_x/3)] [(i_y%3)*3) + (i_x%3)]

The generalized mapping constraint would hence be:

**keep** CONNECT_LINE_BOX_C
**is**

**for each** (line) **using index**
(i_y) **in** matrix_lin {

**for each** (x) **using index**
(i_x) **in** line {

matrix_lin[i_y][i_x] == matrix_box

[((i_y/n_sqrt)%n_sqrt)*n_sqrt + i_x/n_sqrt] // i_y coordinate

[(i_y%n_sqrt)*n_sqrt + i_x%n_sqrt]; // i_x coordinate

};

};

As you can see, *e* lets you describe data structures and rules that describe complex scenarios
in a concise way. Layering constraints is the key to creating stimulus. As
a verification engineer, you will spend a good deal of time in your projects
doing this.

The above code is legal, valid ** e**
code. However, because the constraints are obviously quite complex, to avoid
possible ICFS errors, you should load your

**code. Before generating your environment, you need to use the generation linter. This, however, is an exercise for a different blog article.**

*e*

Feel free to comment on the code and the process above. Perhaps you'll find a different, flexible way to describe the Sudoku game.

**Daniel Bayer**

** **

Hi David and thanks for your comment! You raise a good point with the formula simplification. This would be perfectly fine if all I wanted to solve was a 9x9 puzzle. However, the solution above is aimed to solve all NxN sizes. This is precisely the reason why I chose my constraint to generate an ascending list of sequential numbers, based on the field 'n_sqrt'. You could also solve a 36x36 Sudoku puzzle by simply constraining n_sqrt == 6. Then all the constraints will provide you with a legal Sudoku solution for a field of that size. I think given the complexity of what I am trying to express with my constraints, IntelliGen is actually really efficient and good in understanding and solving the constraint model. If you have machine with lots of RAM to spare, then you could even try to solve 625x625 puzzles :-) Cheers,Daniel

Good stuff.

Seems that Intelligen has problems with generating the list of symbols. This is quite funny as this is really the easiest part. One way to get around this would be to constrain the list explicitly, like:

keep symbols_l == {1;2;3;4;5;6;7;8;9};

Otherwise, i think the formula

line[i_x] == [((i_y/3)%3)*3 + (i_x/3)] [(i_y%3)*3) + (i_x%3)]

can be shortened to

line[i_x] == [(i_y/3)*3 + (i_x/3)] [(i_y%3)*3) + (i_x%3)]

Cheers, David