- A fixed synthetic formal board reported 8/8 PROVEN. After a proof-quality audit, only 5/8 earned TRUSTWORTHY: one assertion was VACUOUS and two were WEAK. 🧵
- Proof Firewall re-audits fixture-authored "LLM-authored" SVA after the engine reports green. A green formal result alone is not tape-out evidence. This demo uses synthetic transition-system IR, not customer RTL.
- ARB3 reads: assert (g0 && g1) |-> (turn == 0). In the synthetic arbiter, g0 && g1 is unreachable. The implication passes without constraining the design, so the result is VACUOUS.
- That check matters because a proven implication can certify nothing if its antecedent never occurs. We test reachability before a green result can receive TRUSTWORTHY and be filed for human sign-off.
- PIPE3 exposes the other side of the audit: assert v2 |-> (s2 == s2). Its tautological consequent survives every relevant injected mutation, so the featured synthetic pipeline case records a 0/6 mutation kill result and is WEAK.
- The gate also calculates cone of influence (COI) and routes each property to TRUSTWORTHY, BOUNDED-PROVEN, VACUOUS, WEAK, DEAD, or VIOLATED. Only TRUSTWORTHY receives a signed demonstration certificate.
- The 8/8-to-5/8 reversal is a fixed synthetic fixture result, not a claim about production RTL, customer designs, or commercial formal engines. It is a concrete case for auditing proof quality before filing a green result.
- For AI-assisted SVA sign-off, should a proof be fileable before its antecedent is reachable and its property kills relevant mutations? #FormalVerification #SystemVerilog #FunctionalVerification #VLSI
- We built Proof Firewall to make that review decision inspectable. The demo makes the synthetic audit and certificate workflow available for inspection: https://veriprajna.com/demos/semiconductor-ai-verification
Published on X · August 21, 2026
On social media
See this post on its original platform
In our archive