Networking and Formal Verification

I attended Oski’s latest Decoding Formal event a couple of weeks ago and again enjoyed a largely customer-centric view of the problems to which they apply formal, and their experiences in making it work for them (with Oski help of course). From an admittedly limited sample of two of these events, I find them very representative of the high-end of formal application, what you can do when you build significant internal expertise or bring in experts like Oski. These events also highlight the kinds of property-checking problem that are attacked at this level, falling outside the range of formal apps (today) and in some cases outside what you might even consider normal usage. I’ll get to that last point in a subsequent blog.

The event opened with a keynote given by Dan Lenowski (Sr. VP Eng. and cofounder of Barefoot Networks). Dan started with a quick overview of the anatomy of a shared network switch (apologies in advance to networking experts – what follows is my non-expert view of the domain): per-lane receive MACs and ingress forwarding pipelines, in the middle packet buffering and queueing, then again per-lane egress forwarding pipelines and transmit MACs. Dan talked about verification challenges for each separately.

Formal plays the biggest role in datapath verification (the central block), where it shines in dealing with combinational complexity across variable-sized packets and variable line-speeds, particularly in verifying the queue arbiter (no surprise to formal experts). Here they use it to model:

• Correctness – port N is only granted if port N has a request pending
• Fairness – port N gets one grant before any other port gets two grants (at the same speed)
• Work-conserving – some port is granted for every cycle that more than one cell is available at the input
• Sufficient bandwidth – port N will wait no more than that port’s fraction of total shared bandwidth before being granted.

Saurabh Shrivastava (Sr. Mgr. at Cavium) spoke next on a methodology for formally verifying software-defined networking (SDN) silicon, an important topic for networking devices today. Saurabh pointed to OpenFlow as a reference standard for SDN where the control layer and forwarding layer are separate and the control layer manages multiple devices/switches. This can obviously be managed, optimized and reprogrammed to handle multiple possible use-cases, today and in the future, such as IoT use-modes and SD-WAN. So highly configurable, but it can’t be slower than hard-wired solutions and, because it is configurable, verification has to deal with a very complex configuration space, across all of which it has to deliver top performance. In other words, a great fit for formal.

Saurabh went into a lot of detail on their formal methodology and I don’t want to steal his thunder (watch the video), but I will say I was impressed by the discipline in their process. They follow a full test-planning and tracking methodology which would be familiar to any simulation-based verification team. They have intensive test-planning and tracking, a common Makefile and regression framework, coverage review, the works. Assertions, constraints and cover properties are all comprehensively reviewed by the team and tracked as verification progresses. Coverage reviews are as detailed as testplan reviews and they mark off what is covered by formal since it then does not have to be covered in simulation.

Saurabh illustrated with 4 designs ranging from relatively simple to more complex, with I thought an illuminating discussion on how they proceeded through managing the complexity of the formal problem in each case. This is when formal runs out of space/time or gets to an inconclusive result on the raw problem and you have to start thinking about cut-points, black-boxes and abstractions. Saurabh started gently with an IPv4 header checksum generator block. They tried proofs with and without an inserted bug. Formal found the buggy case, slowly, on the full RTL but the clean case run was inconclusive. They ran through 3 stages of abstraction to get down to runs where both the bug was found quickly and the clean case returned a proof. In subsequent examples, they used symbolic values, reset abstraction, data coloring and symmetries to get to closure. Good case studies on dealing with complexity management.

You can check out Oski’s Decoding Formalvideos HERE. (The December video was not yet posted at the time I wrote this, I assume it will be soon.)