Fibonacci And Honey Bees Have Something In Common: A Sweet Spot For Formal

Time flies and the OneSpin’s Holiday Puzzle tradition has reached its third year. In December 2016, OneSpin challenged engineers everywhere to solve the Einstein riddle using assertions and a formal verification tool. In December 2017, the challenge was to model the hardest Sudoku in the world using assertions and find a solution with a formal tool. In addition, participants had to prove that the solution was unique and something impossible to do with simulation.

For our third anniversary, we decided to change tack. The OneSpin 2018-19 Holiday Puzzle challenged engineers to design a digital circuit that computes Fibonacci numbers.

To check out the latest OneSpin Holiday Puzzle, The Fibonacci Calculator, click here.

We planned to award three prizes:

• Head Beekeeper: Awarded to the solution with the best overall complexity and performance score.
• Italian Mathematician: Awarded at the discretion of the OneSpin jury to a solution that stands out or particularly impressed us.
• Most Buzzworthy: Awarded to the solution that garnered the most votes in a social media “people’s choice” contest.

Verification engineers know that sometimes functional requirements are not implemented in RTL code in the most straightforward way. While this may cause frustration and generate a myriad of functional corner cases impossible to foresee, there is often a reason for it. Designers have many targets and while functional correctness is obviously crucial, it is not the only one.

Cycle-based performance, timing, area and power consumption are important metrics also. Finding the right trade-off requires creativity and implementation choices that might be more intricate than one would expect or wish for. The perfect example is processors. Implementing a design that complies with a given instruction set architecture (ISA) is relatively easy.

Once all the other targets come into play, things get complicated. Designers need to include complex logic functions such as branch prediction, speculative fetching, pipelines (multiple ones in superscalar micro architectures) and out-of-order execution. Have you seen how many different RISC-V open-source cores are available?

The Fibonacci Calculator challenge forced participants to focus on circuit complexity and performances rather than functional correctness. However, having a clear set of requirements expressed in SystemVerilog Assertions enabled engineers to continuously check that design optimizations, including changes aimed at improving cycle-based performances, were not introducing bugs.

We received many solutions from all over the world and learned from all of them. While most submissions looked correct at first inspection, some revealed bugs when assertions were checked using a formal tool. My guess is that those participants did not have access to a formal tool and relied on simulation to check their design, thus missing some corner cases.

Other solutions were almost correct, but failed to satisfy the assertion set after reset. During my career, I have used all main commercially available formal tools and know that some may include default-implicit assumptions on reset that may mask genuine RTL issues.

My advice is to carefully read the tool’s documentation, even for a simple design with only one reset, and make some basic experiments to precisely understand how the tool handles the SystemVerilog Assertion disable condition and reset.

Overall, this exercise tells us that there can be huge benefits in formalizing at least some functional requirements upfront and using a formal tool to check them as the design matures. The time required to validate optimizations and check them thoroughly can be slashed, enabling fast iterations that can save months of effort.

A few years ago, I reported an experience applying this approach to an industrial design.

Here are the winners:

• Elchanan Rappaport of Veriest wins the Head Beekeeper prize for the solution with the best overall complexity and performance score.
• Ferdinando Pace of Sensirion wins the Italian Mathematician prize for the solution that shows a unique approach to solving the puzzle
• Harry Duque of Axis wins the Most Buzzworthy prize for the solution getting most votes in the popularity contest

This year’s prize is a Fortnum & Mason luxury hamper that, of course includes honey, or a voucher of equivalent value.

We are already busy looking for new ideas for the next Holiday Puzzle. Send your suggestions at [email protected].

A big thank you to all participants. Stay tuned for the next OneSpin Holiday Puzzle later this year!