2023 Synopsys-Intel Formal Sudoku Challenge

This challenge has concluded.

Calling all the heroes who have saved the day by catching sneaky bugs using formal technologies – 

The Synopsys-Intel Formal Sudoku Challenge invites you to participate in a fun formal challenge: solving Sudoku puzzles using Synopsys VC Formal formal property verification (FPV) or formal datapath validation (DPV). 

This challenge, used by Emiliano Morini and his colleagues at Intel to train new formal engineers, hopes to encourage new engineers and remind veteran engineers that formal verification is fun and rewarding! Watch the video below to learn more about what they have done and the rules of the challenge. 

How to participate?

1. Sign up for the challenge TODAY to receive technical instructions and wrapper files.
   • Participation is limited*.
2. Read the technical instructions and create a design/formal testbench to solve ANY Sudoku puzzle. 
3. On September 7th, a set of Sudoku puzzles will be released to registrants. 
4. Solve all the puzzles and submit your design/formal testbench/results per the instructions supplied by September 30th. 
   • Cloud access to Synopsys VC Formal can be provided on an as needed basis to compete. Access will be provided on a specified TBD date and time, exceptions cannot be accommodated. 
5. Winners will be named on November 10th and selected based on level of formal experience, the elegance of the solution, and its performance.