Skip to main content

vj_sim/sched/
sensitivity.rs

1//! SCHED::SENSITIVITY — the inverted-index `SensitivityTable`, static
2//! registration, and the `ValueChangeSink` adapter that routes a committed
3//! value change to the set of processes it must wake (scheduler.md §4;
4//! ARCHITECTURE §6.3; ledger SC-045, SC-046, SC-067, SC-071).
5//!
6//! `notify_change` (Task 7/8's `commit_nba`/`commit_blocking_write`) is the
7//! *only* production caller of [`SensitivityTable::matches`], reached
8//! through the thin [`SensitivityLookupSink`] adapter defined here — this
9//! module owns the lookup, not the decision of what to do with a match (that
10//! is Task 10's `queued_this_pass` dedup and the ready-set push, layered on
11//! top of the `ProcessId`s this module yields).
12
13use rustc_hash::FxHashMap;
14
15use smallvec::SmallVec;
16
17use crate::process::PredicateFn;
18use crate::sched::{EventTerm, EventWaitSet, ProcessId, StaticSensitivity, edge_between};
19use crate::state::{ChangeDelta, EdgeKind, StateCellId, ValueChangeSink};
20use vj_abi::{Bit4, Region, SimTime};
21
22/// One row of the inverted index (scheduler.md §4's literal shape): `Static`
23/// entries are installed once, at process-registration time, from
24/// codegen-supplied `StaticSensitivity` metadata; `Dynamic` entries are
25/// installed/removed every time a process suspends/resumes on a general
26/// `@(...)`/`wait(...)` (built from the live [`EventWaitSet`] at that exact
27/// suspend point) and are gone from the table the instant the owning process
28/// resumes.
29///
30/// `Static::edge == None` means "any change" (`always_comb`/`always_latch`'s
31/// LRM-implicit "all variables read" sensitivity); `Static::edge ==
32/// Some(k)` means "only transitions classifying as `k`" (`always_ff`'s
33/// explicit clock/reset edge). `Dynamic::edge` is not wrapped in `Option`
34/// because scheduler.md's `EventWaitSet`/`EventTerm` family never produces an
35/// untyped "no edge" dynamic term — an any-change dynamic wakeup (e.g. an
36/// `ImplicitAny` disjunct, or a named-event trigger pulse) is represented
37/// directly as `EdgeKind::None`, the same sentinel [`SensitivityTable::matches`]
38/// treats as an unconditional match (any call into `matches` already implies
39/// a real change happened — see `matches`'s doc comment) for `Static`
40/// entries — so one matching rule serves both variants uniformly.
41#[derive(Clone, Copy, Debug)]
42pub enum SensitivityEntry {
43    Static {
44        proc: ProcessId,
45        /// The edge's index in `StaticSensitivity::edges` (reported as the fired
46        /// term, so a native process can tell which member of its event list fired).
47        term_index: usize,
48        edge: Option<EdgeKind>,
49        /// `Some((lsb, width))` for an `always_comb`/`always_latch` that reads
50        /// only a constant bit/part select of the cell (LRM 9.2.2.2.1: the
51        /// longest static prefix, not the whole variable, is in the implicit
52        /// sensitivity list): the entry matches only an update that changed
53        /// those bits (see [`SensitivityTable::narrow_static`]).
54        sel: Option<(u32, u32)>,
55    },
56    Dynamic {
57        proc: ProcessId,
58        term_index: usize,
59        edge: EdgeKind,
60        iff: Option<PredicateFn>,
61        /// `Some(count)` iff this row was installed from the *inner* term of
62        /// an `EventTerm::Repeat { count, inner }` (ledger SC-052) — `None`
63        /// for an ordinary `Edge`/`ImplicitAny`/`NamedEventTrigger` term.
64        /// `matches` surfaces this so `sched::control`'s
65        /// `EngineNotifySink::notify_change` can route a matching firing
66        /// through `RepeatCounters::on_term_fired` before ever enqueueing —
67        /// the sensitivity table itself only tracks *whether* a row is
68        /// repeat-sourced and its declared total, never a live remaining
69        /// count (that lives in `sched::repeat::RepeatCounters`, keyed by
70        /// `(proc, term_index)`, not here).
71        repeat_total: Option<u64>,
72        /// `Some((lsb, width))` for a wait on a bit/part select of the cell
73        /// (`@(v[3])`, `@(posedge v[5:4])`, LRM 9.4.2): the entry matches only
74        /// an update that changed those bits (and, for an edge, whose
75        /// transition on bit `lsb` is that edge) -- decided from the update's
76        /// [`ChangeDelta`], not from the cell's own bit-0 classification.
77        sel: Option<(u32, u32)>,
78    },
79}
80
81/// The inverted index itself: `StateCellId -> SmallVec<SensitivityEntry>`
82/// (scheduler.md §4). `SmallVec<[_; 4]>` per the plan's literal type —
83/// most cells are read by a small, fixed number of always-blocks, so this
84/// avoids a heap allocation per row in the common case.
85#[derive(Default)]
86pub struct SensitivityTable {
87    table: FxHashMap<StateCellId, SmallVec<[SensitivityEntry; 4]>>,
88    /// Reverse index for [`Self::remove_dynamic`]: every cell on whose row a
89    /// `Dynamic` entry of the process was installed since its last removal.
90    /// Lets removal touch only those rows instead of scanning every row of
91    /// `table`. A cell may appear more than once (one entry per installed
92    /// term); removal is idempotent per row, so duplicates are harmless.
93    dynamic_cells: FxHashMap<ProcessId, SmallVec<[StateCellId; 4]>>,
94}
95
96impl SensitivityTable {
97    pub fn new() -> Self {
98        Self {
99            table: FxHashMap::default(),
100            dynamic_cells: FxHashMap::default(),
101        }
102    }
103
104    /// Pushes one `Dynamic` row for `proc` on `cell` and records the cell in
105    /// the reverse index.
106    fn push_dynamic(&mut self, cell: StateCellId, proc: ProcessId, entry: SensitivityEntry) {
107        self.table.entry(cell).or_default().push(entry);
108        self.dynamic_cells.entry(proc).or_default().push(cell);
109    }
110
111    /// Installs one `SensitivityEntry::Static` per `(cell, edge)` pair in
112    /// `sensitivity.edges` — the exact codegen-supplied read-set -> table-row
113    /// translation (SC-045/SC-046). Called exactly once per process, at
114    /// registration time; the production call site (`Engine::register_process`,
115    /// gated on `sensitivity.is_some()`) is Task 18's, not this module's —
116    /// this method itself has no idempotence guard because nothing here can
117    /// tell "first call" from "second call" for the same process, so that
118    /// invariant is the caller's obligation (proved by Task 18's dedicated
119    /// production-call-site test, per this task's own plan text).
120    pub fn install_static(&mut self, sensitivity: &StaticSensitivity, proc: ProcessId) {
121        for (term_index, &(cell, edge)) in sensitivity.edges.iter().enumerate() {
122            self.table
123                .entry(cell)
124                .or_default()
125                .push(SensitivityEntry::Static {
126                    proc,
127                    term_index,
128                    edge,
129                    sel: None,
130                });
131        }
132    }
133
134    /// Narrows `proc`'s installed `Static` entries on `cell` to the bit
135    /// windows `(lsb, width)` it actually reads (LRM 9.2.2.2.1): each entry
136    /// becomes one per window, matching only an update that changed that
137    /// window. A no-op for an empty `windows`; the per-process dedup gate
138    /// makes several matching windows of one update wake the process once.
139    pub fn narrow_static(&mut self, proc: ProcessId, cell: StateCellId, windows: &[(u32, u32)]) {
140        let Some(row) = self.table.get_mut(&cell) else {
141            return;
142        };
143        let mut narrowed: SmallVec<[SensitivityEntry; 4]> = SmallVec::new();
144        row.retain(|e| match *e {
145            SensitivityEntry::Static {
146                proc: p,
147                term_index,
148                edge: None,
149                sel: None,
150            } if p == proc => {
151                for &w in windows {
152                    narrowed.push(SensitivityEntry::Static {
153                        proc,
154                        term_index,
155                        edge: None,
156                        sel: Some(w),
157                    });
158                }
159                false
160            }
161            _ => true,
162        });
163        row.extend(narrowed);
164    }
165
166    /// Installs one `SensitivityEntry::Dynamic` per `(cell, term)` pair a
167    /// suspended `wait(...)`/`@(...)` implies, keyed by that term's index in
168    /// `wait.terms` (the same index `ResumeArg::EventFired { term_index }`
169    /// reports back on the firing wakeup). Recurses through
170    /// `EventTerm::Repeat` to its `inner` term, keeping the *outer* Repeat
171    /// term's index — the repeat *count* is resume-orchestration state (Task
172    /// 12/13's concern: how many times the inner event must fire before the
173    /// process actually resumes), not something the sensitivity table itself
174    /// tracks or needs to.
175    pub fn install_dynamic(&mut self, wait: &EventWaitSet, proc: ProcessId) {
176        for (term_index, term) in wait.terms.iter().enumerate() {
177            self.install_term(term, proc, term_index, None);
178        }
179    }
180
181    /// `repeat_total` is `None` for every top-level term except when
182    /// recursing into an `EventTerm::Repeat`'s `inner` term, where it becomes
183    /// `Some(count)` — threaded down so whatever leaf row(s) `inner`
184    /// installs (an `Edge`/`ImplicitAny`/`NamedEventTrigger`, or, in
185    /// principle, a further nested `Repeat`) carry the declared count `Task
186    /// 3` (ledger SC-052) needs at match time.
187    fn install_term(
188        &mut self,
189        term: &EventTerm,
190        proc: ProcessId,
191        term_index: usize,
192        repeat_total: Option<u64>,
193    ) {
194        match term {
195            EventTerm::Edge { cell, edge, iff } => {
196                self.push_dynamic(
197                    *cell,
198                    proc,
199                    SensitivityEntry::Dynamic {
200                        proc,
201                        term_index,
202                        edge: *edge,
203                        iff: *iff,
204                        repeat_total,
205                        sel: None,
206                    },
207                );
208            }
209            EventTerm::ImplicitAny(cells) => {
210                for &cell in cells {
211                    self.push_dynamic(
212                        cell,
213                        proc,
214                        SensitivityEntry::Dynamic {
215                            proc,
216                            term_index,
217                            edge: EdgeKind::None,
218                            iff: None,
219                            repeat_total,
220                            sel: None,
221                        },
222                    );
223                }
224            }
225            EventTerm::Select {
226                cell,
227                edge,
228                lsb,
229                width,
230            } => {
231                self.push_dynamic(
232                    *cell,
233                    proc,
234                    SensitivityEntry::Dynamic {
235                        proc,
236                        term_index,
237                        edge: *edge,
238                        iff: None,
239                        repeat_total,
240                        sel: Some((*lsb, *width)),
241                    },
242                );
243            }
244            EventTerm::NamedEventTrigger(cell) => {
245                // scheduler.md §8: a named event's "write" is a pure trigger
246                // pulse with no persistent value — matched the same way an
247                // any-change disjunct is (any non-`None` classified change on
248                // its reserved `StateCellId` wakes the waiter).
249                self.push_dynamic(
250                    *cell,
251                    proc,
252                    SensitivityEntry::Dynamic {
253                        proc,
254                        term_index,
255                        edge: EdgeKind::None,
256                        iff: None,
257                        repeat_total,
258                        sel: None,
259                    },
260                );
261            }
262            EventTerm::Repeat { count, inner } => {
263                self.install_term(inner, proc, term_index, Some(*count));
264            }
265        }
266    }
267
268    /// Removes every `Dynamic` entry belonging to `proc`, from every cell —
269    /// "removed the instant the owning process resumes" (scheduler.md §4).
270    /// `Static` entries are untouched: they are installed once at
271    /// registration and must survive for the process's entire lifetime.
272    pub fn remove_dynamic(&mut self, proc: ProcessId) {
273        // Only the rows the process installed onto can hold its `Dynamic`
274        // entries (`push_dynamic` is the sole writer), so visit just those.
275        let Some(cells) = self.dynamic_cells.remove(&proc) else {
276            return;
277        };
278        for cell in cells {
279            if let Some(entries) = self.table.get_mut(&cell) {
280                entries.retain(|entry| {
281                    !matches!(
282                        entry,
283                        SensitivityEntry::Dynamic { proc: p, .. } if *p == proc
284                    )
285                });
286            }
287        }
288    }
289
290    /// Yields every `ProcessId` whose sensitivity entry on `cell` matches the
291    /// just-committed transition classified as `edge`.
292    ///
293    /// `edge` is only ever `infer_edge`'s classification of *bit 0* of the
294    /// old/new value (`sched/notify.rs`'s LRM Table 9-1 scalar posedge/
295    /// negedge table) — it is not a "did the whole cell change" signal, and
296    /// a multi-bit cell can genuinely change (`SignalAccess::write` returns
297    /// `true`) while bit 0 itself stays fixed (e.g. `Narrow(0b10) ->
298    /// Narrow(0b110)`), in which case `infer_edge` reports `EdgeKind::None`
299    /// for a real change. Both production callers of this table
300    /// (`commit_nba`/`commit_blocking_write`, via `notify_change` /
301    /// [`SensitivityLookupSink`]) call in *only* for a write
302    /// `SignalAccess::write` reported as an actual change — so any call
303    /// reaching `matches` at all, regardless of what `edge` it carries,
304    /// represents a real change on `cell`. A "any change" entry
305    /// (`always_comb`/`always_latch`'s LRM-implicit read-set sensitivity,
306    /// SC-046) must therefore fire on *every* such call, not just the ones
307    /// where `infer_edge` happened to classify bit 0 as non-`None` — that is
308    /// the only reading consistent with "wake on any read-set change" rather
309    /// than "wake only when bit 0 of the read-set changes".
310    ///
311    /// Matching rule (uniform across `Static`/`Dynamic`, unifying `Static`'s
312    /// `Option<EdgeKind>` to the same `EdgeKind` sentinel `Dynamic` already
313    /// uses via `.unwrap_or(EdgeKind::None)`):
314    /// - an entry whose edge is `EdgeKind::None` ("any change") matches
315    ///   unconditionally — every call into `matches` is already gated, by
316    ///   its callers, on a real change having happened, so the incoming
317    ///   `edge` classification (which only speaks to bit 0) cannot be used
318    ///   to veto an any-change waiter;
319    /// - an entry whose edge is `EdgeKind::BothEdges` (SV's `edge` keyword,
320    ///   `@(edge sig)`) matches any real committed transition, i.e. an
321    ///   incoming `Posedge` or `Negedge` — `infer_edge` (sched/notify.rs) is
322    ///   documented and proved to never itself produce `BothEdges`, so this
323    ///   is the entry-side wildcard for that keyword, not the incoming-side
324    ///   one;
325    /// - any other edge-qualified entry matches that exact incoming `edge`,
326    ///   or an incoming `EdgeKind::BothEdges` — kept for forward-compatibility
327    ///   even though no production caller passes `BothEdges` as the
328    ///   *incoming* classification today. An edge-qualified (`always_ff`)
329    ///   entry is correctly *not* woken by a bit0-unchanged multi-bit change
330    ///   it wasn't watching for — only the any-change case needs the
331    ///   incoming-`edge`-is-imprecise fix above.
332    ///
333    /// Returns, for every entry matching `(cell, edge)`, the tuple `(proc,
334    /// term_index, repeat_total, iff)` — `term_index` and `repeat_total` are
335    /// `0`/`None` respectively for a `Static` entry (which has no term-index
336    /// concept and is never `Repeat`-sourced); a `Dynamic` entry reports its
337    /// own installed `term_index`/`repeat_total` (Task 3, ledger SC-052 —
338    /// see [`SensitivityEntry::Dynamic`]'s own doc comment). Callers that
339    /// only need the `ProcessId` (every caller predating Task 3) destructure
340    /// and use only the first element.
341    ///
342    /// **Task 5 (ledger SC-068) addition:** `iff` is the fourth element —
343    /// always `None` for a `Static` entry (that variant carries no `iff`
344    /// field: `always_comb`/`always_latch`'s implicit sensitivity has no LRM
345    /// `iff` clause) and a `Dynamic` entry's own installed
346    /// `iff: Option<PredicateFn>` otherwise. This method deliberately does
347    /// NOT evaluate `iff` — it has no `SimHandle`/arena access to call
348    /// through — so a match here means only "this entry's edge/cell
349    /// condition fired," not "the process should wake." The one production
350    /// caller with the access needed to actually invoke a `Some(iff)`
351    /// predicate before deciding to enqueue is `sched::control`'s
352    /// `EngineNotifySink::notify_change`.
353    pub fn matches(
354        &self,
355        cell: StateCellId,
356        edge: EdgeKind,
357    ) -> impl Iterator<Item = (ProcessId, usize, Option<u64>, Option<PredicateFn>)> + '_ {
358        self.matches_delta(cell, edge, None)
359    }
360
361    /// The processes whose wait list holds `cell` now, first-registered
362    /// first, each once: the `Dynamic` rows of a suspended `@`/`wait` and the
363    /// `Static` rows of a procedure's implicit sensitivity (LRM 1800-2023
364    /// 37.27 detail 1, "all waiting processes, static or dynamic"). Read-only.
365    pub fn waiting_on(&self, cell: StateCellId) -> Vec<ProcessId> {
366        let mut out: Vec<ProcessId> = Vec::new();
367        for e in self.table.get(&cell).into_iter().flatten() {
368            let (SensitivityEntry::Static { proc, .. } | SensitivityEntry::Dynamic { proc, .. }) =
369                *e;
370            if !out.contains(&proc) {
371                out.push(proc);
372            }
373        }
374        out
375    }
376
377    /// Whether any entry on `cell` waits on a bit/part select of it, i.e.
378    /// whether a committed update needs to carry a [`ChangeDelta`].
379    pub fn has_select(&self, cell: StateCellId) -> bool {
380        self.table.get(&cell).is_some_and(|row| {
381            row.iter().any(|e| {
382                matches!(
383                    e,
384                    SensitivityEntry::Dynamic { sel: Some(_), .. }
385                        | SensitivityEntry::Static { sel: Some(_), .. }
386                )
387            })
388        })
389    }
390
391    /// [`Self::matches`] with the update's old/new words: a select entry
392    /// (`EventTerm::Select`) matches only if the update changed its bits, and
393    /// takes its edge from bit `lsb` of the transition -- not from the cell's
394    /// own bit 0, which `edge` classifies. With no `delta` a select entry
395    /// falls back to the whole-cell rule (a superset: it can wake for a change
396    /// of a bit it does not select, never miss one).
397    pub fn matches_delta<'a>(
398        &'a self,
399        cell: StateCellId,
400        edge: EdgeKind,
401        delta: Option<&'a ChangeDelta>,
402    ) -> impl Iterator<Item = (ProcessId, usize, Option<u64>, Option<PredicateFn>)> + 'a {
403        self.table
404            .get(&cell)
405            .into_iter()
406            .flatten()
407            .filter_map(move |entry| {
408                let (entry_proc, entry_edge, term_index, repeat_total, iff, sel) = match entry {
409                    SensitivityEntry::Static {
410                        proc,
411                        term_index,
412                        edge,
413                        sel,
414                    } => (
415                        *proc,
416                        edge.unwrap_or(EdgeKind::None),
417                        *term_index,
418                        None,
419                        None,
420                        *sel,
421                    ),
422                    SensitivityEntry::Dynamic {
423                        proc,
424                        edge,
425                        term_index,
426                        repeat_total,
427                        iff,
428                        sel,
429                    } => (*proc, *edge, *term_index, *repeat_total, *iff, *sel),
430                };
431                // The edge the entry is judged against: a select entry with a
432                // delta looks at its own bit, everything else at the cell's.
433                let mut edge = edge;
434                if let (Some((lsb, width)), Some(d)) = (sel, delta) {
435                    if !d.range_changed(lsb, width) {
436                        return None;
437                    }
438                    edge = d.bit(lsb).map_or(EdgeKind::None, |((oa, ob), (na, nb))| {
439                        edge_between(Bit4::from_aval_bval(oa, ob), Bit4::from_aval_bval(na, nb))
440                    });
441                }
442                let is_match = match (entry_edge, edge) {
443                    (EdgeKind::None, _) => true,
444                    (EdgeKind::BothEdges, e) => e == EdgeKind::Posedge || e == EdgeKind::Negedge,
445                    (qualified, e) => e == qualified || e == EdgeKind::BothEdges,
446                };
447                is_match.then_some((entry_proc, term_index, repeat_total, iff))
448            })
449    }
450
451    /// **NEW (Task 18, `wA-sched` plan) — the `#[cfg(test)]`-only production
452    /// backing for `Engine::test_sensitivity_entry_count`** (SC-045's "exactly
453    /// once, at registration" proof; see `sched::control`'s deviations note).
454    /// Total entry count across every cell's row, `Static` and `Dynamic`
455    /// combined. `sched::control` (Task 18) is the same `sched` track that
456    /// owns this file, so this is an in-track, additive extension, not a
457    /// foreign-contract change; the method itself is not test-gated (a plain
458    /// `pub fn`, cheap and side-effect-free) so no `#[cfg(test)]` plumbing is
459    /// needed here, only at the `Engine` accessor's own call site.
460    pub fn entry_count(&self) -> usize {
461        self.table.values().map(|v| v.len()).sum()
462    }
463}
464
465/// A thin [`ValueChangeSink`] adapter over a [`SensitivityTable`]: routes
466/// `notify_change` straight through `SensitivityTable::matches` into a
467/// caller-owned `Vec<ProcessId>` (SC-071 — "a mock STATE implementation
468/// calling `notify_change` is correctly routed to sensitivity lookup").
469/// Task 7/8's `commit_nba`/`commit_blocking_write` take `&mut dyn
470/// ValueChangeSink`, so wrapping a real `SensitivityTable` in this adapter is
471/// how those two production call sites reach real sensitivity matching.
472pub struct SensitivityLookupSink<'a> {
473    table: &'a SensitivityTable,
474    out: &'a mut Vec<ProcessId>,
475}
476
477impl<'a> SensitivityLookupSink<'a> {
478    pub fn new(table: &'a SensitivityTable, out: &'a mut Vec<ProcessId>) -> Self {
479        Self { table, out }
480    }
481}
482
483impl ValueChangeSink for SensitivityLookupSink<'_> {
484    fn notify_change(&mut self, cell: StateCellId, edge: EdgeKind, _at: SimTime, _region: Region) {
485        // This sink's own callers (`notify.rs`'s test module) only ever need
486        // the `ProcessId` half of `matches`'s richer tuple — repeat
487        // counting and `iff` evaluation are `EngineNotifySink`'s concern
488        // (`sched::control`), not this thin adapter's.
489        self.out
490            .extend(self.table.matches(cell, edge).map(|(p, _, _, _)| p));
491    }
492}
493
494#[cfg(test)]
495mod tests {
496    use super::*;
497    use crate::state::FourStateValue;
498
499    const PROC_MAIN: ProcessId = 1;
500
501    // --- install_static / matches (SC-045, SC-046) ---
502
503    #[test]
504    fn always_comb_static_sensitivity_registers_one_entry_per_read_set_member() {
505        let a = StateCellId(1);
506        let b = StateCellId(2);
507        let c = StateCellId(3);
508        let sensitivity = StaticSensitivity {
509            edges: vec![(a, None), (b, None), (c, None)],
510        };
511
512        let mut table = SensitivityTable::new();
513        table.install_static(&sensitivity, PROC_MAIN);
514
515        for cell in [a, b, c] {
516            let hits: Vec<ProcessId> = table
517                .matches(cell, EdgeKind::Posedge)
518                .map(|(p, _, _, _)| p)
519                .collect();
520            assert_eq!(
521                hits,
522                vec![PROC_MAIN],
523                "cell {cell:?} must wake the comb process on any change"
524            );
525        }
526
527        let total: usize = table.table.values().map(|v| v.len()).sum();
528        assert_eq!(total, 3, "exactly one entry per read-set member, no more");
529    }
530
531    #[test]
532    fn always_ff_static_sensitivity_registers_one_edge_qualified_entry() {
533        let clk = StateCellId(10);
534        let sensitivity = StaticSensitivity {
535            edges: vec![(clk, Some(EdgeKind::Posedge))],
536        };
537
538        let mut table = SensitivityTable::new();
539        table.install_static(&sensitivity, PROC_MAIN);
540
541        let posedge_hits: Vec<ProcessId> = table
542            .matches(clk, EdgeKind::Posedge)
543            .map(|(p, _, _, _)| p)
544            .collect();
545        assert_eq!(posedge_hits, vec![PROC_MAIN]);
546
547        let negedge_hits: Vec<ProcessId> = table
548            .matches(clk, EdgeKind::Negedge)
549            .map(|(p, _, _, _)| p)
550            .collect();
551        assert!(
552            negedge_hits.is_empty(),
553            "an edge-qualified always_ff entry must not fire on the opposite edge"
554        );
555    }
556
557    #[test]
558    fn static_entries_survive_many_other_processes_suspend_resume_cycles() {
559        let watched = StateCellId(20);
560        let sensitivity = StaticSensitivity {
561            edges: vec![(watched, None)],
562        };
563
564        let mut table = SensitivityTable::new();
565        table.install_static(&sensitivity, PROC_MAIN);
566
567        // Five unrelated dynamic install/remove churn cycles for other
568        // processes, none of which touch `watched`'s static entry.
569        for other_proc in 100u32..105u32 {
570            let other_cell = StateCellId(1000 + u64::from(other_proc));
571            let wait = EventWaitSet {
572                terms: vec![EventTerm::Edge {
573                    cell: other_cell,
574                    edge: EdgeKind::Posedge,
575                    iff: None,
576                }],
577                ..Default::default()
578            };
579            table.install_dynamic(&wait, other_proc);
580            table.remove_dynamic(other_proc);
581        }
582
583        let hits: Vec<ProcessId> = table
584            .matches(watched, EdgeKind::Negedge)
585            .map(|(p, _, _, _)| p)
586            .collect();
587        assert_eq!(
588            hits,
589            vec![PROC_MAIN],
590            "the static entry must still match after unrelated dynamic churn"
591        );
592    }
593
594    #[test]
595    fn static_entries_installed_exactly_once_at_registration() {
596        let cell = StateCellId(30);
597        let sensitivity = StaticSensitivity {
598            edges: vec![(cell, None)],
599        };
600
601        let mut table = SensitivityTable::new();
602        table.install_static(&sensitivity, PROC_MAIN);
603
604        let total: usize = table.table.values().map(|v| v.len()).sum();
605        assert_eq!(
606            total, 1,
607            "install_static called once must produce exactly one entry"
608        );
609    }
610
611    // --- install_dynamic / remove_dynamic (feeds SC-055/SC-056, Task 10) ---
612
613    #[test]
614    fn dynamic_entry_removed_on_resume_is_gone_from_matches() {
615        let cell = StateCellId(40);
616        let wait = EventWaitSet {
617            terms: vec![EventTerm::Edge {
618                cell,
619                edge: EdgeKind::Posedge,
620                iff: None,
621            }],
622            ..Default::default()
623        };
624
625        let mut table = SensitivityTable::new();
626        table.install_dynamic(&wait, PROC_MAIN);
627        assert_eq!(
628            table
629                .matches(cell, EdgeKind::Posedge)
630                .map(|(p, _, _, _)| p)
631                .collect::<Vec<_>>(),
632            vec![PROC_MAIN],
633            "dynamic entry must be visible to matches before resume"
634        );
635
636        table.remove_dynamic(PROC_MAIN);
637        assert!(
638            table.matches(cell, EdgeKind::Posedge).next().is_none(),
639            "dynamic entry must be gone from matches after remove_dynamic"
640        );
641    }
642
643    // --- ValueChangeSink routing (SC-071) ---
644
645    #[test]
646    fn notify_change_routes_through_sensitivity_lookup() {
647        let cell = StateCellId(50);
648        let sensitivity = StaticSensitivity {
649            edges: vec![(cell, None)],
650        };
651
652        let mut table = SensitivityTable::new();
653        table.install_static(&sensitivity, PROC_MAIN);
654
655        let mut woken: Vec<ProcessId> = Vec::new();
656        {
657            let mut sink = SensitivityLookupSink::new(&table, &mut woken);
658            sink.notify_change(
659                cell,
660                EdgeKind::Posedge,
661                SimTime {
662                    sim_units: 0,
663                    delta: 0,
664                },
665                Region::Nba,
666            );
667        }
668
669        assert_eq!(
670            woken,
671            vec![PROC_MAIN],
672            "notify_change through SensitivityLookupSink must be routed to matches"
673        );
674    }
675
676    #[test]
677    fn implicit_any_dynamic_term_matches_every_listed_cell() {
678        let a = StateCellId(60);
679        let b = StateCellId(61);
680        let wait = EventWaitSet {
681            terms: vec![EventTerm::ImplicitAny(vec![a, b])],
682            ..Default::default()
683        };
684
685        let mut table = SensitivityTable::new();
686        table.install_dynamic(&wait, PROC_MAIN);
687
688        for cell in [a, b] {
689            assert_eq!(
690                table
691                    .matches(cell, EdgeKind::Negedge)
692                    .map(|(p, _, _, _)| p)
693                    .collect::<Vec<_>>(),
694                vec![PROC_MAIN],
695                "ImplicitAny must register an any-change entry for every listed cell"
696            );
697        }
698    }
699
700    #[test]
701    fn select_term_matches_only_when_its_own_bits_change() {
702        // LRM 9.4.2: `@(posedge v[1])` and `@(v[5:4])` look at the selected
703        // bits of the operand, not at the whole signal.
704        let v = StateCellId(70);
705        let wait = EventWaitSet {
706            terms: vec![
707                EventTerm::Select {
708                    cell: v,
709                    edge: EdgeKind::Posedge,
710                    lsb: 1,
711                    width: 1,
712                },
713                EventTerm::Select {
714                    cell: v,
715                    edge: EdgeKind::None,
716                    lsb: 4,
717                    width: 2,
718                },
719            ],
720            ..Default::default()
721        };
722        let mut table = SensitivityTable::new();
723        table.install_dynamic(&wait, PROC_MAIN);
724        assert!(table.has_select(v));
725        let narrow = |val: u64| FourStateValue::Narrow(u128::from(val));
726        let terms = |old: u64, new: u64| -> Vec<usize> {
727            let d = ChangeDelta::between(&narrow(old), &narrow(new));
728            // The cell's own bit 0 is deliberately a bystander.
729            let edge = if (old ^ new) & 1 != 0 {
730                EdgeKind::Posedge
731            } else {
732                EdgeKind::None
733            };
734            table
735                .matches_delta(v, edge, Some(&d))
736                .map(|(_, term, _, _)| term)
737                .collect()
738        };
739        assert_eq!(terms(0b0000, 0b0010), vec![0], "v[1] rose");
740        assert_eq!(terms(0b0010, 0b0000), Vec::<usize>::new(), "v[1] fell");
741        assert_eq!(
742            terms(0b0000, 0b0001),
743            Vec::<usize>::new(),
744            "only v[0] moved"
745        );
746        assert_eq!(terms(0b00_0000, 0b01_0000), vec![1], "v[4] moved");
747        assert_eq!(terms(0b00_0000, 0b10_0000), vec![1], "v[5] moved");
748        assert_eq!(
749            terms(0b01_0000, 0b01_0010),
750            vec![0],
751            "v[1] rose, v[5:4] kept"
752        );
753    }
754
755    #[test]
756    fn named_event_trigger_term_installs_an_any_change_dynamic_entry() {
757        // scheduler.md §8's open design question: a named event's "write" is
758        // matched the same way an any-change disjunct is (any non-`None`
759        // classified change on its reserved StateCellId wakes the waiter).
760        // Mirrors `implicit_any_dynamic_term_matches_every_listed_cell`'s
761        // shape — this branch previously had zero test coverage anywhere in
762        // this file despite being an explicitly-flagged, non-trivial
763        // interpretation.
764        let ev = StateCellId(65);
765        let wait = EventWaitSet {
766            terms: vec![EventTerm::NamedEventTrigger(ev)],
767            ..Default::default()
768        };
769
770        let mut table = SensitivityTable::new();
771        table.install_dynamic(&wait, PROC_MAIN);
772
773        assert_eq!(
774            table
775                .matches(ev, EdgeKind::Posedge)
776                .map(|(p, _, _, _)| p)
777                .collect::<Vec<_>>(),
778            vec![PROC_MAIN],
779            "NamedEventTrigger must register an any-change entry that wakes on a real committed transition"
780        );
781
782        let total: usize = table.table.values().map(|v| v.len()).sum();
783        assert_eq!(
784            total, 1,
785            "exactly one entry for the one NamedEventTrigger term"
786        );
787    }
788
789    #[test]
790    fn repeat_term_installs_its_inner_edge_at_the_outer_term_index() {
791        // The Repeat term sits at a non-zero outer index (1), behind an
792        // unrelated leading term at index 0, so a threading bug that used
793        // the wrong index (e.g. always 0, or the inner term's own
794        // nonexistent index) is distinguishable from the correct behavior —
795        // `matches()` alone can't see `term_index` (it only yields
796        // `ProcessId`), so this reads the installed entry's `term_index`
797        // directly out of the table's private `table` field.
798        let other = StateCellId(71);
799        let clk = StateCellId(70);
800        let wait = EventWaitSet {
801            terms: vec![
802                EventTerm::Edge {
803                    cell: other,
804                    edge: EdgeKind::Posedge,
805                    iff: None,
806                },
807                EventTerm::Repeat {
808                    count: 3,
809                    inner: Box::new(EventTerm::Edge {
810                        cell: clk,
811                        edge: EdgeKind::Posedge,
812                        iff: None,
813                    }),
814                },
815            ],
816            ..Default::default()
817        };
818
819        let mut table = SensitivityTable::new();
820        table.install_dynamic(&wait, PROC_MAIN);
821
822        assert_eq!(
823            table
824                .matches(clk, EdgeKind::Posedge)
825                .map(|(p, _, _, _)| p)
826                .collect::<Vec<_>>(),
827            vec![PROC_MAIN]
828        );
829
830        let clk_entries = table
831            .table
832            .get(&clk)
833            .expect("clk must have an installed entry");
834        assert_eq!(
835            clk_entries.len(),
836            1,
837            "Repeat must install exactly its inner term's entries, not duplicate them"
838        );
839        match clk_entries[0] {
840            SensitivityEntry::Dynamic {
841                term_index,
842                repeat_total,
843                ..
844            } => {
845                assert_eq!(
846                    term_index, 1,
847                    "Repeat must thread the OUTER term's index (1), not the inner term's own (nonexistent) index or a stale 0"
848                );
849                assert_eq!(
850                    repeat_total,
851                    Some(3),
852                    "Task 3: the inner term's installed row must carry the Repeat's own \
853                     declared count (3), for EngineNotifySink to decrement at match time"
854                );
855            }
856            SensitivityEntry::Static { .. } => {
857                panic!("install_dynamic must never produce a Static entry")
858            }
859        }
860
861        // The leading, non-Repeat Edge term at index 0 must carry no
862        // repeat_total at all -- proves install_term's default threading
863        // (`None` for every ordinary term) isn't accidentally contaminated
864        // by the Repeat sibling's count.
865        let other_entries = table
866            .table
867            .get(&other)
868            .expect("other must have an installed entry");
869        match other_entries[0] {
870            SensitivityEntry::Dynamic { repeat_total, .. } => {
871                assert_eq!(
872                    repeat_total, None,
873                    "an ordinary (non-Repeat) Edge term must install repeat_total: None"
874                );
875            }
876            SensitivityEntry::Static { .. } => {
877                panic!("install_dynamic must never produce a Static entry")
878            }
879        }
880
881        let total: usize = table.table.values().map(|v| v.len()).sum();
882        assert_eq!(
883            total, 2,
884            "one entry for the leading Edge term plus one for the Repeat's inner Edge term"
885        );
886    }
887
888    #[test]
889    fn both_edges_incoming_change_matches_either_edge_qualified_waiter() {
890        let clk = StateCellId(80);
891        let mut table = SensitivityTable::new();
892        table.install_static(
893            &StaticSensitivity {
894                edges: vec![(clk, Some(EdgeKind::Posedge))],
895            },
896            10,
897        );
898        table.install_static(
899            &StaticSensitivity {
900                edges: vec![(clk, Some(EdgeKind::Negedge))],
901            },
902            20,
903        );
904
905        let mut hits: Vec<ProcessId> = table
906            .matches(clk, EdgeKind::BothEdges)
907            .map(|(p, _, _, _)| p)
908            .collect();
909        hits.sort_unstable();
910        assert_eq!(
911            hits,
912            vec![10, 20],
913            "an incoming BothEdges change must match both a Posedge- and a Negedge-qualified waiter"
914        );
915    }
916
917    /// The actually-reachable direction of the `edge` keyword case
918    /// (`@(edge sig)`): the *entry* itself carries `EdgeKind::BothEdges`
919    /// (both `Static::edge: Some(BothEdges)` and
920    /// `Dynamic`/`EventTerm::Edge { edge: BothEdges, .. }` can produce this),
921    /// while `infer_edge` (sched/notify.rs) only ever hands `matches` a real
922    /// `Posedge`/`Negedge`/`None` classification — never `BothEdges` — as the
923    /// incoming committed-transition `edge`. A `BothEdges`-qualified entry
924    /// must therefore match both an incoming `Posedge` and an incoming
925    /// `Negedge`, and must not match a vacuous `None`.
926    #[test]
927    fn both_edges_qualified_entry_matches_incoming_posedge_and_negedge() {
928        let clk = StateCellId(90);
929
930        // Static::edge carrying Some(BothEdges).
931        let mut static_table = SensitivityTable::new();
932        static_table.install_static(
933            &StaticSensitivity {
934                edges: vec![(clk, Some(EdgeKind::BothEdges))],
935            },
936            PROC_MAIN,
937        );
938        assert_eq!(
939            static_table
940                .matches(clk, EdgeKind::Posedge)
941                .map(|(p, _, _, _)| p)
942                .collect::<Vec<_>>(),
943            vec![PROC_MAIN],
944            "a Static BothEdges-qualified entry must match a real incoming Posedge"
945        );
946        assert_eq!(
947            static_table
948                .matches(clk, EdgeKind::Negedge)
949                .map(|(p, _, _, _)| p)
950                .collect::<Vec<_>>(),
951            vec![PROC_MAIN],
952            "a Static BothEdges-qualified entry must match a real incoming Negedge"
953        );
954        assert!(
955            static_table.matches(clk, EdgeKind::None).next().is_none(),
956            "a Static BothEdges-qualified entry must not match a vacuous None classification"
957        );
958
959        // Dynamic EventTerm::Edge carrying edge: BothEdges (the literal
960        // `@(edge clk)` waitset shape).
961        let mut dynamic_table = SensitivityTable::new();
962        let wait = EventWaitSet {
963            terms: vec![EventTerm::Edge {
964                cell: clk,
965                edge: EdgeKind::BothEdges,
966                iff: None,
967            }],
968            ..Default::default()
969        };
970        dynamic_table.install_dynamic(&wait, PROC_MAIN);
971        assert_eq!(
972            dynamic_table
973                .matches(clk, EdgeKind::Posedge)
974                .map(|(p, _, _, _)| p)
975                .collect::<Vec<_>>(),
976            vec![PROC_MAIN],
977            "a Dynamic BothEdges-qualified entry must match a real incoming Posedge"
978        );
979        assert_eq!(
980            dynamic_table
981                .matches(clk, EdgeKind::Negedge)
982                .map(|(p, _, _, _)| p)
983                .collect::<Vec<_>>(),
984            vec![PROC_MAIN],
985            "a Dynamic BothEdges-qualified entry must match a real incoming Negedge"
986        );
987        assert!(
988            dynamic_table.matches(clk, EdgeKind::None).next().is_none(),
989            "a Dynamic BothEdges-qualified entry must not match a vacuous None classification"
990        );
991    }
992
993    // --- Task 5 (B-sched, ledger SC-065, SC-066, SC-047, SC-048, SC-068):
994    // EventTerm/EventWaitSet shape + static/dynamic sensitivity closure ---
995
996    /// SC-065's literal acceptance: `EventWaitSet`'s only real semantics is
997    /// `WaitKind::Any` -- the first satisfied term wakes the process, with
998    /// no requirement that any *other* term in the set also match.
999    /// `install_dynamic` installs every term of a 3-term set as an
1000    /// independent OR-alternative row, so matching on any ONE of the three
1001    /// cells alone -- with the other two never having changed at all --
1002    /// must already yield the process. Fails if a future refactor changes
1003    /// `install_dynamic`/`matches` to require joint (AND) satisfaction of
1004    /// every term before a process is reported as matched.
1005    #[test]
1006    fn sc065_event_wait_set_wakes_on_the_first_of_three_or_terms_to_match() {
1007        let cell_1 = StateCellId(200);
1008        let cell_2 = StateCellId(201);
1009        let cell_3 = StateCellId(202);
1010        let wait = EventWaitSet {
1011            terms: vec![
1012                EventTerm::Edge {
1013                    cell: cell_1,
1014                    edge: EdgeKind::Posedge,
1015                    iff: None,
1016                },
1017                EventTerm::Edge {
1018                    cell: cell_2,
1019                    edge: EdgeKind::Posedge,
1020                    iff: None,
1021                },
1022                EventTerm::Edge {
1023                    cell: cell_3,
1024                    edge: EdgeKind::Posedge,
1025                    iff: None,
1026                },
1027            ],
1028            ..Default::default()
1029        };
1030
1031        let mut table = SensitivityTable::new();
1032        table.install_dynamic(&wait, PROC_MAIN);
1033
1034        // Only cell_2 changes -- cell_1/cell_3 are never touched by this
1035        // test at all. A wrongly "joint" implementation has no way to
1036        // report a match here (it would need evidence all three fired).
1037        assert_eq!(
1038            table
1039                .matches(cell_2, EdgeKind::Posedge)
1040                .map(|(p, _, _, _)| p)
1041                .collect::<Vec<_>>(),
1042            vec![PROC_MAIN],
1043            "the first of three OR terms to match alone must wake the process"
1044        );
1045
1046        // Independently, cell_1 alone (a *different* single term) must also
1047        // wake it on its own -- proving no term is privileged/required.
1048        assert_eq!(
1049            table
1050                .matches(cell_1, EdgeKind::Posedge)
1051                .map(|(p, _, _, _)| p)
1052                .collect::<Vec<_>>(),
1053            vec![PROC_MAIN],
1054            "any single OR term matching alone must wake the process, not just the last one"
1055        );
1056    }
1057
1058    /// SC-066's literal acceptance: `EventTerm` has exactly 5 variants (the
1059    /// fifth, `Select`, is the bit/part-select wait of LRM 9.4.2). A
1060    /// `match` with no wildcard arm over one instance of each is the
1061    /// compile-time proof -- this fails to compile (not merely fails at
1062    /// runtime) the moment a 6th variant is added without updating this
1063    /// test, or if any of the 5 named ones is ever removed/renamed.
1064    #[test]
1065    fn sc066_event_term_has_exactly_five_variants_each_constructible() {
1066        let cell = StateCellId(210);
1067        let terms = [
1068            EventTerm::Edge {
1069                cell,
1070                edge: EdgeKind::Posedge,
1071                iff: None,
1072            },
1073            EventTerm::ImplicitAny(vec![cell]),
1074            EventTerm::Select {
1075                cell,
1076                edge: EdgeKind::None,
1077                lsb: 1,
1078                width: 1,
1079            },
1080            EventTerm::NamedEventTrigger(cell),
1081            EventTerm::Repeat {
1082                count: 1,
1083                inner: Box::new(EventTerm::Edge {
1084                    cell,
1085                    edge: EdgeKind::Posedge,
1086                    iff: None,
1087                }),
1088            },
1089        ];
1090        for term in &terms {
1091            // No wildcard arm: exhaustiveness itself is the SC-066 proof.
1092            // Each arm cross-references the already-passing test that
1093            // exercises that variant's firing/matching behavior elsewhere
1094            // in this module.
1095            match term {
1096                // See `sc065_event_wait_set_wakes_on_the_first_of_three_or_
1097                // terms_to_match` and `dynamic_entry_removed_on_resume_is_
1098                // gone_from_matches` above.
1099                EventTerm::Edge { .. } => {}
1100                // See `implicit_any_dynamic_term_matches_every_listed_cell`.
1101                EventTerm::ImplicitAny(_) => {}
1102                // See `select_term_*` below.
1103                EventTerm::Select { .. } => {}
1104                // See `named_event_trigger_term_installs_an_any_change_
1105                // dynamic_entry`.
1106                EventTerm::NamedEventTrigger(_) => {}
1107                // See `repeat_term_installs_its_inner_edge_at_the_outer_
1108                // term_index`.
1109                EventTerm::Repeat { .. } => {}
1110            }
1111        }
1112        assert_eq!(terms.len(), 5, "exactly 5 EventTerm variants constructed");
1113    }
1114
1115    /// SC-047, distinct from `dynamic_entry_removed_on_resume_is_gone_from_
1116    /// matches` (which only proves removal happens) -- this proves survival
1117    /// *until* removal, and that `remove_dynamic` is scoped strictly per-
1118    /// process: installing and removing an unrelated process B's own
1119    /// dynamic entry must never disturb process A's still-live one. A wrong
1120    /// "clear everything" implementation of `remove_dynamic` would pass the
1121    /// existing removal test but fail this one.
1122    #[test]
1123    fn sc047_dynamic_entry_for_a_proc_survives_until_that_procs_own_resume_removes_it() {
1124        const PROC_A: ProcessId = 300;
1125        const PROC_B: ProcessId = 301;
1126        let cell_a = StateCellId(220);
1127        let cell_b = StateCellId(221);
1128
1129        let mut table = SensitivityTable::new();
1130        table.install_dynamic(
1131            &EventWaitSet {
1132                terms: vec![EventTerm::Edge {
1133                    cell: cell_a,
1134                    edge: EdgeKind::Posedge,
1135                    iff: None,
1136                }],
1137                ..Default::default()
1138            },
1139            PROC_A,
1140        );
1141
1142        // Unrelated process B installs and fully resumes (install then
1143        // remove) its own dynamic wait -- must not touch A's entry at all.
1144        table.install_dynamic(
1145            &EventWaitSet {
1146                terms: vec![EventTerm::Edge {
1147                    cell: cell_b,
1148                    edge: EdgeKind::Posedge,
1149                    iff: None,
1150                }],
1151                ..Default::default()
1152            },
1153            PROC_B,
1154        );
1155        table.remove_dynamic(PROC_B);
1156
1157        assert_eq!(
1158            table
1159                .matches(cell_a, EdgeKind::Posedge)
1160                .map(|(p, _, _, _)| p)
1161                .collect::<Vec<_>>(),
1162            vec![PROC_A],
1163            "process A's dynamic entry must still be live after an unrelated process B's own \
1164             install+remove cycle"
1165        );
1166        assert!(
1167            table.matches(cell_b, EdgeKind::Posedge).next().is_none(),
1168            "process B's own entry must be gone after its own remove_dynamic"
1169        );
1170    }
1171
1172    /// SC-048: a dynamic `EventWaitSet` is built fresh at each suspend point
1173    /// and torn down the instant its owner resumes -- so a SAME process
1174    /// suspending twice in succession on two DIFFERENT-shaped wait sets
1175    /// (e.g. a process whose `@(...)` list changes between loop iterations)
1176    /// must, after the second install, match only the second set's cells.
1177    /// A leaked stale entry from the first install would make the first
1178    /// set's cell wake the process too after the second suspend, which this
1179    /// test catches.
1180    #[test]
1181    fn sc048_dynamic_wait_set_built_fresh_at_each_suspend_reflects_that_calls_own_terms() {
1182        let cell_first = StateCellId(230);
1183        let cell_second = StateCellId(231);
1184
1185        let mut table = SensitivityTable::new();
1186
1187        // First suspend: waits on cell_first.
1188        table.install_dynamic(
1189            &EventWaitSet {
1190                terms: vec![EventTerm::Edge {
1191                    cell: cell_first,
1192                    edge: EdgeKind::Posedge,
1193                    iff: None,
1194                }],
1195                ..Default::default()
1196            },
1197            PROC_MAIN,
1198        );
1199        // Resume (per SC-047/SC-048's own "removed the instant the owning
1200        // process resumes"): the table must be told, exactly as
1201        // `dispatch_ready_set` does in production.
1202        table.remove_dynamic(PROC_MAIN);
1203
1204        // Second suspend, same process, a DIFFERENT-shaped wait set.
1205        table.install_dynamic(
1206            &EventWaitSet {
1207                terms: vec![EventTerm::Edge {
1208                    cell: cell_second,
1209                    edge: EdgeKind::Posedge,
1210                    iff: None,
1211                }],
1212                ..Default::default()
1213            },
1214            PROC_MAIN,
1215        );
1216
1217        assert!(
1218            table
1219                .matches(cell_first, EdgeKind::Posedge)
1220                .next()
1221                .is_none(),
1222            "the first suspend's wait set must leave no residue after the second install"
1223        );
1224        assert_eq!(
1225            table
1226                .matches(cell_second, EdgeKind::Posedge)
1227                .map(|(p, _, _, _)| p)
1228                .collect::<Vec<_>>(),
1229            vec![PROC_MAIN],
1230            "only the second, current wait set's own cell must match"
1231        );
1232    }
1233
1234    /// SC-068's own literal acceptance at the sensitivity-table level
1235    /// (`sched::control`'s `engine_never_calls_resume_when_iff_is_false_
1236    /// but_does_on_the_next_true_edge` is this same acceptance proven
1237    /// against the production `Engine` dispatch loop): `matches` surfaces
1238    /// an installed `iff` predicate as the 4th tuple element but does not
1239    /// itself evaluate it (documented on `matches`'s own doc comment); a
1240    /// caller that DOES evaluate it before deciding "the process should
1241    /// wake" -- inlined here as `matches_with_iff`, mirroring
1242    /// `EngineNotifySink::notify_change`'s real filter -- must report no
1243    /// match at all while the predicate reads false, and a match once it
1244    /// reads true. `PredicateFn` is settled (`docs/CONTRACTS.md` D8) as a
1245    /// bare `extern "C" fn(SimHandle) -> bool` with no `StateCellId`
1246    /// parameter of its own (a real compiled guard reads whatever cell it
1247    /// needs through the handle) -- this mock instead reads a thread-local
1248    /// flag the test flips directly.
1249    #[test]
1250    fn sc068_iff_false_produces_no_match_iff_true_does() {
1251        use vj_abi::SimHandle;
1252
1253        thread_local! {
1254            static EN: std::cell::Cell<bool> = const { std::cell::Cell::new(false) };
1255        }
1256        extern "C" fn iff_reads_en(_state: SimHandle) -> bool {
1257            EN.with(|c| c.get())
1258        }
1259
1260        fn matches_with_iff(
1261            table: &SensitivityTable,
1262            cell: StateCellId,
1263            edge: EdgeKind,
1264            handle: SimHandle,
1265        ) -> Vec<ProcessId> {
1266            table
1267                .matches(cell, edge)
1268                .filter(|(_, _, _, iff)| match iff {
1269                    Some(pred) => (pred.0)(handle),
1270                    None => true,
1271                })
1272                .map(|(p, _, _, _)| p)
1273                .collect()
1274        }
1275
1276        let clk = StateCellId(240);
1277        let wait = EventWaitSet {
1278            terms: vec![EventTerm::Edge {
1279                cell: clk,
1280                edge: EdgeKind::Posedge,
1281                iff: Some(PredicateFn(iff_reads_en)),
1282            }],
1283            ..Default::default()
1284        };
1285        let mut table = SensitivityTable::new();
1286        table.install_dynamic(&wait, PROC_MAIN);
1287        let handle = SimHandle(std::ptr::null_mut());
1288
1289        EN.with(|c| c.set(false));
1290        assert!(
1291            matches_with_iff(&table, clk, EdgeKind::Posedge, handle).is_empty(),
1292            "iff=false must produce no match at all, not merely a match resume() ignores"
1293        );
1294
1295        EN.with(|c| c.set(true));
1296        assert_eq!(
1297            matches_with_iff(&table, clk, EdgeKind::Posedge, handle),
1298            vec![PROC_MAIN],
1299            "iff=true must produce the match"
1300        );
1301    }
1302}