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

* Required Fields

Recipients email * (separate multiple addresses with commas)

Your name *

Your email *

Message *

Contact Us

* Required Fields
First Name *

Last Name *

Email *

Company / Institution *

Comments: *

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

Comments(0)Filed under: PSL, ABV, SimVision, IEV, formal, formal verification, ADS, Assertion-Driven Simulation, Joerg Mueller, Sudoku

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:

  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

or

% irun -f irun_sudoku.f 

 

Enjoy!

Joerg Mueller
Solutions Engineer
for Team Verify

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

 

Comments(0)

Leave a Comment


Name
E-mail (will not be published)
Comment
 I have read and agree to the Terms of use and Community Guidelines.
Community Guidelines
The Cadence Design Communities support Cadence users and technologists interacting to exchange ideas, news, technical information, and best practices to solve problems and get the most from Cadence technology. The community is open to everyone, and to provide the most value, we require participants to follow our Community Guidelines that facilitate a quality exchange of ideas and information. By accessing, contributing, using or downloading any materials from the site, you agree to be bound by the full Community Guidelines.