Home > Community > Blogs > Functional Verification > if only gauss had intelligen in 1850

 Login with a Cadence account. Not a member yet? Create a permanent login account to make interactions with Cadence more conveniennt. Register | Membership benefits
 Get email delivery of the Functional Verification blog (individual posts).

## Email

Recipients email * (separate multiple addresses with commas)

Message *

 Send yourself a copy

## Subscribe

Intro copy of the newsletter section here, some intro copy of the newsletter. Instruction of how to subscribe to this newsletter.

First Name *

Last Name *

Email *

Company / Institution *

 Send Yourself A Copy

# If Only Carl Friedrich Gauss had IntelliGen in 1850

The N-queens issue is a challenging but standard puzzle when it comes to the world of constraint solving. It's a generalization of the 8-queens puzzle, whose description can be found in detail in Wikipedia (http://en.wikipedia.org/wiki/Eight_queens_puzzle.)  The challenge is to place N queens on an NxN chessboard in such a way that no pair of queens can attack each other.  For those unfamiliar with chess rules, this means that no two queens can ever be found in the same column, row or diagonal.

Many mathematicians, including the mighty Carl Friedrich Gauss, have tried, and failed, to find algorithms to solve this challenge.  Even today we do not know if the problem can be solved by an efficient algorithm (This is a so-called NP-hard problem in the Theory of Computation)

The solutions of N-queens are rare and irregularly placed in the hyperspace of possible placements.  For instance, the case of 8 queens has 92 non-symmetric solutions out of more than 4 billion possible placements.  So, the ability of a solver to solve N-queens demonstrates the effectiveness of its search mechanisms.

The Specman IntelliGen solving engine is based on what's called a finite-domain solver.  This has many advantages over other BDD or SAT-based solvers used by our competition.  Without getting too deep into details, there are some inherent problems of the BDD/SAT technologies that cause BDD solvers to explode for even small values of N (resources max out at N>=10) and SAT solvers suffer from poor performance (10X slower than IntelliGen for N=40 and simply does not finish for N=100).  In contrast, solving a 100 Queens problem takes only seconds in IntelliGen using the following simple nested for each constraint solution:

`<'#define N 20;extend sys {    rows[N] : list of uint[0..N-1];    keep for each (item_i) using index (i) in rows {       for each (item_j) using index (j) in rows {           i<j => (item_i != item_j and abs(item_j-item_i) != j-i);        };    };        run() is also {        for each (pos) in rows {            for i from 0 to N-1 {                if (i==pos) { outf(" Q"); }                else        { outf(" ."); };            };            out("");        };    };};'>`

What are we doing in the above example?   We have chosen to model the problem with a list of N integers in the range [0..N-1]. Each element represents a row.  Each value is a column position of a queen in that row. So, the constraints used are:

• No queens reside in the same column
• keep i<j => item_i != item_j
• No two queens are ever on the same diagonal. Here we use the abs() built in e method to grab the absolute value of the difference between the column position of each queen.
• keep i<j => abs(item_j-item_i) != j-i)
• It is sufficient to constraint only the cases i<j; otherwise we would double the constraints.
The run() method is just the pretty-printing. We go over all cells of the chessboard and print "Q" if the cell is occupied and "." otherwise.  Here is an example of the printout:

` `

`Starting the test ...`

`Running the test ...`

` . . . . . . . . . . . . Q . . . . . . .`

` . Q . . . . . . . . . . . . . . . . . .`

` . . . Q . . . . . . . . . . . . . . . .`

` . . . . . . . . . . . . . . . . . . . Q`

` . . . . . . . . . . . . . Q . . . . . .`

` . . . . . . . . . . Q . . . . . . . . .`

` Q . . . . . . . . . . . . . . . . . . .`

` . . . . . . . . . . . Q . . . . . . . .`

` . . . . . Q . . . . . . . . . . . . . .`

` . . . . . . . . . . . . . . . Q . . . .`

` . . . . . . Q . . . . . . . . . . . . .`

` . . . . . . . . . . . . . . . . . . Q .`

` . . . . . . . . . . . . . . Q . . . . .`

` . . . . . . . . Q . . . . . . . . . . .`

` . . . . . . . . . . . . . . . . . Q . .`

` . . . . Q . . . . . . . . . . . . . . .`

` . . . . . . . Q . . . . . . . . . . . .`

` . . . . . . . . . . . . . . . . Q . . .`

` . . Q . . . . . . . . . . . . . . . . .`

` . . . . . . . . . Q . . . . . . . . . .`

`No actual running requested.`

`Checking the test ...`

`Checking is complete - 0 DUT errors, 0 DUT warnings.                                               `

You might ask yourself, why is this important for verification?  Well, the faster IntelliGen can solve a very challenging problem like N Queens, the faster it can solve the complex generation constraints of today's largest devices.

How fast is your constraint solving engine?  Challenge your vendors' tools in this complex generation puzzle and post your results if you can.

Vitaly Lagoon

Vitaly Lagoon is an Architect working on the IntelliGen Generation Engine. Vitaly is a principal designer of IntelliGen's constraint solver and an expert on constraint solving techniques and tools. He is also a prolific researcher with more than 20 academic publications on constraint solving and program analysis in the leading international conferences and journals.

By Tzachi Noy on August 23, 2011
Here's what I get:
(you can see that the solution is incorrect)
Specman queens> test -seed=1
Doing setup ...
Generating the test with IntelliGen using seed 1...
Starting the test ...
Running the test ...
Q . . . . . . . . . . . . . . . . . . .
. . . . . . . . . Q . . . . . . . . . .
. . . . . . . . . . Q . . . . . . . . .
. . . . . . . . . . . . . . . . . . Q .
. . . . . Q . . . . . . . . . . . . . .
. . . . . . . . . . . . . Q . . . . . .
. . . . . . . . . . . . . . . . Q . . .
. . . . . . . . . . . . . . . . Q . . .
. . . Q . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . Q . . . . .
. . . . . . . . . . . . . . . . . . . Q
Q . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . Q . .
. Q . . . . . . . . . . . . . . . . . .
. . . . . . . . . Q . . . . . . . . . .
. . . . . . . . . . . . Q . . . . . . .
. . . . . . . . . . . . . Q . . . . . .
. . . . . . . . . . Q . . . . . . . . .
. . . . . . . . . . Q . . . . . . . . .
. . . Q . . . . . . . . . . . . . . . .
No actual running requested.
Checking the test ...
Checking is complete - 0 DUT errors, 0 DUT warnings.

By Vitaly Lagoon on August 23, 2011
Hello Tzachi,
Thanks for trying out the Intelligen example. Based upon your comment, it seems like you may be using an older version of Specman/e. We have updated the Incisive 10.2 release with many enhancements around nested “keep for each” functionality. I would encourage you to upgrade to the latest Incisive 10.2 release and try out this example. I am quite sure that will fix the problem. You can download the latest 10.2 release from http://download.cadence.com site
Feel free to contact me if you have already tested the example with the Incisive 10.2 and are still experiencing the same issue. You can contact me via email: lagoon@cadence.com
Regards,
Vitaly Lagoon