docs: correct SVA vacuity coverage claims

src/lessons/sva-vacuity.test.js

@@ -0,0 +1,30 @@
+import { describe, expect, it } from 'vitest';
+import { readFileSync } from 'node:fs';
+
+const descriptions = [
+  'src/lessons/sva/vacuous-pass/description.html',
+  'src/lessons/sva/cover-property/description.html',
+  'src/lessons/sva/concurrent-sim/description.html'
+].map((file) => readFileSync(file, 'utf8'));
+
+describe('SVA coverage explanations', () => {
+  it('grounds vacuity and cover semantics in the IEEE clauses', () => {
+    for (const text of descriptions) {
+      expect(text).toMatch(/16\.14\.3/);
+      expect(text).toMatch(/16\.14\.8/);
+    }
+  });
+
+  it('does not claim a cover pass action proves the antecedent fired', () => {
+    const text = descriptions.join('\n');
+    expect(text).not.toMatch(/pass action[^.]*confirm(?:s|ing) the antecedent/i);
+    expect(text).not.toMatch(/cover property is essential[^.]*confirm/i);
+  });
+
+  it('uses a sequence cover for the nonvacuous request/grant exercise', () => {
+    const text = descriptions[0];
+    expect(text).toContain('cover sequence');
+    expect(text).toContain('##[1:2]');
+    expect(text).not.toContain('add the <code>assert</code> and <code>cover property</code>');
+  });
+});

src/lessons/sva/concurrent-sim/description.html

@@ -8,8 +8,8 @@
 <p>Add two statements after the property declaration:</p>
 <ul>
   <li><code>req_gnt_check: assert property (req_then_gnt)</code> with an <code>else $error(...)</code> — fires when gnt is late</li>
-  <li><code>cover property (req_then_gnt);</code> — counts how many times the property was exercised</li>
+  <li><code>cover property (req_then_gnt);</code> — records successful evaluation attempts; vacuous successes are tracked separately, so use <code>cover sequence</code> when the request itself must be observed</li>
 </ul>
 <p>Click <strong>Run</strong>. The testbench drives three scenarios: a valid grant, a missing grant, and back-to-back requests. With the assertion in place the missing-grant scenario prints an error in the log.</p>
 <p>Then open the <strong>Waves</strong> tab. The simulator automatically records every <code>assert</code> and <code>cover</code> statement as an <code>__sva__</code> signal alongside the design signals. A high (1) value means the assertion is currently passing; it drops to 0 at the clock edge where the property is violated:</p>
-<blockquote><p>Simulation covers only the paths your testbench drives. The next chapter replaces the testbench with a <strong>formal model checker</strong> that proves assertions hold for <em>every possible input sequence</em> — no testbench required.</p></blockquote>
+<blockquote><p>Simulation covers only the paths your testbench drives. IEEE 1800-2023 §§16.14.3 and 16.14.8 distinguish successful and vacuous coverage attempts. The next chapter replaces the testbench with a <strong>formal model checker</strong> that checks every possible input sequence — no testbench required.</p></blockquote>

src/lessons/sva/cover-property/description.html

@@ -1,4 +1,4 @@
               <p>If an assertion never fires, it could mean the design is correct — or that the triggering condition was <em>never exercised</em>. These are very different situations.</p>
-              <p><code><dfn data-card="cover property records each time a property's sequence fully matches — counting successes rather than failures. While assert property checks 'this must always hold', cover property checks 'did this scenario ever happen?'. It is essential for catching vacuous test suites: if your assert never fires because its antecedent never triggers, cover property exposes this silence. Always pair assert and cover on the same property — zero cover hits with zero assert failures usually means the test is not exercising the right conditions.">cover property</dfn></code> resolves this ambiguity. Its pass action runs each time the property <em>succeeds</em>, confirming the antecedent was actually stimulated:</p>
+              <p><code><dfn data-card="cover property records successful evaluation attempts rather than failures. IEEE 1800-2023 section 16.14.3 counts property coverage at most once per attempt and reports vacuous successes separately. To require a nonvacuous scenario, cover a sequence whose first item is the trigger.">cover property</dfn></code> resolves part of this ambiguity. Its coverage counters distinguish successful and vacuous attempts; a pass action alone does not prove that the antecedent was stimulated:</p>
               <p>Open <code>bus_check.sv</code>. It models a simple bus protocol: when <code>frame_</code> rises (transaction boundary), the <code>ldp_</code> strobe must fall (assert) within 1–2 cycles. The property <code>ldpcheck</code> is already written. Add both the <code>assert property</code> and <code>cover property</code> statements for it.</p>
