Skip to main content

vj_sim/analysis/
inferred_clock.rs

1//! Task 6 (sva T6): procedural clock inference, LRM 1800-2023 16.14.6
2//! conditions (a)/(b)/(c) -- "A clock shall be inferred for the context of
3//! an always or initial procedure that satisfies the following
4//! requirements: (a) There is no blocking timing control in the
5//! procedure. (b) There is exactly one event control in the procedure.
6//! (c) One and only one event expression within the event control of the
7//! procedure satisfies both [... two conditions ...]."
8//!
9//! **Deviation from the plan's §1.6 claim ("new static-analysis work with
10//! no slang accessor -- `AnalyzedProcedure` doesn't expose this"), recorded
11//! here as binding for this module.** `sv_lang::AnalyzedProcedure::
12//! inferred_clock()` (`slang::analysis::AnalyzedProcedure::getInferredClock`,
13//! backed by `DFAResults::inferClock` in the vendored C++,
14//! `vendor/source/analysis/DFAResults.cpp`) turns out to implement
15//! 16.14.6(a)-(c) **verbatim** -- its own source comments literally quote
16//! "16.14.6: There must be no blocking timing controls and exactly one
17//! event control" and then 16.14.6's two numbered sub-conditions word for
18//! word. This was not assumed from the doc comment: this task compiled
19//! all four of 16.14.6's own worked examples (the LRM's `r1`/`r2`/`r3`/`r4`
20//! fragments, reproduced verbatim as this module's probe-corpus-style unit
21//! tests below) through a live `Design`/`Analysis` and confirmed
22//! `inferred_clock()` reproduces the LRM's own stated answer in all four
23//! cases, including the one case (`r2`) where the LRM's answer is the
24//! *qualified* event `posedge clock iff reset == 0`, not the simpler
25//! `posedge reset` alternative, and the two cases (`r3`, `r4`) where the
26//! LRM states no clock can be inferred at all.
27//!
28//! (`infer_structural_clock` below is the one documented exception: slang
29//! analyzes no scope for a procedural checker instance's body, so it has
30//! nothing to ask.)
31//!
32//! Given that, this module is a thin, typed wrapper around the existing
33//! accessor -- never a second, independently-reasoned reimplementation of
34//! the dataflow walk the plan's prose describes -- for the same reason
35//! §1.1/§1.6 already give for reusing `AnalyzedAssertion::clock()` instead
36//! of reimplementing 16.13.3's clock-flow algorithm: slang has already
37//! done this analysis correctly, and a hand-rolled second copy could only
38//! diverge from it, never improve on it.
39//!
40//! `inferred_clock()` itself only runs "if the procedure contains at least
41//! one concurrent assertion" (its own doc comment) -- i.e. it is computed
42//! lazily, exactly when 16.14.6 is actually relevant (a procedure with no
43//! assertion needing an inferred clock has nothing for this function to
44//! answer), so that gate is not a scoping gap for this task's purpose.
45//!
46//! **Correction (sva T6 review r1): the wrapped accessor is NOT a pure
47//! (a)/(b)/(c) signal, and this module cannot make it one.** The paragraph
48//! above establishes that `DFAResults::inferClock` -- called first --
49//! implements (a)-(c) verbatim. But `AnalyzedProcedure`'s constructor
50//! (`vendor/source/analysis/AnalyzedProcedure.cpp`, ~lines 54-66) does not
51//! stop there: when `inferClock` returns null it unconditionally falls
52//! through to `scope->getCompilation().getDefaultClocking(*scope)` and
53//! assigns *that* to the same `inferredClock` field `getInferredClock()`
54//! later returns. That is LRM 16.15's default-clocking fallback ("If no
55//! clock can be inferred from the procedural context, then the clocks
56//! shall be inferred from the default clocking"), folded into the exact
57//! same return value as the (a)-(c) result, with nothing in the C++ or the
58//! Rust `inferred_clock()` surface that says which path produced it.
59//!
60//! This was verified live, not just read off the C++: an LRM `r3`-shaped
61//! procedure (16.14.6(a)-(c) fails -- the qualifying edge expression has no
62//! edge identifier) placed in a module that also declares `default
63//! clocking cb @(posedge other_sig); endclocking` makes
64//! `infer_procedural_clock` return `Ok(Some(_))` referencing `other_sig`,
65//! not `Ok(None)` -- see
66//! `tests::default_clocking_fallback_is_indistinguishable_from_abc` below.
67//!
68//! sv-lang 0.1.9 exposes no lower-level accessor that would let this module
69//! split the two apart: there is no bound
70//! `Compilation::getDefaultClocking`, and `ClockingBlockSymbol::isDefault`
71//! (present on the C++ struct) has no FFI accessor either, so this module
72//! cannot independently ask "does a default clocking block apply to this
73//! scope" and subtract that case out. Reimplementing 16.14.6(a)-(c) by hand
74//! to get a value `inferred_clock()` doesn't provide would be exactly the
75//! second, independently-reasoned reimplementation this module's whole
76//! design (the paragraph above) exists to avoid -- and sv-lang itself is a
77//! pinned dependency this task does not modify.
78//!
79//! The documented, honest contract is therefore: `infer_procedural_clock`
80//! returns the procedure's *effective* inferred clock -- 16.14.6(a)-(c)
81//! when that succeeds, otherwise silently 16.15's default-clocking
82//! fallback when one applies, otherwise `None` -- and a caller cannot tell
83//! which of the two non-`None` cases produced a `Some` from the return
84//! value alone. Any future caller that specifically needs the pure
85//! (a)-(c) signal (e.g. a diagnostic that must say "no clock could be
86//! inferred from the procedural context" per 16.14.6, distinct from "no
87//! default clocking either") cannot get it from this function and must
88//! say so explicitly rather than assume otherwise.
89
90use std::collections::HashSet;
91
92use sv_lang::kinds::{StatementKind, SymbolKind, TimingControlKind};
93use sv_lang::{AnalyzedProcedure, EdgeKind, SemNode, Symbol, TimingControl};
94
95use super::AnalysisError;
96use crate::symid::{SymbolId, SymbolUid, is_value_name};
97
98/// LRM 16.14.6 (a)/(b)/(c) for a procedure that slang's analysis does not list:
99/// one inside a *procedural* checker instance's body (17.3). slang analyzes such
100/// a body as a side effect of analyzing the enclosing procedure and files no scope
101/// result for it, so [`infer_procedural_clock`] has no `AnalyzedProcedure` to ask
102/// (and an `AnalyzedAssertion::procedure` handle into that scope is not safe to
103/// follow: slang keeps the procedures in a `std::vector` and the assertions point
104/// into it before it has finished growing). This is therefore the one place the
105/// three conditions are decided here rather than by slang, mirroring
106/// `DFAResults::inferClock` for the shapes a checker's procedure can take:
107///
108/// - (a) no blocking timing control: a delay, `wait`, or a timing control on
109///   anything but a statement makes the answer `None` (the last is an error here
110///   instead, since `a = #1 b` is not modelled by this walk);
111/// - (b) exactly one event control (a nonblocking assignment's does not count);
112/// - (c) exactly one `edge expr [iff cond]` event of it none of whose terms is
113///   referenced anywhere else in the procedure other than inside assertion
114///   statements or as a clocking event.
115///
116/// An event control that is not of the `edge expr` form (an event variable, a
117/// clocking block name, `@*`) is an error rather than a guess, since that path
118/// would need the event-variable and clocking-block rules of (c) as well.
119///
120/// Unlike [`infer_procedural_clock`], a `None` means only that the procedure
121/// itself yields no clock; the default clocking (16.15) is for the caller.
122pub fn infer_structural_clock<'d>(
123    block: &Symbol<'d>,
124) -> Result<Option<TimingControl<'d>>, AnalysisError> {
125    let unsupported = |what: &str| {
126        AnalysisError::Unsupported(format!(
127            "clock inference for procedure `{}` of a procedural checker instance: {what}",
128            block.hierarchical_path()
129        ))
130    };
131    let Some(body) = crate::process::cfg::proc_body(block) else {
132        return Ok(None);
133    };
134    let mut referenced: HashSet<SymbolId> = HashSet::new();
135    let mut events: Vec<TimingControl<'d>> = Vec::new();
136    let mut stack: Vec<SemNode<'d>> = vec![body.as_sem_node()];
137    while let Some(n) = stack.pop() {
138        if n.as_timing_control().is_some() {
139            return Err(unsupported(
140                "a timing control that is not on a statement (an intra-assignment delay) is not \
141                 modelled",
142            ));
143        }
144        if let Some(e) = n.as_expression() {
145            if is_value_name(e.kind()) {
146                if let Some(sym) = e.referenced_symbol() {
147                    referenced.insert(sym.uid());
148                }
149                continue;
150            }
151        } else if let Some(stmt) = n.as_statement() {
152            let kind = stmt.kind();
153            if kind == StatementKind::ConcurrentAssertion {
154                // 16.14.6(c): a use inside an assertion statement does not count.
155                continue;
156            }
157            if kind == StatementKind::Wait
158                || kind == StatementKind::WaitFork
159                || kind == StatementKind::WaitOrder
160            {
161                return Ok(None);
162            }
163            if kind == StatementKind::Timed {
164                let tc = stmt
165                    .timing_control()
166                    .ok_or_else(|| unsupported("a timed statement with no timing control"))?;
167                if tc.kind() == TimingControlKind::SignalEvent
168                    || tc.kind() == TimingControlKind::EventList
169                {
170                    events.push(tc);
171                } else {
172                    return Ok(None);
173                }
174                // The timing control is inspected above; only the statement it
175                // guards is walked for further uses.
176                stack.extend(
177                    n.children()
178                        .into_iter()
179                        .filter(|c| c.as_timing_control().is_none()),
180                );
181                continue;
182            }
183        }
184        stack.extend(n.children());
185    }
186    let [control] = events.as_slice() else {
187        return Ok(None);
188    };
189    let candidates: Vec<TimingControl<'d>> = if control.kind() == TimingControlKind::EventList {
190        let mut out = Vec::new();
191        for c in control.children() {
192            let Some(tc) = c
193                .as_timing_control()
194                .filter(|t| t.kind() == TimingControlKind::SignalEvent)
195            else {
196                return Err(unsupported(
197                    "an event list with a member that is not a signal event",
198                ));
199            };
200            out.push(tc);
201        }
202        out
203    } else {
204        vec![*control]
205    };
206    let mut found: Option<TimingControl<'d>> = None;
207    for cand in candidates {
208        let Some(expr) = cand.children().first().and_then(|c| c.as_expression()) else {
209            return Err(unsupported("an event with no signal expression"));
210        };
211        if cand.edge() == EdgeKind::None {
212            let is_event_or_clocking = expr.referenced_symbol().is_some_and(|s| {
213                s.kind() == SymbolKind::ClockingBlock
214                    || expr.expr_type().is_some_and(|t| t.is_event())
215            });
216            if is_event_or_clocking && cand.children().len() == 1 {
217                return Err(unsupported(
218                    "an event variable or clocking block as the clocking event is not modelled",
219                ));
220            }
221            continue;
222        }
223        let mut shared = false;
224        let mut terms: Vec<SemNode<'d>> = vec![expr.as_sem_node()];
225        while let Some(t) = terms.pop() {
226            if let Some(e) = t.as_expression()
227                && is_value_name(e.kind())
228            {
229                shared |= e
230                    .referenced_symbol()
231                    .is_some_and(|s| referenced.contains(&s.uid()));
232                continue;
233            }
234            terms.extend(t.children());
235        }
236        if !shared {
237            if found.is_some() {
238                return Ok(None);
239            }
240            found = Some(cand);
241        }
242    }
243    Ok(found)
244}
245
246/// The procedure's *effective* inferred clock: LRM 16.14.6 (a)/(b)/(c) when
247/// those three conditions are jointly satisfied, otherwise LRM 16.15's
248/// default-clocking fallback when a default clocking block applies to
249/// `proc`'s scope, otherwise `Ok(None)`. See the module doc's "Correction"
250/// section for why these two sources cannot be told apart from this
251/// return value, and why this module cannot change that given sv-lang
252/// 0.1.9's exposed surface.
253///
254/// `Err` only if slang's analysis reports an inferred clock whose
255/// `SemNode` is not itself a `TimingControl` -- an API-shape precondition
256/// this function depends on (every real `inferred_clock()` result observed
257/// in this task's own testing, and by the C++ header's own return type
258/// `const ast::TimingControl*`, is one); surfaced as a loud, typed
259/// `AnalysisError` rather than silently treated as "no clock inferred" if
260/// a future `sv-lang` upgrade ever violates it.
261pub fn infer_procedural_clock<'d>(
262    proc: &AnalyzedProcedure<'d>,
263) -> Result<Option<TimingControl<'d>>, AnalysisError> {
264    match proc.inferred_clock() {
265        None => Ok(None),
266        Some(node) => node.as_timing_control().map(Some).ok_or_else(|| {
267            AnalysisError::Unsupported(format!(
268                "AnalyzedProcedure::inferred_clock() for procedure `{}` returned a SemNode of \
269                 kind `{}` that is not a TimingControl -- sv-lang API shape assumption violated",
270                proc.symbol().hierarchical_path(),
271                node.kind_name(),
272            ))
273        }),
274    }
275}
276
277#[cfg(test)]
278mod tests {
279    use super::*;
280    use sv_lang::kinds::TimingControlKind;
281    use sv_lang::{AnalysisFlags, BinaryOp, Compilation, EdgeKind, Session};
282
283    fn compile(src: &str) -> sv_lang::Design {
284        let session = Session::new();
285        let mut comp = Compilation::new(&session).expect("session");
286        comp.add_source(src).expect("add_source");
287        comp.compile().expect("compiles")
288    }
289
290    /// The design's one top-level module's one analyzed procedure (every
291    /// fixture below has exactly one `always`/`always_ff` block).
292    fn the_one_procedure<'d>(
293        design: &'d sv_lang::Design,
294        analysis: &'d sv_lang::Analysis<'d>,
295    ) -> AnalyzedProcedure<'d> {
296        let body = design
297            .top_instances()
298            .next()
299            .expect("one top instance")
300            .instance_body()
301            .expect("instance body");
302        let mut procs: Vec<_> = analysis.procedures(body).collect();
303        assert_eq!(procs.len(), 1, "fixture has exactly one procedure");
304        procs.remove(0)
305    }
306
307    /// LRM 16.14.6, the `r1` example: `always @(posedge mclk) begin q <=
308    /// d1; r1_p1: assert property (r1); r1_p2: assert property (@(posedge
309    /// scanclk) r1); end` -- "the clocking event @(posedge mclk) is
310    /// inferred as the clocking event of r1_p1" (r1_p2 carries its own
311    /// explicit clock and is irrelevant to the *procedure's* inferred
312    /// clock, which this function reports once per procedure).
313    #[test]
314    fn r1_p1_infers_posedge_mclk() {
315        let design = compile(
316            "module m;\n\
317             logic mclk, scanclk, q, d, d1;\n\
318             property r1; q != d; endproperty\n\
319             always @(posedge mclk) begin\n\
320                q <= d1;\n\
321                r1_p1: assert property (r1);\n\
322                r1_p2: assert property (@(posedge scanclk) r1);\n\
323             end\n\
324             endmodule\n",
325        );
326        let analysis = design.analyze(AnalysisFlags::NONE, 1).expect("analysis");
327        let proc = the_one_procedure(&design, &analysis);
328
329        let tc = infer_procedural_clock(&proc)
330            .expect("no API-shape error")
331            .expect("r1_p1's clock is inferred");
332        assert_eq!(tc.kind(), TimingControlKind::SignalEvent);
333        assert_eq!(tc.edge(), EdgeKind::PosEdge);
334        let children = tc.children();
335        assert_eq!(
336            children.len(),
337            1,
338            "no `iff` qualifier on r1's inferred clock"
339        );
340        let signal = children[0].as_expression().expect("event expression");
341        assert_eq!(
342            signal.referenced_symbol().map(|s| s.name().to_string()),
343            Some("mclk".to_string())
344        );
345    }
346
347    /// LRM 16.14.6, the `r2` example: `always_ff @(posedge clock iff reset
348    /// == 0 or posedge reset) begin cnt <= reset ? 0 : cnt + 1; q <=
349    /// $past(d1); r2_p: assert property (r2); end` -- "the inferred clock
350    /// is posedge clock iff reset == 0. The inferred clock is not posedge
351    /// clock because posedge clock is a proper subexpression" and `reset`
352    /// is disqualified from being its own candidate because it is read
353    /// outside the clocking event (`cnt <= reset ? ...`).
354    #[test]
355    fn r2_infers_posedge_clock_iff_reset_eq_0() {
356        let design = compile(
357            "module m;\n\
358             logic clock, reset, cnt, q, d1;\n\
359             property r2; q != d1; endproperty\n\
360             always_ff @(posedge clock iff reset == 0 or posedge reset) begin\n\
361                cnt <= reset ? 0 : cnt + 1;\n\
362                q <= $past(d1);\n\
363                r2_p: assert property (r2);\n\
364             end\n\
365             endmodule\n",
366        );
367        let analysis = design.analyze(AnalysisFlags::NONE, 1).expect("analysis");
368        let proc = the_one_procedure(&design, &analysis);
369
370        let tc = infer_procedural_clock(&proc)
371            .expect("no API-shape error")
372            .expect("r2's clock is inferred");
373        assert_eq!(tc.kind(), TimingControlKind::SignalEvent);
374        assert_eq!(tc.edge(), EdgeKind::PosEdge);
375        let children = tc.children();
376        assert_eq!(
377            children.len(),
378            2,
379            "r2's inferred clock keeps its `iff reset == 0` qualifier"
380        );
381        let signal = children[0].as_expression().expect("event expression");
382        assert_eq!(
383            signal.referenced_symbol().map(|s| s.name().to_string()),
384            Some("clock".to_string())
385        );
386        let iff = children[1].as_expression().expect("iff condition");
387        assert_eq!(iff.binary_op(), Some(BinaryOp::Equality));
388        let lhs = iff.left().expect("iff lhs");
389        assert_eq!(
390            lhs.referenced_symbol().map(|s| s.name().to_string()),
391            Some("reset".to_string()),
392            "the iff condition is `reset == 0`, not `posedge reset`'s own term"
393        );
394    }
395
396    /// LRM 16.14.6, the `r3` example: `always_ff @(clock iff reset == 0 or
397    /// posedge reset) begin ... end` -- "no clock is inferred for the
398    /// context of the always_ff ... The edge expression posedge reset
399    /// cannot be inferred because reset is referenced within the
400    /// procedure, and the expression clock iff reset == 0 cannot be
401    /// inferred because it does not have an edge identifier."
402    #[test]
403    fn r3_infers_nothing_edge_identifier_missing() {
404        let design = compile(
405            "module m;\n\
406             logic clock, reset, cnt, q, d1;\n\
407             property r3; q != d1; endproperty\n\
408             always_ff @(clock iff reset == 0 or posedge reset) begin\n\
409                cnt <= reset ? 0 : cnt + 1;\n\
410                q <= $past(d1);\n\
411                r3_p: assert property (r3);\n\
412             end\n\
413             endmodule\n",
414        );
415        let analysis = design.analyze(AnalysisFlags::NONE, 1).expect("analysis");
416        let proc = the_one_procedure(&design, &analysis);
417
418        let inferred = infer_procedural_clock(&proc).expect("no API-shape error");
419        assert!(
420            inferred.is_none(),
421            "r3: no clock inferred, per the LRM's own text"
422        );
423    }
424
425    /// Pins down the module doc's "Correction" section: an LRM `r3`-shaped
426    /// procedure (16.14.6(a)-(c) fails because `clock iff reset == 0`'s
427    /// qualifying edge expression has no edge identifier -- same body as
428    /// `r3_infers_nothing_edge_identifier_missing` above) placed in a
429    /// module that *also* declares a default clocking block. Per 16.14.6
430    /// alone this procedure has no inferable clock (exactly as `r3`
431    /// proves above with no default clocking in scope); but because
432    /// `AnalyzedProcedure::inferred_clock()` unconditionally folds in
433    /// 16.15's default-clocking fallback, `infer_procedural_clock` returns
434    /// `Some` here, referencing the default clocking block's own event
435    /// (`other_sig`) rather than anything from the procedure's own event
436    /// control. This is the behavior the module doc documents as the
437    /// honest contract, not a bug this task's function can fix (see the
438    /// module doc for why) -- the test exists so that a future `sv-lang`
439    /// upgrade that changes this merge, or a future refactor of this
440    /// function that silently reintroduces the false "pure (a)-(c)" claim
441    /// this module used to make, breaks loudly here instead of going
442    /// unnoticed.
443    #[test]
444    fn default_clocking_fallback_is_indistinguishable_from_abc() {
445        let design = compile(
446            "module m;\n\
447             logic clock, reset, cnt, q, d1, other_sig;\n\
448             property r3; q != d1; endproperty\n\
449             clocking cb @(posedge other_sig);\n\
450             endclocking\n\
451             default clocking cb;\n\
452             always_ff @(clock iff reset == 0 or posedge reset) begin\n\
453                cnt <= reset ? 0 : cnt + 1;\n\
454                q <= $past(d1);\n\
455                r3_p: assert property (r3);\n\
456             end\n\
457             endmodule\n",
458        );
459        let analysis = design.analyze(AnalysisFlags::NONE, 1).expect("analysis");
460        let proc = the_one_procedure(&design, &analysis);
461
462        let tc = infer_procedural_clock(&proc)
463            .expect("no API-shape error")
464            .expect(
465                "the default-clocking fallback fires even though 16.14.6(a)-(c) fails exactly \
466                 as it does in r3_infers_nothing_edge_identifier_missing",
467            );
468        assert_eq!(tc.kind(), TimingControlKind::SignalEvent);
469        assert_eq!(tc.edge(), EdgeKind::PosEdge);
470        let children = tc.children();
471        assert_eq!(
472            children.len(),
473            1,
474            "the default clocking block's own event carries no `iff` qualifier"
475        );
476        let signal = children[0].as_expression().expect("event expression");
477        assert_eq!(
478            signal.referenced_symbol().map(|s| s.name().to_string()),
479            Some("other_sig".to_string()),
480            "the returned clock is the DEFAULT CLOCKING's event, not derived from the \
481             procedure's own (a)-(c)-failing event control -- confirming the two sources are \
482             folded together and cannot be told apart from this function's return value"
483        );
484    }
485
486    /// A procedure with a sampled value function and NO concurrent assertion
487    /// still gets its clock (LRM 16.9.3's "inferred from the procedural
488    /// context"): `$past`/`$rose` in `always @(posedge clk)`.
489    #[test]
490    fn a_procedure_with_only_a_sampled_call_infers_its_clock() {
491        let design = compile(
492            "module m;\n\
493             logic clk, b, r;\n\
494             always @(posedge clk) r <= $rose(b);\n\
495             endmodule\n",
496        );
497        let analysis = design.analyze(AnalysisFlags::NONE, 1).expect("analysis");
498        let proc = the_one_procedure(&design, &analysis);
499        let tc = infer_procedural_clock(&proc)
500            .expect("no API-shape error")
501            .expect("the always block's clock is inferred");
502        assert_eq!(tc.edge(), EdgeKind::PosEdge);
503    }
504
505    /// LRM 16.14.6, the `r4` example: `always @(posedge mclk) begin #10 q
506    /// <= d1; @(negedge mclk) #10 q1 <= !d1; r4_p: assert property (r4);
507    /// end` -- "no clock is inferred due to multiple event controls and
508    /// delays in the always procedure."
509    #[test]
510    fn r4_infers_nothing_multiple_event_controls_and_delays() {
511        let design = compile(
512            "module m;\n\
513             logic mclk, q, q1, d1;\n\
514             property r4; q != d1; endproperty\n\
515             always @(posedge mclk) begin\n\
516                #10 q <= d1;\n\
517                @(negedge mclk)\n\
518                #10 q1 <= !d1;\n\
519                r4_p: assert property (r4);\n\
520             end\n\
521             endmodule\n",
522        );
523        let analysis = design.analyze(AnalysisFlags::NONE, 1).expect("analysis");
524        let proc = the_one_procedure(&design, &analysis);
525
526        let inferred = infer_procedural_clock(&proc).expect("no API-shape error");
527        assert!(
528            inferred.is_none(),
529            "r4: no clock inferred, per the LRM's own text"
530        );
531    }
532
533    /// `infer_structural_clock` is run on the one procedure of a module here;
534    /// the function itself only looks at the procedure's own statements, so a
535    /// module procedure exercises the same walk as a procedural checker's.
536    fn structural(src: &str) -> Result<Option<(EdgeKind, String)>, AnalysisError> {
537        let design = compile(src);
538        let analysis = design.analyze(AnalysisFlags::NONE, 1).expect("analysis");
539        let proc = the_one_procedure(&design, &analysis);
540        let block = proc.symbol();
541        Ok(infer_structural_clock(&block)?.map(|tc| {
542            let signal = tc.children()[0].as_expression().expect("event expression");
543            let name = signal
544                .referenced_symbol()
545                .map(|s| s.name().to_string())
546                .expect("a named clock");
547            (tc.edge(), name)
548        }))
549    }
550
551    /// 16.14.6, the `r1` shape: one edge event control, its signal read nowhere
552    /// else, an assertion that does not count as a use of it.
553    #[test]
554    fn structural_clock_is_the_single_edge_event() {
555        let inferred = structural(
556            "module m;\n\
557             logic mclk, q, d;\n\
558             always @(posedge mclk) begin\n\
559                q <= d;\n\
560                p: assert property (q != d);\n\
561             end\n\
562             endmodule\n",
563        )
564        .expect("no error");
565        assert_eq!(inferred, Some((EdgeKind::PosEdge, "mclk".to_string())));
566    }
567
568    /// 16.14.6(c): the clock term must not be referenced elsewhere in the
569    /// procedure, so `q <= clk` disqualifies `posedge clk`.
570    #[test]
571    fn structural_clock_term_read_in_the_body_is_not_a_clock() {
572        let inferred = structural(
573            "module m;\n\
574             logic clk, q;\n\
575             always @(posedge clk) q <= clk;\n\
576             endmodule\n",
577        )
578        .expect("no error");
579        assert_eq!(inferred, None);
580    }
581
582    /// 16.14.6(a): a blocking delay in the procedure means no inferred clock.
583    #[test]
584    fn structural_clock_blocking_delay_infers_nothing() {
585        let inferred = structural(
586            "module m;\n\
587             logic clk, q, d;\n\
588             always @(posedge clk) begin #1 q <= d; end\n\
589             endmodule\n",
590        )
591        .expect("no error");
592        assert_eq!(inferred, None);
593    }
594
595    /// 16.14.6(b): two event controls (the r4 shape) mean no inferred clock.
596    #[test]
597    fn structural_clock_two_event_controls_infer_nothing() {
598        let inferred = structural(
599            "module m;\n\
600             logic mclk, q, q1, d1;\n\
601             always @(posedge mclk) begin\n\
602                @(negedge mclk) q1 <= !d1;\n\
603                q <= d1;\n\
604             end\n\
605             endmodule\n",
606        )
607        .expect("no error");
608        assert_eq!(inferred, None);
609    }
610
611    /// An event variable as the clocking event is the (c) case this walk does not
612    /// model, so it is an error rather than a guess.
613    #[test]
614    fn structural_clock_event_variable_is_a_loud_error() {
615        let err = structural(
616            "module m;\n\
617             event e;\n\
618             logic q, d;\n\
619             always @(e) q <= d;\n\
620             endmodule\n",
621        )
622        .expect_err("an event-variable clock is refused");
623        assert!(
624            err.to_string().contains("event variable or clocking block"),
625            "{err}"
626        );
627    }
628
629    /// A timing control that is not on a statement (`q = #1 d`) is refused too.
630    #[test]
631    fn structural_clock_intra_assignment_delay_is_a_loud_error() {
632        let err = structural(
633            "module m;\n\
634             logic clk, q, d;\n\
635             always @(posedge clk) q = #1 d;\n\
636             endmodule\n",
637        )
638        .expect_err("an intra-assignment delay is refused");
639        assert!(err.to_string().contains("intra-assignment delay"), "{err}");
640    }
641}