Skip to content

fix: make BMC lesson verdicts explicit #18

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
thomasnormal merged 2 commits into from
Oct 2, 2026
Merged

fix: make BMC lesson verdicts explicit #18

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2859b6f
fix: make BMC lesson verdicts explicit
thomasahle Oct 2, 2026
6324eb5
test: fold BMC verdict review nits
thomasahle Oct 2, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 17 additions & 0 deletions artifacts/tutorial/SUMMARY.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,22 @@
# sv-tutorial: make lessons pass, fix wrong content, make the QA honest

## 2026-10-02 BMC verdict follow-up

Commit `e3e28d0` makes the bounded outcome of every active BMC lesson explicit.
The 23 checker lessons with unconstrained inputs now explain that the completed
syntax exercise should report `COUNTEREXAMPLE FOUND` with a model witness; the
three design-constrained lessons (`sva/formal-intro`, `sva/seq-args`, and
`sva/formal-assume`) expect `PROVED within the BMC bound`. The runtime returns
the parsed verdict, completion accepts only the lesson's declared verdict, and
the solution e2e asserts the wording and counterexample witness. Starters for
formal-intro, formal-assume, and disable-iff no longer silently complete.

Validation: `npm test` passes (78 passed, 4 skipped), `npm run build` passes,
and the pinned-bundle BMC browser smoke passes 4/4. The full formal browser
spec was not completed because the temporary checkout lacked `mox-lec` assets;
the split-view smoke also still targets the quarantined UVM route and needs a
separate fixture PR. This change does not rebuild or repin WASM.

## 2026-09-30 continuation

The repository baseline is `24175be` (`origin/main`). The required install,
Expand Down
85 changes: 48 additions & 37 deletions e2e/solutions.spec.js
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,14 +15,13 @@
* equivalence check). These are the only cases where mox-bmc can prove
* unsat because the design itself rules out counterexamples.
*
* expectUnsat: false — only checks that [z3] ran and exit codes are 0.
* Property-only modules (checker modules with free input ports and
* assertions but no design logic) always produce [z3] sat because BMC
* can trivially assign free inputs to violate any non-trivial property.
* That is expected and correct behaviour for these lessons.
* expectUnsat: false — expects a bounded counterexample for the completed
* syntax exercise. These checker modules intentionally leave their inputs
* free, so a non-trivial assertion is violated by some legal input trace.
*/

import { test, expect } from '@playwright/test';
import lessonMeta from '../src/lessons/meta.js';

// ── Navigation helper ─────────────────────────────────────────────────────────

