diff --git a/artifacts/tutorial/triggered/solution-refdiff.json b/artifacts/tutorial/triggered/solution-refdiff.json new file mode 100644 index 0000000..5f8b1a3 --- /dev/null +++ b/artifacts/tutorial/triggered/solution-refdiff.json @@ -0,0 +1,23 @@ +{ + "source": "/var/tmp/thomas-ahle/sv-tutorial/src/lessons/sva/triggered/trigger_check.sol.sv", + "sha256": "7766530f0b1a59923a25d2f0a3ab441801dd5abd4d7eec84e64e5cb8a4861314", + "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/sequence-methods.test.js b/src/lessons/sva/sequence-methods.test.js new file mode 100644 index 0000000..4072ad9 --- /dev/null +++ b/src/lessons/sva/sequence-methods.test.js @@ -0,0 +1,19 @@ +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/triggered/description.html'), + 'utf8' +); + +describe('sequence method lesson', () => { + it('describes triggered and matched according to IEEE 1800-2023', () => { + expect(description).toContain('IEEE 1800-2023 §16.9.11'); + expect(description).toContain('IEEE 1800-2023 §16.13.5'); + expect(description).toMatch(/IEEE 1800-2023 §§16\.9\.11 and 16\.13\.6/); + expect(description).toContain('inside another sequence'); + expect(description).not.toMatch(/\.triggered[^.]*can only be used in the antecedent/i); + expect(description).not.toMatch(/\.matched[^.]*stays true until the next clock edge of a different clock domain/i); + }); +}); diff --git a/src/lessons/sva/triggered/description.html b/src/lessons/sva/triggered/description.html index 0267a5d..1dde925 100644 --- a/src/lessons/sva/triggered/description.html +++ b/src/lessons/sva/triggered/description.html @@ -1,4 +1,4 @@ -

Every named sequence has a built-in property .triggered that is true at the clock tick where the sequence reaches its endpoint:

+

Every named sequence has a built-in method .triggered that is true at the clock tick where the sequence reaches its endpoint (IEEE 1800-2023 §§16.9.11 and 16.13.6):

sequence s_req_done;
   @(posedge clk) req ##1 !busy;
 endsequence
@@ -6,6 +6,6 @@
 // .triggered is true at the clock tick where s_req_done reaches its endpoint
 s_req_done.triggered |-> ...

This lets you build modular properties: define a sequence once, then reference its endpoint from multiple properties without duplicating the sequence body.

-

The related .matched property extends the endpoint signal so it stays true until the next clock edge of a different clock domain — useful for cross-clock handshake assertions.

+

The related .matched method is useful when a sequence is composed across clocks. It reports the source sequence's endpoint result at the first sampling event of the destination clock; same-clock composition remains valid, while .triggered directly tests the endpoint at that point (IEEE 1800-2023 §16.13.5).

Open trigger_check.sv and complete the property: when the request sequence ends, ack must arrive within 3 cycles.

-

.triggered can only be used in the antecedent of an implication or as a standalone assertion — it is not a sequence itself. If you need to use a sequence endpoint inside another sequence, embed the sequence directly with seq1 ##0 seq2 (zero-delay concatenation).

+

.triggered can also be used inside another sequence. IEEE 1800-2023 §16.9.11 shows an expression such as reset ##1 inst ##1 e1.triggered ##1 branch_back; the method tests the endpoint at that point without requiring the source sequence to start there.