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)
-