Managing Initial State to Head Start Formal Verification
Wouldn’t it be nice to get a head start on some things in life? How great would it be to just be able to walk straight to the front of any queue you find yourself in? For me, I’d like a head start on those long flights from the UK to California. If I could start them somewhere over the Rocky Mountains, then it would be a much more pleasant journey… aside from the mountain waves turbulence! While money, fame or just downright rudeness can potentially get you to the front of a queue, I’m going to have to wait for someone to invent teleportation to cut down that journey time.
The common theme here with these dreams is the idea that we don’t like wasted time. Time when we could be doing something useful but instead end up twiddling our thumbs or crushing candy. The same is true when it comes to verification runs, we want to minimize the amount of time that we spend waiting to get results back. When it comes to Formal we have a number of approaches we can take to try and jump start our verification.
The standard setup for a Formal run is to begin from a reset state. This makes sense a lot of the time because it’s a state where everything is known and it stops us getting spurious failures from incorrect initial states. There are however some situations where the best place to start may not be the reset state. In designs with a significant amount of sequential depth it can increase the complexity for the Formal tool to cover all the different states. You may have a bug which sits very deep inside the design state space but that in reality is quite simple, let’s say an FSM state transition that can only occur after 4096 cycles but a design bug causes it at 4095. Starting from the reset state means the tool has a lot of sequential depth to cover before it reaches that bug. The Formal tool does of course have a level of money and fame that allows it to take shortcuts through that long queue, but is there a way we can give it even more of a head start?
There are two interesting ways that we can go about this. The first one is to actually give the tool a specific state to start from in the form of an FSDB. Generating an initial state from a simulation in this way is great because it gives you a valid starting point, just one that gives you a head start. This is a fantastic approach for bug hunting, but, any proofs you get aren’t necessarily true for all cases.
An alternative approach is to abstract the initial state completely. This is a great way to jump start your verification because it allows the tool more freedom. The Formal tool is always going to try and fail your assertions, so if you allow it the option to choose any starting value for your registers then it will pick ones that are going to cause you a failure. Whether you choose to start from a completely unknown initial state or preload certain values it can make a huge difference in the amount of time that it takes for the tool to come back with a result. The only catch to this is of course the risk of spurious failures. Abstracting the initial state calls for properties that are written specially to take advantage of this technique such as inductive assertions. An inductive assertion says “If something is true now, then it should be true in the future” for example,
A==B |=> A==B
By writing assertions in this way you can help to reduce the risk of spurious failures as the tool has to line up A and B before the check can even become active. You may of course need some additional constraints but this can make a big difference. Checks which may have previously needed to cover thousands of cycles in order to fail can now give you a 2 cycle failure as you have given the initial state a head start to right before the bug.
Abstracting the initial state is an extremely powerful technique to reduce the runtime of the Formal tool and using this technique can get you results fast. It is however important to ensure that you understand the implications of using an unknown initial state and the spurious failures that it can create – nothing in life comes free!
