Support `disable iff` with sequences (#7090)
This commit is contained in:
Ryszard Rozak
GitHub
parent
0e26b049ea
commit
ff3028aca3
|
|
@ -54,8 +54,10 @@ private:
|
|||
AstSenItem* m_seniAlwaysp = nullptr; // Last sensitivity in always
|
||||
// Reset each assertion:
|
||||
AstNodeExpr* m_disablep = nullptr; // Last disable
|
||||
AstIf* m_disableSeqIfp = nullptr; // Used for handling disable iff in sequences
|
||||
// Other:
|
||||
V3UniqueNames m_cycleDlyNames{"__VcycleDly"}; // Cycle delay counter name generator
|
||||
V3UniqueNames m_disableCntNames{"__VdisableCnt"}; // Disable condition counter name generator
|
||||
bool m_inAssign = false; // True if in an AssignNode
|
||||
bool m_inAssignDlyLhs = false; // True if in AssignDly's LHS
|
||||
bool m_inSynchDrive = false; // True if in synchronous drive
|
||||
|
|
@ -374,6 +376,11 @@ private:
|
|||
new AstConst{flp, 1}}});
|
||||
beginp->addStmtsp(loopp);
|
||||
}
|
||||
if (m_disableSeqIfp) {
|
||||
AstIf* const disableSeqIfp = m_disableSeqIfp->cloneTree(false);
|
||||
disableSeqIfp->addThensp(nodep->nextp()->unlinkFrBackWithNext());
|
||||
nodep->addNextHere(disableSeqIfp);
|
||||
}
|
||||
nodep->replaceWith(beginp);
|
||||
VL_DO_DANGLING(nodep->deleteTree(), nodep);
|
||||
}
|
||||
|
|
@ -648,16 +655,64 @@ private:
|
|||
iterate(nodep->propp());
|
||||
}
|
||||
void visit(AstPExpr* nodep) override {
|
||||
VL_RESTORER(m_inPExpr);
|
||||
m_inPExpr = true;
|
||||
|
||||
if (AstLogNot* const notp = VN_CAST(nodep->backp(), LogNot)) {
|
||||
notp->replaceWith(nodep->unlinkFrBack());
|
||||
VL_DO_DANGLING(pushDeletep(notp), notp);
|
||||
iterate(nodep);
|
||||
} else {
|
||||
iterateChildren(nodep);
|
||||
return;
|
||||
}
|
||||
VL_RESTORER(m_inPExpr);
|
||||
VL_RESTORER(m_disableSeqIfp);
|
||||
m_inPExpr = true;
|
||||
|
||||
if (m_disablep) {
|
||||
const AstSampled* sampledp;
|
||||
if (m_disablep->exists([&sampledp](const AstSampled* const sp) {
|
||||
sampledp = sp;
|
||||
return true;
|
||||
})) {
|
||||
sampledp->v3warn(E_UNSUPPORTED,
|
||||
"Unsupported: $sampled inside disabled condition of a sequence");
|
||||
m_disablep = new AstConst{m_disablep->fileline(), AstConst::BitFalse{}};
|
||||
// always a copy is used, so remove it now
|
||||
pushDeletep(m_disablep);
|
||||
}
|
||||
FileLine* const flp = nodep->fileline();
|
||||
// Add counter which counts times the condition turned true
|
||||
AstVar* const disableCntp
|
||||
= new AstVar{flp, VVarType::MODULETEMP, m_disableCntNames.get(""),
|
||||
nodep->findBasicDType(VBasicDTypeKwd::UINT32)};
|
||||
disableCntp->lifetime(VLifetime::STATIC_EXPLICIT);
|
||||
m_modp->addStmtsp(disableCntp);
|
||||
AstVarRef* const readCntRefp = new AstVarRef{flp, disableCntp, VAccess::READ};
|
||||
AstVarRef* const writeCntRefp = new AstVarRef{flp, disableCntp, VAccess::WRITE};
|
||||
AstAssign* const incrStmtp = new AstAssign{
|
||||
flp, writeCntRefp, new AstAdd{flp, readCntRefp, new AstConst{flp, 1}}};
|
||||
AstAlways* const alwaysp
|
||||
= new AstAlways{flp, VAlwaysKwd::ALWAYS,
|
||||
new AstSenTree{flp, new AstSenItem{flp, VEdgeType::ET_POSEDGE,
|
||||
m_disablep->cloneTree(false)}},
|
||||
incrStmtp};
|
||||
disableCntp->addNextHere(alwaysp);
|
||||
|
||||
// Store value of that counter at the beginning of sequence evaluation
|
||||
AstBegin* const bodyp = nodep->bodyp();
|
||||
AstVar* const initialCntp = new AstVar{flp, VVarType::BLOCKTEMP, "__VinitialCnt",
|
||||
nodep->findBasicDType(VBasicDTypeKwd::UINT32)};
|
||||
initialCntp->lifetime(VLifetime::AUTOMATIC_EXPLICIT);
|
||||
bodyp->stmtsp()->addHereThisAsNext(initialCntp);
|
||||
AstAssign* const assignp
|
||||
= new AstAssign{flp, new AstVarRef{flp, initialCntp, VAccess::WRITE},
|
||||
readCntRefp->cloneTree(false)};
|
||||
initialCntp->addNextHere(assignp);
|
||||
|
||||
m_disableSeqIfp
|
||||
= new AstIf{flp, new AstEq{flp, new AstVarRef{flp, initialCntp, VAccess::READ},
|
||||
readCntRefp->cloneTree(false)}};
|
||||
// Delete it, because it is always copied before insetion to the AST
|
||||
pushDeletep(m_disableSeqIfp);
|
||||
}
|
||||
iterateChildren(nodep);
|
||||
}
|
||||
void visit(AstNodeModule* nodep) override {
|
||||
VL_RESTORER(m_defaultClockingp);
|
||||
|
|
|
|||
|
|
@ -5489,10 +5489,6 @@ class WidthVisitor final : public VNVisitor {
|
|||
newp->dtypeFrom(nodep);
|
||||
nodep->replaceWith(newp);
|
||||
VL_DO_DANGLING(pushDeletep(nodep), nodep);
|
||||
} else if (nodep->disablep()) {
|
||||
nodep->disablep()->v3warn(E_UNSUPPORTED,
|
||||
"Unsupported: Disable iff with sequence expression");
|
||||
VL_DO_DANGLING(pushDeletep(nodep->disablep()->unlinkFrBack()), nodep);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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('simulator')
|
||||
|
||||
test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing'])
|
||||
|
||||
test.execute()
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,52 @@
|
|||
// DESCRIPTION: Verilator: Verilog Test module
|
||||
//
|
||||
// This file ONLY is placed under the Creative Commons Public Domain.
|
||||
// SPDX-FileCopyrightText: 2026 Antmicro
|
||||
// SPDX-License-Identifier: CC0-1.0
|
||||
|
||||
`define stop $stop
|
||||
`define checkh(gotv,
|
||||
expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got='h%p exp='h%p\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0)
|
||||
|
||||
module t ( /*AUTOARG*/
|
||||
// Inputs
|
||||
clk
|
||||
);
|
||||
|
||||
input clk;
|
||||
|
||||
typedef struct {
|
||||
int fails;
|
||||
int passs;
|
||||
} result_t;
|
||||
|
||||
result_t results [int];
|
||||
result_t expected[int];
|
||||
|
||||
localparam MAX = 15;
|
||||
integer cyc = 0;
|
||||
|
||||
assert property (@(posedge clk) disable iff (cyc == 5 || cyc > MAX) 1 ##1 cyc < 10)
|
||||
results[1].passs++;
|
||||
else results[1].fails++;
|
||||
|
||||
assert property (@(posedge clk) disable iff (1) 1 ##1 0)
|
||||
results[2].passs++;
|
||||
else results[2].fails++;
|
||||
|
||||
assert property (@(posedge clk) disable iff (0) 1 ##1 0)
|
||||
results[3].passs++;
|
||||
else results[3].fails++;
|
||||
|
||||
always @(clk) begin
|
||||
++cyc;
|
||||
if (cyc == MAX) begin
|
||||
expected[1] = '{2, 3};
|
||||
// expected[2] shouldn't be initialized
|
||||
expected[3] = '{6, 0};
|
||||
`checkh(results, expected);
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
|
@ -0,0 +1,6 @@
|
|||
%Error-UNSUPPORTED: t/t_property_sexpr_disable_sampled_unsup.v:23:48: Unsupported: $sampled inside disabled condition of a sequence
|
||||
: ... note: In instance 't'
|
||||
23 | assert property (@(posedge clk) disable iff ($sampled(cyc) == 4) 1 ##1 cyc % 3 == 0) passes++;
|
||||
| ^~~~~~~~
|
||||
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
|
||||
%Error: Exiting due to
|
||||
|
|
@ -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.lint(expect_filename=test.golden_filename,
|
||||
verilator_flags2=['--assert', '--timing', '--error-limit 1000'],
|
||||
fails=True)
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,35 @@
|
|||
// DESCRIPTION: Verilator: Verilog Test module
|
||||
//
|
||||
// This file ONLY is placed under the Creative Commons Public Domain.
|
||||
// SPDX-FileCopyrightText: 2026 Antmicro
|
||||
// SPDX-License-Identifier: CC0-1.0
|
||||
|
||||
`define stop $stop
|
||||
`define checkh(gotv,
|
||||
expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got='h%p exp='h%p\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0)
|
||||
|
||||
module t ( /*AUTOARG*/
|
||||
// Inputs
|
||||
clk
|
||||
);
|
||||
|
||||
input clk;
|
||||
|
||||
localparam MAX = 10;
|
||||
int cyc = 0;
|
||||
int passes = 0;
|
||||
int fails = 0;
|
||||
|
||||
assert property (@(posedge clk) disable iff ($sampled(cyc) == 4) 1 ##1 cyc % 3 == 0) passes++;
|
||||
else fails++;
|
||||
|
||||
always @(posedge clk) begin
|
||||
cyc <= cyc + 1;
|
||||
if (cyc == MAX) begin
|
||||
`checkh(passes, 3);
|
||||
`checkh(fails, 4);
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
|
@ -1,23 +1,23 @@
|
|||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:75:14: Unsupported: sequence match items
|
||||
75 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:65:14: Unsupported: sequence match items
|
||||
65 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
|
||||
| ^
|
||||
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:75:29: Unsupported: ## range cycle delay range expression
|
||||
75 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:65:29: Unsupported: ## range cycle delay range expression
|
||||
65 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:74:13: Unsupported: property variable declaration
|
||||
74 | integer l_b;
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:64:13: Unsupported: property variable declaration
|
||||
64 | integer l_b;
|
||||
| ^~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:16: Unsupported: sequence match items
|
||||
92 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:16: Unsupported: sequence match items
|
||||
82 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
|
||||
| ^
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:51: Unsupported: [-> boolean abbrev expression
|
||||
92 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:51: Unsupported: [-> boolean abbrev expression
|
||||
82 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
|
||||
| ^~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:54: Unsupported: boolean abbrev (in sequence expression)
|
||||
92 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:54: Unsupported: boolean abbrev (in sequence expression)
|
||||
82 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
|
||||
| ^
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:90:14: Unsupported: property variable declaration
|
||||
90 | realtime l_t;
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:80:14: Unsupported: property variable declaration
|
||||
80 | realtime l_t;
|
||||
| ^~~
|
||||
%Error: Exiting due to
|
||||
|
|
|
|||
|
|
@ -27,24 +27,8 @@
|
|||
: ... note: In instance 't'
|
||||
43 | assert property (@(posedge clk) (##1 val) |-> (##1 val)) $display("[%0t] two delays implication stmt, fileline:%d", $time, 43);
|
||||
| ^~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:45:52: Unsupported: Disable iff with sequence expression
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:46:18: Unsupported: Implication with sequence expression
|
||||
: ... note: In instance 't'
|
||||
45 | assert property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 45);
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:47:52: Unsupported: Disable iff with sequence expression
|
||||
: ... note: In instance 't'
|
||||
47 | assume property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 47);
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:49:51: Unsupported: Disable iff with sequence expression
|
||||
: ... note: In instance 't'
|
||||
49 | cover property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 49);
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:52:37: Unsupported: Disable iff with sequence expression
|
||||
: ... note: In instance 't'
|
||||
52 | @(posedge clk) disable iff (cyc != 5) ##1 0;
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:56:18: Unsupported: Implication with sequence expression
|
||||
: ... note: In instance 't'
|
||||
56 | ##1 cyc == 4 |-> 1;
|
||||
46 | ##1 cyc == 4 |-> 1;
|
||||
| ^~~
|
||||
%Error: Exiting due to
|
||||
|
|
|
|||
|
|
@ -42,16 +42,6 @@ module t ( /*AUTOARG*/
|
|||
|
||||
assert property (@(posedge clk) (##1 val) |-> (##1 val)) $display("[%0t] two delays implication stmt, fileline:%d", $time, `__LINE__);
|
||||
|
||||
assert property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, `__LINE__);
|
||||
|
||||
assume property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, `__LINE__);
|
||||
|
||||
cover property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, `__LINE__);
|
||||
|
||||
property prop_disableiff;
|
||||
@(posedge clk) disable iff (cyc != 5) ##1 0;
|
||||
endproperty
|
||||
|
||||
property prop_implication;
|
||||
##1 cyc == 4 |-> 1;
|
||||
endproperty
|
||||
|
|
|
|||
Loading…
Reference in New Issue