Formal Verification of SystemVerilog in Memora8: RTL Contracts and Proof Scope
Memora8 is developing a formal verification path for real SystemVerilog modules. This article explains why simulation and formal methods complement each other, how RTL properties are checked, what the current SystemVerilog subset supports, how SJP binds results to RTL and contracts, and why verification claims are made property by property.