Lint Rules¶
ASSERT_NAMING¶
Assert label must start with a_.
Rationale: A consistent a_ prefix on assertion labels allows engineers
to instantly distinguish assertions from assumptions (m_) and cover
directives (c_) in log files, waveforms, and formal reports without
reading the full directive syntax.
Violation:
req_ack: assert property (@(posedge clk) req |-> ##[1:3] ack);
Correct usage:
a_req_ack: assert property (@(posedge clk) req |-> ##[1:3] ack);
Severity: WARNING
ASSERT_MISSING_LABEL¶
Assert statements must have a label.
Rationale: Labels on assertions enable targeted waveform search, log filtering, and coverage reporting. Without a label, tracing a failing assertion back to its source in a large design is time-consuming. Most formal and simulation tools can filter and report assertions by label.
Violation:
assert property (@(posedge clk) req |-> ##[1:3] ack);
Correct usage:
a_req_ack: assert property (@(posedge clk) req |-> ##[1:3] ack);
Severity: ERROR
ASSUME_NAMING¶
Assume label must start with m_.
Rationale: The m_ prefix (model/assume) distinguishes constraint
assumptions from assertions (a_) and coverage (c_) in formal tool
reports and log files, making intent immediately clear during review.
Violation:
req_stable: assume property (@(posedge clk) $stable(req));
Correct usage:
m_req_stable: assume property (@(posedge clk) $stable(req));
Severity: WARNING
COVER_NAMING¶
Cover label must start with c_.
Rationale: A consistent c_ prefix on cover directives distinguishes
coverage intent from assertions (a_) and assumptions (m_) when
reviewing formal reachability reports and simulation coverage logs.
Violation:
req_seen: cover property (@(posedge clk) req);
Correct usage:
c_req_seen: cover property (@(posedge clk) req);
Severity: WARNING
FUNC_NO_NON_OLAP_COVER¶
Avoid non-overlapping implication (|=>) in cover property.
Rationale: Using |=> with a cover property directive causes coverage
to be reported one cycle after the trigger, collecting vacuous or false-positive
hits. The cover directive should express direct observability; use ##1
or restructure the property to avoid |=>.
Violation:
c_req_ack: cover property (@(posedge clk) req |=> ack);
Correct usage:
c_req_ack: cover property (@(posedge clk) req ##1 ack);
Severity: ERROR
FUNC_NO_OLAP_COVER¶
Avoid overlapping implication (|->) in cover property.
Rationale: Using |-> with a cover property directive can collect
vacuous coverage when the antecedent does not hold, giving a false sense of
coverage completeness. Use ##0 for same-cycle coverage or restructure
without implication.
Violation:
c_req_ack: cover property (@(posedge clk) req |-> ack);
Correct usage:
c_req_ack: cover property (@(posedge clk) req ##0 ack);
Severity: ERROR
FUNC_MISSING_FAIL_ABLK¶
Assert statement must have a fail action block.
Rationale: Without an else fail action block, a failing assertion
produces only a generic simulator error with no design-context information.
A fail action block with $error or $fatal lets you print signal
values, timestamps, and custom messages, drastically reducing debug time.
Violation:
a_req_ack: assert property (@(posedge clk) req |-> ##[1:3] ack);
Correct usage:
a_req_ack: assert property (@(posedge clk) req |-> ##[1:3] ack)
else $error("req=%0b ack=%0b", req, ack);
Severity: ERROR
FUNC_AVOID_$_RANGE_IN_CONSEQ_A¶
Avoid unbounded ##[0:$] range in assertion consequent.
Rationale: An assertion with an infinite range ($) in its consequent
can never FAIL — it will always find a future cycle where the condition holds,
or wait indefinitely. This makes the assertion useless for verification. Use
a deterministic bounded delay instead.
Violation:
a_ack: assert property (@(posedge clk) $rose(req) |-> ##[0:$] ack);
Correct usage:
a_ack: assert property (@(posedge clk) $rose(req) |-> ##[1:8] ack);
Severity: ERROR
References: Ben Cohen, SVA Handbook https://payhip.com/b/7HvMk
DBG_MISS_END_LBL_PROP¶
Property declaration must have an end-label.
Rationale: End-labels (e.g., endproperty: p_my_prop) create a visual
bracket around the property body, making it easier to identify boundaries in
large files and enabling consistent navigation in editors. They are especially
valuable when properties span many lines.
Violation:
property p_req_ack;
@(posedge clk) req |-> ##[1:3] ack;
endproperty
Correct usage:
property p_req_ack;
@(posedge clk) req |-> ##[1:3] ack;
endproperty: p_req_ack
Severity: ERROR
DBG_MISS_END_LBL_SEQ¶
Sequence declaration must have an end-label.
Rationale: End-labels (e.g., endsequence: s_my_seq) visually bracket
the sequence body and improve navigability in large files. They are especially
valuable in deeply nested or multi-line sequence definitions.
Violation:
sequence s_req_rise;
@(posedge clk) ##1 $rose(req);
endsequence
Correct usage:
sequence s_req_rise;
@(posedge clk) ##1 $rose(req);
endsequence: s_req_rise
Severity: ERROR
NO_AA_EXISTS_SVA¶
Avoid associative array exists() method inside SVA.
Rationale: IEEE LRM 1800 §16.6 requires sampled associative array elements
to persist until assertion evaluation completes, but many EDA tools have not
fully adopted this requirement and impose restrictions or prohibit it entirely.
Avoid exists() inside SVA to maintain broad tool compatibility.
Violation:
a_mem: assert property (@(posedge clk)
(valid, v=mem.exists(addr)) |-> v);
Correct usage: Sample the exists() result into a logic signal in an
always block and reference that signal in SVA.
Severity: ERROR
References: IEEE 1800 LRM §16.6. Rule suggested by Ben Cohen.
FUNC_AVOID_DOLLAR_TIME¶
Use $realtime instead of $time in SVA.
Rationale: $time returns an integer truncated to simulation time
precision, losing sub-precision timing information. $realtime returns
a real-valued time that accurately reflects actual simulation time, which
is essential for timing assertions where sub-precision differences matter.
Violation:
a_timeout: assert property (@(posedge clk)
start |-> ($time - t0 < TIMEOUT));
Correct usage:
a_timeout: assert property (@(posedge clk)
start |-> ($realtime - t0 < TIMEOUT));
Severity: ERROR
STYLE_AVOID_FIRST_MATCH_A¶
Avoid first_match() in SVA for formal verification.
Rationale: first_match() creates multiple concurrent threads that
formal tools must evaluate simultaneously, potentially causing state-space
explosion and degraded performance. It also adds complexity that makes
failures harder to debug. While acceptable in simulation, it is generally
discouraged for formal analysis.
Violation:
a_req: assert property (@(posedge clk)
first_match(req ##[1:5] ack) |-> done);
Correct usage: Restructure using deterministic timing or goto repetition
to eliminate the need for first_match.
Severity: ERROR
References: Ben Cohen, SVA Handbook https://payhip.com/b/7HvMk
COMPAT_NO_POP_BACK_SVA¶
Avoid queue method pop_back() inside SVA.
Rationale: IEEE LRM 1800 §16.6 requires sampled queue elements to persist
until assertion evaluation completes, but many EDA tools restrict or prohibit
queue method calls inside SVA expressions for performance reasons. Avoid
pop_back() in SVA to ensure broad simulator and formal tool compatibility.
Violation:
a_data: assert property (@(posedge clk)
$rose(valid) |-> (q.pop_back() == 8'hA5));
Correct usage: Sample the queue element into a logic variable in an always block and reference that variable in SVA.
Severity: ERROR
References: IEEE 1800 LRM §16.6. Rule suggested by Ben Cohen.
COMPAT_NO_POP_FRONT_SVA¶
Avoid queue method pop_front() inside SVA.
Rationale: IEEE LRM 1800 §16.6 requires sampled queue elements to persist
until assertion evaluation completes, but many EDA tools restrict or prohibit
queue method calls inside SVA. Avoid pop_front() in SVA for broad
simulator and formal tool compatibility.
Violation:
a_data: assert property (@(posedge clk)
$rose(valid) |-> (q.pop_front() == 8'hA5));
Correct usage: Sample the queue element into a logic variable in an always block and reference that variable in SVA.
Severity: ERROR
References: IEEE 1800 LRM §16.6. Rule suggested by Ben Cohen.
STYLE_AVOID_RANGE_IN_ANT_A¶
Avoid cycle ranges in assertion antecedent.
Rationale: Range repetition in an antecedent (e.g., ##[1:10]) creates
multiple concurrent threads, one per possible delay value. Only one thread
can be non-vacuous while others generate spurious vacuous passes. Use goto
repetition ([->1]) to ensure exactly one match thread.
Violation:
a_rdy: assert property (@(posedge clk)
$rose(req) ##[1:10] rdy |-> ##[1:2] ack);
Correct usage:
a_rdy: assert property (@(posedge clk)
$rose(req) ##1 rdy[->1] |-> ##[1:2] ack);
Severity: ERROR
References: Ben Cohen, SVA Handbook https://payhip.com/b/7HvMk §2.2.2.2
REUSE_NO_TIMELITERAL¶
Avoid explicit time literals in SVA property declarations.
Rationale: Hard-coded time values (e.g., 10ns, 100ps) in SVA make
properties non-reusable across designs with different clock frequencies or
timing budgets. Use parameters or `` define` macros so timing can be
adjusted without modifying the assertion source.
Violation:
p_timeout: property (@(posedge clk)
start |-> done within 100ns);
Correct usage:
parameter TIMEOUT_CYCLES = 20;
p_timeout: property (@(posedge clk)
start |-> ##[1:TIMEOUT_CYCLES] done);
Severity: ERROR
STYLE_AVOID_WITHIN_A¶
Avoid the within sequence operator in SVA.
Rationale: The within operator, while part of the LRM, has misleading
semantics that frequently cause incorrect assertion intent. Its interaction
with threading and overlap semantics is non-intuitive, leading to assertions
that appear correct but check something different from what was intended.
Explicit sequence composition using ## and repetition operators is clearer
and more portable.
Violation:
a_ack: assert property (@(posedge clk)
(req ##1 ack) within (start ##[1:10] stop));
Correct usage: Express the temporal relationship explicitly using ##
delays and repetition without relying on within.
Severity: ERROR
References: Ben Cohen, SVA Handbook https://payhip.com/b/7HvMk
PERF_MISSING_IMPLICATION_OPER¶
SVA property without an implication operator hurts simulation performance.
Rationale: A property without |-> or |=> evaluates its consequent
on every active clock edge, creating a continuous evaluation thread with no
gating condition. This significantly degrades simulation performance on large
designs. Add an antecedent with an implication operator to gate evaluation
on meaningful trigger conditions. Exception: the forbid property style.
Violation:
p_no_x: property (@(posedge clk) !$isunknown(data));
Correct usage:
p_no_x: property (@(posedge clk) valid |-> !$isunknown(data));
Severity: ERROR
PERF_NO_LARGE_DELAY¶
Avoid large cycle delays (> 100 by default) in SVA properties.
Rationale: Large delay values (e.g., ##500) force the simulator to
maintain evaluation threads for hundreds of cycles, significantly increasing
memory and runtime overhead. If a large delay is genuinely required, use a
parameterized constant and document the justification. The threshold is
configurable via cfgMaxDelay (default: 100).
Violation:
p_resp: property (@(posedge clk) req |-> ##500 ack);
Correct usage:
parameter MAX_RESP = 20;
p_resp: property (@(posedge clk) req |-> ##[1:MAX_RESP] ack);
Severity: ERROR
PERF_PASS_ACT_BLK¶
Assert statement must not have a pass action block.
Rationale: A pass action block executes on every successful assertion evaluation, which can occur millions of times per simulation run. This severely degrades simulation performance. Pass action blocks are almost never needed; remove them or use coverage-based approaches instead.
Violation:
a_req_ack: assert property (@(posedge clk) req |-> ack)
$info("pass");
Correct usage:
a_req_ack: assert property (@(posedge clk) req |-> ack)
else $error("FAIL: req=%0b ack=%0b", req, ack);
Severity: ERROR
PERF_AVOID_$_RANGE_IN_ANT_A¶
Avoid unbounded ##[1:$] range in assertion antecedent.
Rationale: An unbounded range in the antecedent forces the tool to spawn and maintain an unbounded number of concurrent threads, one per possible cycle count. This causes state-space explosion in formal tools and significant slowdown in simulation. Use a finite bound based on expected design behavior.
Violation:
a_ack: assert property (@(posedge clk)
req ##[1:$] rdy |-> ack);
Correct usage:
a_ack: assert property (@(posedge clk)
req ##[1:10] rdy |-> ack);
Severity: ERROR
References: Ben Cohen, SVA Handbook https://payhip.com/b/7HvMk
PROP_NAMING¶
Property declaration must start with p_.
Rationale: A consistent p_ prefix on property names allows engineers
to instantly identify and filter property declarations in log files, waveforms,
and code search. It also visually separates properties from sequences
(typically s_ prefixed) and module-level signals.
Violation:
property req_ack;
@(posedge clk) req |-> ##[1:3] ack;
endproperty: req_ack
Correct usage:
property p_req_ack;
@(posedge clk) req |-> ##[1:3] ack;
endproperty: p_req_ack
Severity: WARNING
REUSE_NO_ONE_LINER_FAIL_ABLK¶
Fail action block must use begin/end, not a one-liner.
Rationale: A one-liner fail action block cannot be extended without
structural refactoring. Using begin/end from the start allows additional
debug statements, coverage increments, or task calls to be added later
without changing the block structure, improving long-term reusability.
Violation:
a_req_ack: assert property (@(posedge clk) req |-> ack)
else $error("FAIL");
Correct usage:
a_req_ack: assert property (@(posedge clk) req |-> ack)
else begin
$error("FAIL: req=%0b ack=%0b", req, ack);
end
Severity: ERROR
DBG_USE_SIMPLE_EXPR_IN_CONSEQ¶
Avoid complex consequent expressions; prefer multiple simple properties.
Rationale: A property with multiple implication operators or a consequent
containing more than two && expressions is difficult to debug when it
fails — the failing sub-expression is not immediately obvious from the error
report. Splitting into smaller properties lets the tool pinpoint exactly which
condition failed.
Violation:
p_complex: property (@(posedge clk)
req |-> ack && data_valid && !err && count > 0);
Correct usage:
p_ack: assert property (@(posedge clk) req |-> ack);
p_valid: assert property (@(posedge clk) req |-> data_valid);
p_noerr: assert property (@(posedge clk) req |-> !err);
Severity: ERROR
DELAY_BEFORE_ROSE¶
A ##1 delay is required immediately before $rose.
Rationale: $rose(sig) samples the signal on two consecutive clocks.
Without a preceding ##1, the assertion may fire on the very first active
clock before sig has a defined previous value, causing spurious failures
at time zero or after resets when signal history is undefined.
Violation:
p_rose_bad: property (@(posedge clk) $rose(req) |-> ack);
Correct usage:
p_rose_ok: property (@(posedge clk) ##1 $rose(req) |-> ack);
Severity: ERROR
FUNC_AVOID_EV_ALW¶
Avoid eventually always (Unbounded Weak-Weak).
Rationale: Weak eventually allows the assertion to pass vacuously if
the simulation ends before stabilization is observed. Additionally, expecting
permanent stability in dynamic simulation leads to false failures when system
state is later disturbed by resets or power sequences.
Violation:
a_stab: assert property (@(posedge clk) eventually always stable(data));
Correct usage:
a_stab: assert property (@(posedge clk) s_eventually [1:100] stable(data));
Severity: ERROR
FUNC_AVOID_EV_S_ALW¶
Avoid eventually s_always (Unbounded Weak-Strong).
Rationale: This pattern asserts that a condition will eventually lock into a permanent strong state. In directed or constrained-random testbenches, this is highly susceptible to failures when test phases shift (e.g., low-power entry/exit). Add explicit disable conditions or bound the stability window.
Violation:
a_lock: assert property (@(posedge clk) eventually s_always locked);
Correct usage:
a_lock: assert property (@(posedge clk)
s_eventually [1:50] locked disable iff (reset));
Severity: ERROR
FUNC_AVOID_S_EV_ALW¶
Avoid s_eventually always (Unbounded Strong-Weak).
Rationale: Asserting that a signal eventually becomes permanently true is fragile in dynamic simulation. Any subsequent reset, power-gating sequence, or testbench re-initialization will disturb the signal, producing persistent false assertion failures.
Violation:
a_stab: assert property (@(posedge clk) s_eventually always stable(data));
Correct usage:
a_stab: assert property (@(posedge clk) s_eventually [1:100] stable(data));
Severity: ERROR
FUNC_AVOID_S_EV_S_ALW¶
Avoid s_eventually s_always (Unbounded Strong-Strong).
Rationale: Demanding that a signal stabilizes and holds permanently is unrealistic in simulation. Any subsequent reset or mode change will violate this expectation, causing persistent false failures.
Violation:
a_lock: assert property (@(posedge clk) s_eventually s_always locked);
Correct usage:
a_lock: assert property (@(posedge clk)
s_eventually [1:50] s_always [0:10] locked);
Severity: ERROR
FUNC_AVOID_WEAK_EVENTUALLY¶
Avoid weak eventually; use s_eventually.
Rationale: The weak eventually operator passes vacuously if the
simulation ends before the condition becomes true, making liveness assertions
meaningless — they can never fail. Use s_eventually (strong eventually)
to enforce that the condition must be observed within the simulation run.
Violation:
a_done: assert property (@(posedge clk) start |-> eventually done);
Correct usage:
a_done: assert property (@(posedge clk) start |-> s_eventually done);
Severity: ERROR
FUNC_AVOID_BOUNDED_NEXTTIME¶
Avoid bounded weak nexttime [k]; use s_nexttime [k].
Rationale: Bounded weak nexttime [k] allows vacuously true passes at
simulation limits when insufficient clock cycles remain, potentially masking
functional verification blind spots. Use s_nexttime [k] to prevent such
vacuous passes.
Violation:
a_nxt: assert property (@(posedge clk) req |-> nexttime [2] ack);
Correct usage:
a_nxt: assert property (@(posedge clk) req |-> s_nexttime [2] ack);
Severity: ERROR
FUNC_AVOID_NEXTTIME¶
Avoid unbounded weak nexttime; use s_nexttime.
Rationale: Weak nexttime evaluates to true vacuously if the simulation
ends or clock ticks terminate before the next cycle is observed, making the
assertion ineffective. Use s_nexttime (strong nexttime) to enforce that
the next-cycle condition is strictly observed.
Violation:
a_nxt: assert property (@(posedge clk) req |-> nexttime ack);
Correct usage:
a_nxt: assert property (@(posedge clk) req |-> s_nexttime ack);
Severity: ERROR
FUNC_AVOID_WEAK_UNTIL¶
Avoid weak until; use s_until.
Rationale: The weak until operator allows non-terminating evaluation —
if the simulation ends before the termination condition is met, the assertion
passes vacuously. Use s_until (strong until) to guarantee the termination
condition is actually observed within the simulation run.
Violation:
a_hold: assert property (@(posedge clk) busy until ready);
Correct usage:
a_hold: assert property (@(posedge clk) busy s_until ready);
Severity: ERROR
FUNC_AVOID_WEAK_UNTIL_WITH¶
Avoid weak until_with; use s_until_with.
Rationale: Like until, the weak until_with operator passes vacuously
at simulation end if the termination condition is never reached. Use
s_until_with (strong until_with) to enforce that the endpoint condition
is strictly observed within the simulation run.
Violation:
a_hold: assert property (@(posedge clk) busy until_with ready);
Correct usage:
a_hold: assert property (@(posedge clk) busy s_until_with ready);
Severity: ERROR
NO_IMPLICATION_PROPERTY¶
Avoid logical implication -> in property; use |-> or |=>.
Rationale: The -> operator is a combinational logical implication, not
a temporal one. Inside a property it evaluates statically in a single clock
step and does not express sequential behavior. SVA temporal implication
operators |-> (overlapping) and |=> (non-overlapping) should be used
to express sequential intent correctly.
Violation:
p_bad: property (@(posedge clk) (req -> ack));
Correct usage:
p_ok: property (@(posedge clk) req |-> ack);
Severity: ERROR
NO_COVER_SEQ¶
Avoid cover sequence; use cover property instead.
Rationale: cover sequence is deprecated in practice and has limited
support across EDA tools. cover property is the standard, universally
supported form for temporal coverage collection and should always be preferred.
Violation:
c_req: cover sequence (@(posedge clk) req ##1 ack);
Correct usage:
c_req: cover property (@(posedge clk) req ##1 ack);
Severity: ERROR
PROP_UNUSED_FORMAL_ARG¶
Property has a formal argument that is never used in its body.
Rationale: Unused formal arguments indicate dead parameters — either a check was planned but never implemented, or a refactor left the signature inconsistent with the body. Callers must still pass values for them, creating misleading interfaces and dead code.
Violation:
property p_req_ack(input logic clk, input logic unused_sig);
@(posedge clk) req |-> ack;
endproperty: p_req_ack
Correct usage:
property p_req_ack(input logic clk);
@(posedge clk) req |-> ack;
endproperty: p_req_ack
Severity: ERROR
PROP_UNUSED_LOCAL_VAR¶
Local variable declared inside a property is never used.
Rationale: An unused local variable in a property body is dead code — it consumes simulator resources on every evaluation thread without contributing to the check. It typically indicates an incomplete implementation or leftover from a refactor.
Violation:
property p_data_check;
int unused_cnt;
@(posedge clk) valid |-> data != 0;
endproperty: p_data_check
Correct usage:
property p_data_check;
@(posedge clk) valid |-> data != 0;
endproperty: p_data_check
Severity: ERROR
SEQ_UNUSED_FORMAL_ARG¶
Sequence has a formal argument that is never used in its body.
Rationale: Unused formal arguments in a sequence definition indicate dead parameters. Callers must still pass values for them, creating misleading signatures and dead code. Remove unused arguments to keep interfaces clean and intent clear.
Violation:
sequence s_req(logic clk, logic unused);
@(posedge clk) ##1 $rose(req);
endsequence: s_req
Correct usage:
sequence s_req(logic clk);
@(posedge clk) ##1 $rose(req);
endsequence: s_req
Severity: WARNING
DELAY_BEFORE_CHANGED¶
A ##1 delay is required immediately before $changed.
Rationale: $changed(sig) compares the current sampled value of sig
with its value on the previous clock edge. Without a preceding ##1, the
assertion evaluates on the very first active clock, where there is no
well-defined previous value — the comparison is against an indeterminate initial
state. This causes spurious failures at simulation time zero and immediately
after any reset that re-initialises signal history.
Violation:
p_changed_bad: property (@(posedge clk) req |-> $changed(gnt));
Correct usage:
p_changed_ok: property (@(posedge clk) req |-> ##1 $changed(gnt));
Severity: ERROR
DELAY_BEFORE_FELL¶
A ##1 delay is required immediately before $fell.
Rationale: $fell(sig) samples the signal on two consecutive clock edges.
Without a preceding ##1, the assertion may evaluate before a valid previous
value exists — at time zero or immediately after reset when signal history is
undefined — producing spurious failures that obscure genuine bugs.
Violation:
p_fell_bad: property (@(posedge clk) req |-> $fell(gnt));
Correct usage:
p_fell_ok: property (@(posedge clk) req |-> ##1 $fell(gnt));
Severity: ERROR
STYLE_NO_CLK_WITHOUT_EDGE¶
Avoid @(clk) as a clocking event; use @(posedge clk) or @(negedge clk).
Rationale: A clocking event specified as @(clk) without an explicit
edge qualifier samples the clock on both the rising and falling edges. The
assertion then fires twice per clock period, producing duplicate or conflicting
evaluation results that are almost never the intended behaviour. An explicit
posedge or negedge qualifier makes the sampling intent unambiguous and
eliminates the double-trigger hazard.
Violation:
p_req_gnt: property (@(clk) req |-> ##1 gnt);
Correct usage:
p_req_gnt: property (@(posedge clk) req |-> ##1 gnt);
Severity: ERROR
STYLE_NO_IMM_SVA_IN_ALWAYS_COMB¶
Avoid plain immediate assertions inside always_comb; use assert final.
Rationale: A plain immediate assertion (assert (expr)) placed inside an
always_comb block fires on every delta cycle during combinatorial settling,
not just at the end of the time step. Intermediate glitches on input signals
cause the assertion to trigger before the output has reached its stable value,
producing spurious failures. The deferred form assert final evaluates only
after all combinatorial activity in the time step has resolved, giving the
correct and stable result.
Violation:
always_comb begin
assert (a == b) else $error("mismatch");
end
Correct usage:
always_comb begin
assert final (a == b) else $error("mismatch");
end
Severity: ERROR
STYLE_NO_MIXED_IMPL_OPER¶
Do not use |-> and |=> in the same property.
Rationale: Mixing overlapping (|->) and non-overlapping (|=>)
implication operators in a single property makes the temporal semantics
ambiguous. The consequent of |-> starts in the same clock cycle as the
antecedent, while |=> starts one cycle later; combining both in the same
property requires the reader to reason about two different reference points
simultaneously, increasing the risk of misinterpretation or misdiagnosis when
the property fails. Each property should express one consistent implication
style.
Violation:
p_mixed: property (@(posedge clk) a |-> (b |=> c));
Correct usage:
p_ab_olap: property (@(posedge clk) a |-> b);
p_b_nolap: property (@(posedge clk) b |=> c);
Severity: ERROR
STYLE_NO_NESTED_IMPL¶
Avoid nesting an implication operator inside the consequent of another implication.
Rationale: A property of the form a |-> (b |-> c) places an implication
inside the consequent of an outer implication. When such a property fails, it
is unclear whether the outer or inner implication triggered the violation, and
formal coverage tools may report the inner check as always vacuously true
relative to the outer context. Decomposing into two independent properties
allows the tool to report failures precisely and independently for each check.
Violation:
p_nested: property (@(posedge clk) a |-> (b |-> c));
Correct usage:
p_ab: assert property (@(posedge clk) a |-> b);
p_bc: assert property (@(posedge clk) b |-> c);
Severity: ERROR
PERF_NO_UB_REPEAT_IN_ANT¶
Avoid unbounded consecutive repetition [*] or [+] in an assertion antecedent.
Rationale: The operators [*] (zero-or-more consecutive matches) and
[+] (one-or-more consecutive matches) in an antecedent force the evaluation
engine to spawn and maintain an unlimited number of concurrent match threads,
one for each possible cycle count. In simulation this causes significant memory
and runtime overhead; in formal tools it leads to state-space explosion that
can render the proof intractable. Replace with a finite upper bound derived
from expected design behaviour.
Violation:
a_req_gnt: assert property (@(posedge clk) req[*] |-> gnt);
Correct usage:
a_req_gnt: assert property (@(posedge clk) req[*1:5] |-> gnt);
Severity: ERROR
PROP_LOCAL_VAR_NOT_USED_IN_CONSEQ¶
Local variable captured in the antecedent is never referenced in the consequent.
Rationale: A local variable assigned via antecedent capture
(e.g., (valid, captured = data)) is almost always intended to be compared
in the consequent (e.g., captured == expected). If the consequent does not
reference the variable, the captured value is silently discarded and the
intended check is never performed — the property verifies less than the author
expected without producing any warning.
Violation:
property p_data_check;
int captured;
@(posedge clk)
(valid, captured = data) |-> (data > 0);
endproperty: p_data_check
Correct usage:
property p_data_check;
int captured;
@(posedge clk)
(valid, captured = data) |-> (captured > 0);
endproperty: p_data_check
Severity: ERROR
SEQ_UNUSED_LOCAL_VAR¶
Local variable declared inside a sequence is never used.
Rationale: An unused local variable in a sequence body is dead code. The simulator allocates and tracks it on every evaluation thread without it contributing anything to the check. This wastes resources and typically indicates an incomplete implementation — a variable was declared in anticipation of a check that was never written — or a remnant from refactoring.
Violation:
sequence seq_check;
int unused_cnt;
valid ##1 (data > 0);
endsequence
Correct usage:
sequence seq_check;
valid ##1 (data > 0);
endsequence
Severity: ERROR
STYLE_THROUGHOUT_RHS_BOOL¶
RHS of throughout must be a multi-cycle sequence expression, not a plain boolean.
Rationale: The throughout operator has the form
boolean_cond throughout sequence_expr. Its purpose is to assert that a
condition holds continuously across every clock cycle spanned by a multi-cycle
sequence on the right-hand side. When the RHS is a plain boolean signal rather
than a sequence with cycle delays or repetitions, throughout degenerates
to a single-cycle evaluation that is semantically identical to a simple
conjunction — the temporal meaning of throughout is lost, and the intent
of the property becomes misleading to readers.
Violation:
p_valid_throughout: property (@(posedge clk)
valid throughout ack);
Correct usage:
p_valid_throughout: property (@(posedge clk)
valid throughout (req ##[1:5] ack));
Severity: ERROR
PROP_UNUSED_PROPERTY¶
Property declared but never referenced by any assertion, assumption, or cover directive.
Rationale: A property that is declared but never bound to an
assert property, assume property, or cover property statement
contributes zero verification value — it is never evaluated by the tool.
This typically indicates either dead code left over from a refactoring, or an
incomplete implementation where the binding statement was written but then
deleted, or was simply forgotten. Either way, the property must be either
instantiated or removed.
Violation:
property p_req_gnt;
@(posedge clk) req |-> ##1 gnt;
endproperty: p_req_gnt
// No assert/assume/cover statement references p_req_gnt
Correct usage:
property p_req_gnt;
@(posedge clk) req |-> ##1 gnt;
endproperty: p_req_gnt
a_req_gnt: assert property (p_req_gnt);
Severity: ERROR
SEQ_UNUSED_SEQUENCE¶
Sequence declared but never referenced by any property or assertion.
Rationale: A sequence that is declared but never instantiated inside a property, assertion, or cover directive is never evaluated and provides no verification coverage. It is either dead code from a refactor, or an incomplete implementation where the property that was supposed to use the sequence was never written. Unused sequences should be removed to keep the SVA codebase lean and free of misleading dead code.
Violation:
sequence seq_req_gnt;
req ##1 gnt;
endsequence
// No property or assertion references seq_req_gnt
Correct usage:
sequence seq_req_gnt;
req ##1 gnt;
endsequence
property p_req_gnt;
@(posedge clk) seq_req_gnt;
endproperty: p_req_gnt
a_req_gnt: assert property (p_req_gnt);
Severity: ERROR