Exploiting the power of reset in formal verification

Anders Nordstrom is a senior corporate applications engineer in Synopsys’ Verification Group working on formal methodology and features on the VC Formal tool. He has 20 years’ experience in assertion-based verification and formal property verification, in EDA and as a verification engineer.

The reset state of a module or SoC that is being verified can have a huge impact on the scope and correctness of the verification. When using simulation for verification, the reset phase is usually not a large concern. However, when using formal property verification (FPV), the reset state of the design is much more important and can be a powerful ally in your verification strategy.

In almost all cases, you have to properly reset an SoC before doing functional verification. This is true when using simulation, but when using FPV there are more options. An SoC that has not been reset is in an unknown state and all its state elements have unknown or X values. If you simulate a device by driving values on all its inputs without resetting it, some values will propagate to the state elements and eventually take known values. However, the device is in a random state and is unlikely to perform any of the desired functions. Hence, the first step in a functional simulation is to assert the reset pin and simulate for a number of clock cycles until all flip-flops have taken their reset values. State elements in the data path doesn’t need to be reset, since they will take known values when data is passed through the device, but all control structures need to be reset in order to work correctly.

When using FPV on a design, reset is an important consideration. As in simulation, we almost always start verification from a known state, the reset state. Reaching the reset state is often done in the same way as in simulation, by asserting the reset pin and simulating for a number of clock cycles until all resettable flip-flops have taken their reset values. However, there are additional ways to specify reset in FPV that enable additional verification, not possible with simulation.

One variant of simulation-based reset is to use a waveform dump file and apply the design state at the end of the reset sequence as a reset state for formal analysis. This achieves the same thing as asserting the reset pin and then simulating, but may be faster and easier if the reset sequence is complex. Another approach is to use a design state other than reset as the initial state for FPV. This is a powerful method for bug hunting since much deeper design states can be reached. Any assertion failures found are valid, even though a different starting state was used, and indicate a design bug.

Another way of specifying the reset state is to specify rules or constraints instead of absolute values, e.g. requiring that the state vector of a finite state machine (FSM) is onehot, but not specifying which state to start in. This allows the formal verification tool to verify all legal reset states at once.

One property of an arbiter is that it should never assert more than one grant at the time regardless of how many requests it receives. This can be expressed in SVA (SystemVerilog Asssertions) as:

gnt_oh0: assert property (@(posedge clk) $onehot0({gnt3,gnt2,gnt1,gnt0}));

A round-robin arbiter needs a variable to remember which request was serviced last. To verify the assertion above – that only one grant at the time is asserted – in simulation, the design is reset to the idle state and then a sequence of requests is asserted to ensure the property is not violated.

Verifying the property using FPV is a lot easier. Instead of always resetting the previous request variable to the idle state, just specify that it has to have a legal value but do not specify the value. This can be expressed in SVA as:

prev_req: assume property (@(posedge clk) prev_req < 3’d5)

Proving the property means that it is true for all values of previous request, and so there is no need to verify each case individually. Proving that no more than one grant will be asserted for every possible previous grant is much more powerful than enumerating and verifying a subset of states in simulation.

Using alternative methods to reset the design under test is just one example of where FPV can do more complete verification than simulation.