assume property'],
+ ['disable-iff', 'clause are provided', 'add disable iff'],
+ ];
+ for (const [name, required, forbidden] of cases) {
+ const text = readFileSync(path.join(root, name, 'description.html'), 'utf8');
+ expect(text).toContain(required);
+ expect(text).not.toContain(forbidden);
+ }
+ });
});
diff --git a/src/lessons/meta.js b/src/lessons/meta.js
index c4b8c59..3e000d4 100644
--- a/src/lessons/meta.js
+++ b/src/lessons/meta.js
@@ -28,32 +28,32 @@ export default {
'sva/concurrent-sim': { title: 'Concurrent Assertions in Simulation', focus: '/src/monitor.sv', runner: null },
'sva/vacuous-pass': { title: 'Vacuous Pass', focus: '/src/vacuous.sv' },
'sva/isunknown': { title: '$isunknown — Detecting X and Z', focus: '/src/xcheck.sv' },
- 'sva/immediate-assert': { title: 'Immediate Assertions', focus: '/src/fifo_checker.sv', runner: 'bmc' },
- 'sva/sequence-basics': { title: 'Sequences and Properties', focus: '/src/grant_check.sv', runner: 'bmc' },
- 'sva/implication': { title: 'Implication: |-> and |=>', focus: '/src/implication.sv', runner: 'bmc' },
- 'sva/formal-intro': { title: 'Bounded Model Checking', focus: '/src/top.sv', runner: 'bmc' },
- 'sva/clock-delay': { title: 'Clock Delay ##m and ##[m:n]', focus: '/src/delay_check.sv', runner: 'bmc' },
- 'sva/rose-fell': { title: '$rose and $fell', focus: '/src/edge_check.sv', runner: 'bmc' },
- 'sva/req-ack': { title: 'Request / Acknowledge', focus: '/src/req_ack.sv', runner: 'bmc' },
- 'sva/consecutive-rep': { title: 'Consecutive Repetition [*m]', focus: '/src/hold_check.sv', runner: 'bmc' },
- 'sva/nonconsec-rep': { title: 'Goto Repetition [->m]', focus: '/src/multi_ack.sv', runner: 'bmc' },
- 'sva/nonconsec-eq': { title: 'Non-Consecutive Equal Repetition [=m]', focus: '/src/multi_ack2.sv', runner: 'bmc' },
- 'sva/throughout': { title: 'throughout — Stability During a Sequence', focus: '/src/spi_check.sv', runner: 'bmc' },
- 'sva/sequence-ops': { title: 'Sequence Composition: intersect, within, and, or', focus: '/src/bus_check.sv', runner: 'bmc' },
- 'sva/seq-args': { title: 'Sequence Formal Arguments', focus: '/src/sram_check.sv', runner: 'bmc' },
- 'sva/stable-past': { title: '$stable and $past', focus: '/src/stable_check.sv', runner: 'bmc' },
- 'sva/changed': { title: '$changed and $sampled', focus: '/src/toggle_check.sv', runner: 'bmc' },
- 'sva/disable-iff': { title: 'disable iff — Reset Handling', focus: '/src/reset_check.sv', runner: 'bmc' },
- 'sva/abort': { title: 'Aborting Properties: reject_on and accept_on', focus: '/src/abort_check.sv', runner: 'bmc' },
- 'sva/cover-property': { title: 'cover property', focus: '/src/bus_check.sv', runner: 'bmc' },
- 'sva/local-vars': { title: 'Local Variables in Sequences', focus: '/src/pipeline_check.sv', runner: 'bmc' },
- 'sva/onehot': { title: '$onehot, $onehot0, $countones', focus: '/src/arbiter_check.sv', runner: 'bmc' },
- 'sva/triggered': { title: '.triggered — Sequence Endpoint Detection', focus: '/src/trigger_check.sv', runner: 'bmc' },
- 'sva/checker': { title: 'The checker Construct', focus: '/src/top.sv', runner: 'bmc' },
- 'sva/recursive': { title: 'Recursive Properties', focus: '/src/lock_check.sv', runner: 'bmc' },
- 'sva/formal-assume': { title: 'assume property', focus: '/src/top.sv', runner: 'both' },
- 'sva/always-eventually': { title: 'always and s_eventually', focus: '/src/liveness.sv', runner: 'bmc' },
- 'sva/until': { title: 'until and s_until', focus: '/src/hold_check.sv', runner: 'bmc' },
+ 'sva/immediate-assert': { title: 'Immediate Assertions', focus: '/src/fifo_checker.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/sequence-basics': { title: 'Sequences and Properties', focus: '/src/grant_check.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/implication': { title: 'Implication: |-> and |=>', focus: '/src/implication.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/formal-intro': { title: 'Bounded Model Checking', focus: '/src/top.sv', runner: 'bmc', bmcExpected: 'proved' },
+ 'sva/clock-delay': { title: 'Clock Delay ##m and ##[m:n]', focus: '/src/delay_check.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/rose-fell': { title: '$rose and $fell', focus: '/src/edge_check.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/req-ack': { title: 'Request / Acknowledge', focus: '/src/req_ack.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/consecutive-rep': { title: 'Consecutive Repetition [*m]', focus: '/src/hold_check.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/nonconsec-rep': { title: 'Goto Repetition [->m]', focus: '/src/multi_ack.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/nonconsec-eq': { title: 'Non-Consecutive Equal Repetition [=m]', focus: '/src/multi_ack2.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/throughout': { title: 'throughout — Stability During a Sequence', focus: '/src/spi_check.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/sequence-ops': { title: 'Sequence Composition: intersect, within, and, or', focus: '/src/bus_check.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/seq-args': { title: 'Sequence Formal Arguments', focus: '/src/sram_check.sv', runner: 'bmc', bmcExpected: 'proved' },
+ 'sva/stable-past': { title: '$stable and $past', focus: '/src/stable_check.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/changed': { title: '$changed and $sampled', focus: '/src/toggle_check.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/disable-iff': { title: 'disable iff — Reset Handling', focus: '/src/reset_check.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/abort': { title: 'Aborting Properties: reject_on and accept_on', focus: '/src/abort_check.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/cover-property': { title: 'cover property', focus: '/src/bus_check.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/local-vars': { title: 'Local Variables in Sequences', focus: '/src/pipeline_check.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/onehot': { title: '$onehot, $onehot0, $countones', focus: '/src/arbiter_check.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/triggered': { title: '.triggered — Sequence Endpoint Detection', focus: '/src/trigger_check.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/checker': { title: 'The checker Construct', focus: '/src/top.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/recursive': { title: 'Recursive Properties', focus: '/src/lock_check.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/formal-assume': { title: 'assume property', focus: '/src/top.sv', runner: 'both', bmcExpected: 'proved' },
+ 'sva/always-eventually': { title: 'always and s_eventually', focus: '/src/liveness.sv', runner: 'bmc', bmcExpected: 'counterexample' },
+ 'sva/until': { title: 'until and s_until', focus: '/src/hold_check.sv', runner: 'bmc', bmcExpected: 'counterexample' },
'sva/lec': { title: 'Logical Equivalence Checking', focus: '/src/top.sv', runner: 'lec', module1: 'Spec', module2: 'Impl' },
// ── UVM ───────────────────────────────────────────────────────────────────
diff --git a/src/lessons/sva/disable-iff/description.html b/src/lessons/sva/disable-iff/description.html
index 3ced6f8..786bbd0 100644
--- a/src/lessons/sva/disable-iff/description.html
+++ b/src/lessons/sva/disable-iff/description.html
@@ -2,5 +2,5 @@
@(posedge clk) disable iff (reset_condition)
antecedent |=> consequent;
While the reset condition is true, the property evaluates as vacuously true — no failure is reported.
- Open reset_check.sv and add disable iff (!rst_n) between the clock specification and the implication.
+ Open reset_check.sv. The clock and disable iff (!rst_n) clause are provided; complete the implication that follows them.
disable iff is asynchronous: the property is disabled the moment the condition becomes true, not at the next clock edge.
diff --git a/src/lessons/sva/disable-iff/reset_check.sv b/src/lessons/sva/disable-iff/reset_check.sv
index 97f2821..cfb7a9e 100644
--- a/src/lessons/sva/disable-iff/reset_check.sv
+++ b/src/lessons/sva/disable-iff/reset_check.sv
@@ -3,9 +3,9 @@ module reset_check(
input logic req, ack
);
property req_ack_p;
- @(posedge clk)
- // TODO: add disable iff (!rst_n) before the implication
- req |=> ack;
+ @(posedge clk) disable iff (!rst_n)
+ // TODO: when req fires outside reset, ack must be high on the next cycle
+ ;
endproperty
req_ack_a: assert property (req_ack_p);
diff --git a/src/lessons/sva/formal-assume/description.html b/src/lessons/sva/formal-assume/description.html
index 5d96893..dfc6ba9 100644
--- a/src/lessons/sva/formal-assume/description.html
+++ b/src/lessons/sva/formal-assume/description.html
@@ -3,8 +3,8 @@
Think of assume as the dual of assert: assert says "the design must guarantee this", while assume says "the environment promises this".
Open top.sv. A traffic-light FSM cycles RED → GREEN → YELLOW → RED. The state output should never reach the illegal value 3.
- - Add an
assume property that constrains BMC to start in reset: rst is high at the first clock edge. Put it in an initial block so it is checked only once, at that first edge: initial assume property (@(posedge clk) rst);
- - Add an
assert property that checks state 3 is unreachable within the BMC bound — add a disable iff (rst) so it isn't checked during reset itself.
+ - The starter already provides the one-time
assume property that constrains BMC to start in reset. Read it as the environment assumption for this exercise.
+ - Complete the
assert property body so state 3 is unreachable within the BMC bound, keeping the provided disable iff (rst) so it isn't checked during reset itself.
Use run to simulate the FSM cycling through states, then verify to formally prove state 3 is unreachable.
Without the assume, BMC may start with rst low and state = 3 at cycle 0: the register has no value until reset has been applied, so any initial state is possible. Assuming reset at the first edge excludes those unreachable initial states. Assume only what the environment really promises, which is an input like rst. An assumption on the design's own state (for example rst |-> state == 0) would fail in simulation, because state is still X at the first edge.
diff --git a/src/lessons/sva/formal-assume/top.sv b/src/lessons/sva/formal-assume/top.sv
index 37c6675..a21d400 100644
--- a/src/lessons/sva/formal-assume/top.sv
+++ b/src/lessons/sva/formal-assume/top.sv
@@ -13,5 +13,11 @@ module top(
end
// TODO: assume property — rst is high at the first clock edge (constrains BMC's initial states)
- // TODO: assert property — state 3 is never reached (disable during rst)
+ initial assume property (@(posedge clk) rst);
+
+ no_invalid: assert property (
+ @(posedge clk) disable iff (rst)
+ // TODO: state 3 is never reached
+ ;
+ );
endmodule
diff --git a/src/lessons/sva/formal-intro/description.html b/src/lessons/sva/formal-intro/description.html
index 673dae8..26265c6 100644
--- a/src/lessons/sva/formal-intro/description.html
+++ b/src/lessons/sva/formal-intro/description.html
@@ -6,6 +6,6 @@
counterexample found? → FAIL
no counterexample? → NO COUNTEREXAMPLE (within depth N)
There is no testbench needed for BMC. The tool treats all inputs as free variables and tries to find a counterexample. If it cannot find one within the bound, the result is no counterexample within the explored depth — a bounded result, not an unbounded proof.
- Open top.sv. A 4-bit counter resets to 0 when rst is high. Add a concurrent assertion inside the module that checks this reset property — use implication to say "if rst fires, then on the next cycle cnt must be zero."
+ Open top.sv. The 4-bit counter and the assertion skeleton are provided. Complete the concurrent property so it checks that when rst is high, cnt is zero on the next cycle — use implication for the "if rst fires, then ..." relationship.
Press verify to have BMC check every possible input sequence up to the bound. The log labels an unsat result as PROVED within the BMC bound and a sat result as COUNTEREXAMPLE FOUND.
BMC is bounded: a proof at depth N does not guarantee correctness at depth N+1. Full unbounded proof requires induction or deeper techniques — but for reset properties and most pipeline assertions, a modest bound is sufficient.
diff --git a/src/lessons/sva/formal-intro/top.sv b/src/lessons/sva/formal-intro/top.sv
index ac3bb34..0358dbb 100644
--- a/src/lessons/sva/formal-intro/top.sv
+++ b/src/lessons/sva/formal-intro/top.sv
@@ -6,5 +6,11 @@ module top(
if (rst) cnt <= 4'b0;
else cnt <= cnt + 1;
- // TODO: assert that when rst fires, cnt is 0 on the next cycle
+ property reset_clears;
+ @(posedge clk)
+ // TODO: when rst fires, cnt must be 0 on the next cycle
+ ;
+ endproperty
+
+ reset_clears_a: assert property (reset_clears);
endmodule
diff --git a/src/lib/bmc-verdict.js b/src/lib/bmc-verdict.js
new file mode 100644
index 0000000..b14f3c8
--- /dev/null
+++ b/src/lib/bmc-verdict.js
@@ -0,0 +1,6 @@
+export const BMC_EXPECTED_VERDICTS = new Set(['counterexample', 'proved']);
+
+export function bmcRunPasses(lesson, result) {
+ if (lesson?.bmcExpected) return result?.verdict === lesson.bmcExpected;
+ return result?.ok === true;
+}
diff --git a/src/lib/bmc-verdict.test.js b/src/lib/bmc-verdict.test.js
new file mode 100644
index 0000000..2b1cab9
--- /dev/null
+++ b/src/lib/bmc-verdict.test.js
@@ -0,0 +1,22 @@
+import { describe, expect, it } from 'vitest';
+import { bmcRunPasses } from './bmc-verdict.js';
+
+describe('BMC lesson verdicts', () => {
+ it('accepts the expected counterexample as a completed lesson result', () => {
+ expect(bmcRunPasses({ bmcExpected: 'counterexample' }, { verdict: 'counterexample', ok: false })).toBe(true);
+ });
+
+ it('does not accept the wrong bounded verdict', () => {
+ expect(bmcRunPasses({ bmcExpected: 'proved' }, { verdict: 'counterexample', ok: false })).toBe(false);
+ });
+
+ it('fails closed when the bounded verdict is missing', () => {
+ expect(bmcRunPasses({ bmcExpected: 'proved' }, { ok: true })).toBe(false);
+ expect(bmcRunPasses({ bmcExpected: 'counterexample' }, { verdict: null, ok: false })).toBe(false);
+ });
+
+ it('keeps non-BMC completion tied to the runner result', () => {
+ expect(bmcRunPasses({}, { verdict: 'counterexample', ok: false })).toBe(false);
+ expect(bmcRunPasses({}, { verdict: 'proved', ok: true })).toBe(true);
+ });
+});
diff --git a/src/routes/lesson/[part]/[name]/+page.svelte b/src/routes/lesson/[part]/[name]/+page.svelte
index 6d47665..f866de7 100644
--- a/src/routes/lesson/[part]/[name]/+page.svelte
+++ b/src/routes/lesson/[part]/[name]/+page.svelte
@@ -8,6 +8,7 @@
import { darkMode, vimMode } from '$lib/stores/settings.js';
import { completedSlugs, completedSourceHashes } from '$lib/stores/completed.js';
import { cloneFiles, mergeFiles, topNameForLesson } from '$lib/lesson-utils.js';
+ import { bmcRunPasses } from '$lib/bmc-verdict.js';
import { termCard } from '$lib/actions/term-card.js';
import { highlightCode } from '$lib/actions/highlight-code.js';
import CodeEditor from '$lib/components/CodeEditor.svelte';
@@ -490,7 +491,9 @@
typeof entry === 'string' && /SVA assertion failed/i.test(entry)
);
if (runGeneration !== workspaceLoadGeneration) return;
- lastRunPassed = result?.ok === true && !hasAssertionFailure;
+ lastRunPassed = useBmc
+ ? bmcRunPasses(lesson, result) && !hasAssertionFailure
+ : result?.ok === true && !hasAssertionFailure;
if (lastRunPassed) {
completedSourceHashes.update(s => new Map([...s, [lesson.slug, runSourceHash]]));
if (browser) {
@@ -571,6 +574,19 @@
{@html lesson.html}
+ {#if lesson.bmcExpected === 'counterexample'}
+
+ {:else if lesson.bmcExpected === 'proved'}
+
+ {/if}