Skip to content

Commit 91198cd

Browse files
committed
docs: fold sampled value review nits
1 parent fa58268 commit 91198cd

3 files changed

Lines changed: 25 additions & 1 deletion

File tree

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
{
2+
"source": "/var/tmp/thomas-ahle/sv-tutorial/src/lessons/sva/stable-past/stable_check.sol.sv",
3+
"sha256": "79af4e5df559411a2ac4e89be3d432009d9951233415fb4301a7a9f612ba8dbf",
4+
"reference_cached": false,
5+
"reference": {
6+
"verdict": "PASS",
7+
"exit": 0,
8+
"final_status": "completed"
9+
},
10+
"mox": {
11+
"verdict": "PASS",
12+
"exit": 0,
13+
"phase": "simulate",
14+
"final_status": "completed"
15+
},
16+
"category": "both_pass",
17+
"output_equal": true,
18+
"equivalent": true,
19+
"metadata": {
20+
"_has_pass": false
21+
},
22+
"build_dir": "/var/tmp/thomas-ahle/wt/landing/build-dev-fast"
23+
}

‎src/lessons/sva/sampling-copy.test.js‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ const plainText = description.replace(/<[^>]+>/g, ' ');
1111
describe('sampled value lesson', () => {
1212
it('describes sampling and four-state stability accurately', () => {
1313
expect(description).toContain('IEEE 1800-2023 §16.5.1');
14+
expect(description).toContain('IEEE 1800-2023 §16.9.3');
1415
expect(description).toContain('===');
1516
expect(description).toContain('sampled values taken from the Preponed region');
1617
expect(description).not.toContain('evaluated in SVA\'s Observed region');

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
<p>Two more sampled value functions for tracking signal history:</p>
22
<ul>
3-
<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>
3+
<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>
44
<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>
55
</ul>
66
<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>

0 commit comments

Comments
 (0)