Full article coming soon. Outline below.
Outline
- Reading the microarchitecture specification — what to look for
- Writing the Verification Plan — scope, intent, and coverage goals
- Writing the Verification Architecture Specification
- Building the formal testbench in SystemVerilog
- Writing SVA properties — sequences, properties, and auxiliary code
- Setting up the JasperGold environment with TCL scripting
- Running proofs — interpreting results, vacuity, and unreachability
- Complexity reduction — when and how to use abstraction and blackboxing
- Bug triage and root-cause collaboration with the design team
- Coverage closure — what done actually looks like