Formal Verification of Digital Systems

Verification Plan

For any DUT, the verification plan can be divided into four sections to cover different aspects of the design. It very well depends on the specifications of the DUT, but I like to at least think in these four dimensions to start with and then add as necessary.

• Forward progress: For ready/valid protocol this includes checks for deadlock scenarios. We want to make sure the interface responds to every incoming request. For example:

  1. If at any cycle, Valid is asserted and Ready is low, then we eventually see a Ready for the request.

• Handshaking Protocol: This will include protocol specifications including data/signal stability for the interface. For example:

  1. When Valid is high but Ready is not asserted then,

     • Valid should remain asserted until accepted.

     • Data should remain stable on the bus.

  2. When Valid is asserted, corresponding data cannot be unknown on the bus.

• Data Integrity: If the DUT has memory then we want to check that data written to a location is the data read from that location. The data at the output is what was sent at the input. Every data seen at input gets at the output eventually.

• Functional logic: If the DUT we are verifying performs any data manipulation then we want to ensure the correct manipulated data is seen at the output.

In our design, the DUT has three ports, Valid, Data, and Ready. The direction of these signals will depend on the DUT. For example, the Read Address Channel on AXI- Manager sends the Valid along with the address and receives Ready as an input. The directions will be opposite for read address port on AXI-Subordinate.

Now, let's convert the test plan into Assertion-based Verification IP (ABVIP). For this DUT, we only need to cover the forward progress and handshaking. Data integrity and functional checks are not required as these are not a requirement of this interface. Say, if we were doing verification of a FIFO/memory block or a manipulation unit (ALU), then we require data integrity and functional properties.

Starting with forward progress we can write property, forward_progress_P, using strong eventuality operator. For strong operators, the property requires infinite clock ticks, which is possible in formal proof but is not the case for dynamic verifications like UVM-test-benches. For that, we can use a bounded version of the property where we expect the Ready to be asserted within some defined clock ticks after Valid has been asserted.

Also, let us assume the default clock and disable reset construct is already defined in our ABVIP so we don't need to rewrite them in our properties.

property forward_progress_P (valid, ready);

valid && !ready |-> s_eventually ready;

endproperty

// Same property for dynamic simulation.

// s_eventually will work in formal but not in UVM test-benches.

property bounded_forward_progress_P (valid, ready, Bound);

valid && !ready |-> ##[0:Bound] ready;

endproperty

For handshaking properties, we check for signal stability and correct protocol handshake as per the specification. Properties valid_data_stability_P, and data_not_unknown_when_valid_P checks for the required protocol requirements.

property valid_data_stability_P (valid, ready, data);

valid && !ready |-> ##1 valid && $stable(data);

endproperty

property data_not_unknown_when_valid_P (valid, ready, data);

valid && !ready |-> !$isunknown(data);

endproperty

Assertions vs Assumptions

Now that we have described the required properties to check our DUT, how do we decide whether they need to be asserted or assumed during formal verification ?

As a suggestion and mostly a rule,

1. Any SystemVerilog properties that constraints the input state-space of our DUT are assumptions in our formal ABVIP.

2. Properties that checks the validity of output signals are assertions in formal ABVIP (they can also include internal signals)

So in our case, when the DUT is in AXI manager-like configuration we will assert properties valid_data_stability_P and data_not_unknown_when_valid_P. We assume the property forward_progress_P. Similarly, for AXI-subordinate configuration assertions will become assumptions and vice-versa.