Early Holiday Present: Sudoku Solver Using Incisive Enterprise Verifier (IEV) and Assertion-Driven Simulation (ADS)

13 Dec 2011 • 1 minute read

Allow me to interrupt the excellent "Meet R&D" series to share a small holiday present. On the Functional Verification Shared Code Forum I've just posted a ZIP file with Sudoku solver code for Incisive Enterprise Verifier (IEV). The file is at /forums/T/21110.aspx

The Details:
First, we map a standard 9x9 Sudoku puzzle into a 9x9 Verilog number array with unknown (X) locations, and then apply 3 sets of PSL assertions to constrain:

a) unique numbers in rows

b) unique numbers in columns

c) unique numbers within squares

The solution is calculated using IEV's Assertion-Drive Simulation capability -- recall prior posts on how "ADS" works and user experiences -- specifically, we use the "search" command with the results shown in the familiar SimVision waveform viewer.

If the provided Sudoku puzzle has no solution the tool will report a conflict as follows:

formalverifier: *E,VACNUL: Verification cannot proceed because conflicting constraints have blocked all paths. Remodel your constraints before invoking the tool again.

formalverifier: *W,SRDEAD: The tool has encountered a deadend state. Use debug -solver -deadend command to view the conflicting constraints.

For example, if we add another numeral ‘6' in column 1 (by adding "s[1][1] = 4'd6") we will see a message highlighting the constraint in conflict with the Sudoku:

FormalVerifier> debug -solver -deadend

Deadend-state constraints/conditions

sudoku.gen_col[1].col_unique, file ../rtl/sudoku_solver.psl, line 18

To run the solver code after you unpack & install it:

% cd iev
% iev -f iev_sudoku.f

% irun -f irun_sudoku.f

Enjoy!

Joerg Mueller
Solutions Engineer
for Team Verify

On Twitter: http://twitter.com/teamverify, @teamverify