Exempt sequence event controls from default disable iff and assertion control and cleanup redundant comments
This commit is contained in:
Yilou Wang
parent
1fc3771cf3
commit
3f09b5fbb7
|
|
@ -91,9 +91,7 @@ public:
|
|||
};
|
||||
|
||||
// Lower a sequence used as an event control ('@seq', IEEE 1800-2023 9.4.2.4) into a
|
||||
// synthesized event plus an internal 'cover sequence' that fires the event on every
|
||||
// end-of-match. Runs before V3AssertNfa so the sequence's automaton is built by the
|
||||
// ordinary cover-sequence path; nothing sequence-event-specific reaches V3AssertNfa.
|
||||
// synthesized event fired by an internal 'cover sequence' on each end-of-match
|
||||
class SeqEventLowerVisitor final : public VNVisitor {
|
||||
// STATE
|
||||
AstNodeModule* m_modp = nullptr; // Current module
|
||||
|
|
@ -605,18 +603,19 @@ class AssertVisitor final : public VNVisitor {
|
|||
|
||||
bool selfDestruct = false;
|
||||
bool passspGated = false;
|
||||
if (const AstCover* const snodep = VN_CAST(nodep, Cover)) {
|
||||
const AstCover* const coverp = VN_CAST(nodep, Cover);
|
||||
// A sequence event control is not an assertion directive; no assertion control
|
||||
const bool seqEvent = coverp && coverp->isSeqEvent();
|
||||
if (coverp) {
|
||||
++m_statCover;
|
||||
if (snodep->isSeqEvent()) {
|
||||
// Synthesized driver for a sequence used as an event control; keep the
|
||||
// action (the event fire) with no coverage bucket, independent of
|
||||
// --coverage.
|
||||
if (seqEvent) {
|
||||
// Keep the event-fire action, with no coverage bucket
|
||||
} else if (!v3Global.opt.coverageUser()) {
|
||||
selfDestruct = true;
|
||||
} else {
|
||||
// V3Coverage assigned us a bucket to increment.
|
||||
AstCoverInc* const covincp = VN_AS(snodep->coverincsp(), CoverInc);
|
||||
UASSERT_OBJ(covincp, snodep, "Missing AstCoverInc under assertion");
|
||||
AstCoverInc* const covincp = VN_AS(coverp->coverincsp(), CoverInc);
|
||||
UASSERT_OBJ(covincp, coverp, "Missing AstCoverInc under assertion");
|
||||
covincp->unlinkFrBackWithNext(); // next() might have AstAssign for trace
|
||||
if (message != "") covincp->declp()->comment(message);
|
||||
if (passsp) {
|
||||
|
|
@ -660,7 +659,8 @@ class AssertVisitor final : public VNVisitor {
|
|||
FileLine* const flp = nodep->fileline();
|
||||
bool passspAlreadyGated = false;
|
||||
if (passsp && VN_IS(passsp, If)) passspAlreadyGated = VN_AS(passsp, If)->user1();
|
||||
if (passsp && !passspGated && !passspAlreadyGated && !VN_IS(propExprp, PExpr)) {
|
||||
if (passsp && !passspGated && !passspAlreadyGated && !VN_IS(propExprp, PExpr)
|
||||
&& !seqEvent) {
|
||||
passsp = newIfAssertPassOn(passsp, nodep->directive(), nodep->userType(),
|
||||
/*vacuous=*/false);
|
||||
}
|
||||
|
|
@ -670,7 +670,7 @@ class AssertVisitor final : public VNVisitor {
|
|||
AstNode* bodysp = assertBody(nodep, propExprp, passsp, failsp);
|
||||
if (disablep) bodysp = new AstIf{flp, new AstLogNot{flp, disablep}, bodysp};
|
||||
// Add assertOn check last, for better combining
|
||||
bodysp = newIfAssertOn(bodysp, nodep->directive(), nodep->userType());
|
||||
if (!seqEvent) bodysp = newIfAssertOn(bodysp, nodep->directive(), nodep->userType());
|
||||
if (sentreep) bodysp = new AstAlways{flp, VAlwaysKwd::ALWAYS, sentreep, bodysp};
|
||||
|
||||
if (passsp && !passsp->backp()) VL_DO_DANGLING(pushDeletep(passsp), passsp);
|
||||
|
|
|
|||
|
|
@ -2876,11 +2876,17 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
bool senTreeOwned = false; // True if we created senTreep locally
|
||||
AstPropSpec* const propSpecp = VN_CAST(assertp->propp(), PropSpec);
|
||||
UASSERT_OBJ(propSpecp, assertp, "Concurrent assertion must have PropSpec");
|
||||
AstCover* const coverp = VN_CAST(assertp, Cover);
|
||||
const bool isCover = coverp != nullptr;
|
||||
const bool isCoverSeq = coverp && coverp->isCoverSeq();
|
||||
// A sequence event control is not an assertion directive; no default
|
||||
// disable iff, no assertion control
|
||||
const bool isSeqEvent = coverp && coverp->isSeqEvent();
|
||||
// Inherit module defaults (IEEE 14.12, 16.15) when assertion has none.
|
||||
if (!propSpecp->sensesp() && m_defaultClockingp) {
|
||||
propSpecp->sensesp(m_defaultClockingp->sensesp()->cloneTree(true));
|
||||
}
|
||||
if (!propSpecp->disablep() && m_defaultDisablep) {
|
||||
if (!propSpecp->disablep() && m_defaultDisablep && !isSeqEvent) {
|
||||
propSpecp->disablep(m_defaultDisablep->condp()->cloneTreePure(true));
|
||||
}
|
||||
if (!senTreep && propSpecp->sensesp()) {
|
||||
|
|
@ -2892,9 +2898,6 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
if (!senTreep) return;
|
||||
|
||||
FileLine* const flp = assertp->fileline();
|
||||
const bool isCover = VN_IS(assertp, Cover);
|
||||
AstCover* const coverp = VN_CAST(assertp, Cover);
|
||||
const bool isCoverSeq = coverp && coverp->isCoverSeq();
|
||||
|
||||
SvaGraph graph;
|
||||
SvaNfaBuilder builder{graph, m_modp, m_propTempNames, isCoverSeq};
|
||||
|
|
@ -2939,13 +2942,16 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
std::vector<AstNodeExpr*> perMidSrcs;
|
||||
|
||||
AstNodeExpr* const alwaysTriggerp
|
||||
= assertOnCond(flp, assertp->userType(), assertp->directive());
|
||||
= isSeqEvent ? new AstConst{flp, AstConst::BitTrue{}}
|
||||
: assertOnCond(flp, assertp->userType(), assertp->directive());
|
||||
AstNodeExpr* const outputExprp = m_loweringp->lower(
|
||||
flp, graph, alwaysTriggerp, senTreep, result.finalCondp, isCover,
|
||||
disableExprp ? disableExprp->cloneTreePure(false) : nullptr, negated,
|
||||
needMatch ? &matchExprp : nullptr, disableCntVarp, snapshotVarp,
|
||||
needPerSrcFail ? &requiredStepSrcs : nullptr, isCoverSeq ? &perMidSrcs : nullptr,
|
||||
assertp->userType(), assertp->directive());
|
||||
isSeqEvent ? VAssertType{VAssertType::INTERNAL} : assertp->userType(),
|
||||
isSeqEvent ? VAssertDirectiveType{VAssertDirectiveType::INTERNAL}
|
||||
: assertp->directive());
|
||||
|
||||
AstSenTree* const perSrcSenTreep
|
||||
= (requiredStepSrcs.size() >= 2) ? senTreep->cloneTree(false) : nullptr;
|
||||
|
|
|
|||
|
|
@ -1466,7 +1466,9 @@ private:
|
|||
iterateAndNextNull(nodep->sensesp());
|
||||
if (m_senip && m_senip != nodep->sensesp())
|
||||
nodep->v3warn(E_UNSUPPORTED, "Unsupported: Only one PSL clock allowed per assertion");
|
||||
if (!nodep->disablep() && m_defaultDisablep) {
|
||||
const AstCover* const coverp = VN_CAST(nodep->backp(), Cover);
|
||||
const bool seqEvent = coverp && coverp->isSeqEvent();
|
||||
if (!nodep->disablep() && m_defaultDisablep && !seqEvent) {
|
||||
nodep->disablep(m_defaultDisablep->condp()->cloneTreePure(true));
|
||||
}
|
||||
m_disablep = nodep->disablep();
|
||||
|
|
|
|||
|
|
@ -1612,9 +1612,8 @@ class AstCover final : public AstNodeCoverOrAssert {
|
|||
// @astgen op3 := coverincsp: List[AstNode] // Coverage node
|
||||
bool m_isCoverSeq = false; // 'cover sequence' (IEEE 1800-2023 16.14.3): fires per
|
||||
// end-of-match, not per property success
|
||||
bool m_isSeqEvent = false; // Synthesized to implement a sequence used as an event
|
||||
// control (IEEE 1800-2023 9.4.2.4); its action fires the
|
||||
// event on every end-of-match, independent of --coverage
|
||||
bool m_isSeqEvent = false; // Synthesized for a sequence used as an event control
|
||||
// (IEEE 1800-2023 9.4.2.4)
|
||||
public:
|
||||
ASTGEN_MEMBERS_AstCover;
|
||||
AstCover(FileLine* fl, AstNode* propp, AstNode* stmtsp, VAssertType type,
|
||||
|
|
|
|||
|
|
@ -33,8 +33,7 @@ module t (
|
|||
endsequence
|
||||
// verilog_format: on
|
||||
|
||||
// seq_dc has no clocking event, so it inherits the default clocking and must
|
||||
// behave identically to the explicitly-clocked seq above.
|
||||
// seq_dc inherits the default clocking; counts must match seq
|
||||
default clocking @(posedge clk);
|
||||
endclocking
|
||||
|
||||
|
|
@ -42,13 +41,8 @@ module t (
|
|||
a ##1 b ##1 c;
|
||||
endsequence
|
||||
|
||||
// A sequence used as an `@` event control resumes once per sequence end point
|
||||
// (IEEE 1800-2023 9.4.2.4). seq_hits/seq_hits2 are two waiters on the same
|
||||
// multi-cycle sequence; ref_hits is an independent shift-register oracle (end
|
||||
// point at posedge N when a@N-2, b@N-1, c@N); one_hits is the single-cycle case.
|
||||
// rng_hits waits on the ranged form: end points at posedge N when b@N and a@N-d
|
||||
// for any d in 1..3; simultaneous end points resume a blocked waiter once, so
|
||||
// rng_ref counts cycles with at least one end point.
|
||||
// ref_hits and rng_ref are independent shift-register oracles;
|
||||
// simultaneous end points resume a blocked waiter once
|
||||
initial forever begin
|
||||
@seq;
|
||||
seq_hits = seq_hits + 1;
|
||||
|
|
@ -79,9 +73,7 @@ module t (
|
|||
b1 <= b;
|
||||
end
|
||||
|
||||
// a/b/c are spaced to crc[0]/crc[4]/crc[8] -- past the ##2 window -- so the
|
||||
// left-shift LFSR cannot correlate a@T, b@T+1, c@T+2 into one bit; otherwise
|
||||
// the multi-cycle end-point machinery would collapse into a triviality.
|
||||
// a/b/c bit spacing exceeds the ##2 window to decorrelate the LFSR taps
|
||||
always @(posedge clk) begin
|
||||
cyc <= cyc + 1;
|
||||
crc <= {crc[30:0], crc[31] ^ crc[21] ^ crc[1] ^ crc[0]};
|
||||
|
|
|
|||
|
|
@ -0,0 +1,18 @@
|
|||
#!/usr/bin/env python3
|
||||
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
|
||||
#
|
||||
# This program is free software; you can redistribute it and/or modify it
|
||||
# under the terms of either the GNU Lesser General Public License Version 3
|
||||
# or the Perl Artistic License Version 2.0.
|
||||
# SPDX-FileCopyrightText: 2026 Wilson Snyder
|
||||
# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
|
||||
|
||||
import vltest_bootstrap
|
||||
|
||||
test.scenarios('vlt')
|
||||
|
||||
test.compile(verilator_flags2=['--timing'])
|
||||
|
||||
test.execute()
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,73 @@
|
|||
// DESCRIPTION: Verilator: Verilog Test module
|
||||
//
|
||||
// This file ONLY is placed under the Creative Commons Public Domain.
|
||||
// SPDX-FileCopyrightText: 2026 PlanV GmbH
|
||||
// SPDX-License-Identifier: CC0-1.0
|
||||
|
||||
// verilog_format: off
|
||||
`define stop $stop
|
||||
`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0);
|
||||
// verilog_format: on
|
||||
|
||||
module t (
|
||||
input clk
|
||||
);
|
||||
int unsigned crc = 32'h1;
|
||||
bit a, b, rst;
|
||||
bit a1;
|
||||
int cyc;
|
||||
int hits, ref_hits, one_hits, one_ref;
|
||||
|
||||
// Neither the default disable iff nor $assertoff may suppress a sequence event control
|
||||
default disable iff (rst);
|
||||
|
||||
// verilog_format: off // verible does not support clocking events inside sequence declarations
|
||||
sequence seq;
|
||||
@(posedge clk) a ##1 b;
|
||||
endsequence
|
||||
|
||||
sequence seq_one;
|
||||
@(posedge clk) 1;
|
||||
endsequence
|
||||
// verilog_format: on
|
||||
|
||||
initial begin
|
||||
$assertoff;
|
||||
#300 $assertkill;
|
||||
end
|
||||
|
||||
initial forever begin
|
||||
@seq;
|
||||
hits = hits + 1;
|
||||
end
|
||||
initial forever begin
|
||||
@seq_one;
|
||||
one_hits = one_hits + 1;
|
||||
end
|
||||
|
||||
always @(posedge clk) begin
|
||||
if (a1 && b) ref_hits = ref_hits + 1;
|
||||
one_ref = one_ref + 1;
|
||||
a1 <= a;
|
||||
end
|
||||
|
||||
always @(posedge clk) begin
|
||||
cyc <= cyc + 1;
|
||||
crc <= {crc[30:0], crc[31] ^ crc[21] ^ crc[1] ^ crc[0]};
|
||||
a <= crc[0];
|
||||
b <= crc[4];
|
||||
rst <= crc[2];
|
||||
end
|
||||
|
||||
always @(negedge clk) begin
|
||||
if (cyc == 60) $finish;
|
||||
end
|
||||
|
||||
final begin
|
||||
`checkd(hits, ref_hits);
|
||||
`checkd(one_hits, one_ref);
|
||||
`checkd(hits, 19); // Other simulator: 19
|
||||
`checkd(one_hits, 60); // Other simulator: 60
|
||||
$write("*-* All Finished *-*\n");
|
||||
end
|
||||
endmodule
|
||||
Loading…
Reference in New Issue