Find deep corner bugs with exhaustive formal verification

As an independent consultant, I offer a surgeon’s precision to ASIC verification. While simulation-based flows are necessary, they are rarely sufficient for today’s high-stakes silicon projects. I specialize in applying Formal Methods to solve the industry's toughest challenges.

Expertise and tech stack

Formal methodology

  • We signoff an RTL block when these tasks have been done:

    • Checkers: one end-to-end SVA property per specification requirement

    • Constraints: perform over-constraint analysis (no dead code)

    • Complexity: bounded proofs must exceed the maximum latency of the design

    • Coverage: each line of RTL is linked to at least one proven property

  • Breaking down the DUT’s intended behaviour to a set of logic rules, each represented by one or a few SVA properties.

  • A technique to verify the data integrity and ordering of a design by proving that every data entering a design exits correctly.

  • Setup and use of semi-automated apps to do:

    • FSM deadlock / livelock analysis

    • X propagation

    • Automated property generation (superlint)

    • Connectivity checking

    • RTL mutation

  • Use formal tools to ensure that the RTL’s output matches a bit-accurate C model.

Tool workflows

  • Initial formal testbench definition, either by hand or through generation scripts.

  • Production ready script flows to launch the formal tool, compile RTL, perform analysis and collect statistics. TCL, Python, Make.

  • Avoid reinventing the wheel by integrating reusable Assertion IP from trusted vendors to verify common protocols like AXI.

Some technologies and protocols from past projects

    • Verifying new RTL to signoff ready

    • Integration of 3rd party Assertion IPs

    • Security: verifying access rules at the interconnect

    • Interrupt rules

    • Data transport

    • C to RTL equivalence checking using VC Formal DPV (Data Path Validation, formerly HECTOR)