Support `always` / `always[m:n]` / `s_always[m:n]` property operators (#7482)
This commit is contained in:
Yilou Wang
GitHub
parent
e4803f29b6
commit
c8893b64de
|
|
@ -528,6 +528,30 @@ class SvaNfaBuilder final {
|
|||
return {currentp, nullptr, {}};
|
||||
}
|
||||
|
||||
// always[lo:hi] / s_always[lo:hi] (IEEE 1800-2023 16.12.11).
|
||||
BuildResult buildPropAlways(AstPropAlways* nodep, SvaStateVertex* entryVtxp,
|
||||
bool isTopLevelStep = false) {
|
||||
FileLine* const flp = nodep->fileline();
|
||||
AstNodeExpr* const propp = nodep->propp();
|
||||
const int lo = getConstInt(nodep->loBoundp());
|
||||
const int hi = getConstInt(nodep->hiBoundp());
|
||||
UASSERT_OBJ(lo >= 0 && hi >= lo, nodep, "PropAlways bounds invariant (V3Width)");
|
||||
SvaStateVertex* currentp = addDelayChain(entryVtxp, lo, flp);
|
||||
for (int k = 0; k <= hi - lo; ++k) {
|
||||
if (k > 0) {
|
||||
SvaStateVertex* const nextp = scopedCreateVertex();
|
||||
guardedEdge(currentp, nextp, flp);
|
||||
currentp = nextp;
|
||||
}
|
||||
SvaStateVertex* const checkp = scopedCreateVertex();
|
||||
SvaTransEdge* const linkp
|
||||
= guardedLink(currentp, checkp, sampled(propp->cloneTreePure(false)), flp);
|
||||
if (isTopLevelStep && !m_inUnboundedScope) linkp->m_rejectOnFail = true;
|
||||
currentp = checkp;
|
||||
}
|
||||
return {currentp, nullptr, {}};
|
||||
}
|
||||
|
||||
BuildResult buildGotoRep(AstSGotoRep* repp, SvaStateVertex* entryVtxp) {
|
||||
FileLine* const flp = repp->fileline();
|
||||
AstNodeExpr* const exprp = repp->exprp();
|
||||
|
|
@ -734,6 +758,9 @@ public:
|
|||
if (AstSConsRep* const repp = VN_CAST(nodep, SConsRep)) {
|
||||
return buildConsRep(repp, entryVtxp, isTopLevelStep);
|
||||
}
|
||||
if (AstPropAlways* const alwaysp = VN_CAST(nodep, PropAlways)) {
|
||||
return buildPropAlways(alwaysp, entryVtxp, isTopLevelStep);
|
||||
}
|
||||
if (AstSGotoRep* const repp = VN_CAST(nodep, SGotoRep)) {
|
||||
return buildGotoRep(repp, entryVtxp);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -2027,6 +2027,32 @@ public:
|
|||
}
|
||||
string name() const override VL_MT_STABLE { return m_name; }
|
||||
};
|
||||
class AstPropAlways final : public AstNodeExpr {
|
||||
// always[m:n] / s_always[m:n] (IEEE 1800-2023 16.12.11)
|
||||
// @astgen op1 := propp : AstNodeExpr
|
||||
// @astgen op2 := loBoundp : AstNodeExpr
|
||||
// @astgen op3 := hiBoundp : AstNodeExpr
|
||||
const bool m_isStrong = false; // s_always
|
||||
public:
|
||||
AstPropAlways(FileLine* fl, AstNodeExpr* propp, AstNodeExpr* loBoundp, AstNodeExpr* hiBoundp,
|
||||
bool isStrong)
|
||||
: ASTGEN_SUPER_PropAlways(fl)
|
||||
, m_isStrong{isStrong} {
|
||||
this->propp(propp);
|
||||
this->loBoundp(loBoundp);
|
||||
this->hiBoundp(hiBoundp);
|
||||
}
|
||||
ASTGEN_MEMBERS_AstPropAlways;
|
||||
void dump(std::ostream& str) const override;
|
||||
void dumpJson(std::ostream& str) const override;
|
||||
string emitVerilog() override { V3ERROR_NA_RETURN(""); }
|
||||
string emitC() override { V3ERROR_NA_RETURN(""); }
|
||||
string emitSimpleOperator() override { V3ERROR_NA_RETURN(""); }
|
||||
bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
|
||||
int instrCount() const override { V3ERROR_NA_RETURN(0); }
|
||||
bool isStrong() const { return m_isStrong; }
|
||||
bool isMultiCycleSva() const override { return true; }
|
||||
};
|
||||
class AstRand final : public AstNodeExpr {
|
||||
// $random/$random(seed) or $urandom/$urandom(seed)
|
||||
// Return a random number, based upon width()
|
||||
|
|
|
|||
|
|
@ -456,6 +456,14 @@ void AstSConsRep::dumpJson(std::ostream& str) const {
|
|||
dumpJsonBoolFuncIf(str, unbounded);
|
||||
dumpJsonGen(str);
|
||||
} // LCOV_EXCL_STOP
|
||||
void AstPropAlways::dump(std::ostream& str) const {
|
||||
this->AstNodeExpr::dump(str);
|
||||
if (isStrong()) str << " [strong]";
|
||||
}
|
||||
void AstPropAlways::dumpJson(std::ostream& str) const {
|
||||
dumpJsonBoolFuncIf(str, isStrong);
|
||||
dumpJsonGen(str);
|
||||
}
|
||||
void AstConsQueue::dump(std::ostream& str) const {
|
||||
this->AstNodeExpr::dump(str);
|
||||
if (lhsIsValue()) str << " [LVAL]";
|
||||
|
|
|
|||
|
|
@ -1058,6 +1058,18 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
|
|||
puts("\n");
|
||||
}
|
||||
void visit(AstPExpr* nodep) override { iterateConst(nodep->bodyp()); }
|
||||
void visit(AstPropAlways* nodep) override {
|
||||
puts(nodep->isStrong() ? "s_always" : "always");
|
||||
if (!VN_IS(nodep->loBoundp(), Unbounded) || !VN_IS(nodep->hiBoundp(), Unbounded)) {
|
||||
puts(" [");
|
||||
iterateConst(nodep->loBoundp());
|
||||
puts(":");
|
||||
iterateConst(nodep->hiBoundp());
|
||||
puts("]");
|
||||
}
|
||||
puts(" ");
|
||||
iterateConst(nodep->propp());
|
||||
}
|
||||
void visit(AstSExpr* nodep) override {
|
||||
iterateConstNull(nodep->preExprp());
|
||||
{
|
||||
|
|
|
|||
|
|
@ -1545,6 +1545,65 @@ class WidthVisitor final : public VNVisitor {
|
|||
nodep->dtypeSetBit();
|
||||
}
|
||||
}
|
||||
void visit(AstPropAlways* nodep) override {
|
||||
// IEEE 1800-2023 16.12.11
|
||||
assertAtExpr(nodep);
|
||||
if (m_vup->prelim()) {
|
||||
userIterateAndNext(nodep->propp(), WidthVP{SELF, BOTH}.p());
|
||||
if (!VN_IS(nodep->loBoundp(), Unbounded)) {
|
||||
userIterateAndNext(nodep->loBoundp(), WidthVP{SELF, BOTH}.p());
|
||||
V3Const::constifyParamsEdit(nodep->loBoundp());
|
||||
}
|
||||
if (!VN_IS(nodep->hiBoundp(), Unbounded)) {
|
||||
userIterateAndNext(nodep->hiBoundp(), WidthVP{SELF, BOTH}.p());
|
||||
V3Const::constifyParamsEdit(nodep->hiBoundp());
|
||||
}
|
||||
const bool loUnbounded = VN_IS(nodep->loBoundp(), Unbounded);
|
||||
const bool hiUnbounded = VN_IS(nodep->hiBoundp(), Unbounded);
|
||||
if (loUnbounded || hiUnbounded) {
|
||||
if (nodep->isStrong()) {
|
||||
nodep->v3error("s_always range must be bounded (IEEE 1800-2023 16.12.11)");
|
||||
} else {
|
||||
nodep->v3warn(E_UNSUPPORTED,
|
||||
"Unsupported: unbounded always range (always [m:$])");
|
||||
}
|
||||
nodep->dtypeSetBit();
|
||||
return;
|
||||
}
|
||||
const AstConst* const loConstp = VN_CAST(nodep->loBoundp(), Const);
|
||||
const AstConst* const hiConstp = VN_CAST(nodep->hiBoundp(), Const);
|
||||
if (!loConstp) {
|
||||
nodep->v3error("always range low bound must be a constant expression"
|
||||
" (IEEE 1800-2023 16.12.11)");
|
||||
}
|
||||
if (!hiConstp) {
|
||||
nodep->v3error("always range high bound must be a constant expression"
|
||||
" (IEEE 1800-2023 16.12.11)");
|
||||
}
|
||||
if (loConstp && loConstp->toSInt() < 0) {
|
||||
nodep->v3error("always range low bound must be non-negative"
|
||||
" (IEEE 1800-2023 16.12.11)");
|
||||
}
|
||||
if (loConstp && hiConstp && hiConstp->toSInt() < loConstp->toSInt()) {
|
||||
nodep->v3error("always range high bound must be >= low bound"
|
||||
" (IEEE 1800-2023 16.12.11)");
|
||||
}
|
||||
bool hasPropertyOp = nodep->propp()->isMultiCycleSva();
|
||||
if (!hasPropertyOp) {
|
||||
nodep->propp()->foreach([&](const AstNode* np) {
|
||||
if (VN_IS(np, Implication) || VN_IS(np, Until) || VN_IS(np, PropSpec)) {
|
||||
hasPropertyOp = true;
|
||||
}
|
||||
});
|
||||
}
|
||||
if (hasPropertyOp) {
|
||||
nodep->v3warn(E_UNSUPPORTED,
|
||||
"Unsupported: property/sequence operator inside bounded"
|
||||
" always (IEEE 1800-2023 16.12.11)");
|
||||
}
|
||||
nodep->dtypeSetBit();
|
||||
}
|
||||
}
|
||||
void visit(AstRising* nodep) override {
|
||||
assertAtExpr(nodep);
|
||||
if (m_vup->prelim()) {
|
||||
|
|
|
|||
|
|
@ -6753,11 +6753,13 @@ pexpr<nodeExprp>: // IEEE: property_expr (The name pexpr is important as regex
|
|||
| yS_NEXTTIME '[' constExpr ']' pexpr %prec yS_NEXTTIME
|
||||
{ $$ = $5; BBUNSUP($1, "Unsupported: s_nexttime[] (in property expression)"); DEL($3); }
|
||||
| yALWAYS pexpr
|
||||
{ $$ = $2; BBUNSUP($1, "Unsupported: always (in property expression)"); }
|
||||
| yALWAYS anyrange pexpr %prec yALWAYS
|
||||
{ $$ = $3; BBUNSUP($1, "Unsupported: always[] (in property expression)"); DEL($2); }
|
||||
| yS_ALWAYS anyrange pexpr %prec yS_ALWAYS
|
||||
{ $$ = $3; BBUNSUP($1, "Unsupported: s_always (in property expression)"); DEL($2); }
|
||||
{ $$ = $2; }
|
||||
| yALWAYS '[' constExpr ':' constExpr ']' pexpr %prec yALWAYS
|
||||
{ $$ = new AstPropAlways{$1, $7, $3, $5, false}; }
|
||||
| yS_ALWAYS '[' constExpr ':' constExpr ']' pexpr %prec yS_ALWAYS
|
||||
{ $$ = new AstPropAlways{$1, $7, $3, $5, true}; }
|
||||
| yS_ALWAYS pexpr
|
||||
{ $$ = new AstPropAlways{$1, $2, new AstUnbounded{$1}, new AstUnbounded{$1}, true}; }
|
||||
| yS_EVENTUALLY pexpr
|
||||
{ $$ = $2; BBUNSUP($1, "Unsupported: s_eventually (in property expression)"); }
|
||||
| yS_EVENTUALLY anyrange pexpr %prec yS_EVENTUALLY
|
||||
|
|
|
|||
|
|
@ -1,15 +1,9 @@
|
|||
%Error-UNSUPPORTED: t/t_assert_always_unsup.v:20:5: Unsupported: always[] (in property expression)
|
||||
20 | always [2:5] a;
|
||||
| ^~~~~~
|
||||
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
|
||||
%Error-UNSUPPORTED: t/t_assert_always_unsup.v:24:5: Unsupported: s_always (in property expression)
|
||||
24 | s_always [2:5] a;
|
||||
| ^~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_assert_always_unsup.v:28:5: Unsupported: eventually[] (in property expression)
|
||||
28 | eventually [2:5] a;
|
||||
%Error-UNSUPPORTED: t/t_assert_always_unsup.v:20:5: Unsupported: eventually[] (in property expression)
|
||||
20 | eventually [2:5] a;
|
||||
| ^~~~~~~~~~
|
||||
%Error: t/t_assert_always_unsup.v:32:18: syntax error, unexpected ']', expecting ':'
|
||||
32 | eventually [2] a;
|
||||
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
|
||||
%Error: t/t_assert_always_unsup.v:24:18: syntax error, unexpected ']', expecting ':'
|
||||
24 | eventually [2] a;
|
||||
| ^
|
||||
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
|
||||
%Error: Cannot continue
|
||||
|
|
|
|||
|
|
@ -16,14 +16,6 @@ module t (
|
|||
val = ~val;
|
||||
end
|
||||
|
||||
property p_alw;
|
||||
always [2:5] a;
|
||||
endproperty
|
||||
|
||||
property p_s_alw;
|
||||
s_always [2:5] a;
|
||||
endproperty
|
||||
|
||||
property p_ev;
|
||||
eventually [2:5] a;
|
||||
endproperty
|
||||
|
|
|
|||
|
|
@ -650,6 +650,22 @@ module Vt_debug_emitv_t;
|
|||
$display("pass");
|
||||
end
|
||||
end
|
||||
begin : assert_prop_always
|
||||
assert property (@(posedge clk) always ['sh0:
|
||||
'sh3] in
|
||||
) begin
|
||||
end
|
||||
else begin
|
||||
end
|
||||
end
|
||||
begin : assert_prop_s_always
|
||||
assert property (@(posedge clk) s_always ['sh1:
|
||||
'sh2] in
|
||||
) begin
|
||||
end
|
||||
else begin
|
||||
end
|
||||
end
|
||||
int signed a;
|
||||
int signed ao;
|
||||
initial begin
|
||||
|
|
|
|||
|
|
@ -330,6 +330,9 @@ module t (/*AUTOARG*/
|
|||
cover_concurrent: cover property(prop);
|
||||
cover_concurrent_stmt: cover property(prop) $display("pass");
|
||||
|
||||
assert_prop_always: assert property (@(posedge clk) always [0:3] in);
|
||||
assert_prop_s_always: assert property (@(posedge clk) s_always [1:2] in);
|
||||
|
||||
|
||||
int a;
|
||||
int ao;
|
||||
|
|
|
|||
|
|
@ -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('vlt')
|
||||
|
||||
test.compile()
|
||||
|
||||
test.execute()
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,107 @@
|
|||
// 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 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
|
||||
);
|
||||
|
||||
bit [63:0] crc = 64'h5aef0c8d_d70a4497;
|
||||
int cyc = 0;
|
||||
logic a_high = 1'b1;
|
||||
logic a_low = 1'b0;
|
||||
wire a_rand = crc[0];
|
||||
wire rst_rand = crc[5];
|
||||
|
||||
// Per-assertion queues record the simulation cyc on each pass / else fire.
|
||||
// For "always [m:n] P" the action runs at cyc=K+n on success and at the
|
||||
// detected-violation cyc on failure -- both deterministic given the inputs.
|
||||
int high_bounded_pass_q[$];
|
||||
int high_sbounded_pass_q[$];
|
||||
int high_degenerate_pass_q[$];
|
||||
int low_bounded_fail_q[$];
|
||||
int low_degenerate_fail_q[$];
|
||||
int rand_bounded_pass_q[$];
|
||||
int rand_bounded_fail_q[$];
|
||||
int disable_bounded_pass_q[$];
|
||||
int disable_bounded_fail_q[$];
|
||||
|
||||
// Bare always (collapses to immediate P).
|
||||
assert property (@(posedge clk) always 1'b1);
|
||||
|
||||
// Bounded weak always over constant-true input.
|
||||
assert property (@(posedge clk) always [0:3] a_high) high_bounded_pass_q.push_back(cyc);
|
||||
|
||||
// Bounded strong s_always over constant-true input.
|
||||
assert property (@(posedge clk) s_always [1:2] a_high) high_sbounded_pass_q.push_back(cyc);
|
||||
|
||||
// Degenerate [0:0]: equivalent to immediate sample.
|
||||
assert property (@(posedge clk) always [0:0] a_high) high_degenerate_pass_q.push_back(cyc);
|
||||
|
||||
// Constant-false: every attempt fails.
|
||||
assert property (@(posedge clk) always [0:3] a_low)
|
||||
;
|
||||
else low_bounded_fail_q.push_back(cyc);
|
||||
|
||||
assert property (@(posedge clk) always [0:0] a_low)
|
||||
;
|
||||
else low_degenerate_fail_q.push_back(cyc);
|
||||
|
||||
// CRC-driven random input: window [cyc..cyc+3] of a_rand.
|
||||
assert property (@(posedge clk) always [0:3] a_rand) rand_bounded_pass_q.push_back(cyc);
|
||||
else rand_bounded_fail_q.push_back(cyc);
|
||||
|
||||
// disable iff suppresses attempts whose start cyc has rst_rand=1.
|
||||
assert property (@(posedge clk) disable iff (rst_rand) always [0:3] a_rand)
|
||||
disable_bounded_pass_q.push_back(cyc);
|
||||
else disable_bounded_fail_q.push_back(cyc);
|
||||
|
||||
// Bare always inside named property.
|
||||
property p_always_true;
|
||||
@(posedge clk) always (1'b1);
|
||||
endproperty
|
||||
assert property (p_always_true);
|
||||
|
||||
// disable iff inside named property.
|
||||
property p_disable_named;
|
||||
@(posedge clk) disable iff (rst_rand) always [1:2] a_high;
|
||||
endproperty
|
||||
assert property (p_disable_named);
|
||||
|
||||
always @(posedge clk) begin
|
||||
cyc <= cyc + 1;
|
||||
crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
|
||||
if (cyc == 19) begin
|
||||
// Constant-true window [0:3]: K=0..16 succeed at cyc K+3 = 3..19.
|
||||
`checkd(high_bounded_pass_q.size(), 17);
|
||||
`checkd(high_bounded_pass_q[0], 3);
|
||||
`checkd(high_bounded_pass_q[$], 19);
|
||||
// Strong [1:2]: K=0..17 succeed at cyc K+2 = 2..19.
|
||||
`checkd(high_sbounded_pass_q.size(), 18);
|
||||
`checkd(high_sbounded_pass_q[0], 2);
|
||||
`checkd(high_sbounded_pass_q[$], 19);
|
||||
// Degenerate [0:0]: K=0..19 succeed at cyc K = 0..19.
|
||||
`checkd(high_degenerate_pass_q.size(), 20);
|
||||
`checkd(high_degenerate_pass_q[0], 0);
|
||||
`checkd(high_degenerate_pass_q[$], 19);
|
||||
// Constant-false: every attempt fails immediately.
|
||||
`checkd(low_bounded_fail_q.size(), 20);
|
||||
`checkd(low_degenerate_fail_q.size(), 20);
|
||||
// CRC + disable streams: counts pinned (cross-checked against Questa).
|
||||
`checkd(rand_bounded_pass_q.size(), 0);
|
||||
`checkd(rand_bounded_fail_q.size(), 20);
|
||||
`checkd(disable_bounded_pass_q.size(), 0);
|
||||
`checkd(disable_bounded_fail_q.size(), 13);
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
end
|
||||
end
|
||||
|
||||
endmodule
|
||||
|
|
@ -0,0 +1,34 @@
|
|||
%Error: t/t_prop_always_bad.v:13:20: always range low bound must be non-negative (IEEE 1800-2023 16.12.11)
|
||||
: ... note: In instance 't'
|
||||
13 | assert property (always [-1:3] a);
|
||||
| ^~~~~~
|
||||
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
|
||||
%Error: t/t_prop_always_bad.v:14:20: always range high bound must be >= low bound (IEEE 1800-2023 16.12.11)
|
||||
: ... note: In instance 't'
|
||||
14 | assert property (always [5:2] a);
|
||||
| ^~~~~~
|
||||
%Error: t/t_prop_always_bad.v:15:28: Expecting expression to be constant, but variable isn't const: 'x'
|
||||
: ... note: In instance 't'
|
||||
15 | assert property (always [x:3] a);
|
||||
| ^
|
||||
%Error: t/t_prop_always_bad.v:15:20: always range low bound must be a constant expression (IEEE 1800-2023 16.12.11)
|
||||
: ... note: In instance 't'
|
||||
15 | assert property (always [x:3] a);
|
||||
| ^~~~~~
|
||||
%Error: t/t_prop_always_bad.v:16:30: Expecting expression to be constant, but variable isn't const: 'x'
|
||||
: ... note: In instance 't'
|
||||
16 | assert property (always [1:x] a);
|
||||
| ^
|
||||
%Error: t/t_prop_always_bad.v:16:20: always range high bound must be a constant expression (IEEE 1800-2023 16.12.11)
|
||||
: ... note: In instance 't'
|
||||
16 | assert property (always [1:x] a);
|
||||
| ^~~~~~
|
||||
%Error: t/t_prop_always_bad.v:17:20: s_always range must be bounded (IEEE 1800-2023 16.12.11)
|
||||
: ... note: In instance 't'
|
||||
17 | assert property (s_always a);
|
||||
| ^~~~~~~~
|
||||
%Error: t/t_prop_always_bad.v:18:20: s_always range must be bounded (IEEE 1800-2023 16.12.11)
|
||||
: ... note: In instance 't'
|
||||
18 | assert property (s_always [1:$] a);
|
||||
| ^~~~~~~~
|
||||
%Error: Exiting due to
|
||||
|
|
@ -0,0 +1,16 @@
|
|||
#!/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('vlt')
|
||||
|
||||
test.lint(expect_filename=test.golden_filename, fails=True)
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,20 @@
|
|||
// 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
|
||||
|
||||
module t (input clk);
|
||||
int x;
|
||||
logic a;
|
||||
|
||||
default clocking cb @(posedge clk); endclocking
|
||||
|
||||
assert property (always [-1:3] a);
|
||||
assert property (always [5:2] a);
|
||||
assert property (always [x:3] a);
|
||||
assert property (always [1:x] a);
|
||||
assert property (s_always a);
|
||||
assert property (s_always [1:$] a);
|
||||
|
||||
endmodule
|
||||
|
|
@ -0,0 +1,18 @@
|
|||
%Error-UNSUPPORTED: t/t_prop_always_unsup.v:12:35: Unsupported: unbounded always range (always [m:$])
|
||||
: ... note: In instance 't'
|
||||
12 | assert property (@(posedge clk) always [2:$] a);
|
||||
| ^~~~~~
|
||||
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
|
||||
%Error-UNSUPPORTED: t/t_prop_always_unsup.v:15:35: Unsupported: property/sequence operator inside bounded always (IEEE 1800-2023 16.12.11)
|
||||
: ... note: In instance 't'
|
||||
15 | assert property (@(posedge clk) always [0:3] (a |-> b));
|
||||
| ^~~~~~
|
||||
%Error-UNSUPPORTED: t/t_prop_always_unsup.v:16:35: Unsupported: property/sequence operator inside bounded always (IEEE 1800-2023 16.12.11)
|
||||
: ... note: In instance 't'
|
||||
16 | assert property (@(posedge clk) always [0:3] (a |=> b));
|
||||
| ^~~~~~
|
||||
%Error-UNSUPPORTED: t/t_prop_always_unsup.v:17:35: Unsupported: property/sequence operator inside bounded always (IEEE 1800-2023 16.12.11)
|
||||
: ... note: In instance 't'
|
||||
17 | assert property (@(posedge clk) always [0:3] (a ##1 b));
|
||||
| ^~~~~~
|
||||
%Error: Exiting due to
|
||||
|
|
@ -0,0 +1,16 @@
|
|||
#!/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('vlt')
|
||||
|
||||
test.lint(expect_filename=test.golden_filename, fails=True)
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,19 @@
|
|||
// 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
|
||||
|
||||
module t (input clk);
|
||||
logic a;
|
||||
logic b;
|
||||
|
||||
// IEEE-legal but engine has no sim-end liveness.
|
||||
assert property (@(posedge clk) always [2:$] a);
|
||||
|
||||
// Nested sequence/property operators inside bounded always.
|
||||
assert property (@(posedge clk) always [0:3] (a |-> b));
|
||||
assert property (@(posedge clk) always [0:3] (a |=> b));
|
||||
assert property (@(posedge clk) always [0:3] (a ##1 b));
|
||||
|
||||
endmodule
|
||||
|
|
@ -23,21 +23,12 @@
|
|||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:63:5: Unsupported: s_nexttime[] (in property expression)
|
||||
63 | s_nexttime [2] a;
|
||||
| ^~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:67:14: Unsupported: always (in property expression)
|
||||
67 | nexttime always a;
|
||||
| ^~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:67:5: Unsupported: nexttime (in property expression)
|
||||
67 | nexttime always a;
|
||||
| ^~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:71:18: Unsupported: always (in property expression)
|
||||
71 | nexttime [2] always a;
|
||||
| ^~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:71:5: Unsupported: nexttime[] (in property expression)
|
||||
71 | nexttime [2] always a;
|
||||
| ^~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:75:18: Unsupported: always (in property expression)
|
||||
75 | nexttime [2] always a;
|
||||
| ^~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:75:5: Unsupported: nexttime[] (in property expression)
|
||||
75 | nexttime [2] always a;
|
||||
| ^~~~~~~~
|
||||
|
|
@ -47,9 +38,6 @@
|
|||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:79:5: Unsupported: nexttime (in property expression)
|
||||
79 | nexttime s_eventually a;
|
||||
| ^~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:83:33: Unsupported: always (in property expression)
|
||||
83 | nexttime s_eventually [2:$] always a;
|
||||
| ^~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:83:14: Unsupported: s_eventually[] (in property expression)
|
||||
83 | nexttime s_eventually [2:$] always a;
|
||||
| ^~~~~~~~~~~~
|
||||
|
|
|
|||
|
|
@ -5,58 +5,40 @@
|
|||
%Error-UNSUPPORTED: t/t_property_unsup.v:80:20: Unsupported: eventually[] (in property expression)
|
||||
80 | assert property (eventually[0: 2] counter == 3);
|
||||
| ^~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:90:21: Unsupported: always (in property expression)
|
||||
90 | assert property ((always a) implies (always a));
|
||||
| ^~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:90:40: Unsupported: always (in property expression)
|
||||
90 | assert property ((always a) implies (always a));
|
||||
| ^~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:92:26: Unsupported: always (in property expression)
|
||||
92 | assert property ((a or(always b)) implies (a or(always b)));
|
||||
| ^~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:92:51: Unsupported: always (in property expression)
|
||||
92 | assert property ((a or(always b)) implies (a or(always b)));
|
||||
| ^~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:94:21: Unsupported: eventually[] (in property expression)
|
||||
94 | assert property ((eventually[0: 1] a) implies (eventually[0: 1] a));
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:90:21: Unsupported: eventually[] (in property expression)
|
||||
90 | assert property ((eventually[0: 1] a) implies (eventually[0: 1] a));
|
||||
| ^~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:94:50: Unsupported: eventually[] (in property expression)
|
||||
94 | assert property ((eventually[0: 1] a) implies (eventually[0: 1] a));
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:90:50: Unsupported: eventually[] (in property expression)
|
||||
90 | assert property ((eventually[0: 1] a) implies (eventually[0: 1] a));
|
||||
| ^~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:96:21: Unsupported: s_eventually (in property expression)
|
||||
96 | assert property ((s_eventually a) implies (s_eventually a));
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:92:21: Unsupported: s_eventually (in property expression)
|
||||
92 | assert property ((s_eventually a) implies (s_eventually a));
|
||||
| ^~~~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:96:46: Unsupported: s_eventually (in property expression)
|
||||
96 | assert property ((s_eventually a) implies (s_eventually a));
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:92:46: Unsupported: s_eventually (in property expression)
|
||||
92 | assert property ((s_eventually a) implies (s_eventually a));
|
||||
| ^~~~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:106:23: Unsupported: #-# (in property expression)
|
||||
106 | assert property ((a #-# b) implies (a #-# b));
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:102:23: Unsupported: #-# (in property expression)
|
||||
102 | assert property ((a #-# b) implies (a #-# b));
|
||||
| ^~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:106:41: Unsupported: #-# (in property expression)
|
||||
106 | assert property ((a #-# b) implies (a #-# b));
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:102:41: Unsupported: #-# (in property expression)
|
||||
102 | assert property ((a #-# b) implies (a #-# b));
|
||||
| ^~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:116:21: Unsupported: always (in property expression)
|
||||
116 | assert property ((always a) iff (always a));
|
||||
| ^~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:116:36: Unsupported: always (in property expression)
|
||||
116 | assert property ((always a) iff (always a));
|
||||
| ^~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:118:21: Unsupported: eventually[] (in property expression)
|
||||
118 | assert property ((eventually[0: 1] a) iff (eventually[0: 1] a));
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:112:21: Unsupported: eventually[] (in property expression)
|
||||
112 | assert property ((eventually[0: 1] a) iff (eventually[0: 1] a));
|
||||
| ^~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:118:46: Unsupported: eventually[] (in property expression)
|
||||
118 | assert property ((eventually[0: 1] a) iff (eventually[0: 1] a));
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:112:46: Unsupported: eventually[] (in property expression)
|
||||
112 | assert property ((eventually[0: 1] a) iff (eventually[0: 1] a));
|
||||
| ^~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:120:21: Unsupported: s_eventually (in property expression)
|
||||
120 | assert property ((s_eventually a) iff (s_eventually a));
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:114:21: Unsupported: s_eventually (in property expression)
|
||||
114 | assert property ((s_eventually a) iff (s_eventually a));
|
||||
| ^~~~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:120:42: Unsupported: s_eventually (in property expression)
|
||||
120 | assert property ((s_eventually a) iff (s_eventually a));
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:114:42: Unsupported: s_eventually (in property expression)
|
||||
114 | assert property ((s_eventually a) iff (s_eventually a));
|
||||
| ^~~~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:130:23: Unsupported: #-# (in property expression)
|
||||
130 | assert property ((a #-# b) iff (a #-# b));
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:124:23: Unsupported: #-# (in property expression)
|
||||
124 | assert property ((a #-# b) iff (a #-# b));
|
||||
| ^~~
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:130:37: Unsupported: #-# (in property expression)
|
||||
130 | assert property ((a #-# b) iff (a #-# b));
|
||||
%Error-UNSUPPORTED: t/t_property_unsup.v:124:37: Unsupported: #-# (in property expression)
|
||||
124 | assert property ((a #-# b) iff (a #-# b));
|
||||
| ^~~
|
||||
%Error: Exiting due to
|
||||
|
|
|
|||
|
|
@ -86,10 +86,6 @@ module sva_implies2 (
|
|||
b
|
||||
);
|
||||
|
||||
p0 :
|
||||
assert property ((always a) implies (always a));
|
||||
p1 :
|
||||
assert property ((a or(always b)) implies (a or(always b)));
|
||||
p2 :
|
||||
assert property ((eventually[0: 1] a) implies (eventually[0: 1] a));
|
||||
p3 :
|
||||
|
|
@ -112,8 +108,6 @@ module sva_iff2 (
|
|||
b
|
||||
);
|
||||
|
||||
p0 :
|
||||
assert property ((always a) iff (always a));
|
||||
p1 :
|
||||
assert property ((eventually[0: 1] a) iff (eventually[0: 1] a));
|
||||
p2 :
|
||||
|
|
|
|||
Loading…
Reference in New Issue