diff --git a/artifacts/tutorial/stable-past/solution-refdiff.json b/artifacts/tutorial/stable-past/solution-refdiff.json new file mode 100644 index 0000000..8ea4f39 --- /dev/null +++ b/artifacts/tutorial/stable-past/solution-refdiff.json @@ -0,0 +1,23 @@ +{ + "source": "/var/tmp/thomas-ahle/sv-tutorial/src/lessons/sva/stable-past/stable_check.sol.sv", + "sha256": "79af4e5df559411a2ac4e89be3d432009d9951233415fb4301a7a9f612ba8dbf", + "reference_cached": false, + "reference": { + "verdict": "PASS", + "exit": 0, + "final_status": "completed" + }, + "mox": { + "verdict": "PASS", + "exit": 0, + "phase": "simulate", + "final_status": "completed" + }, + "category": "both_pass", + "output_equal": true, + "equivalent": true, + "metadata": { + "_has_pass": false + }, + "build_dir": "/var/tmp/thomas-ahle/wt/landing/build-dev-fast" +} diff --git a/src/lessons/sva/sampling-copy.test.js b/src/lessons/sva/sampling-copy.test.js new file mode 100644 index 0000000..a1b287b --- /dev/null +++ b/src/lessons/sva/sampling-copy.test.js @@ -0,0 +1,22 @@ +import { describe, expect, it } from 'vitest'; +import { readFileSync } from 'node:fs'; +import path from 'node:path'; + +const description = readFileSync( + path.resolve(process.cwd(), 'src/lessons/sva/stable-past/description.html'), + 'utf8' +); +const plainText = description.replace(/<[^>]+>/g, ' '); + +describe('sampled value lesson', () => { + it('describes sampling and four-state stability accurately', () => { + expect(description).toContain('IEEE 1800-2023 §16.5.1'); + expect(description).toContain('IEEE 1800-2023 §16.9.3'); + expect(description).toContain('==='); + expect(description).toContain('sampled values taken from the Preponed region'); + expect(description).not.toContain('evaluated in SVA\'s Observed region'); + expect( + plainText.match(/while\s+valid\s+is\s+high\s+and\s+ready\s+is\s+low,\s+data\s+must\s+not\s+change\s+on\s+the\s+next\s+cycle/gi) + ).toHaveLength(1); + }); +}); diff --git a/src/lessons/sva/stable-past/description.html b/src/lessons/sva/stable-past/description.html index e65464d..2bb52c6 100644 --- a/src/lessons/sva/stable-past/description.html +++ b/src/lessons/sva/stable-past/description.html @@ -1,8 +1,7 @@

Two more sampled value functions for tracking signal history:

-

Open stable_check.sv. The spec is: while valid is high and ready is low, data must not change on the next cycle.

-

Complete the property body: while valid is high and ready is low, data must not change on the next cycle.

-

$stable(data) is equivalent to writing data == $past(data) — use whichever reads more naturally for your spec.

+

Open stable_check.sv. The spec is: while valid is high and ready is low, data must not change on the next cycle. Complete the property body with the sampled-value functions.

+

$stable(data) compares sampled four-state values. For an explicit equivalent, use data === $past(data); case equality keeps an X-to-X or Z-to-Z comparison stable, unlike == (IEEE 1800-2023 §16.9.3).