Extend formal property verification to protocol-driven datapaths

Unlocking formal for datapaths

Dynamic packet sizes and complex error scenarios make protocol verification a challenge for any testbench. Trying to define the large array of packet sizes and configurations within a formal testbench can make that challenge feel impossible. However, with sound, upfront planning and an understanding of where difficulties are likely to arise, it is possible to unlock the promise of formal for datapath applications.

Let’s explore formal datapath verification using transaction deconstruction to simplify formal property definitions; reducing our state space using simplification through assumption defined constraints; and compartmentalizing special cases through use of formal control points.

Transaction deconstruction

If the proofs in the form of property defined assertions provide the muscle of the formal flow, a structure based SystemVerilog RTL testbench provides the skeleton upon which everything can be built. Each cycle populates the structure fields which describe the packet header. By creating a synthesizable, description of a well-defined transaction header, a dynamic packet can be viewed statically and a basis for constrained evaluation is established.

Figure 1. Formal transaction representation (Mentor)

Simplification through constraints

Once the packet has been described and captured, helper RTL can be used in combination with the formal transactions to frame and define transaction behavior in a synthesizable way.

Helper RTL is created to define received packet length via a small counter which starts, stops and resets at packet boundaries. By using the structure-defined packet fields created in the first section, an expected length for well-formed packets is made available. When the packet count and expected length are equated using SVA assumptions, the packet is formally framed; the SV assertion evaluates and restricts the helper RTL to the packet boundary. The length field and true packet size are thus linked by a synthesizable construct.

Additionally, the overall state space is reduced and proofs will be easier to explore as size violations are synthesized away. Figure 2 provides a graphical representation of the reduced state space due to the packet size constraint. Truncated and overrun packets are now removed from analysis.

Figure 2. Typical solution block-level diagram (Mentor)

In order to further reduce the state space, protocol and design assumptions captured within the project specifications should be implemented as formal assumptions. Each assumption is a documented verification limitation and can be evaluated for its validity and tied directly to a requirements document.

The assumptions are mapped into the state-space chart shown in Figure 3, demonstrating state-space removal for each protocol violation.

Figure 3: Packet protocol restrictions (Mentor)

Not only do these constraints limit state space and increase the likelihood of property convergence, they also act as a natural gate to debug complexity. By including conditions that a design is unable to handle, formal will flag an assertion error. The first failure formal finds will halt analysis until resolved. Because of this, an underconstrained testbench will result in a protracted lesson in ‘peeling the onion’. A frustrating and time consuming effort as each design constraint is discovered in debug rather than up front.

Formal control points

Some of the assumption statements used to limit state space are overly restrictive. For instance, when a DUT receives invalid field values it may be required to report the error and take no action. In that case, it is desirable to isolate checks for good packet behavior from bad. Different sets of assertions will need to be evaluated for each condition and different sets of assumptions made. The formal testbench can take advantage of the formal tool’s intrinsic manipulation of undriven signals by creating new undriven wires called ‘formal control points’.

The formal testbench uses formal control points to gate broad transaction behavior. Using them, we can take advantage of reduced state space for individual proofs while preserving important breadth within the formal environment.

Figure 4 shows the results of our formal testbench development.

Figure 4: Packet-size state-space reduction (Mentor)

An initially broad state space has been narrowed by restricting packet truncation and overrun behaviors that are not expected in our system, perhaps eliminated by similar testing upstream. Protocol errors are isolated in order to reduce the local state space of good packet testing which relies on good packet formation as defined by our struct and helper RTL. Using formal control points to isolate good packet behavior will also help us with initial testing. We can focus on reliable good behavior of our DUT before delving into the often treacherous realm of error detection and handling. Additionally, formal control points allow us to recapture verification space by creating errored packet checks using the same control point.

Conclusion

With a solid methodology base and upfront planning, the benefits of formal property verification, such as full path confidence and requirements-based property definition, can be leveraged for protocol-driven datapaths. Incorporating layered SystemVerilog constructs to provide a transaction-like protocol description simplifies property creation for both well-formed packets and error scenarios. Ultimately though, the key to successful formal datapath analysis is reduction of the typically large state spaces resulting from variable and dynamic packet sizes. Proper interleaving of SystemVerilog helper constructs with protocol targeted assumptions defines a manageable state space and unlocks the promise of formal driven, full path verification for datapaths too.

To learn more about how this methodology can help you fulfill the promise of full path verification and traceable requirements, including example code snippets and diagrams, please download the white paper Extending Formal Property Verification to Protocol-Driven Datapaths: The Secret to Datapath Formal Verification.

About the author

Rusty Stuber is a verification consultant for Mentor Graphics, following stints as an ASIC design engineer with LSI Logic; a designer, manager and project lead with Xilinx; and a verification engineer and verification team lead for Seagate. Additionally Rusty has served as Technical Working group chair for the RapidIO Trade Association and holds patents relating to IP design.