diff --git a/src/lessons/sva-vacuity.test.js b/src/lessons/sva-vacuity.test.js new file mode 100644 index 0000000..90a4c1c --- /dev/null +++ b/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 assert and cover property'); + }); +}); diff --git a/src/lessons/sva/concurrent-sim/description.html b/src/lessons/sva/concurrent-sim/description.html index 8b3e588..0334ffa 100644 --- a/src/lessons/sva/concurrent-sim/description.html +++ b/src/lessons/sva/concurrent-sim/description.html @@ -8,8 +8,8 @@

Add two statements after the property declaration:

Click Run. 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.

Then open the Waves tab. The simulator automatically records every assert and cover statement as an __sva__ 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:

-

Simulation covers only the paths your testbench drives. The next chapter replaces the testbench with a formal model checker that proves assertions hold for every possible input sequence — no testbench required.

+

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 formal model checker that checks every possible input sequence — no testbench required.

diff --git a/src/lessons/sva/cover-property/description.html b/src/lessons/sva/cover-property/description.html index 7345311..f93c14c 100644 --- a/src/lessons/sva/cover-property/description.html +++ b/src/lessons/sva/cover-property/description.html @@ -1,4 +1,4 @@

If an assertion never fires, it could mean the design is correct — or that the triggering condition was never exercised. These are very different situations.

-

cover property resolves this ambiguity. Its pass action runs each time the property succeeds, confirming the antecedent was actually stimulated:

+

cover property 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:

Open bus_check.sv. It models a simple bus protocol: when frame_ rises (transaction boundary), the ldp_ strobe must fall (assert) within 1–2 cycles. The property ldpcheck is already written. Add both the assert property and cover property statements for it.

-

Always pair assert and cover on the same property. A simulation that sees no assertion failures but also no cover hits has told you almost nothing.

+

Always pair assert 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 cover sequence or inspect the nonvacuous coverage counter.

diff --git a/src/lessons/sva/vacuous-pass/description.html b/src/lessons/sva/vacuous-pass/description.html index 0700962..94f5849 100644 --- a/src/lessons/sva/vacuous-pass/description.html +++ b/src/lessons/sva/vacuous-pass/description.html @@ -1,12 +1,12 @@ -

An implication property antecedent |-> consequent passes vacuously when the antecedent never evaluates to true. The assertion fires zero times and reports no failures — which can be falsely reassuring.

-

The fix is to always pair an assert with a companion cover property on the same property. cover does not pass vacuously: its pass action only fires when the antecedent actually matched and the full sequence succeeded:

+

An implication property antecedent |-> consequent passes vacuously when the antecedent never evaluates to true. The assertion fires zero times and reports no failures — which can be falsely reassuring.

+

Pair the assert with coverage, but do not treat a cover property 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:

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);
+rg_cover: cover sequence (@(posedge clk) $rose(req) ##[1:2] gnt) + $display("request and grant observed at t=%0t", $time);

This lesson has two steps:

    -
  1. Open vacuous.sv and add the assert and cover statements. Run — notice the cover never fires, because tb.sv never drives req high.
    2. -
  2. Open tb.sv and uncomment the TODO lines to pulse req and then drive gnt high. Run again — the cover fires, confirming the property was actually exercised.
    3. +
  3. Open vacuous.sv and add the assert property and cover sequence statements for the request/grant window. Run — with no request, the assertion is vacuous and there is no nonvacuous request/grant match.
    4. +
  4. Open tb.sv and uncomment the TODO lines to pulse req and then drive gnt high. Run again — the sequence cover fires, proving that the request/grant scenario was exercised.
-

If the simulation ends with zero cover hits and zero assert failures, the property has told you nothing. A clean run only means something when the cover confirms the antecedent fired.

+

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.

diff --git a/src/lessons/sva/vacuous-pass/vacuous.sol.sv b/src/lessons/sva/vacuous-pass/vacuous.sol.sv index 07e6e3a..87d7cd8 100644 --- a/src/lessons/sva/vacuous-pass/vacuous.sol.sv +++ b/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 diff --git a/src/lessons/sva/vacuous-pass/vacuous.sv b/src/lessons/sva/vacuous-pass/vacuous.sv index 9720061..70acbe6 100644 --- a/src/lessons/sva/vacuous-pass/vacuous.sv +++ b/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