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}