Home > Community > Blogs > Functional Verification > early holiday present sudoku solver using incisive enterprise verifier iev and assertion driven simulation ads

 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

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

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 http://www.cadence.com/community/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:

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

or

% irun -f irun_sudoku.f

Enjoy!

Joerg Mueller
Solutions Engineer
for Team Verify