Introduction

Verification of designs that transport data in a serial manner is a known challenge for both simulation and formal verification. The complexity of such designs stems from the “serialised” nature of packet flow where the state of each packet depends upon the history of all the previous packets in flight. What is interesting about such designs is that they’re present everywhere in all kinds of hardware designs. Packet based serialised data flow can be seen in a range of different designs from networking routers, bus protocols, bus bridges, load-store units in CPU, packing and unpacking designs, and SoC peripherals such as I2C, I2S, USB, UART, Ethernet and so on. Inherently these designs are complex with multiple mutually interacting state machines controlling different activities in the design. At a high level the designs are about data flow but the control mesh that routes the data correctly can be very difficult to verify completely with directed testing based approach or even constrained random simulation. If you throw in this mix the fact that you can have multiple clock domains – one for the input and the other for the output the chances of simulation obtaining a near exhaustive result is close to impossible. Formal verification of such designs is also a challenging task. In this article, I present a case study of verifying a packet based design using formal verification.

Scalable Formal Verification of Serial Designs

Abstraction is one of the main methods to control the complexity of formal verification so that we not only find deep bugs in such designs but also obtain exhaustive proofs. The role of abstraction in computer science and formal methods can be traced back to the famous 1977 paper by Cousot & Cousot [hyperlink] where they discussed abstract interpretations and Galois connection. A lot has happened in these intervening fifty years in the field of formal and abstractions and Ed Clarke et al.’s paper on Model Checking and Abstraction [hyperlink] provides a good foundation on the role of abstraction in model checking. I’ve been pursuing research and application of abstraction for scalable formal verification for the last 17 years – starting from the early days of my Doctorate [hyperlink] which was in problem reduction techniques for scalable model checking. Over the years, I’ve looked at a range of published literature on this topic. What I’ve found to work very well in practice is a combination of data and temporal abstraction techniques dating back to the foundational work done by Tom Melham and Mike Gordon. Though a lot of early work done by Melham and Gordon was in the context of theorem proving and higher order logic their application is highly relevant to model checking as well, and this is what has inspired me to build my own abstraction based solutions.

Basic Concept of Abstraction

Critical to any abstraction technique is the ability to abstract away non-essential details of the underlying design being verified. What is considered as non-essential largely depends on what is being verified. Abstracting away too much design can result in spurious failures but also in false positives. The topic of false positive has not been discussed a lot in the formal verification literature in the context of abstraction but it is an important artefact to consider. Because abstractions inherently constrain away what is deemed as un-necessary information, aggressive abstraction can act as an over-constraint on some legal design behaviours which if abstracted away would make verification not find the bugs in those legal design behaviours.

Optimising Abstraction

To obtain abstract models for verifying serial packet based designs, the central requirement for verification is that packets are not dropped, duplicated, reordered, and are delivered at the correct time to the correct destination. To verify such packet based systems I devised a family of abstractions that can verify such systems safely without leaving behind bugs in the design and at the same time provide significant improvement in proof convergence. Some of my work has been reported in various places before [DAC 2014, DAC 2015, JUG 2015, FV2016, DarbariSingleton2016]. What is important to highlight here is that when I compared the two- transaction method with the scoreboard built by another EDA company, I found my scoreboard to be vastly superior in performance [CDNLive 2014] and this was down to using invariants as auxiliary properties together with an assume guarantee flow. Here I describe the main concepts of one of these abstractions which I named as a smart tracker method [DAC 2014 hyperlink] which I also used in the verification of this packet based design.

Smart Tracker Abstraction

The idea of this is very simple.

Case Study

Design Description

The design a packet base design where the number of packets being accepted every clock cycle at the inputs is not a fixed number. Packets of different lengths are accepted every clock cycle on the input ports and are routed to the output ports in some number of cycles which is not precisely known as it depends on the history of what else was in flight and the packet length of course which is a variable.

• Verification Approach
• Intuition
• Some sample signal names and register names to outline the method
• Key assertions and constraints
• Results

Hopefully some interesting graphs to show performance! And analysis of results.

Discussion/Summary

The case study shown in this article is similar to some of the modules Axiomise teaches in its training program. In our training program, we go beyond abstraction and discuss a host of advanced techniques that provide fast & scalable proof convergence. Axiomise provides vendor agnostic, cutting edge formal verification training focused on methodology. To make sure it is compatible with all the main tools, the training program goes through rigorous testing to make sure the modules work with all the tools. In this context, I recently started to play with VC Formal the latest offering from Synopsys, and the only tool in the market that I didn’t lay my hand on so far. I thought throwing a design of this complexity would be a good litmus test to see what the tools looks like, and I must say I’ve been pleasantly surprised with what I saw.

This article was first published on the Tech Design Forum. It is reproduced here in its original form for informational and archival purposes, with appropriate acknowledgment to the original publisher.