Support `weak`/`strong` keywords in property expressions (#8054)
Signed-off-by: Artur Bieniek <abieniek@antmicro.com>
This commit is contained in:
Artur Bieniek
GitHub
parent
e413e67ab3
commit
1a4bcac666
|
|
@ -2596,6 +2596,12 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
});
|
||||
}
|
||||
|
||||
static VPropStrength effectiveAssertPropStrength(const AstPropSpec* const propSpecp) {
|
||||
if (propSpecp->propStrength() != VPropStrength::DEFAULT) return propSpecp->propStrength();
|
||||
return propSpecp->fileline()->language() <= V3LangCode::L1800_2005 ? VPropStrength::STRONG
|
||||
: VPropStrength::WEAK;
|
||||
}
|
||||
|
||||
// Bare `assert property (p until q)` with boolean operands stays on
|
||||
// V3AssertPre's AstLoop lowering, which preserves per-attempt action-block
|
||||
// firings that this NFA's single-bit aggregated state cannot. Strong bare
|
||||
|
|
@ -2937,7 +2943,15 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
if (hoistClockedSeq(specp)) return;
|
||||
}
|
||||
|
||||
AstNode* const propp = assertp->propp();
|
||||
AstPropSpec* const propp = VN_AS(assertp->propp(), PropSpec);
|
||||
const bool isCover = VN_IS(assertp, Cover);
|
||||
if (!isCover && effectiveAssertPropStrength(propp) == VPropStrength::STRONG) {
|
||||
propp->v3warn(E_UNSUPPORTED,
|
||||
"Unsupported: strong property in " + assertp->verilogKwd() + ".");
|
||||
replaceBodyOnBuildError(assertp->fileline(), propp, /*errorEmitted=*/true);
|
||||
return;
|
||||
}
|
||||
|
||||
if (!hasMultiCycleExpr(propp)) return;
|
||||
if (isBareTopLevelUntil(propp)) return;
|
||||
|
||||
|
|
@ -2963,27 +2977,23 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
|
||||
AstSenTree* senTreep = assertp->sentreep();
|
||||
bool senTreeOwned = false; // True if we created senTreep locally
|
||||
AstPropSpec* const propSpecp = VN_CAST(assertp->propp(), PropSpec);
|
||||
UASSERT_OBJ(propSpecp, assertp, "Concurrent assertion must have PropSpec");
|
||||
AstCover* const coverp = VN_CAST(assertp, Cover);
|
||||
const bool isCover = coverp != nullptr;
|
||||
const bool isCoverSeq = coverp && coverp->isCoverSeq();
|
||||
// A sequence event control is not an assertion directive; no default
|
||||
// disable iff, no assertion control
|
||||
const bool isSeqEvent = coverp && coverp->isSeqEvent();
|
||||
// Inherit module defaults (IEEE 14.12, 16.15) when assertion has none.
|
||||
if (!propSpecp->sensesp() && m_defaultClockingp) {
|
||||
propSpecp->sensesp(m_defaultClockingp->sensesp()->cloneTree(true));
|
||||
if (!propp->sensesp() && m_defaultClockingp) {
|
||||
propp->sensesp(m_defaultClockingp->sensesp()->cloneTree(true));
|
||||
}
|
||||
if (!propSpecp->disablep() && m_defaultDisablep && !isSeqEvent) {
|
||||
propSpecp->disablep(m_defaultDisablep->condp()->cloneTreePure(true));
|
||||
if (!propp->disablep() && m_defaultDisablep && !isSeqEvent) {
|
||||
propp->disablep(m_defaultDisablep->condp()->cloneTreePure(true));
|
||||
}
|
||||
if (!senTreep && propSpecp->sensesp()) {
|
||||
senTreep
|
||||
= new AstSenTree{propSpecp->fileline(), propSpecp->sensesp()->cloneTree(true)};
|
||||
if (!senTreep && propp->sensesp()) {
|
||||
senTreep = new AstSenTree{propp->fileline(), propp->sensesp()->cloneTree(true)};
|
||||
senTreeOwned = true;
|
||||
}
|
||||
AstNodeExpr* disableExprp = propSpecp->disablep();
|
||||
AstNodeExpr* disableExprp = propp->disablep();
|
||||
if (!senTreep) return;
|
||||
|
||||
// NFA lowering clones repeated operands and may hoist them into an
|
||||
|
|
@ -2992,7 +3002,7 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
{
|
||||
VL_RESTORER(m_sampledValueClockp);
|
||||
m_sampledValueClockp = senTreep;
|
||||
iterate(propSpecp->propp());
|
||||
iterate(propp->propp());
|
||||
}
|
||||
|
||||
FileLine* const flp = assertp->fileline();
|
||||
|
|
@ -3007,7 +3017,7 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
// replace the body on real semantic errors. Any hoisted temps
|
||||
// from this attempt become orphan MODULETEMPs; V3Dead removes
|
||||
// them along with the dead always_comb driver.
|
||||
replaceBodyOnBuildError(flp, propSpecp, result.errorEmitted);
|
||||
replaceBodyOnBuildError(flp, propp, result.errorEmitted);
|
||||
if (senTreeOwned) VL_DO_DANGLING(pushDeletep(senTreep), senTreep);
|
||||
return;
|
||||
}
|
||||
|
|
@ -3015,7 +3025,7 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
// Build succeeded. Now create snapshot mechanism for disable iff if needed.
|
||||
// Done here (not before build) so failed builds don't pollute the AST.
|
||||
const DisableVars disableVars
|
||||
= createDisableCounterMechanism(flp, disableExprp, parts.hasImplication, propSpecp);
|
||||
= createDisableCounterMechanism(flp, disableExprp, parts.hasImplication, propp);
|
||||
AstVar* const disableCntVarp = disableVars.cntp;
|
||||
AstVar* const snapshotVarp = disableVars.snapp;
|
||||
const bool disableExprUnlinked = disableCntVarp && disableExprp;
|
||||
|
|
@ -3087,7 +3097,7 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
// does not use it.
|
||||
VL_DO_DANGLING(outputExprp->deleteTree(), outputExprp);
|
||||
} else {
|
||||
AstNode* const innerPropp = propSpecp->propp();
|
||||
AstNode* const innerPropp = propp->propp();
|
||||
innerPropp->replaceWith(outputExprp);
|
||||
VL_DO_DANGLING(pushDeletep(innerPropp), innerPropp);
|
||||
// If we collected per-mid (N==1) but didn't clone, drop the spare.
|
||||
|
|
|
|||
|
|
@ -299,6 +299,34 @@ constexpr VAssertType::en operator|(VAssertType::en lhs, VAssertType::en rhs) {
|
|||
|
||||
// ######################################################################
|
||||
|
||||
class VPropStrength final {
|
||||
public:
|
||||
enum en : uint8_t {
|
||||
DEFAULT = 0, // Resolve from assertion/coverage context
|
||||
WEAK,
|
||||
STRONG,
|
||||
};
|
||||
enum en m_e;
|
||||
// cppcheck-suppress noExplicitConstructor
|
||||
constexpr VPropStrength(en _e)
|
||||
: m_e{_e} {}
|
||||
const char* ascii() const {
|
||||
static const char* const names[] = {"default", "weak", "strong"};
|
||||
return names[m_e];
|
||||
}
|
||||
};
|
||||
constexpr bool operator==(const VPropStrength& lhs, const VPropStrength& rhs) {
|
||||
return lhs.m_e == rhs.m_e;
|
||||
}
|
||||
constexpr bool operator==(const VPropStrength& lhs, VPropStrength::en rhs) {
|
||||
return lhs.m_e == rhs;
|
||||
}
|
||||
constexpr bool operator!=(const VPropStrength& lhs, VPropStrength::en rhs) {
|
||||
return lhs.m_e != rhs;
|
||||
}
|
||||
|
||||
// ######################################################################
|
||||
|
||||
class VAttrType final {
|
||||
public:
|
||||
// clang-format off
|
||||
|
|
|
|||
|
|
@ -1687,17 +1687,24 @@ class AstPropSpec final : public AstNode {
|
|||
// @astgen op1 := sensesp : Optional[AstSenItem]
|
||||
// @astgen op2 := disablep : Optional[AstNodeExpr]
|
||||
// @astgen op3 := propp : AstNode
|
||||
VPropStrength m_propStrength = VPropStrength::DEFAULT;
|
||||
|
||||
public:
|
||||
AstPropSpec(FileLine* fl, AstSenItem* sensesp, AstNodeExpr* disablep, AstNode* propp)
|
||||
: ASTGEN_SUPER_PropSpec(fl) {
|
||||
AstPropSpec(FileLine* fl, AstSenItem* sensesp, AstNodeExpr* disablep, AstNode* propp,
|
||||
VPropStrength propStrength = VPropStrength::DEFAULT)
|
||||
: ASTGEN_SUPER_PropSpec(fl)
|
||||
, m_propStrength{propStrength} {
|
||||
this->sensesp(sensesp);
|
||||
this->disablep(disablep);
|
||||
this->propp(propp);
|
||||
}
|
||||
ASTGEN_MEMBERS_AstPropSpec;
|
||||
void dump(std::ostream& str) const override;
|
||||
void dumpJson(std::ostream& str) const override;
|
||||
bool hasDType() const override VL_MT_SAFE {
|
||||
return true;
|
||||
} // Used under Cover, which expects a bool child
|
||||
VPropStrength propStrength() const { return m_propStrength; }
|
||||
};
|
||||
class AstPull final : public AstNode {
|
||||
// @astgen op1 := lhsp : AstNodeExpr
|
||||
|
|
|
|||
|
|
@ -1996,6 +1996,18 @@ string AstBasicDType::prettyDTypeName(bool) const {
|
|||
void AstNodeExpr::dump(std::ostream& str) const { this->AstNode::dump(str); }
|
||||
void AstNodeExpr::dumpJson(std::ostream& str) const { dumpJsonGen(str); }
|
||||
|
||||
void AstPropSpec::dump(std::ostream& str) const {
|
||||
this->AstNode::dump(str);
|
||||
if (propStrength() != VPropStrength::DEFAULT) {
|
||||
str << " [" << VString::upcase(propStrength().ascii()) << "]";
|
||||
}
|
||||
}
|
||||
void AstPropSpec::dumpJson(std::ostream& str) const {
|
||||
if (propStrength() != VPropStrength::DEFAULT)
|
||||
dumpJsonStr(str, "strength", propStrength().ascii());
|
||||
dumpJsonGen(str);
|
||||
}
|
||||
|
||||
AstConst::~AstConst() {
|
||||
// Only rare constants carry originating parameter-name metadata. For all other AstConst nodes,
|
||||
// the V3Number bit keeps this destructor from touching AstNetlist's side table. When the bit
|
||||
|
|
|
|||
|
|
@ -1130,7 +1130,12 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
|
|||
}
|
||||
|
||||
puts(" ");
|
||||
if (nodep->propStrength() != VPropStrength::DEFAULT) {
|
||||
puts(nodep->propStrength().ascii());
|
||||
puts("(");
|
||||
}
|
||||
iterateConstNull(nodep->propp());
|
||||
if (nodep->propStrength() != VPropStrength::DEFAULT) puts(")");
|
||||
puts("\n");
|
||||
}
|
||||
void visit(AstPExpr* nodep) override { iterateConst(nodep->bodyp()); }
|
||||
|
|
|
|||
|
|
@ -6686,16 +6686,27 @@ sequence_declarationBody<nodep>: // IEEE: part of sequence_declaration
|
|||
property_spec<propSpecp>: // IEEE: property_spec
|
||||
//UNSUP: This rule has been super-specialized to what is supported now
|
||||
//UNSUP remove below
|
||||
'@' '(' senitem ')' yDISABLE yIFF '(' expr ')' pexpr
|
||||
{ $$ = new AstPropSpec{$1, $3, $8, $10}; }
|
||||
| '@' '(' senitem ')' pexpr
|
||||
{ $$ = new AstPropSpec{$1, $3, nullptr, $5}; }
|
||||
| '@' senitemVar pexpr
|
||||
{ $$ = new AstPropSpec{$1, $2, nullptr, $3}; }
|
||||
| yDISABLE yIFF '(' expr ')' '@' '(' senitem ')' pexpr
|
||||
{ $$ = new AstPropSpec{$1, $8, $4, $10}; }
|
||||
| yDISABLE yIFF '(' expr ')' pexpr { $$ = new AstPropSpec{$4->fileline(), nullptr, $4, $6}; }
|
||||
| pexpr { $$ = new AstPropSpec{$1->fileline(), nullptr, nullptr, $1}; }
|
||||
'@' '(' senitem ')' yDISABLE yIFF '(' expr ')' property_exprSpec
|
||||
{ $$ = $10; $$->fileline($1); $$->sensesp($3); $$->disablep($8); }
|
||||
| '@' '(' senitem ')' property_exprSpec
|
||||
{ $$ = $5; $$->fileline($1); $$->sensesp($3); }
|
||||
| '@' senitemVar property_exprSpec
|
||||
{ $$ = $3; $$->fileline($1); $$->sensesp($2); }
|
||||
| yDISABLE yIFF '(' expr ')' '@' '(' senitem ')' property_exprSpec
|
||||
{ $$ = $10; $$->fileline($1); $$->sensesp($8); $$->disablep($4); }
|
||||
//UNSUP remove above
|
||||
| yDISABLE yIFF '(' expr ')' property_exprSpec
|
||||
{ $$ = $6; $$->fileline($4->fileline()); $$->disablep($4); }
|
||||
| property_exprSpec { $$ = $1; }
|
||||
;
|
||||
|
||||
property_exprSpec<propSpecp>: // A property expression plus explicit weak/strong strength
|
||||
pexpr
|
||||
{ $$ = new AstPropSpec{$1->fileline(), nullptr, nullptr, $1}; }
|
||||
| ySTRONG '(' sexpr ')'
|
||||
{ $$ = new AstPropSpec{$1, nullptr, nullptr, $3, VPropStrength::STRONG}; }
|
||||
| yWEAK '(' sexpr ')'
|
||||
{ $$ = new AstPropSpec{$1, nullptr, nullptr, $3, VPropStrength::WEAK}; }
|
||||
;
|
||||
|
||||
property_exprCaseIf<nodeExprp>: // IEEE: part of property_expr for if/case
|
||||
|
|
@ -6761,10 +6772,6 @@ pexpr<nodeExprp>: // IEEE: property_expr (The name pexpr is important as regex
|
|||
//
|
||||
yNOT pexpr
|
||||
{ $$ = new AstLogNot{$1, $2, /*fromProperty=*/true}; }
|
||||
| ySTRONG '(' sexpr ')'
|
||||
{ $$ = $3; BBUNSUP($2, "Unsupported: strong (in property expression)"); }
|
||||
| yWEAK '(' sexpr ')'
|
||||
{ $$ = $3; BBUNSUP($2, "Unsupported: weak (in property expression)"); }
|
||||
// // IEEE: pexpr yOR pexpr
|
||||
// // IEEE: pexpr yAND pexpr
|
||||
// // Under ~p~sexpr and/or ~p~sexpr
|
||||
|
|
|
|||
|
|
@ -21,6 +21,7 @@ module t (
|
|||
int n_imp_ov = 0; // cover property (a |-> b) -- overlapped implication
|
||||
int n_seq = 0; // cover property (a ##1 b) -- identity with |=>
|
||||
int n_seq0 = 0; // cover property (a ##0 b) -- identity with |->
|
||||
int n_strong = 0; // cover property (strong(a ##1 b))
|
||||
int n_bool = 0; // cover property (a) -- bare boolean baseline
|
||||
int n_named = 0; // cover property (named pr) -- identity with |=>
|
||||
|
||||
|
|
@ -42,6 +43,8 @@ module t (
|
|||
cover property (a ##1 b) n_seq++;
|
||||
cp_seq0 :
|
||||
cover property (a ##0 b) n_seq0++;
|
||||
cp_strong :
|
||||
cover property (strong(a ##1 b)) n_strong++;
|
||||
cp_bool :
|
||||
cover property (a) n_bool++;
|
||||
cp_named :
|
||||
|
|
@ -62,6 +65,7 @@ module t (
|
|||
// corresponding sequence cover, not the vacuous implication value.
|
||||
`checkd(n_imp_no, n_seq); // Other sims: pass, 73
|
||||
`checkd(n_imp_ov, n_seq0); // Other sims: pass, 45
|
||||
`checkd(n_strong, n_seq);
|
||||
// A named-property cover lowers the same implication, so it also counts
|
||||
// non-vacuously (regression guard for the property-inlining path).
|
||||
`checkd(n_named, n_imp_no);
|
||||
|
|
@ -69,6 +73,7 @@ module t (
|
|||
`checkd(n_imp_ov, 27); // Other sims: pass, 73
|
||||
`checkd(n_seq, 28); // Other sims: 45, 27
|
||||
`checkd(n_seq0, 27);
|
||||
`checkd(n_strong, 28);
|
||||
`checkd(n_bool, 55); // Other sims: pass, 25
|
||||
`checkd(n_named, 28); // Other sims: 73, 54, 54
|
||||
end
|
||||
|
|
|
|||
|
|
@ -756,6 +756,18 @@ module Vt_debug_emitv_t;
|
|||
else begin
|
||||
end
|
||||
end
|
||||
begin : assert_prop_weak
|
||||
assert property (@(posedge clk) weak(in)
|
||||
) begin
|
||||
end
|
||||
else begin
|
||||
end
|
||||
end
|
||||
begin : cover_prop_strong
|
||||
cover property (@(posedge clk) strong(in)
|
||||
) begin
|
||||
end
|
||||
end
|
||||
int signed a;
|
||||
int signed ao;
|
||||
initial begin
|
||||
|
|
|
|||
|
|
@ -365,7 +365,8 @@ module t (/*AUTOARG*/
|
|||
assert_prop_reject_on: assert property (@(posedge clk) reject_on (in) in);
|
||||
assert_prop_sync_accept_on: assert property (@(posedge clk) sync_accept_on (in) in);
|
||||
assert_prop_sync_reject_on: assert property (@(posedge clk) sync_reject_on (in) in);
|
||||
|
||||
assert_prop_weak: assert property (@(posedge clk) weak(in));
|
||||
cover_prop_strong: cover property (@(posedge clk) strong(in));
|
||||
|
||||
int a;
|
||||
int ao;
|
||||
|
|
|
|||
|
|
@ -0,0 +1,47 @@
|
|||
%Error: t/t_prop_bad.v:14:40: syntax error, unexpected s_eventually, expecting IDENTIFIER-for-type
|
||||
14 | assert property (@(posedge clk) weak(s_eventually a));
|
||||
| ^~~~~~~~~~~~
|
||||
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
|
||||
%Error: t/t_prop_bad.v:15:40: syntax error, unexpected s_always, expecting IDENTIFIER-for-type
|
||||
15 | assert property (@(posedge clk) weak(s_always [1:2] a));
|
||||
| ^~~~~~~~
|
||||
%Error: t/t_prop_bad.v:16:40: syntax error, unexpected nexttime, expecting IDENTIFIER-for-type
|
||||
16 | assert property (@(posedge clk) weak(nexttime a));
|
||||
| ^~~~~~~~
|
||||
%Error: t/t_prop_bad.v:17:40: syntax error, unexpected s_nexttime, expecting IDENTIFIER-for-type
|
||||
17 | assert property (@(posedge clk) weak(s_nexttime a));
|
||||
| ^~~~~~~~~~
|
||||
%Error: t/t_prop_bad.v:18:40: syntax error, unexpected always, expecting IDENTIFIER-for-type
|
||||
18 | assert property (@(posedge clk) weak(always a));
|
||||
| ^~~~~~
|
||||
%Error: t/t_prop_bad.v:19:40: syntax error, unexpected eventually, expecting IDENTIFIER-for-type
|
||||
19 | assert property (@(posedge clk) weak(eventually [1:2] a));
|
||||
| ^~~~~~~~~~
|
||||
%Error: t/t_prop_bad.v:20:42: syntax error, unexpected |->
|
||||
20 | assert property (@(posedge clk) weak(a |-> b));
|
||||
| ^~~
|
||||
%Error: t/t_prop_bad.v:21:42: syntax error, unexpected |=>
|
||||
21 | assert property (@(posedge clk) weak(a |=> b));
|
||||
| ^~~
|
||||
%Error: t/t_prop_bad.v:22:42: syntax error, unexpected implies
|
||||
22 | assert property (@(posedge clk) weak(a implies b));
|
||||
| ^~~~~~~
|
||||
%Error: t/t_prop_bad.v:23:42: syntax error, unexpected iff
|
||||
23 | assert property (@(posedge clk) weak(a iff b));
|
||||
| ^~~
|
||||
%Error: t/t_prop_bad.v:24:40: syntax error, unexpected accept_on, expecting IDENTIFIER-for-type
|
||||
24 | assert property (@(posedge clk) weak(accept_on (a) b));
|
||||
| ^~~~~~~~~
|
||||
%Error: t/t_prop_bad.v:25:40: syntax error, unexpected reject_on, expecting IDENTIFIER-for-type
|
||||
25 | assert property (@(posedge clk) weak(reject_on (a) b));
|
||||
| ^~~~~~~~~
|
||||
%Error: t/t_prop_bad.v:26:40: syntax error, unexpected if, expecting IDENTIFIER-for-type
|
||||
26 | assert property (@(posedge clk) weak(if (a) b else c));
|
||||
| ^~
|
||||
%Error: t/t_prop_bad.v:27:40: syntax error, unexpected strong, expecting IDENTIFIER-for-type
|
||||
27 | assert property (@(posedge clk) weak(strong(a)));
|
||||
| ^~~~~~
|
||||
%Error: t/t_prop_bad.v:28:42: syntax error, unexpected weak, expecting IDENTIFIER-for-type
|
||||
28 | assert property (@(posedge clk) strong(weak(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('linter')
|
||||
|
||||
test.lint(fails=True, expect_filename=test.golden_filename)
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,29 @@
|
|||
// DESCRIPTION: Verilator: Verilog Test module
|
||||
//
|
||||
// This file ONLY is placed under the Creative Commons Public Domain.
|
||||
// SPDX-FileCopyrightText: 2026 Antmicro
|
||||
// SPDX-License-Identifier: CC0-1.0
|
||||
|
||||
module t (
|
||||
input clk
|
||||
);
|
||||
logic a = 1'b1;
|
||||
logic b = 1'b1;
|
||||
logic c = 1'b1;
|
||||
|
||||
assert property (@(posedge clk) weak(s_eventually a));
|
||||
assert property (@(posedge clk) weak(s_always [1:2] a));
|
||||
assert property (@(posedge clk) weak(nexttime a));
|
||||
assert property (@(posedge clk) weak(s_nexttime a));
|
||||
assert property (@(posedge clk) weak(always a));
|
||||
assert property (@(posedge clk) weak(eventually [1:2] a));
|
||||
assert property (@(posedge clk) weak(a |-> b));
|
||||
assert property (@(posedge clk) weak(a |=> b));
|
||||
assert property (@(posedge clk) weak(a implies b));
|
||||
assert property (@(posedge clk) weak(a iff b));
|
||||
assert property (@(posedge clk) weak(accept_on (a) b));
|
||||
assert property (@(posedge clk) weak(reject_on (a) b));
|
||||
assert property (@(posedge clk) weak(if (a) b else c));
|
||||
assert property (@(posedge clk) weak(strong(a)));
|
||||
assert property (@(posedge clk) strong(weak(a)));
|
||||
endmodule
|
||||
|
|
@ -0,0 +1,6 @@
|
|||
%Error-UNSUPPORTED: t/t_prop_strong_default_unsup.v:13:5: Unsupported: strong property in assert.
|
||||
: ... note: In instance 't'
|
||||
13 | @(posedge clk) a ##1 a;
|
||||
| ^
|
||||
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
|
||||
%Error: Exiting due to
|
||||
|
|
@ -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('linter')
|
||||
|
||||
test.lint(fails=True,
|
||||
expect_filename=test.golden_filename,
|
||||
verilator_flags2=['--language 1800-2005'])
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,17 @@
|
|||
// DESCRIPTION: Verilator: Verilog Test module
|
||||
//
|
||||
// This file ONLY is placed under the Creative Commons Public Domain.
|
||||
// SPDX-FileCopyrightText: 2026 Antmicro
|
||||
// SPDX-License-Identifier: CC0-1.0
|
||||
|
||||
module t (
|
||||
input clk
|
||||
);
|
||||
logic a = 1'b1;
|
||||
|
||||
property p_default_2005;
|
||||
@(posedge clk) a ##1 a;
|
||||
endproperty
|
||||
|
||||
assert property (p_default_2005);
|
||||
endmodule
|
||||
|
|
@ -0,0 +1,6 @@
|
|||
%Error-UNSUPPORTED: t/t_prop_strong_unsup.v:12:20: Unsupported: strong property in assume.
|
||||
: ... note: In instance 't'
|
||||
12 | assume property (@(posedge clk) strong(a ##1 a));
|
||||
| ^
|
||||
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
|
||||
%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('linter')
|
||||
|
||||
test.lint(fails=True, expect_filename=test.golden_filename)
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,13 @@
|
|||
// DESCRIPTION: Verilator: Verilog Test module
|
||||
//
|
||||
// This file ONLY is placed under the Creative Commons Public Domain.
|
||||
// SPDX-FileCopyrightText: 2026 Antmicro
|
||||
// SPDX-License-Identifier: CC0-1.0
|
||||
|
||||
module t (
|
||||
input clk
|
||||
);
|
||||
logic a = 1'b1;
|
||||
|
||||
assume property (@(posedge clk) strong(a ##1 a));
|
||||
endmodule
|
||||
|
|
@ -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('linter')
|
||||
|
||||
test.lint()
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,15 @@
|
|||
// DESCRIPTION: Verilator: Verilog Test module
|
||||
//
|
||||
// This file ONLY is placed under the Creative Commons Public Domain.
|
||||
// SPDX-FileCopyrightText: 2026 Antmicro
|
||||
// SPDX-License-Identifier: CC0-1.0
|
||||
|
||||
module t (
|
||||
input clk
|
||||
);
|
||||
logic a = 1'b1;
|
||||
|
||||
property p_unused_strong;
|
||||
@(posedge clk) strong(a);
|
||||
endproperty
|
||||
endmodule
|
||||
|
|
@ -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,58 @@
|
|||
// DESCRIPTION: Verilator: Verilog Test module
|
||||
//
|
||||
// This file ONLY is placed under the Creative Commons Public Domain.
|
||||
// SPDX-FileCopyrightText: 2026 Antmicro
|
||||
// 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 (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0);
|
||||
// verilog_format: on
|
||||
|
||||
module t (
|
||||
input clk
|
||||
);
|
||||
|
||||
int cyc = 0;
|
||||
event e;
|
||||
bit [7:0] hit = 0;
|
||||
|
||||
always @(posedge clk) begin
|
||||
++cyc;
|
||||
if (cyc < 5) begin
|
||||
->e;
|
||||
end else begin
|
||||
`checkd(hit, 'b1111111);
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
end
|
||||
end
|
||||
|
||||
assert property (@(e) weak(##1 1 ##1 1));
|
||||
assert property (@(e) weak(1 ##1 1 ##1 1));
|
||||
assert property (@(e) weak(1 ##1 1));
|
||||
|
||||
assert property (@(e) weak(##1 1 ##1 1)) begin
|
||||
hit |= 'b1;
|
||||
end
|
||||
assert property (@(e) weak(1 ##1 1 ##1 1)) begin
|
||||
hit |= 'b10;
|
||||
end
|
||||
assert property (@(e) weak(1 ##1 1)) begin
|
||||
hit |= 'b100;
|
||||
end
|
||||
|
||||
assert property (@(e) weak(##1 1 ##1 0)) else begin
|
||||
hit |= 'b1000;
|
||||
end
|
||||
assert property (@(e) weak(##1 0)) else begin
|
||||
hit |= 'b10000;
|
||||
end
|
||||
assert property (@(e) weak(1 ##1 1 ##1 0)) else begin
|
||||
hit |= 'b100000;
|
||||
end
|
||||
assert property (@(e) weak(1 ##1 0)) else begin
|
||||
hit |= 'b1000000;
|
||||
end
|
||||
|
||||
endmodule
|
||||
|
|
@ -1,44 +1,38 @@
|
|||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:24:11: Unsupported: strong (in property expression)
|
||||
24 | strong(a);
|
||||
| ^
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:48:5: Unsupported: nexttime (in property expression)
|
||||
48 | nexttime a;
|
||||
| ^~~~~~~~
|
||||
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:28:9: Unsupported: weak (in property expression)
|
||||
28 | weak(a);
|
||||
| ^
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:56:5: Unsupported: nexttime (in property expression)
|
||||
56 | nexttime a;
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:52:5: Unsupported: nexttime[] (in property expression)
|
||||
52 | nexttime [2] a;
|
||||
| ^~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:60:5: Unsupported: nexttime[] (in property expression)
|
||||
60 | nexttime [2] a;
|
||||
| ^~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:64:5: Unsupported: s_nexttime (in property expression)
|
||||
64 | s_nexttime a;
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:56:5: Unsupported: s_nexttime (in property expression)
|
||||
56 | s_nexttime a;
|
||||
| ^~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:68:5: Unsupported: s_nexttime[] (in property expression)
|
||||
68 | s_nexttime [2] a;
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:60:5: Unsupported: s_nexttime[] (in property expression)
|
||||
60 | s_nexttime [2] a;
|
||||
| ^~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:72:5: Unsupported: nexttime (in property expression)
|
||||
72 | nexttime always a;
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:64:5: Unsupported: nexttime (in property expression)
|
||||
64 | nexttime always a;
|
||||
| ^~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:76:5: Unsupported: nexttime[] (in property expression)
|
||||
76 | nexttime [2] always a;
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:68:5: Unsupported: nexttime[] (in property expression)
|
||||
68 | nexttime [2] always a;
|
||||
| ^~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:80:5: Unsupported: nexttime[] (in property expression)
|
||||
80 | nexttime [2] always a;
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:72:5: Unsupported: nexttime[] (in property expression)
|
||||
72 | nexttime [2] always a;
|
||||
| ^~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:84:5: Unsupported: nexttime (in property expression)
|
||||
84 | nexttime s_eventually a;
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:76:5: Unsupported: nexttime (in property expression)
|
||||
76 | nexttime s_eventually a;
|
||||
| ^~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:88:14: Unsupported: s_eventually[] (in property expression)
|
||||
88 | nexttime s_eventually [2:$] always a;
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:80:14: Unsupported: s_eventually[] (in property expression)
|
||||
80 | nexttime s_eventually [2:$] always a;
|
||||
| ^~~~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:88:5: Unsupported: nexttime (in property expression)
|
||||
88 | nexttime s_eventually [2:$] always a;
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:80:5: Unsupported: nexttime (in property expression)
|
||||
80 | nexttime s_eventually [2:$] always a;
|
||||
| ^~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:107:26: Unsupported: property argument data type
|
||||
107 | property p_arg_propery(property inprop);
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:99:26: Unsupported: property argument data type
|
||||
99 | property p_arg_propery(property inprop);
|
||||
| ^~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:110:26: Unsupported: sequence argument data type
|
||||
110 | property p_arg_seqence(sequence inseq);
|
||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:102:26: Unsupported: sequence argument data type
|
||||
102 | property p_arg_seqence(sequence inseq);
|
||||
| ^~~~~~~~
|
||||
%Error: Exiting due to
|
||||
|
|
|
|||
|
|
@ -20,14 +20,6 @@ module t (
|
|||
`ifdef PARSING_TIME
|
||||
// NOTE this grammar hasn't been checked with other simulators,
|
||||
// is here just to avoid uncovered code lines in the grammar.
|
||||
property p_strong;
|
||||
strong(a);
|
||||
endproperty
|
||||
|
||||
property p_weak;
|
||||
weak(a);
|
||||
endproperty
|
||||
|
||||
property p_until;
|
||||
a until b;
|
||||
endproperty
|
||||
|
|
|
|||
Loading…
Reference in New Issue