diff --git a/Changes b/Changes index bd47bdfd3..c650faff4 100644 --- a/Changes +++ b/Changes @@ -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). diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index d22004656..df9fbbe07 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -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); } diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index 4643a5e10..e7c60a61a 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -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: diff --git a/src/V3AstNodeOther.h b/src/V3AstNodeOther.h index 9ac6180b4..c38cc4773 100644 --- a/src/V3AstNodeOther.h +++ b/src/V3AstNodeOther.h @@ -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. diff --git a/src/V3Width.cpp b/src/V3Width.cpp index 23d77fae6..00a0d157c 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -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()); diff --git a/src/verilog.l b/src/verilog.l index 1092bedcb..b46bdd1bd 100644 --- a/src/verilog.l +++ b/src/verilog.l @@ -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; } diff --git a/src/verilog.y b/src/verilog.y index 745128bd3..792de8573 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -888,6 +888,7 @@ BISONPRE_VERSION(3.7,%define api.header.include {"V3ParseBison.h"}) %token yD_HIGH "$high" %token yD_HYPOT "$hypot" %token yD_INCREMENT "$increment" +%token yD_INFERRED_DISABLE "$inferred_disable" %token yD_INFO "$info" %token yD_ISUNBOUNDED "$isunbounded" %token yD_ISUNKNOWN "$isunknown" @@ -2798,8 +2799,12 @@ module_or_generate_item_declaration: // ==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: // 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: // 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: // ==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; } ; diff --git a/test_regress/t/t_EXAMPLE.v b/test_regress/t/t_EXAMPLE.v index 75a416220..c3eb28a02 100644 --- a/test_regress/t/t_EXAMPLE.v +++ b/test_regress/t/t_EXAMPLE.v @@ -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 diff --git a/test_regress/t/t_assert_disable_bad.v b/test_regress/t/t_assert_disable_bad.v index 07b3bc342..7bb6c04ad 100644 --- a/test_regress/t/t_assert_disable_bad.v +++ b/test_regress/t/t_assert_disable_bad.v @@ -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 diff --git a/test_regress/t/t_assert_disable_count.py b/test_regress/t/t_assert_disable_count.py new file mode 100755 index 000000000..2c4ffdce2 --- /dev/null +++ b/test_regress/t/t_assert_disable_count.py @@ -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() diff --git a/test_regress/t/t_assert_disable_count.v b/test_regress/t/t_assert_disable_count.v new file mode 100644 index 000000000..3a424467c --- /dev/null +++ b/test_regress/t/t_assert_disable_count.v @@ -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 diff --git a/test_regress/t/t_assert_disable_iff.v b/test_regress/t/t_assert_disable_iff.v index 7a5b2b2fd..23ec387bc 100644 --- a/test_regress/t/t_assert_disable_iff.v +++ b/test_regress/t/t_assert_disable_iff.v @@ -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 diff --git a/test_regress/t/t_disable_iff_multi_bad.out b/test_regress/t/t_disable_iff_multi_bad.out index 24b6b78a6..cf6dedeb4 100644 --- a/test_regress/t/t_disable_iff_multi_bad.out +++ b/test_regress/t/t_disable_iff_multi_bad.out @@ -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