Add 12 new SVA lessons from Mehta book

Tier 1 — core language gaps:
- sva/nonconsec-eq: [=m] non-consecutive equal repetition
- sva/throughout: throughout operator for signal stability
- sva/sequence-ops: intersect, within, and, or composition
- sva/isunknown: $isunknown() X/Z detection (with testbench)
- sva/changed: $changed() and $sampled()

Tier 2 — formal/temporal operators:
- sva/always-eventually: s_eventually and always (LTL operators)
- sva/until: s_until, until_with temporal "hold" operators
- sva/abort: reject_on / accept_on property preemption

Tier 3 — structural/reusable:
- sva/triggered: .triggered sequence endpoint detection
- sva/checker: checker construct for reusable assertion bundles
- sva/recursive: recursive properties for "hold until" patterns

Curriculum updated: new chapters "Sequence Operators" and expanded
"Formal Verification"; abort added to Properties & Implication;
isunknown/changed added to Sampled Value Functions;
triggered/checker/recursive added to Advanced Properties.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: thomasahle

src/lessons/index.js

@@ -73,12 +73,13 @@ export const parts = [
     title: 'SystemVerilog Assertions',
     chapters: [
       { title: 'Your First Assertion',      lessons: [L('sva/immediate-assert'), L('sva/sequence-basics')] },
-      { title: 'Clock Delay & Sequences',   lessons: [L('sva/clock-delay'), L('sva/consecutive-rep'), L('sva/nonconsec-rep')] },
-      { title: 'Properties & Implication',  lessons: [L('sva/implication'), L('sva/req-ack'), L('sva/disable-iff'), L('sva/vacuous-pass')] },
-      { title: 'Sampled Value Functions',   lessons: [L('sva/rose-fell'), L('sva/stable-past')] },
+      { title: 'Clock Delay & Sequences',   lessons: [L('sva/clock-delay'), L('sva/consecutive-rep'), L('sva/nonconsec-rep'), L('sva/nonconsec-eq')] },
+      { title: 'Sequence Operators',        lessons: [L('sva/throughout'), L('sva/sequence-ops')] },
+      { title: 'Properties & Implication',  lessons: [L('sva/implication'), L('sva/req-ack'), L('sva/disable-iff'), L('sva/vacuous-pass'), L('sva/abort')] },
+      { title: 'Sampled Value Functions',   lessons: [L('sva/rose-fell'), L('sva/stable-past'), L('sva/isunknown'), L('sva/changed')] },
       { title: 'Coverage',                  lessons: [L('sva/cover-property')] },
-      { title: 'Advanced Properties',       lessons: [L('sva/local-vars'), L('sva/onehot')] },
-      { title: 'Formal Verification',       lessons: [L('sva/formal-intro'), L('sva/formal-assume'), L('sva/lec')] },
+      { title: 'Advanced Properties',       lessons: [L('sva/local-vars'), L('sva/onehot'), L('sva/triggered'), L('sva/checker'), L('sva/recursive')] },
+      { title: 'Formal Verification',       lessons: [L('sva/formal-intro'), L('sva/formal-assume'), L('sva/always-eventually'), L('sva/until'), L('sva/lec')] },
     ],
   },
   {

src/lessons/sva/abort/abort_check.sol.sv

@@ -0,0 +1,9 @@
+module abort_check(input logic clk, start, ack, err);
+
+  property p_burst_ok;
+    @(posedge clk) start |=> reject_on(err) (##[1:4] ack);
+  endproperty
+
+  burst_ok_a: assert property (p_burst_ok);
+
+endmodule

src/lessons/sva/abort/abort_check.sv

@@ -0,0 +1,13 @@
+module abort_check(input logic clk, start, ack, err);
+
+  // Spec: after start, ack must arrive within 4 cycles.
+  // If err fires mid-transfer, fail immediately.
+  property p_burst_ok;
+    @(posedge clk)
+      // TODO: start |=> reject_on(err) (##[1:4] ack);
+      ;
+  endproperty
+
+  burst_ok_a: assert property (p_burst_ok);
+
+endmodule

src/lessons/sva/abort/description.html

@@ -0,0 +1,10 @@
+<p>Sometimes an in-progress property should be terminated early — either because an abort condition renders the check irrelevant, or because its occurrence should itself be flagged as a failure. SVA provides two operators for this:</p>
+<ul>
+  <li><code>reject_on(cond) prop</code> — if <code>cond</code> becomes true while <code>prop</code> is being evaluated, <strong>fail</strong> immediately.</li>
+  <li><code>accept_on(cond) prop</code> — if <code>cond</code> becomes true, <strong>pass</strong> immediately (abort without failure).</li>
+</ul>
+<p>Both have synchronous variants — <code>sync_reject_on</code> and <code>sync_accept_on</code> — that only sample <code>cond</code> at the property's clock edge instead of asynchronously.</p>
+<p>Example: a burst transfer should normally complete with <code>ack</code> within 4 cycles, but if an error fires mid-burst the property should immediately fail:</p>
+<pre>start |=> reject_on(err) (##[1:4] ack)</pre>
+<p>Open <code>abort_check.sv</code> and complete the property body using <code>reject_on</code>.</p>
+<blockquote><p><code>reject_on(cond) seq</code> is equivalent to <code>(!cond) throughout seq</code> — both fail when <code>cond</code> goes true during the sequence window. <code>reject_on</code> is more expressive because it also applies to composite properties, not just sequences.</p></blockquote>

src/lessons/sva/abort/meta.json

@@ -0,0 +1,4 @@
+{
+  "title": "Aborting Properties: reject_on and accept_on",
+  "focus": "/src/abort_check.sv"
+}

src/lessons/sva/always-eventually/description.html

@@ -0,0 +1,17 @@
+<p>SVA provides two operators for reasoning about entire future traces rather than bounded windows:</p>
+<ul>
+  <li><code>s_eventually prop</code> — <strong>strong eventually</strong>: <code>prop</code> must become true at some future clock tick. Fails if the trace ends without it occurring.</li>
+  <li><code>always prop</code> — <code>prop</code> must hold at <em>every</em> clock tick from now on.</li>
+</ul>
+<p>The <em>strong</em> vs <em>weak</em> distinction matters for formal tools: a weak property (<code>eventually</code>) is satisfied vacuously by a finite trace that never reaches the condition, while a strong property (<code>s_eventually</code>) demands the condition eventually occurs:</p>
+<pre>// After POR, the lock signal must eventually assert
+property p_lock_live;
+  @(posedge clk) $rose(rst_n) |-> s_eventually lock;
+endproperty
+
+// Once locked, it stays locked
+property p_lock_stable;
+  @(posedge clk) lock |-> always lock;
+endproperty</pre>
+<p>Open <code>liveness.sv</code> and fill in both property bodies.</p>
+<blockquote><p><code>s_eventually</code> and <code>always</code> used as property operators are <strong>IEEE 1800-2012</strong> features. They express Linear Temporal Logic (LTL) properties and require a formal tool that supports unbounded reasoning. Bounded model checking can only falsify them within its bound, not fully prove them.</p></blockquote>

src/lessons/sva/always-eventually/liveness.sol.sv

@@ -0,0 +1,14 @@
+module liveness(input logic clk, rst_n, lock);
+
+  property p_lock_live;
+    @(posedge clk) $rose(rst_n) |-> s_eventually lock;
+  endproperty
+
+  property p_lock_stable;
+    @(posedge clk) lock |-> always lock;
+  endproperty
+
+  lock_live_a:   assert property (p_lock_live);
+  lock_stable_a: assert property (p_lock_stable);
+
+endmodule

src/lessons/sva/always-eventually/liveness.sv

@@ -0,0 +1,20 @@
+module liveness(input logic clk, rst_n, lock);
+
+  // After POR, the lock signal must eventually assert (liveness)
+  property p_lock_live;
+    @(posedge clk)
+      // TODO: $rose(rst_n) |-> s_eventually lock;
+      ;
+  endproperty
+
+  // Once lock asserts it never de-asserts (safety)
+  property p_lock_stable;
+    @(posedge clk)
+      // TODO: lock |-> always lock;
+      ;
+  endproperty
+
+  lock_live_a:   assert property (p_lock_live);
+  lock_stable_a: assert property (p_lock_stable);
+
+endmodule

src/lessons/sva/always-eventually/meta.json

@@ -0,0 +1,4 @@
+{
+  "title": "always and s_eventually",
+  "focus": "/src/liveness.sv"
+}

src/lessons/sva/changed/description.html

@@ -0,0 +1,6 @@
+<p><code>$changed(sig)</code> returns true when a signal's sampled value differs from its value at the previous clock edge — a concise way to write <code>sig !== $past(sig)</code>:</p>
+<pre>update |=> $changed(data)</pre>
+<p>The companion function <code>$sampled(expr)</code> returns the value of an expression as sampled in the preponed region (the settled value at the clock edge). It is most useful inside action blocks to print what the checker actually saw:</p>
+<pre>else $error("data unchanged: 0x%0h", $sampled(data));</pre>
+<p>Open <code>toggle_check.sv</code> and complete the property body: while <code>update</code> is high, <code>data</code> must change every cycle.</p>
+<blockquote><p><code>$changed</code> uses four-state inequality (<code>!==</code>) so it is also true when a signal transitions to or from X. To ignore X transitions use <code>data != $past(data)</code> (two-state inequality) instead.</p></blockquote>