diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index a6ffed210..a447b707a 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -5595,9 +5595,13 @@ public: }; class AstLogNot final : public AstNodeUniop { // @astgen makeDfgVertex +private: + const bool m_fromProperty; // True if from property 'not' keyword (IEEE 1800-2023 16.12.3), + // false for boolean '!' (IEEE 1800-2023 11.4.7) public: - AstLogNot(FileLine* fl, AstNodeExpr* lhsp) - : ASTGEN_SUPER_LogNot(fl, lhsp) { + AstLogNot(FileLine* fl, AstNodeExpr* lhsp, bool fromProperty = false) + : ASTGEN_SUPER_LogNot(fl, lhsp) + , m_fromProperty{fromProperty} { dtypeSetBit(); } ASTGEN_MEMBERS_AstLogNot; @@ -5609,6 +5613,9 @@ public: bool cleanOut() const override { return true; } bool cleanLhs() const override { return true; } bool sizeMattersLhs() const override { return false; } + bool fromProperty() const { return m_fromProperty; } + void dump(std::ostream& str) const override; + void dumpJson(std::ostream& str) const override; }; class AstNToI final : public AstNodeUniop { // String to any-size integral diff --git a/src/V3AstNodes.cpp b/src/V3AstNodes.cpp index fbdc2d26e..f3cede99c 100644 --- a/src/V3AstNodes.cpp +++ b/src/V3AstNodes.cpp @@ -1912,6 +1912,14 @@ void AstCCast::dumpJson(std::ostream& str) const { dumpJsonNumFunc(str, size); dumpJsonGen(str); } +void AstLogNot::dump(std::ostream& str) const { + this->AstNodeUniop::dump(str); + if (fromProperty()) str << " [fromProperty]"; +} +void AstLogNot::dumpJson(std::ostream& str) const { + dumpJsonBoolFuncIf(str, fromProperty); + dumpJsonGen(str); +} void AstCvtArrayToArray::dump(std::ostream& str) const { this->AstNodeExpr::dump(str); str << " reverse=" << reverse(); diff --git a/src/V3Width.cpp b/src/V3Width.cpp index dca08d7cc..dfc8d239b 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -7658,7 +7658,7 @@ class WidthVisitor final : public VNVisitor { } } - void visit_log_not(AstNode* nodep) { + void visit_log_not(AstLogNot* nodep) { // CALLER: LogNot // Width-check: lhs 1 bit // Real: Allowed; implicitly compares with zero @@ -7674,7 +7674,10 @@ class WidthVisitor final : public VNVisitor { if (m_vup->prelim()) { iterateCheckBool(nodep, "LHS", nodep->op1p(), BOTH); nodep->dtypeSetBit(); - if (m_underSExpr) { + // IEEE 1800-2023 16.12.3: property 'not' is not a sequence operator. + // Boolean '!' is allowed in sequences (16.7 expression_or_dist). + // The parser distinguishes the two via AstLogNot::fromProperty(). + if (m_underSExpr && nodep->fromProperty()) { nodep->v3error("Unexpected 'not' in sequence expression context"); AstConst* const newp = new AstConst{nodep->fileline(), 0}; newp->dtypeFrom(nodep); diff --git a/src/verilog.y b/src/verilog.y index 36ca106c0..a8904701b 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6737,7 +6737,7 @@ pexpr: // IEEE: property_expr (The name pexpr is important as regex // // Expanded below // yNOT pexpr - { $$ = new AstLogNot{$1, $2}; } + { $$ = new AstLogNot{$1, $2, /*fromProperty=*/true}; } | ySTRONG '(' sexpr ')' { $$ = $3; BBUNSUP($2, "Unsupported: strong (in property expression)"); } | yWEAK '(' sexpr ')' diff --git a/test_regress/t/t_assert_bang_in_seq.py b/test_regress/t/t_assert_bang_in_seq.py new file mode 100755 index 000000000..032a880d7 --- /dev/null +++ b/test_regress/t/t_assert_bang_in_seq.py @@ -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(verilator_flags2=['--assert', '--timing']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_assert_bang_in_seq.v b/test_regress/t/t_assert_bang_in_seq.v new file mode 100644 index 000000000..b0c831229 --- /dev/null +++ b/test_regress/t/t_assert_bang_in_seq.v @@ -0,0 +1,79 @@ +// 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 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); +`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0); +// verilog_format: on + +module t ( + input clk +); + + int cyc; + reg [63:0] crc; + + // Non-adjacent CRC bits avoid LFSR shift correlation. + wire a = crc[0]; + wire b = crc[4]; + wire c = crc[8]; + wire d = crc[12]; + + int count_fail1 = 0; + int count_fail2 = 0; + int count_fail3 = 0; + int count_fail4 = 0; + int count_fail5 = 0; + int count_fail6 = 0; + + // Test 1: a ##1 !b -- boolean ! as consequent of cycle delay. + assert property (@(posedge clk) a ##1 !b) + else count_fail1 <= count_fail1 + 1; + + // Test 2: a ##1 (!b && !c) -- conjunction of two bangs in seq. + assert property (@(posedge clk) a ##1 (!b && !c)) + else count_fail2 <= count_fail2 + 1; + + // Test 3: a |-> ##1 !b -- bang on consequent of overlapping implication + // (mirrors core-v-verif `|-> ##1 !irq_enabled`). + assert property (@(posedge clk) a |-> ##1 !b) + else count_fail3 <= count_fail3 + 1; + + // Test 4: a ##1 !$past(b) -- bang applied to sampled value function. + assert property (@(posedge clk) a ##1 !$past(b)) + else count_fail4 <= count_fail4 + 1; + + // Test 5: a ##0 !b ##1 c -- bang interleaved between cycle delays. + assert property (@(posedge clk) a ##0 !b ##1 c) + else count_fail5 <= count_fail5 + 1; + + // Test 6: a |=> !d -- bang on consequent of non-overlapping implication. + assert property (@(posedge clk) a |=> !d) + else count_fail6 <= count_fail6 + 1; + + always @(posedge clk) begin +`ifdef TEST_VERBOSE + $write("[%0t] cyc==%0d crc=%x a=%b b=%b c=%b d=%b\n", $time, cyc, crc, a, b, c, d); +`endif + cyc <= cyc + 1; + crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; + if (cyc == 0) begin + crc <= 64'h5aef0c8d_d70a4497; + end + else if (cyc == 99) begin + `checkh(crc, 64'hc77bb9b3784ea091); + `checkd(count_fail1, 66); // Questa: 66 + `checkd(count_fail2, 69); // Questa: 69 + `checkd(count_fail3, 26); // Questa: 26 + `checkd(count_fail4, 66); // Questa: 66 + `checkd(count_fail5, 80); // Questa: 80 + `checkd(count_fail6, 27); // Questa: 27 + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule