Support ## delay on implication RHS in SVA properties (#7284)
This commit is contained in:
Yilou Wang
GitHub
parent
998ec5b1d7
commit
25c3bc814e
|
|
@ -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) { <original body> } 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;
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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,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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in New Issue