Decoding Formal Pippa SlaytonPippa Slayton is Marketing and Business Development Manager at Oski Technology. She has 8+ years experience in the high-tech industry and drives marketing campaigns, marketing strategy, product launches, social media, and community building and event program management for Oski’s formal … More » ## Recap of the 2016 Oski Formal Puzzler – “Chessboard Challenge” (+ Video)March 24th, 2016 by Pippa Slayton
In December 2015, Oski challenged formal users to build the fastest testbench to solve our Participants were presented with one King on a 5 x 5 chessboard with 25 squares, constraints for at most 3 total moves in any single direction, and two goals, A and B. Goal A is easily eliminated as an achievable goal, even without the use of formal tools. Given the constraints, every move has an inverse move, which means the 24th move will always return to the starting square. Since the constraints imply a maximum of 24 moves, each square can only be visited once if all 25 squares are visited. So in 24 moves the King is back at its starting position, having visited that square twice, and cannot have visited all 25 squares. This is proof that goal A is not achievable. Goal B on the other hand, is attainable, but offers a significant challenge for formal users. For goal B, the King must visit all the squares, except the center square. The challenge lies in the proof convergence for the formal tools. A naïve solution using formal verification exists for both goals, but in each case, it is hard for formal tools to prove. For goal A, for example, a formal verification solution will not converge, even after 12 hours of a formal run. This is a problem that presents itself for both goals A and B. Formal tools can solve it, but with difficulty, and varying degrees of success. The reason is formal complexity. In both cases, the proof encounters an exponential curve in time-to-converge, which is difficult to conquer. The variety of techniques submitted by participants presented a number of worthy solutions, with varying degrees of success. In all cases, formal techniques were needed to help the tool go faster, and fight formal complexity.
In this technique, the formal search is started from a deep state, i.e., the checker remains disabled until all 24 moves are exhausted. A speedup of 40x is achieved in getting a witness for the King to visit all the squares except the center.
Armed with seven other helper checkers, using the Assume-Guarantee, Bingham proved that it’s impossible for the King to visit all the squares, and helped the formal tool to reach its goal 30x faster than a solution without this technique. The use of this technique requires a good understanding of the puzzle, was very powerful and distinguished the winning solution from all the others. Other popular techniques that proved to be helpful in solving this puzzle included One solution even used
Overall, the general enthusiasm for the puzzle was impressive; as mentioned above, even the simulation engineers had a go at solving it. Research students used open-source tools like NuSMV and SPIN to produce the solution. As mentioned above, some participants applied bug hunting techniques by disabling checkers at lower depths, some narrowed down the formal search by identifying symmetry in the start position of the King. In many ways this challenge is analogous to real world combinatorial problems with schedulers, virtual mapping arrays and free lists, which is perhaps why it attracted interest from participants across the industry. Engineers from large semiconductor companies, IP vendors, PhD students and tool vendors offered different approaches in a number of different languages including SystemVerilog, SMV, Python. While general levels of interest were strong, and several participants submitted more than one solution, the approach, techniques and mindset required is strongly relevant to the verification of structures in real designs, and offered formal users everywhere an opportunity to sharpen their strategies for the real world application of formal verification.
Tags: "Decoding Formal" Club, chessboard challenge, formal analysis, formal sign-off, formal verification, Oski Technology, Pippa Slayton, Vigyan Singhal Category: Blog |