-              <blockquote><p>Always pair <code>assert</code> and <code>cover</code> on the same property. A simulation that sees no assertion failures but also no cover hits has told you almost nothing.</p></blockquote>
+              <blockquote><p>Always pair <code>assert</code> and coverage on the same intent. IEEE 1800-2023 §§16.14.3 and 16.14.8 define vacuous success; when the trigger itself must be observed, use <code>cover sequence</code> or inspect the nonvacuous coverage counter.</p></blockquote>

src/lessons/sva/vacuous-pass/description.html

@@ -1,12 +1,12 @@
-<p>An implication property <code>antecedent |-> consequent</code> <strong><dfn data-card="Vacuous pass: an implication property trivially passes when its antecedent never triggers. The logic is 'if false, then anything' — mathematically valid, but useless for verification. A test suite where every assertion passes vacuously tells you nothing about correctness. This is why cover property is essential: it confirms the antecedent actually fired at least once.">passes vacuously</dfn></strong> when the antecedent never evaluates to true. The assertion fires zero times and reports no failures — which can be falsely reassuring.</p>
-<p>The fix is to always pair an <code>assert</code> with a companion <code>cover property</code> on the same property. <code>cover</code> does <em>not</em> pass vacuously: its pass action only fires when the antecedent actually matched and the full sequence succeeded:</p>
+<p>An implication property <code>antecedent |-> consequent</code> <strong><dfn data-card="Vacuous pass: an implication property trivially passes when its antecedent never triggers. The logic is 'if false, then anything' — mathematically valid, but useless for verification. A test suite where every assertion passes vacuously tells you nothing about correctness. IEEE 1800-2023 section 16.14.8 defines this nonvacuous distinction; cover the triggering sequence when you need evidence that it occurred.">passes vacuously</dfn></strong> when the antecedent never evaluates to true. The assertion fires zero times and reports no failures — which can be falsely reassuring.</p>
+<p>Pair the <code>assert</code> with coverage, but do not treat a <code>cover property</code> pass action as proof that the antecedent matched. IEEE 1800-2023 §16.14.3 defines coverage per evaluation attempt and reports vacuous successes separately; §16.14.8 defines the vacuous case. If you need to require a nonvacuous match, cover the triggering sequence itself:</p>
 <pre>rg_assert: assert property (req_gnt)
   else $display("FAIL at t=%0t", $time);
-rg_cover:  cover  property (req_gnt)
-           $display("antecedent fired at t=%0t", $time);</pre>
+rg_cover:  cover sequence (@(posedge clk) $rose(req) ##[1:2] gnt)
+           $display("request and grant observed at t=%0t", $time);</pre>
 <p>This lesson has two steps:</p>
 <ol>
-  <li>Open <code>vacuous.sv</code> and add the <code>assert</code> and <code>cover</code> statements. Run — notice the cover never fires, because <code>tb.sv</code> never drives <code>req</code> high.</li>
-  <li>Open <code>tb.sv</code> and uncomment the TODO lines to pulse <code>req</code> and then drive <code>gnt</code> high. Run again — the cover fires, confirming the property was actually exercised.</li>
+  <li>Open <code>vacuous.sv</code> and add the <code>assert property</code> and <code>cover sequence</code> statements for the request/grant window. Run — with no request, the assertion is vacuous and there is no nonvacuous request/grant match.</li>
+  <li>Open <code>tb.sv</code> and uncomment the TODO lines to pulse <code>req</code> and then drive <code>gnt</code> high. Run again — the sequence cover fires, proving that the request/grant scenario was exercised.</li>
 </ol>
-<blockquote><p>If the simulation ends with zero <code>cover</code> hits and zero <code>assert</code> failures, the property has told you nothing. A clean run only means something when the cover confirms the antecedent fired.</p></blockquote>
+<blockquote><p>If the simulation ends with zero nonvacuous coverage and zero assertion failures, the property may still be vacuous. A clean run only means something when the trigger or its sequence is covered.</p></blockquote>

src/lessons/sva/vacuous-pass/vacuous.sol.sv

@@ -9,7 +9,7 @@ module vacuous_demo (
 
   rg_assert: assert property (req_gnt)
     else $display("req_gnt FAIL at t=%0t", $time);
-  rg_cover:  cover  property (req_gnt)
-             $display("req_gnt antecedent fired at t=%0t", $time);
+  rg_cover:  cover sequence (@(posedge clk) $rose(req) ##[1:2] gnt)
+             $display("req_gnt sequence observed at t=%0t", $time);
 
 endmodule

src/lessons/sva/vacuous-pass/vacuous.sv

@@ -9,6 +9,6 @@ module vacuous_demo (
       $rose(req) |-> ##[1:2] gnt;
   endproperty
 
-  // TODO: add an assert property and a cover property for req_gnt
+  // TODO: add an assert property and a cover sequence for the request/grant window
 
 endmodule