Dr Ashish Darbari – founder and CEO of Axiomise is proud to present a webinar hosted by Synopsys on Exhaustive Formal Verification of Packet-Based Designs on 19 Sep 2018. Please register here to join it.

ABSTRACT

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 serialized nature of packet flow, where the state of each packet depends upon the history of all the previous packets in flight. These type of designs can be seen all around in network routers, bus protocols, bus bridges, load-store units in CPU, packing and unpacking designs, and SoC peripherals such as I2C, I2S, USB, UART, and Ethernet.

This webinar presents a case study to verify a packet-based design using the Synopsys VC Formal Property Verification (FPV) app. The crux of the solution presented is based on abstraction. Based on experience and coupled with VC Formal’s ease of use, abstraction provides a powerful tractable solution to an otherwise intractable problem. In addition, the multi-property proof engine technology of the FPV app aids abstraction-based methodology and provides a significant speedup in the computing performance and tractability required to build exhaustive proofs for such packet-based designs.

Some of the questions that we answer in this webinar are:

• Why verification of serial designs is a challenge?
• How abstraction can be used for verifying serial designs?
• Impact of abstraction on exhaustive proofs
• Coping with inconclusive proofs
• Extending the reach of formal to convert inconclusive proofs to exhaustive
• Finding bugs