Improve h2/h3 lesson styles and add waveform callouts

- Add .lesson-body h2/h3 CSS rules with border separator and correct sizing
- Mention the Waves tab in always_ff, sequence-basics, clock-delay, rose-fell lessons

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

Author: thomasahle

src/app.css

@@ -168,4 +168,20 @@
   }
 
   .lesson-body strong { font-weight: 600; }
+
+  .lesson-body h2 {
+    font-size: 0.95rem;
+    font-weight: 600;
+    margin: 1.1rem 0 0.35rem;
+    color: rgb(var(--foreground));
+    border-bottom: 1px solid rgb(var(--border));
+    padding-bottom: 0.25rem;
+  }
+
+  .lesson-body h3 {
+    font-size: 0.88rem;
+    font-weight: 600;
+    margin: 0.9rem 0 0.25rem;
+    color: rgb(var(--foreground));
+  }
 }

src/lessons/sv/always-ff/description.html

@@ -6,3 +6,4 @@
   else        q <= d;
 end</pre>
               <blockquote><p>Active-low reset (<code>rst_n</code>) is conventional in RTL: the signal name ends in <code>_n</code> and asserts at 0.</p></blockquote>
+              <blockquote><p>After clicking <strong>Run</strong>, open the <strong>Waves</strong> tab to see <code>clk</code>, <code>rst_n</code>, <code>d</code>, and <code>q</code> plotted over time. You should see <code>q</code> follow <code>d</code> one cycle later once reset is released.</p></blockquote>

src/lessons/sva/clock-delay/description.html

@@ -6,3 +6,4 @@
 </ul>
 <p>Open <code>delay_check.sv</code>. The spec is: <em>after a memory request (<code>mem_req</code>), the response (<code>mem_ack</code>) must arrive within 2 to 5 clock cycles.</em></p>
 <p>Complete the property body using <code>|-> ##[2:5]</code>.</p>
+<blockquote><p>If the bound is wrong the model checker will produce a counterexample. Open the <strong>Waves</strong> tab to see which cycle <code>mem_req</code> fired and how many cycles later <code>mem_ack</code> arrived — this makes it easy to spot off-by-one errors in the delay range.</p></blockquote>

src/lessons/sva/rose-fell/description.html

@@ -6,3 +6,4 @@
 <p>These are more precise than a bare level check: <code>$rose(req)</code> triggers once per rising edge, not on every cycle that <code>req</code> stays high.</p>
 <p>Open <code>edge_check.sv</code>. The spec is: <em>when chip-select <code>cs_n</code> falls (goes active-low), <code>ack</code> must rise within 1–2 clock cycles.</em></p>
 <p>Complete the property using <code>$fell(cs_n) |=> ##[0:1] $rose(ack)</code>.</p>
+<blockquote><p>The <strong>Waves</strong> tab shows the counterexample when an assertion fails. You can see exactly when <code>cs_n</code> fell and whether <code>ack</code> rose in time — transitions are far easier to read in a waveform than in text logs.</p></blockquote>

src/lessons/sva/sequence-basics/description.html

@@ -7,3 +7,4 @@
 <p>Open <code>grant_check.sv</code>. The spec is: <em>when <code>cStart</code> is high, <code>req</code> must be high the same cycle and <code>gnt</code> must be high exactly 2 cycles later.</em></p>
 <p>Fill in the sequence body, the property body, and add the <code>assert property</code> statement.</p>
 <blockquote><p>A property is never evaluated on its own — it must be <strong>asserted</strong>, <strong>covered</strong>, or <strong>assumed</strong>.</p></blockquote>
+<blockquote><p>When the model checker finds a violation it outputs a counterexample — inspect the <strong>Waves</strong> tab to see the exact cycle-by-cycle signal values that triggered the failure.</p></blockquote>