diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 81ae8e891..11417d5e5 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -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. diff --git a/src/V3AstAttr.h b/src/V3AstAttr.h index afca1bcc2..2d1c00ec3 100644 --- a/src/V3AstAttr.h +++ b/src/V3AstAttr.h @@ -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 diff --git a/src/V3AstNodeOther.h b/src/V3AstNodeOther.h index 4b2b62bac..859b606d7 100644 --- a/src/V3AstNodeOther.h +++ b/src/V3AstNodeOther.h @@ -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 diff --git a/src/V3AstNodes.cpp b/src/V3AstNodes.cpp index a7f0d3775..4dcad4a3e 100644 --- a/src/V3AstNodes.cpp +++ b/src/V3AstNodes.cpp @@ -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 diff --git a/src/V3EmitV.cpp b/src/V3EmitV.cpp index 405204084..aa712df59 100644 --- a/src/V3EmitV.cpp +++ b/src/V3EmitV.cpp @@ -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()); } diff --git a/src/verilog.y b/src/verilog.y index da1a24ed1..4c729b893 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6686,16 +6686,27 @@ sequence_declarationBody: // IEEE: part of sequence_declaration property_spec: // 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: // 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: // IEEE: part of property_expr for if/case @@ -6761,10 +6772,6 @@ pexpr: // 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 diff --git a/test_regress/t/t_cover_property.v b/test_regress/t/t_cover_property.v index d68118d96..97174b434 100644 --- a/test_regress/t/t_cover_property.v +++ b/test_regress/t/t_cover_property.v @@ -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 diff --git a/test_regress/t/t_debug_emitv.out b/test_regress/t/t_debug_emitv.out index b88e201e3..7a60f15f8 100644 --- a/test_regress/t/t_debug_emitv.out +++ b/test_regress/t/t_debug_emitv.out @@ -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 diff --git a/test_regress/t/t_debug_emitv.v b/test_regress/t/t_debug_emitv.v index 1255b5c3c..3058f9260 100644 --- a/test_regress/t/t_debug_emitv.v +++ b/test_regress/t/t_debug_emitv.v @@ -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; diff --git a/test_regress/t/t_prop_bad.out b/test_regress/t/t_prop_bad.out new file mode 100644 index 000000000..30bf9603d --- /dev/null +++ b/test_regress/t/t_prop_bad.out @@ -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 diff --git a/test_regress/t/t_prop_bad.py b/test_regress/t/t_prop_bad.py new file mode 100755 index 000000000..38cf36b43 --- /dev/null +++ b/test_regress/t/t_prop_bad.py @@ -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() diff --git a/test_regress/t/t_prop_bad.v b/test_regress/t/t_prop_bad.v new file mode 100644 index 000000000..91c8be133 --- /dev/null +++ b/test_regress/t/t_prop_bad.v @@ -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 diff --git a/test_regress/t/t_prop_strong_default_unsup.out b/test_regress/t/t_prop_strong_default_unsup.out new file mode 100644 index 000000000..3eaabbd33 --- /dev/null +++ b/test_regress/t/t_prop_strong_default_unsup.out @@ -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 diff --git a/test_regress/t/t_prop_strong_default_unsup.py b/test_regress/t/t_prop_strong_default_unsup.py new file mode 100755 index 000000000..434490788 --- /dev/null +++ b/test_regress/t/t_prop_strong_default_unsup.py @@ -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() diff --git a/test_regress/t/t_prop_strong_default_unsup.v b/test_regress/t/t_prop_strong_default_unsup.v new file mode 100644 index 000000000..ce126a724 --- /dev/null +++ b/test_regress/t/t_prop_strong_default_unsup.v @@ -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 diff --git a/test_regress/t/t_prop_strong_unsup.out b/test_regress/t/t_prop_strong_unsup.out new file mode 100644 index 000000000..d1ce08407 --- /dev/null +++ b/test_regress/t/t_prop_strong_unsup.out @@ -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 diff --git a/test_regress/t/t_prop_strong_unsup.py b/test_regress/t/t_prop_strong_unsup.py new file mode 100755 index 000000000..38cf36b43 --- /dev/null +++ b/test_regress/t/t_prop_strong_unsup.py @@ -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() diff --git a/test_regress/t/t_prop_strong_unsup.v b/test_regress/t/t_prop_strong_unsup.v new file mode 100644 index 000000000..115df5144 --- /dev/null +++ b/test_regress/t/t_prop_strong_unsup.v @@ -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 diff --git a/test_regress/t/t_prop_strong_unused.py b/test_regress/t/t_prop_strong_unused.py new file mode 100755 index 000000000..a5ea6627e --- /dev/null +++ b/test_regress/t/t_prop_strong_unused.py @@ -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() diff --git a/test_regress/t/t_prop_strong_unused.v b/test_regress/t/t_prop_strong_unused.v new file mode 100644 index 000000000..85e81368f --- /dev/null +++ b/test_regress/t/t_prop_strong_unused.v @@ -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 diff --git a/test_regress/t/t_prop_weak.py b/test_regress/t/t_prop_weak.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/test_regress/t/t_prop_weak.py @@ -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() diff --git a/test_regress/t/t_prop_weak.v b/test_regress/t/t_prop_weak.v new file mode 100644 index 000000000..065a711c8 --- /dev/null +++ b/test_regress/t/t_prop_weak.v @@ -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 diff --git a/test_regress/t/t_property_pexpr_parse_unsup.out b/test_regress/t/t_property_pexpr_parse_unsup.out index 6a23bc18e..600c592f2 100644 --- a/test_regress/t/t_property_pexpr_parse_unsup.out +++ b/test_regress/t/t_property_pexpr_parse_unsup.out @@ -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 diff --git a/test_regress/t/t_property_pexpr_unsup.v b/test_regress/t/t_property_pexpr_unsup.v index 10798685e..f627bf35c 100644 --- a/test_regress/t/t_property_pexpr_unsup.v +++ b/test_regress/t/t_property_pexpr_unsup.v @@ -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