Breakfast Bytes Blogs

The annual Jasper User Group was held in November. I've already written several posts about the event:

• Jasper User Group Preview
• Announcing Jasper C2RTL App: Formal for Algorithmic Designs
• Datapath Formal Verification 101: Technology and Technique
• Jasper User Group: Ziyad's State of the Formal Union

Best Paper Award

Every year, the Jasper User Group presents the best paper award. This is voted on by the attendees, it is not the result of Cadence people getting together in a back room. This year the winner was David Gilday from Arm with Human Guided Proof Closure.

If you have any experience with formal, you know that formal tools, including model checkers, often struggle to achieve proof closure. There are many reasons for this, the most common being computational complexity (multiplier arrays are the canonical example here) or that the state space is too complex (such as requiring very high cyclic depth to get to the point of interest). As you might guess from the title of David's presentation, one solution is to help the formal tool with helper properties that can be proved easily, and then can help other proofs, and get you to full closure.

However, creating helpers by hand can take a lot of effort. The bulk of David's presentation was about techniques for doing this more automatically and reducing the effort. This is what Arm calls "human-guided proof closure".

The diagram above shows the whole state space, the reset state from where analysis starts, the bounded reachable state space, and so on.

• Representable state space (rectangle in grey)
• Reset state(s) (the little yellow oval)
• Bounded reachable state spaces (in blue rings)
• Total reachable state space (in dark grey)
• Reachable state transitions (in black)
• Unreachable state transitions (in light grey)
• States where our property of interest is true (in green)
• States where the property is false (outside the box in red) which indicates a counter-example.

The arrows represent state transitions. They are all within the reachable state space. The grey dotted arrows are state transitions that are not reachable from the reset state, but may be described in the RTL, properties, and so on. So although they are unreachable, they may involve Xs, plus they have next-states defined which might go from unreachable state space to reachable. But none go the other way by definition (otherwise the next states would form part of the reachable state space). For the property we want to prove, the green box shows where it is true. It will be at least as large as the reachable state space. The red box shows where a property is false and indicates a counter-example. For example, the arrow crossing the top of the red box indicates a counter-example.

In general, we are not interested in all of this. Just the states that are reachable from reset, the state transitions that are reachable, and the states where the property is true. A lot of what the formal prover has to do is to consider only the reachable states, so it doesn't need to consider tempting arrows like the one that is outside the reachable space but crosses from inside the green rectangle (true) to outside it. This might look like a counter-example but is unreachable. Helper properties are one way of describing reachability that the tool can use.

One useful way to work is proof by induction. This is inexpensive compared to some other approaches. This is similar to mathematical induction. The base case is that a property P holds immediately after reset. The induction step is that for all states where P holds, if you take the transition to the next state, then P still holds. These are shown in the above diagram. Note that some places indicated are multiple states, and some are outside the reachable states. We are interested in more than one state transition, so in the K transition case, we are interested in states where P is true and whether it is still true K cycles later. One case where this is not true is the red oval at the top where the property is true for a number of cycles and then fails (leaves the green box). But the tool, at this point, doesn't have any knowledge about the reachable state space so it won't ignore this transition.

The approach of human-guided proof closure is to use helpers to eliminate unreachable states from the inductive step and we use counter-examples for the inductive step to discover what helpers we need to create. For example, if we had a dream property that was only true for reachable states, then a property like that would be provable by induction. But then the prover can use this property to only start the proof within states that are reachable (and, by definition, you can't get to an unreachable state from there).

Here's the example design that David used for the rest of the presentation. It is a normal FIFO with full and empty signals, along with a checker that checks, for example, that the full and empty signals are handled correctly. The FIFO only has four entries. So there are three properties to be proved: chk_full, chk_empty, and chk_data. Just the H engine is used for induction. However, this is a simple example, and other engines would have no problem proving these properties in a reasonable time. But using just H, if we only give it a limited time it won't manage to prove these three properties in that time.

If we use state space tunneling (SST), an SST visualize trace is a counter-example of an inductive step proof attempt (like the red oval we've seen before). Note that this is not a counter-example for the design, but it is a counter-example of an attempt to prove the inductive step which is failing because it is starting from an unreachable state. So we can manually create helper properties that describe the reachable state space. What is happening is that the proof is failing when the count gets large...larger than the allowable values for the count which has to be 0 to 4 (remember, there are 4 entries in the FIFO). So 5 and above are unreachable states. The read and write pointers are intended to be one-hot (only one bit in the register set) even though, from the point of view of unreachable states, any value might be in the register even though they are actually unreachable. The "not quite" is to illustrate just how, even for this small design, writing the helpers by hand is tricky.

This is where the automated flow comes in. It is usually easy to work out what state elements are involved, even if the expressions relating them are not obvious. The helper library is written in TCL as you can see above in the yellow box. The curly brackets contain the elements of interest. The key thing is that there is no need to manually work out an expression relating the signals. With no reachable states except reset, the tool then runs a proof and finds counter-examples. Those are the states that actually are reachable. This is then repeated, as David went into in his presentation. The helpers are then proved, and then the properties of interest are proved, making use of the helpers.

The above diagram summarizes the flow. David went into detail on one problem, namely when the state space of signal list has too many sates, and how to use virtual signals to describe key relationships.

Results

He wrapped up with some results from Arm processors.

• A-class processor core
  • Real bug discovered in the process of discovering helpers
  • Proof closure of helpers proved after the bug was resolved
• R-class processor core
  • Proof closure of memory management unit in under 2 hours, previously undetermined after several days
• M-class processor core
  • Proof properties of key end-to-end properties for fetch queue
  • 10% more properties proven in core regressions

Summary

Learn More

All the presentations (in both pdf and video form) are on the Jasper User Group (JUG 2021) one-stop resource page. David Gilday's presentation is the last one on the list. You can access this if you are registered for Cadence support, you don't have to have been registered for JUG21.

The Claret Jug

If you play golf, you will know about The Open Golf Championship (often called the British Open, but there were no other championships back in 1860 when it started so no need to put a country name in the title...we Brits don't put a country name on our stamps either since there were no other stamps back in 1840 either). You probably know that the trophy for the winner is The Claret Jug. Actually, the original is far too important to award the original, which is kept at the R&A in St Andrews, and it is a replica that the winner receives today to take home for a year.

All of which is a long preamble as to how it would be great if the winner of the best paper at JUG received a claret jug or something similar. By the way, "claret" is a British term for red Bordeaux wine, so jugs like this would have been used to drink wine from the barrel before universal bottling was introduced. So we need a campaign: a jug for JUG!

Sign up for Sunday Brunch, the weekly Breakfast Bytes email.