Fix `disable iff` in simple properties (#6890)

This commit is contained in:
Ryszard Rozak 2026-01-07 16:02:52 +01:00 committed by GitHub
parent c7361f177b
commit da14e7c4bb
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
5 changed files with 687 additions and 696 deletions

View File

@ -697,7 +697,11 @@ class AssertVisitor final : public VNVisitor {
m_inSampled = true;
iterateChildren(nodep);
}
nodep->replaceWith(nodep->exprp()->unlinkFrBack());
if (nodep->exprp()) {
nodep->replaceWith(nodep->exprp()->unlinkFrBack());
} else {
nodep->unlinkFrBack();
}
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
void visit(AstVarRef* nodep) override {

View File

@ -632,6 +632,11 @@ private:
// Unlink and just keep a pointer to it, convert to sentree as needed
m_senip = nodep->sensesp();
iterateNull(nodep->disablep());
if (VN_AS(nodep->backp(), NodeCoverOrAssert)->type() == VAssertType::CONCURRENT) {
const AstNodeDType* const propDtp = nodep->propp()->dtypep();
nodep->propp(new AstSampled{nodep->fileline(), nodep->propp()->unlinkFrBack()});
nodep->propp()->dtypeFrom(propDtp);
}
iterate(nodep->propp());
}
void visit(AstPExpr* nodep) override {

View File

@ -6353,11 +6353,11 @@ concurrent_assertion_statement<nodeStmtp>: // ==IEEE: concurrent_assertion_stat
// // IEEE: assume_property_statement
// // action_block expanded here
assertOrAssume yPROPERTY '(' property_spec ')' stmt %prec prLOWER_THAN_ELSE
{ $$ = new AstAssert{$<fl>1, new AstSampled{$<fl>1, $4}, $6, nullptr, VAssertType::CONCURRENT, $1}; }
{ $$ = new AstAssert{$<fl>1, $4, $6, nullptr, VAssertType::CONCURRENT, $1}; }
| assertOrAssume yPROPERTY '(' property_spec ')' stmt yELSE stmt
{ $$ = new AstAssert{$<fl>1, new AstSampled{$<fl>1, $4}, $6, $8, VAssertType::CONCURRENT, $1}; }
{ $$ = new AstAssert{$<fl>1, $4, $6, $8, VAssertType::CONCURRENT, $1}; }
| assertOrAssume yPROPERTY '(' property_spec ')' yELSE stmt
{ $$ = new AstAssert{$<fl>1, new AstSampled{$<fl>1, $4}, nullptr, $7, VAssertType::CONCURRENT, $1}; }
{ $$ = new AstAssert{$<fl>1, $4, nullptr, $7, VAssertType::CONCURRENT, $1}; }
// // IEEE: cover_property_statement
| yCOVER yPROPERTY '(' property_spec ')' stmt
{ $$ = new AstCover{$1, $4, $6, VAssertType::CONCURRENT}; }

View File

@ -4,55 +4,61 @@
// without warranty, 2019 by Peter Monsson.
// SPDX-License-Identifier: CC0-1.0
module t (/*AUTOARG*/
// Inputs
clk
);
module t ( /*AUTOARG*/
// Inputs
clk
);
input clk;
int cyc;
input clk;
int cyc;
Test test (/*AUTOINST*/
// Inputs
.clk (clk));
Test test ( /*AUTOINST*/
// Inputs
.clk(clk),
.cyc(cyc)
);
always @(posedge clk) begin
cyc <= cyc + 1;
if (cyc == 10) begin
$write("*-* All Finished *-*\n");
$finish;
end
end
always @(posedge clk) begin
cyc <= cyc + 1;
if (cyc == 10) begin
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule
module Test (
input clk
input clk,
input int cyc
);
`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) $stop;
else $stop;
assert property (@(posedge clk) disable iff (1) 0) $stop;
else $stop;
assert property (@(posedge clk) disable iff (1) 1) $stop;
else $stop;
assert property (@(posedge clk) disable iff (1) 1) $stop;
else $stop;
assert property (@(posedge clk) disable iff (0) 1);
assert property (@(posedge clk) disable iff (0) 1);
//
// Cover properties behave differently
//
// Pass 1st cycle
assert property (@(cyc) disable iff (cyc != $sampled(cyc)) cyc == 0);
cover property (@(posedge clk) disable iff (1) 1) $stop;
//
// Cover properties behave differently
//
cover property (@(posedge clk) disable iff (1) 0) $stop;
cover property (@(posedge clk) disable iff (1) 1) $stop;
cover property (@(posedge clk) disable iff (0) 1) $display("*COVER: ok");
cover property (@(posedge clk) disable iff (1) 0) $stop;
cover property (@(posedge clk) disable iff (0) 0) $stop;
cover property (@(posedge clk) disable iff (0) 1) $display("*COVER: ok");
cover property (@(posedge clk) disable iff (0) 0) $stop;
endmodule

File diff suppressed because it is too large Load Diff