docs: correct SVA sampled-value guidance

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"
+}

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);
+  });
+});

src/lessons/sva/stable-past/description.html

@@ -1,8 +1,7 @@
 <p>Two more sampled value functions for tracking signal history:</p>
 <ul>
-  <li><code><dfn data-card="$stable(sig) is a sampled value function that returns true when sig's value at the current clock edge equals its value at the previous clock edge — i.e., the signal did not change. It is equivalent to (sig === $past(sig)). $stable is often used in bus-hold assertions: while valid is high and ready is low, the data bus must not change.">$stable</dfn>(sig)</code> — true when <code>sig</code> did <em>not</em> change between the previous and current clock edge</li>
-  <li><code><dfn data-card="$past(sig) returns the sampled value of sig from the previous clock edge — one cycle ago. $past(sig, n) goes back exactly n cycles. It is evaluated in SVA's Observed region, just like $rose and $stable. Use it to express data-flow properties: 'the output must equal the input from 2 cycles ago.' For detecting whether a signal simply did not change, $stable(sig) is more readable than sig === $past(sig), but both are equivalent.">$past</dfn>(sig)</code> — the value of <code>sig</code> from exactly 1 cycle ago; <code>$past(sig, n)</code> goes back <code>n</code> cycles</li>
+  <li><code><dfn data-card="$stable(sig) is a sampled value function that returns true when sig's value at the current clock edge equals its value at the previous clock edge — i.e., the signal did not change. It is equivalent to (sig === $past(sig)). $stable is often used in bus-hold assertions: while valid is high and ready is low, the data bus must not change at each sampling event.">$stable</dfn>(sig)</code> — true when <code>sig</code> did <em>not</em> change between the previous and current clock edge</li>
+  <li><code><dfn data-card="$past(sig) returns the sampled value of sig from the previous clock edge — one cycle ago. $past(sig, n) goes back exactly n cycles. Concurrent assertions use sampled values taken from the Preponed region (IEEE 1800-2023 §16.5.1), then evaluate the assertion in the Observed region. Use $past to express data-flow properties: 'the output must equal the input from 2 cycles ago.'">$past</dfn>(sig)</code> — the value of <code>sig</code> from exactly 1 cycle ago; <code>$past(sig, n)</code> goes back <code>n</code> cycles</li>
 </ul>
-<p>Open <code>stable_check.sv</code>. The spec is: <em>while <code>valid</code> is high and <code>ready</code> is low, <code>data</code> must not change on the next cycle.</em></p>
-<p>Complete the property body: while <code>valid</code> is high and <code>ready</code> is low, <code>data</code> must not change on the next cycle.</p>
-<blockquote><p><code>$stable(data)</code> is equivalent to writing <code>data == $past(data)</code> — use whichever reads more naturally for your spec.</p></blockquote>
+<p>Open <code>stable_check.sv</code>. The spec is: <em>while <code>valid</code> is high and <code>ready</code> is low, <code>data</code> must not change on the next cycle.</em> Complete the property body with the sampled-value functions.</p>
+<blockquote><p><code>$stable(data)</code> compares sampled four-state values. For an explicit equivalent, use <code>data === $past(data)</code>; case equality keeps an X-to-X or Z-to-Z comparison stable, unlike <code>==</code> (IEEE 1800-2023 §16.9.3).</p></blockquote>