github/verilator
1
0
Fork 1
mirror of https://github.com/verilator/verilator.git synced 2024-12-29 10:47:34 +00:00
Code Issues Packages Projects Releases Wiki Activity

Support default disable iff and $inferred_disable (#4016).

Browse Source
This commit is contained in:
Wilson Snyder 2024-11-26 22:27:32 -05:00
parent e14903cfb2
commit 99daa8d24b
13 changed files with 185 additions and 59 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changes
View File

@ -18,6 +18,7 @@ Verilator 5.031 devel
* Support vpiDefName (#3906) (#5572). [Krzysztof Starecki]
* Support parameter names in pattern initialization (#5593) (#5596). [Greg Davill]
* Support randomize size constraints with restrictions (#5582 partial) (#5611). [Ryszard Rozak, Antmicro Ltd.]
* Support `default disable iff` and `$inferred_disable` (#4016). [Srinivasan Venkataramanan]
* Support `pure constraint`.
* Add `--no-std-waiver` and default reading of standard lint waivers file (#5607).
* Add `--no-std-package` as subset-alias of `--no-std` (#5607).

30
src/V3AssertPre.cpp
View File

@ -45,7 +45,8 @@ private:
AstNodeModule* m_modp = nullptr; // Current module
AstClocking* m_clockingp = nullptr; // Current clocking block
// Reset each module:
AstClocking* m_defaultClockingp = nullptr; // Default clocking for the current module
AstClocking* m_defaultClockingp = nullptr; // Default clocking for current module
AstDefaultDisable* m_defaultDisablep = nullptr; // Default disable for current module
// Reset each assertion:
AstSenItem* m_senip = nullptr; // Last sensitivity
// Reset each always:
@ -522,6 +523,21 @@ private:
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
void visit(AstDefaultDisable* nodep) override {
// Done with these
VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep);
}
void visit(AstInferredDisable* nodep) override {
AstNode* newp;
if (m_defaultDisablep) {
newp = m_defaultDisablep->condp()->cloneTreePure(true);
} else {
newp = new AstConst{nodep->fileline(), AstConst::BitFalse{}};
}
nodep->replaceWith(newp);
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
void visit(AstPropSpec* nodep) override {
nodep = substitutePropertyCall(nodep);
// No need to iterate the body, once replace will get iterated
@ -530,6 +546,9 @@ private:
nodep->v3warn(E_UNSUPPORTED, "Unsupported: Only one PSL clock allowed per assertion");
// Block is the new expression to evaluate
AstNodeExpr* blockp = VN_AS(nodep->propp()->unlinkFrBack(), NodeExpr);
if (!nodep->disablep() && m_defaultDisablep) {
nodep->disablep(m_defaultDisablep->condp()->cloneTreePure(true));
}
if (AstNodeExpr* const disablep = nodep->disablep()) {
m_disablep = disablep->cloneTreePure(false);
if (VN_IS(nodep->backp(), Cover)) {
@ -547,6 +566,7 @@ private:
}
void visit(AstNodeModule* nodep) override {
VL_RESTORER(m_defaultClockingp);
VL_RESTORER(m_defaultDisablep);
VL_RESTORER(m_modp);
m_defaultClockingp = nullptr;
nodep->foreach([&](AstClocking* const clockingp) {
@ -558,6 +578,14 @@ private:
m_defaultClockingp = clockingp;
}
});
m_defaultDisablep = nullptr;
nodep->foreach([&](AstDefaultDisable* const disablep) {
if (m_defaultDisablep) {
disablep->v3error("Only one 'default disable iff' allowed per module"
" (IEEE 1800-2023 16.15)");
}
m_defaultDisablep = disablep;
});
m_modp = nodep;
iterateChildren(nodep);
}

12
src/V3AstNodeExpr.h
View File

@ -4501,6 +4501,18 @@ public:
};
// === AstNodeTermop ===
class AstInferredDisable final : public AstNodeTermop {
public:
AstInferredDisable(FileLine* fl)
: ASTGEN_SUPER_InferredDisable(fl) {
dtypeSetLogicSized(1, VSigning::UNSIGNED);
}
ASTGEN_MEMBERS_AstInferredDisable;
string emitVerilog() override { return "%f$inferred_disable"; }
string emitC() override { V3ERROR_NA_RETURN(""); }
bool cleanOut() const override { return true; }
bool same(const AstNode* /*samep*/) const override { return true; }
};
class AstTime final : public AstNodeTermop {
VTimescale m_timeunit; // Parent module time unit
public:

10
src/V3AstNodeOther.h
View File

@ -1076,6 +1076,16 @@ public:
bool same(const AstNode*) const override { return true; }
string path() const { return m_path; }
};
class AstDefaultDisable final : public AstNode {
// @astgen op1 := condp : AstNodeExpr
public:
AstDefaultDisable(FileLine* fl, AstNodeExpr* condp)
: ASTGEN_SUPER_DefaultDisable(fl) {
this->condp(condp);
}
ASTGEN_MEMBERS_AstDefaultDisable;
};
class AstDpiExport final : public AstNode {
// We could put an AstNodeFTaskRef instead of the verilog function name,
// however we're not *calling* it, so that seems somehow wrong.

8
src/V3Width.cpp
View File

@ -670,6 +670,11 @@ class WidthVisitor final : public VNVisitor {
}
}
}
void visit(AstDefaultDisable* nodep) override {
assertAtStatement(nodep);
// it's like an if() condition.
iterateCheckBool(nodep, "default disable iff condiftion", nodep->condp(), BOTH);
}
void visit(AstDelay* nodep) override {
if (VN_IS(m_procedurep, Final)) {
nodep->v3error("Delays are not legal in final blocks (IEEE 1800-2023 9.2.3)");
@ -1391,6 +1396,9 @@ class WidthVisitor final : public VNVisitor {
// queue_slice[#:$] and queue_bitsel[$] etc handled in V3WidthSel
nodep->v3warn(E_UNSUPPORTED, "Unsupported/illegal unbounded ('$') in this context.");
}
void visit(AstInferredDisable* nodep) override {
if (m_vup->prelim()) nodep->dtypeSetBit();
}
void visit(AstIsUnbounded* nodep) override {
if (m_vup->prelim()) {
userIterateAndNext(nodep->lhsp(), WidthVP{SELF, BOTH}.p());

1
src/verilog.l
View File

@ -474,6 +474,7 @@ vnum {vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
"$fell_gclk" { FL; return yD_FELL_GCLK; }
"$high" { FL; return yD_HIGH; }
"$increment" { FL; return yD_INCREMENT; }
"$inferred_disable" { FL; return yD_INFERRED_DISABLE; }
"$info" { FL; return yD_INFO; }
"$isunbounded" { FL; return yD_ISUNBOUNDED; }
"$isunknown" { FL; return yD_ISUNKNOWN; }

12
src/verilog.y
View File

@ -888,6 +888,7 @@ BISONPRE_VERSION(3.7,%define api.header.include {"V3ParseBison.h"})
%token<fl> yD_HIGH "$high"
%token<fl> yD_HYPOT "$hypot"
%token<fl> yD_INCREMENT "$increment"
%token<fl> yD_INFERRED_DISABLE "$inferred_disable"
%token<fl> yD_INFO "$info"
%token<fl> yD_ISUNBOUNDED "$isunbounded"
%token<fl> yD_ISUNKNOWN "$isunknown"
@ -2798,8 +2799,12 @@ module_or_generate_item_declaration<nodep>: // ==IEEE: module_or_generate_it
| clocking_declaration { $$ = $1; }
| yDEFAULT yCLOCKING idAny/*new-clocking_identifier*/ ';'
{ $$ = nullptr; BBUNSUP($1, "Unsupported: default clocking identifier"); }
| yDEFAULT yDISABLE yIFF expr/*expression_or_dist*/ ';'
{ $$ = nullptr; BBUNSUP($1, "Unsupported: default disable iff"); }
| defaultDisable { $$ = $1; }
;
defaultDisable<nodep>: // IEEE: part of module_/checker_or_generate_item_declaration
yDEFAULT yDISABLE yIFF expr/*expression_or_dist*/ ';'
{ $$ = new AstDefaultDisable{$1, $4}; }
;
aliasEqList: // IEEE: part of net_alias
@ -4423,6 +4428,7 @@ system_f_call_or_t<nodeExprp>: // IEEE: part of system_tf_call (can be task
| yD_HYPOT '(' expr ',' expr ')' { $$ = new AstHypotD{$1, $3, $5}; }
| yD_INCREMENT '(' exprOrDataType ')' { $$ = new AstAttrOf{$1, VAttrType::DIM_INCREMENT, $3, nullptr}; }
| yD_INCREMENT '(' exprOrDataType ',' expr ')' { $$ = new AstAttrOf{$1, VAttrType::DIM_INCREMENT, $3, $5}; }
| yD_INFERRED_DISABLE parenE { $$ = new AstInferredDisable{$1}; }
| yD_ISUNBOUNDED '(' expr ')' { $$ = new AstIsUnbounded{$1, $3}; }
| yD_ISUNKNOWN '(' expr ')' { $$ = new AstIsUnknown{$1, $3}; }
| yD_ITOR '(' expr ')' { $$ = new AstIToRD{$1, $3}; }
@ -7113,7 +7119,7 @@ checker_or_generate_item_declaration<nodep>: // ==IEEE: checker_or_generate_ite
| clocking_declaration { $$ = $1; }
| yDEFAULT yCLOCKING idAny/*clocking_identifier*/ ';' { }
{ $$ = nullptr; BBUNSUP($1, "Unsupported: checker default clocking"); }
| yDEFAULT yDISABLE yIFF expr/*expression_or_dist*/ ';' { }
| defaultDisable
{ $$ = nullptr; BBUNSUP($1, "Unsupported: checker default disable iff"); }
| ';' { $$ = nullptr; }
;

8
test_regress/t/t_EXAMPLE.v
View File

@ -16,6 +16,9 @@
// any use, without warranty, 2024 by Wilson Snyder.
// SPDX-License-Identifier: CC0-1.0
`define stop $stop
`define checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0x exp=%0x (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0);
module t(/*AUTOARG*/
// Inputs
clk
@ -64,10 +67,9 @@ module t(/*AUTOARG*/
end
else if (cyc == 99) begin
$write("[%0t] cyc==%0d crc=%x sum=%x\n", $time, cyc, crc, sum);
if (crc !== 64'hc77bb9b3784ea091) $stop;
`checkh(crc, 64'hc77bb9b3784ea091);
// What checksum will we end up with (above print should match)
`define EXPECTED_SUM 64'h4afe43fb79d7b71e
if (sum !== `EXPECTED_SUM) $stop;
`checkh(sum, 64'h4afe43fb79d7b71e);
$write("*-* All Finished *-*\n");
$finish;
end

6
test_regress/t/t_assert_disable_bad.v
View File

@ -5,7 +5,8 @@
// SPDX-License-Identifier: CC0-1.0
module t (/*AUTOARG*/
clk
// Inputs
clk
);
input clk;
@ -18,8 +19,7 @@ module t (/*AUTOARG*/
end
property check(int cyc_mod_2, logic expected);
@(posedge clk)
disable iff (cyc == 0) cyc % 2 == cyc_mod_2 |=> val == expected;
@(posedge clk) disable iff (cyc == 0) cyc % 2 == cyc_mod_2 |=> val == expected;
endproperty
// Test should fail due to duplicated disable iff statements

18
test_regress/t/t_assert_disable_count.py Executable file
View File

@ -0,0 +1,18 @@
#!/usr/bin/env python3
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# Copyright 2024 by Wilson Snyder. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0
import vltest_bootstrap
test.scenarios('simulator')
test.compile(verilator_flags2=['--assert'])
test.execute()
test.passes()

69
test_regress/t/t_assert_disable_count.v Normal file
View File

@ -0,0 +1,69 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain, for
// any use, without warranty, 2024 by Wilson Snyder.
// SPDX-License-Identifier: CC0-1.0
`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);
module t (/*AUTOARG*/
// Inputs
clk
);
input clk;
int cyc;
Sub sub ();
default disable iff (cyc[0]);
int a_false;
always @(posedge clk iff !cyc[0]) begin
if (cyc < 4 || cyc > 9) ;
else a_false = a_false + 1;
end
int a0_false;
a0: assert property (@(posedge clk) disable iff (cyc[0]) (cyc < 4 || cyc > 9))
else a0_false = a0_false + 1;
int a1_false;
// Note that Verilator supports $inferred_disable in general expression locations
// This is a superset of what IEEE specifies
a1: assert property (@(posedge clk) disable iff ($inferred_disable) (cyc < 4 || cyc > 9))
else a1_false = a1_false + 1;
int a2_false;
// Implicitly uses $inferred_disable
a2: assert property (@(posedge clk) (cyc < 4 || cyc > 9))
else a2_false = a2_false + 1;
int a3_false;
// A different disable iff expression
a3: assert property (@(posedge clk) disable iff (cyc == 5) (cyc < 4 || cyc > 9))
else a3_false = a3_false + 1;
always @(posedge clk) begin
cyc <= cyc + 1;
if (cyc == 20) begin
`checkd(a_false, 3);
`checkd(a0_false, a_false);
`checkd(a1_false, a_false);
`checkd(a2_false, a_false);
`checkd(a3_false, 5);
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule
module Sub;
initial begin
if ($inferred_disable !== 0) $stop;
end
endmodule

62
test_regress/t/t_assert_disable_iff.v
View File

@ -10,73 +10,47 @@ module t (/*AUTOARG*/
);
input clk;
integer cyc; initial cyc=1;
int cyc;
Test test (/*AUTOINST*/
// Inputs
.clk (clk));
always @ (posedge clk) begin
if (cyc!=0) begin
cyc <= cyc + 1;
if (cyc==10) begin
$write("*-* All Finished *-*\n");
$finish;
end
always @(posedge clk) begin
cyc <= cyc + 1;
if (cyc == 10) begin
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule
module Test
(
input clk
);
module Test (
input clk
);
`ifdef FAIL_ASSERT_1
assert property (
@(posedge clk) disable iff (0)
0
) else $display("wrong disable");
assert property (@(posedge clk) disable iff (0) 0)
else $display("wrong disable");
`endif
assert property (
@(posedge clk) disable iff (1)
0
);
assert property (@(posedge clk) disable iff (1) 0);
assert property (
@(posedge clk) disable iff (1)
1
);
assert property (@(posedge clk) disable iff (1) 1);
assert property (
@(posedge clk) disable iff (0)
1
);
assert property (@(posedge clk) disable iff (0) 1);
//
// Cover properties behave differently
//
cover property (
@(posedge clk) disable iff (1)
1
) $stop;
cover property (@(posedge clk) disable iff (1) 1) $stop;
cover property (
@(posedge clk) disable iff (1)
0
) $stop;
cover property (@(posedge clk) disable iff (1) 0) $stop;
cover property (
@(posedge clk) disable iff (0)
1
) $display("*COVER: ok");
cover property (@(posedge clk) disable iff (0) 1) $display("*COVER: ok");
cover property (
@(posedge clk) disable iff (0)
0
) $stop;
cover property (@(posedge clk) disable iff (0) 0) $stop;
endmodule

7
test_regress/t/t_disable_iff_multi_bad.out
View File

@ -1,8 +1,5 @@
%Error-UNSUPPORTED: t/t_disable_iff_multi_bad.v:13:4: Unsupported: default disable iff
13 | default disable iff (!rstn);
| ^~~~~~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_disable_iff_multi_bad.v:14:4: Unsupported: default disable iff
%Error: t/t_disable_iff_multi_bad.v:14:4: Only one 'default disable iff' allowed per module (IEEE 1800-2023 16.15)
: ... note: In instance 't'
14 | default disable iff (!rstn);
| ^~~~~~~
%Error: Exiting due to