Expand Down Expand Up @@ -69,8 +68,9 @@ async function goToLesson(page, chapterName, lessonName) {
// runner: 'lec' → logical equivalence check (verify button; expects [z3] unsat)
// runner: 'cocotb' → cocotb Python tests (run/test button)
//
// expectUnsat: true → module has design logic; mox-bmc should prove unsat.
// expectUnsat: false → property-only module; [z3] sat is expected and OK.
const bmcExpectedByTitle = new Map(
Object.values(lessonMeta).map((meta) => [meta.title, meta.bmcExpected])
);

const LESSONS = [
// ── SystemVerilog Basics ────────────────────────────────────────────────────
Expand All @@ -93,35 +93,33 @@ const LESSONS = [
{ chapter: 'Runtime Assertions', title: 'Concurrent Assertions in Simulation', runner: null, expectAssertionFail: true },
{ chapter: 'Runtime Assertions', title: 'Vacuous Pass', runner: null },
{ chapter: 'Runtime Assertions', title: '$isunknown — Detecting X and Z', runner: null },
{ chapter: 'Your First Formal Assertion', title: 'Immediate Assertions', runner: 'bmc', expectUnsat: false },
{ chapter: 'Your First Formal Assertion', title: 'Sequences and Properties', runner: 'bmc', expectUnsat: false },
{ chapter: 'Implication & BMC', title: 'Implication: |-> and |=>', runner: 'bmc', expectUnsat: false },
// formal-intro: up-counter design — reset guarantees cnt == 0 → proved unsat
{ chapter: 'Implication & BMC', title: 'Bounded Model Checking', runner: 'bmc', expectUnsat: true },
{ chapter: 'Core Sequences', title: 'Clock Delay ##m and ##[m:n]', runner: 'bmc', expectUnsat: false },
{ chapter: 'Core Sequences', title: '$rose and $fell', runner: 'bmc', expectUnsat: false },
{ chapter: 'Core Sequences', title: 'Request / Acknowledge', runner: 'bmc', expectUnsat: false },
{ chapter: 'Repetition Operators', title: 'Consecutive Repetition [*m]', runner: 'bmc', expectUnsat: false },
{ chapter: 'Repetition Operators', title: 'Goto Repetition [->m]', runner: 'bmc', expectUnsat: false },
{ chapter: 'Repetition Operators', title: 'Non-Consecutive Equal Repetition [=m]', runner: 'bmc', expectUnsat: false },
{ chapter: 'Sequence Operators', title: 'throughout — Stability During a Sequence', runner: 'bmc', expectUnsat: false },
{ chapter: 'Sequence Operators', title: 'Sequence Composition: intersect, within, and, or', runner: 'bmc', expectUnsat: false },
{ chapter: 'Sampled Value Functions', title: '$stable and $past', runner: 'bmc', expectUnsat: false },
{ chapter: 'Sampled Value Functions', title: '$changed and $sampled', runner: 'bmc', expectUnsat: false },
{ chapter: 'Protocols & Coverage', title: 'disable iff — Reset Handling', runner: 'bmc', expectUnsat: false },
{ chapter: 'Protocols & Coverage', title: 'Aborting Properties: reject_on and accept_on', runner: 'bmc', expectUnsat: false },
{ chapter: 'Protocols & Coverage', title: 'cover property', runner: 'bmc', expectUnsat: false },
{ chapter: 'Advanced Properties', title: 'Local Variables in Sequences', runner: 'bmc', expectUnsat: false },
{ chapter: 'Advanced Properties', title: '$onehot, $onehot0, $countones', runner: 'bmc', expectUnsat: false },
{ chapter: 'Advanced Properties', title: '.triggered — Sequence Endpoint Detection', runner: 'bmc', expectUnsat: false },
{ chapter: 'Advanced Properties', title: 'The checker Construct', runner: 'bmc', expectUnsat: false },
{ chapter: 'Advanced Properties', title: 'Recursive Properties', runner: 'bmc', expectUnsat: false },
// formal-assume: traffic-light FSM + assume → state space constrained → proved unsat
{ chapter: 'Formal Verification', title: 'assume property', runner: 'both', expectUnsat: true },
{ chapter: 'Formal Verification', title: 'always and s_eventually', runner: 'bmc', expectUnsat: false },
{ chapter: 'Formal Verification', title: 'until and s_until', runner: 'bmc', expectUnsat: false },
// lec: two circuit implementations compared — proved equivalent → unsat
{ chapter: 'Formal Verification', title: 'Logical Equivalence Checking', runner: 'lec', expectUnsat: true },
{ chapter: 'Your First Formal Assertion', title: 'Immediate Assertions', runner: 'bmc' },
{ chapter: 'Your First Formal Assertion', title: 'Sequences and Properties', runner: 'bmc' },
{ chapter: 'Implication & BMC', title: 'Implication: |-> and |=>', runner: 'bmc' },
{ chapter: 'Implication & BMC', title: 'Bounded Model Checking', runner: 'bmc' },
{ chapter: 'Core Sequences', title: 'Clock Delay ##m and ##[m:n]', runner: 'bmc' },
{ chapter: 'Core Sequences', title: '$rose and $fell', runner: 'bmc' },
{ chapter: 'Core Sequences', title: 'Request / Acknowledge', runner: 'bmc' },
{ chapter: 'Repetition Operators', title: 'Consecutive Repetition [*m]', runner: 'bmc' },
{ chapter: 'Repetition Operators', title: 'Goto Repetition [->m]', runner: 'bmc' },
{ chapter: 'Repetition Operators', title: 'Non-Consecutive Equal Repetition [=m]', runner: 'bmc' },
{ chapter: 'Sequence Operators', title: 'throughout — Stability During a Sequence', runner: 'bmc' },
{ chapter: 'Sequence Operators', title: 'Sequence Composition: intersect, within, and, or', runner: 'bmc' },
{ chapter: 'Sequence Operators', title: 'Sequence Formal Arguments', runner: 'bmc' },
{ chapter: 'Sampled Value Functions', title: '$stable and $past', runner: 'bmc' },
{ chapter: 'Sampled Value Functions', title: '$changed and $sampled', runner: 'bmc' },
{ chapter: 'Protocols & Coverage', title: 'disable iff — Reset Handling', runner: 'bmc' },
{ chapter: 'Protocols & Coverage', title: 'Aborting Properties: reject_on and accept_on', runner: 'bmc' },
{ chapter: 'Protocols & Coverage', title: 'cover property', runner: 'bmc' },
{ chapter: 'Advanced Properties', title: 'Local Variables in Sequences', runner: 'bmc' },
{ chapter: 'Advanced Properties', title: '$onehot, $onehot0, $countones', runner: 'bmc' },
{ chapter: 'Advanced Properties', title: '.triggered — Sequence Endpoint Detection', runner: 'bmc' },
{ chapter: 'Advanced Properties', title: 'The checker Construct', runner: 'bmc' },
{ chapter: 'Advanced Properties', title: 'Recursive Properties', runner: 'bmc' },
{ chapter: 'Formal Verification', title: 'assume property', runner: 'both' },
{ chapter: 'Formal Verification', title: 'always and s_eventually', runner: 'bmc' },
{ chapter: 'Formal Verification', title: 'until and s_until', runner: 'bmc' },
{ chapter: 'Formal Verification', title: 'Logical Equivalence Checking', runner: 'lec' },

// ── UVM ────────────────────────────────────────────────────────────────────
{ chapter: 'UVM Foundations', title: 'The First UVM Test', runner: null },
Expand Down Expand Up @@ -167,13 +165,26 @@ for (const lesson of LESSONS) {
await expect(logs).toContainText('unsat', { timeout: Z3_TIMEOUT });

} else if (lesson.runner === 'bmc' || lesson.runner === 'both') {
const expectedVerdict = bmcExpectedByTitle.get(lesson.title);
expect(expectedVerdict, `${lesson.title} must declare bmcExpected in src/lessons/meta.js`).toMatch(
/^(counterexample|proved)$/
);
await page.getByTestId('verify-button').click();
await assertNoCompileError(logs);
await expect(logs).not.toContainText('# mox-bmc exit code: 1', { timeout: COMPILE_TIMEOUT });
await expect(logs).toContainText('[z3]', { timeout: Z3_TIMEOUT });
if (lesson.expectUnsat) {
const expectation = page.getByTestId('bmc-expectation');
await expect(expectation).toBeVisible();
if (expectedVerdict === 'proved') {
await expect(expectation).toContainText('PROVED within the BMC bound');
await expect(logs).toContainText('[z3] unsat', { timeout: Z3_TIMEOUT });
await expect(logs).not.toContainText('[z3] sat');
await expect(logs).toContainText('# verdict: PROVED within the BMC bound', { timeout: Z3_TIMEOUT });
} else {
await expect(expectation).toContainText('COUNTEREXAMPLE FOUND');
await expect(logs).toContainText('[z3] sat', { timeout: Z3_TIMEOUT });
await expect(logs).toContainText('# verdict: COUNTEREXAMPLE FOUND', { timeout: Z3_TIMEOUT });
await expect(logs).toContainText('# counterexample:', { timeout: Z3_TIMEOUT });
}

} else if (lesson.runner === 'cocotb') {
Expand Down
29 changes: 27 additions & 2 deletions src/lessons/bmc-presentation.test.js
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,13 @@
import { describe, expect, it } from 'vitest';
import { readdirSync, readFileSync } from 'node:fs';
import { readFileSync } from 'node:fs';
import path from 'node:path';
import metas from './meta.js';
import { BMC_EXPECTED_VERDICTS } from '../lib/bmc-verdict.js';

const root = path.resolve(process.cwd(), 'src/lessons/sva');
const bmcLessons = readdirSync(root).filter((name) => name !== 'lec' && name !== 'concurrent-sim');
const bmcLessons = Object.entries(metas)
.filter(([, meta]) => meta.runner === 'bmc' || meta.runner === 'both')
.map(([slug]) => slug.split('/').pop());

describe('BMC lesson presentation', () => {
it('does not promise a Waves tab for BMC runs', () => {
Expand All @@ -23,4 +27,25 @@ describe('BMC lesson presentation', () => {
);
expect(offenders).toEqual([]);
});

it('declares the expected bounded verdict for every BMC lesson', () => {
const missing = Object.entries(metas)
.filter(([, meta]) => meta.runner === 'bmc' || meta.runner === 'both')
.filter(([, meta]) => !BMC_EXPECTED_VERDICTS.has(meta.bmcExpected))
.map(([slug]) => slug);
expect(missing).toEqual([]);
});

it('keeps the formal starter tasks aligned with the supplied skeletons', () => {
const cases = [
['formal-intro', 'assertion skeleton are provided', 'Add a concurrent assertion'],
['formal-assume', 'starter already provides', 'Add an <code>assume property</code>'],
['disable-iff', 'clause are provided', 'add <code>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);
}
});
});
Loading
Loading