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}