Fixes #7549.
This commit is contained in:
parent
5820d2936c
commit
8eca6b8fe7
|
|
@ -5595,9 +5595,13 @@ public:
|
||||||
};
|
};
|
||||||
class AstLogNot final : public AstNodeUniop {
|
class AstLogNot final : public AstNodeUniop {
|
||||||
// @astgen makeDfgVertex
|
// @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:
|
public:
|
||||||
AstLogNot(FileLine* fl, AstNodeExpr* lhsp)
|
AstLogNot(FileLine* fl, AstNodeExpr* lhsp, bool fromProperty = false)
|
||||||
: ASTGEN_SUPER_LogNot(fl, lhsp) {
|
: ASTGEN_SUPER_LogNot(fl, lhsp)
|
||||||
|
, m_fromProperty{fromProperty} {
|
||||||
dtypeSetBit();
|
dtypeSetBit();
|
||||||
}
|
}
|
||||||
ASTGEN_MEMBERS_AstLogNot;
|
ASTGEN_MEMBERS_AstLogNot;
|
||||||
|
|
@ -5609,6 +5613,9 @@ public:
|
||||||
bool cleanOut() const override { return true; }
|
bool cleanOut() const override { return true; }
|
||||||
bool cleanLhs() const override { return true; }
|
bool cleanLhs() const override { return true; }
|
||||||
bool sizeMattersLhs() const override { return false; }
|
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 {
|
class AstNToI final : public AstNodeUniop {
|
||||||
// String to any-size integral
|
// String to any-size integral
|
||||||
|
|
|
||||||
|
|
@ -1912,6 +1912,14 @@ void AstCCast::dumpJson(std::ostream& str) const {
|
||||||
dumpJsonNumFunc(str, size);
|
dumpJsonNumFunc(str, size);
|
||||||
dumpJsonGen(str);
|
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 {
|
void AstCvtArrayToArray::dump(std::ostream& str) const {
|
||||||
this->AstNodeExpr::dump(str);
|
this->AstNodeExpr::dump(str);
|
||||||
str << " reverse=" << reverse();
|
str << " reverse=" << reverse();
|
||||||
|
|
|
||||||
|
|
@ -7658,7 +7658,7 @@ class WidthVisitor final : public VNVisitor {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
void visit_log_not(AstNode* nodep) {
|
void visit_log_not(AstLogNot* nodep) {
|
||||||
// CALLER: LogNot
|
// CALLER: LogNot
|
||||||
// Width-check: lhs 1 bit
|
// Width-check: lhs 1 bit
|
||||||
// Real: Allowed; implicitly compares with zero
|
// Real: Allowed; implicitly compares with zero
|
||||||
|
|
@ -7674,7 +7674,10 @@ class WidthVisitor final : public VNVisitor {
|
||||||
if (m_vup->prelim()) {
|
if (m_vup->prelim()) {
|
||||||
iterateCheckBool(nodep, "LHS", nodep->op1p(), BOTH);
|
iterateCheckBool(nodep, "LHS", nodep->op1p(), BOTH);
|
||||||
nodep->dtypeSetBit();
|
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");
|
nodep->v3error("Unexpected 'not' in sequence expression context");
|
||||||
AstConst* const newp = new AstConst{nodep->fileline(), 0};
|
AstConst* const newp = new AstConst{nodep->fileline(), 0};
|
||||||
newp->dtypeFrom(nodep);
|
newp->dtypeFrom(nodep);
|
||||||
|
|
|
||||||
|
|
@ -6737,7 +6737,7 @@ pexpr<nodeExprp>: // IEEE: property_expr (The name pexpr is important as regex
|
||||||
// // Expanded below
|
// // Expanded below
|
||||||
//
|
//
|
||||||
yNOT pexpr
|
yNOT pexpr
|
||||||
{ $$ = new AstLogNot{$1, $2}; }
|
{ $$ = new AstLogNot{$1, $2, /*fromProperty=*/true}; }
|
||||||
| ySTRONG '(' sexpr ')'
|
| ySTRONG '(' sexpr ')'
|
||||||
{ $$ = $3; BBUNSUP($2, "Unsupported: strong (in property expression)"); }
|
{ $$ = $3; BBUNSUP($2, "Unsupported: strong (in property expression)"); }
|
||||||
| yWEAK '(' sexpr ')'
|
| yWEAK '(' sexpr ')'
|
||||||
|
|
|
||||||
|
|
@ -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()
|
||||||
|
|
@ -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
|
||||||
Loading…
Reference in New Issue