diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 515976c4a..024e91fd9 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -609,7 +609,37 @@ private: FileLine* const flp = nodep->fileline(); AstNodeExpr* const rhsp = nodep->rhsp()->unlinkFrBack(); AstNodeExpr* lhsp = nodep->lhsp()->unlinkFrBack(); - if (nodep->isOverlapped()) { + if (AstPExpr* const pexprp = VN_CAST(rhsp, PExpr)) { + // Implication with sequence expression on RHS (IEEE 1800-2023 16.11, 16.12.7). + // The PExpr was already lowered from the property expression by V3AssertProp. + // Wrap the PExpr body with the antecedent check so the sequence only + // starts when the antecedent holds. + AstNodeExpr* condp; + if (nodep->isOverlapped()) { + // Overlapped implication (|->): check antecedent on same cycle. + // disable iff is applied at the assertion level, not at the + // antecedent gate, matching the existing non-PExpr overlapped path. + condp = new AstSampled{flp, lhsp}; + condp->dtypeFrom(lhsp); + } else { + // Non-overlapped implication (|=>): check antecedent from previous cycle + if (m_disablep) { + lhsp + = new AstAnd{flp, new AstNot{flp, m_disablep->cloneTreePure(false)}, lhsp}; + } + AstPast* const pastp = new AstPast{flp, lhsp}; + pastp->dtypeFrom(lhsp); + pastp->sentreep(newSenTree(nodep)); + condp = pastp; + } + // Wrap existing PExpr body: if (antecedent) { } else { /* vacuous pass + // */ } + AstBegin* const bodyp = pexprp->bodyp(); + AstNode* const origStmtsp = bodyp->stmtsp()->unlinkFrBackWithNext(); + AstIf* const guardp = new AstIf{flp, condp, origStmtsp}; + bodyp->addStmtsp(guardp); + nodep->replaceWith(pexprp); + } else if (nodep->isOverlapped()) { nodep->replaceWith(new AstLogOr{flp, new AstLogNot{flp, lhsp}, rhsp}); } else { if (m_disablep) { @@ -667,6 +697,16 @@ private: iterate(nodep); return; } + // Sequence expression as antecedent of implication is not yet supported + if (AstImplication* const implp = VN_CAST(nodep->backp(), Implication)) { + if (implp->lhsp() == nodep) { + implp->v3warn(E_UNSUPPORTED, + "Unsupported: Implication with sequence expression as antecedent"); + nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}}); + VL_DO_DANGLING(pushDeletep(nodep), nodep); + return; + } + } VL_RESTORER(m_inPExpr); VL_RESTORER(m_disableSeqIfp); m_inPExpr = true; diff --git a/src/V3Width.cpp b/src/V3Width.cpp index 606382e36..fe0502087 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -5623,16 +5623,6 @@ class WidthVisitor final : public VNVisitor { BOTH); // it's like an if() condition. } nodep->dtypeSetBit(); - if (m_hasSExpr) { - if (VN_IS(m_seqUnsupp, Implication)) { - m_seqUnsupp->v3warn(E_UNSUPPORTED, - "Unsupported: Implication with sequence expression"); - AstConst* const newp = new AstConst{nodep->fileline(), 0}; - newp->dtypeFrom(nodep); - nodep->replaceWith(newp); - VL_DO_DANGLING(pushDeletep(nodep), nodep); - } - } } } diff --git a/test_regress/t/t_property_imply_delay.py b/test_regress/t/t_property_imply_delay.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/test_regress/t/t_property_imply_delay.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(timing_loop=True, verilator_flags2=['--assert', '--timing']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_property_imply_delay.v b/test_regress/t/t_property_imply_delay.v new file mode 100644 index 000000000..b1b4311c4 --- /dev/null +++ b/test_regress/t/t_property_imply_delay.v @@ -0,0 +1,69 @@ +// 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 (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0); +// verilog_format: on + +module t ( + input clk +); + + int cyc; + reg [63:0] crc; + + // Take CRC data and apply to testblock inputs + // Use bits far apart (not adjacent) to break LFSR shift correlation, + // ensuring ##1 and ##2 delay assertions see uncorrelated a/b values. + wire a = crc[0]; + wire b = crc[4]; + + int count_fail_overlap1 = 0; + int count_fail_overlap2 = 0; + int count_fail_nonoverlap = 0; + + // Overlapped implication with 1-cycle delay: a |-> ##1 b + assert property (@(negedge clk) a |-> ##1 b) + else count_fail_overlap1 = count_fail_overlap1 + 1; + + // Overlapped implication with 2-cycle delay: a |-> ##2 b + assert property (@(negedge clk) a |-> ##2 b) + else count_fail_overlap2 = count_fail_overlap2 + 1; + + // Non-overlapped: a |=> ##1 b (equivalent to a |-> ##2 b) + assert property (@(negedge clk) a |=> ##1 b) + else count_fail_nonoverlap = count_fail_nonoverlap + 1; + + // Test loop + always @(posedge clk) begin +`ifdef TEST_VERBOSE + $write("[%0t] cyc==%0d crc=%x a=%b b=%b\n", $time, cyc, crc, a, b); +`endif + cyc <= cyc + 1; + crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; + if (cyc == 0) begin + // Setup + crc <= 64'h5aef0c8d_d70a4497; + end + else if (cyc == 99) begin + `checkh(crc, 64'hc77bb9b3784ea091); + + // |=> ##1 is equivalent to |-> ##2 + `checkd(count_fail_nonoverlap, count_fail_overlap2); + + // Result check + `checkd(count_fail_overlap1, 22); + `checkd(count_fail_overlap2, 25); + `checkd(count_fail_nonoverlap, 25); + + $write("*-* All Finished *-*\n"); + $finish; + end + end + +endmodule diff --git a/test_regress/t/t_property_sexpr_unsup.out b/test_regress/t/t_property_sexpr_unsup.out index 137ce4bfb..d442825fa 100644 --- a/test_regress/t/t_property_sexpr_unsup.out +++ b/test_regress/t/t_property_sexpr_unsup.out @@ -1,34 +1,26 @@ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:29:41: Unsupported: Implication with sequence expression +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:29:41: Unsupported: Implication with sequence expression as antecedent : ... note: In instance 't' 29 | assert property (@(posedge clk) ##1 1 |-> 1) $display("[%0t] single delay with const implication stmt, fileline:%d", $time, 29); | ^~~ ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:31:41: Unsupported: Implication with sequence expression +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:31:41: Unsupported: Implication with sequence expression as antecedent : ... note: In instance 't' 31 | assert property (@(posedge clk) ##1 1 |-> not (val)) $display("[%0t] single delay implication with negated var stmt, fileline:%d", $time, 31); | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:33:37: Unsupported: Implication with sequence expression - : ... note: In instance 't' - 33 | assert property (@(posedge clk) 1 |-> ##1 val) $display("[%0t] single delay implication with negated var stmt, fileline:%d", $time, 33); - | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:35:45: Unsupported: Implication with sequence expression +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:35:45: Unsupported: Implication with sequence expression as antecedent : ... note: In instance 't' 35 | assert property (@(posedge clk) (##1 val) |-> (not val)) $display("[%0t] single delay with negated implication stmt, fileline:%d", $time, 35); | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:37:45: Unsupported: Implication with sequence expression +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:37:45: Unsupported: Implication with sequence expression as antecedent : ... note: In instance 't' 37 | assert property (@(posedge clk) ##1 (val) |-> not (val)) $display("[%0t] single delay with negated implication brackets stmt, fileline:%d", $time, 37); | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:41:41: Unsupported: Implication with sequence expression +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:41:41: Unsupported: Implication with sequence expression as antecedent : ... note: In instance 't' 41 | assert property (@(posedge clk) ##1 1 |-> 0) $display("[%0t] disable iff with cond implication stmt, fileline:%d", $time, 41); | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:43:45: Unsupported: Implication with sequence expression +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:43:45: Unsupported: Implication with sequence expression as antecedent : ... 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:46:18: Unsupported: Implication with sequence expression - : ... note: In instance 't' - 46 | ##1 cyc == 4 |-> 1; - | ^~~ %Error: Exiting due to