From 5adecb9fa3bd676c74de97d98ee1caffd2728b97 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bart=C5=82omiej=20Chmiel?= Date: Thu, 6 Nov 2025 14:42:27 +0100 Subject: [PATCH] Support multi-expression sequences (#6639) --- src/CMakeLists.txt | 2 + src/Makefile_obj.in | 1 + src/V3Assert.cpp | 70 +++-- src/V3AssertPre.cpp | 80 +----- src/V3AssertProp.cpp | 264 +++++++++++++++++ src/V3AssertProp.h | 32 +++ src/V3AstNodeExpr.h | 24 +- src/V3AstNodeStmt.h | 11 + src/V3EmitV.cpp | 23 +- src/V3Width.cpp | 35 ++- src/Verilator.cpp | 3 + src/verilog.y | 5 +- test_regress/t/t_debug_emitv.out | 4 +- test_regress/t/t_debug_emitv.v | 4 +- test_regress/t/t_expect.out | 11 +- test_regress/t/t_property_sexpr.out | 272 +++++++++--------- test_regress/t/t_property_sexpr.v | 196 ++++++------- test_regress/t/t_property_sexpr_bad.out | 4 +- test_regress/t/t_property_sexpr_bad.v | 4 +- test_regress/t/t_property_sexpr_cov.dat.out | 5 + test_regress/t/t_property_sexpr_cov.out | 58 ++-- test_regress/t/t_property_sexpr_cov.py | 1 + test_regress/t/t_property_sexpr_cov.v | 3 + test_regress/t/t_property_sexpr_multi.py | 18 ++ test_regress/t/t_property_sexpr_multi.v | 249 ++++++++++++++++ .../t/t_property_sexpr_parse_unsup.out | 42 +-- test_regress/t/t_property_sexpr_unsup.out | 55 ++-- test_regress/t/t_property_sexpr_unsup.v | 14 +- test_regress/t/t_sequence_sexpr_unsup.out | 167 +++++------ test_regress/t/t_sequence_sexpr_unsup.v | 3 - 30 files changed, 1107 insertions(+), 553 deletions(-) create mode 100644 src/V3AssertProp.cpp create mode 100644 src/V3AssertProp.h create mode 100644 test_regress/t/t_property_sexpr_cov.dat.out create mode 100755 test_regress/t/t_property_sexpr_multi.py create mode 100644 test_regress/t/t_property_sexpr_multi.v diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ab1058fd2..629093a2a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -43,6 +43,7 @@ set(HEADERS V3ActiveTop.h V3Assert.h V3AssertPre.h + V3AssertProp.h V3Ast.h V3AstAttr.h V3AstInlines.h @@ -207,6 +208,7 @@ set(COMMON_SOURCES V3ActiveTop.cpp V3Assert.cpp V3AssertPre.cpp + V3AssertProp.cpp V3Ast.cpp V3AstNodes.cpp V3Begin.cpp diff --git a/src/Makefile_obj.in b/src/Makefile_obj.in index a64e4ec18..983f26e62 100644 --- a/src/Makefile_obj.in +++ b/src/Makefile_obj.in @@ -232,6 +232,7 @@ RAW_OBJS_PCH_ASTNOMT = \ V3ActiveTop.o \ V3Assert.o \ V3AssertPre.o \ + V3AssertProp.o \ V3Begin.o \ V3Branch.o \ V3CCtors.o \ diff --git a/src/V3Assert.cpp b/src/V3Assert.cpp index 31ecce928..0940b6e5b 100644 --- a/src/V3Assert.cpp +++ b/src/V3Assert.cpp @@ -143,6 +143,9 @@ class AssertVisitor final : public VNVisitor { VDouble0 m_statPastVars; // Statistic tracking bool m_inSampled = false; // True inside a sampled expression bool m_inRestrict = false; // True inside restrict assertion + AstNode* m_passsp = nullptr; // Current pass statement + AstNode* m_failsp = nullptr; // Current fail statement + bool m_underAssert = false; // Visited from assert // METHODS static AstNodeExpr* assertOnCond(FileLine* fl, VAssertType type, @@ -288,25 +291,18 @@ class AssertVisitor final : public VNVisitor { return ifp; } - static AstNode* assertBody(AstNodeCoverOrAssert* nodep, AstNodeExpr* propp, AstNode* passsp, - AstNode* failsp) { - if (AstPExpr* const pExpr = VN_CAST(propp, PExpr)) { - AstNodeExpr* const condp = pExpr->condp(); - UASSERT_OBJ(condp, pExpr, "Should have condition"); - AstIf* const ifp = assertCond(nodep, condp->unlinkFrBack(), passsp, failsp); - - AstNode* const precondps = pExpr->precondp(); - UASSERT_OBJ(precondps, pExpr, "Should have precondition"); - precondps->unlinkFrBackWithNext()->addNext(ifp); - AstNodeStmt* const aonp = newIfAssertOn(precondps, nodep->directive(), nodep->type()); - FileLine* const flp = precondps->fileline(); - AstFork* const forkp = new AstFork{flp, VJoinType::JOIN_NONE}; - forkp->addForksp(new AstBegin{flp, "", aonp, true}); - return forkp; + AstNode* assertBody(AstNodeCoverOrAssert* nodep, AstNode* propp, AstNode* passsp, + AstNode* failsp) { + AstNode* bodyp = nullptr; + if (AstPExpr* const pexprp = VN_CAST(propp, PExpr)) { + AstFork* const forkp = new AstFork{nodep->fileline(), VJoinType::JOIN_NONE}; + forkp->addForksp(pexprp->bodyp()->unlinkFrBack()); + VL_DO_DANGLING(pushDeletep(pexprp), pexprp); + bodyp = forkp; + } else { + bodyp = assertCond(nodep, VN_AS(propp, NodeExpr), passsp, failsp); } - - AstIf* const ifp = assertCond(nodep, propp, passsp, failsp); - return newIfAssertOn(ifp, nodep->directive(), nodep->type()); + return newIfAssertOn(bodyp, nodep->directive(), nodep->type()); } AstNodeStmt* newFireAssertUnchecked(const AstNodeStmt* nodep, const string& message, @@ -336,7 +332,6 @@ class AssertVisitor final : public VNVisitor { { AssertDeFuture{nodep->propp(), m_modp, m_modPastNum++}; } iterateChildren(nodep); - AstNodeExpr* const propp = VN_AS(nodep->propp()->unlinkFrBackWithNext(), NodeExpr); AstSenTree* const sentreep = nodep->sentreep(); const string& message = nodep->name(); AstNode* passsp = nodep->passsp(); @@ -384,7 +379,15 @@ class AssertVisitor final : public VNVisitor { nodep->v3fatalSrc("Unknown node type"); } - AstNode* bodysp = assertBody(nodep, propp, passsp, failsp); + VL_RESTORER(m_passsp); + VL_RESTORER(m_failsp); + VL_RESTORER(m_underAssert); + m_passsp = passsp; + m_failsp = failsp; + m_underAssert = true; + iterate(nodep->propp()); + + AstNode* bodysp = assertBody(nodep, nodep->propp()->unlinkFrBack(), passsp, failsp); if (sentreep) { bodysp = new AstAlways{nodep->fileline(), VAlwaysKwd::ALWAYS, sentreep, bodysp}; } @@ -631,7 +634,7 @@ class AssertVisitor final : public VNVisitor { } void visit(AstVarRef* nodep) override { iterateChildren(nodep); - if (m_inSampled && !VString::startsWith(nodep->name(), "__VpropPrecond")) { + if (m_inSampled && !VString::startsWith(nodep->name(), "__VcycleDly")) { if (!nodep->access().isReadOnly()) { nodep->v3warn(E_UNSUPPORTED, "Unsupported: Write to variable in sampled expression"); @@ -651,16 +654,27 @@ class AssertVisitor final : public VNVisitor { m_inSampled = false; iterateChildren(nodep); } + void visit(AstPExprClause* nodep) override { + if (m_underAssert) { + if (nodep->pass() && m_passsp) { + // Cover adds COVERINC by AstNode::addNext, thus need to clone next too. + nodep->replaceWith(m_passsp->cloneTree(true)); + } else if (!nodep->pass() && m_failsp) { + // Asserts with multiple statements are wrapped in implicit begin/end blocks so no + // need to clone next. + nodep->replaceWith(m_failsp->cloneTree(false)); + } else { + nodep->unlinkFrBack(); + } + VL_DO_DANGLING(pushDeletep(nodep), nodep); + } + } void visit(AstPExpr* nodep) override { - { + if (m_underAssert) { VL_RESTORER(m_inSampled); m_inSampled = false; - iterateAndNextNull(nodep->precondp()); - } - iterate(nodep->condp()); - if (!m_inRestrict) { - VL_DO_DANGLING(pushDeletep(nodep), nodep); - } else { + iterateChildren(nodep); + } else if (m_inRestrict) { VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep); } } diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 1c7885a67..d91761f7e 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -56,15 +56,11 @@ private: AstNodeExpr* m_disablep = nullptr; // Last disable // Other: V3UniqueNames m_cycleDlyNames{"__VcycleDly"}; // Cycle delay counter name generator - V3UniqueNames m_propPrecondNames{"__VpropPrecond"}; // Cycle delay temporaries name generator bool m_inAssign = false; // True if in an AssignNode bool m_inAssignDlyLhs = false; // True if in AssignDly's LHS bool m_inSynchDrive = false; // True if in synchronous drive std::vector m_xrefsp; // list of xrefs that need name fixup - AstNodeExpr* m_hasUnsupp = nullptr; // True if assert has unsupported construct inside - AstPExpr* m_pExpr = nullptr; // Current AstPExpr - bool m_hasSExpr = false; // True if assert has AstSExpr inside - bool m_inSExpr = false; // True if in AstSExpr + bool m_inPExpr = false; // True if in AstPExpr // METHODS @@ -343,7 +339,7 @@ private: } AstSenItem* sensesp = nullptr; if (!m_defaultClockingp) { - if (!m_pExpr && !m_inSExpr) { + if (!m_inPExpr) { nodep->v3error("Usage of cycle delays requires default clocking" " (IEEE 1800-2023 14.11)"); VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep); @@ -419,33 +415,6 @@ private: } } nodep->user1(true); - } else if (m_inSExpr && !nodep->user1()) { - AstVar* const preVarp - = new AstVar{nodep->varp()->fileline(), VVarType::BLOCKTEMP, - m_propPrecondNames.get(nodep->varp()) + "__" + nodep->varp()->name(), - nodep->varp()->dtypep()}; - preVarp->lifetime(VLifetime::STATIC_EXPLICIT); - m_modp->addStmtsp(preVarp); - AstVarRef* const origp - = new AstVarRef{nodep->fileline(), nodep->varp(), VAccess::READ}; - origp->user1(true); - AstVarRef* const precondp - = new AstVarRef{preVarp->fileline(), preVarp, VAccess::WRITE}; - precondp->user1(true); - - // Pack assignments in sampled as in concurrent assertions they are needed. - // Then, in assert's propp, sample only non-precondition variables. - AstSampled* const sampledp = new AstSampled{origp->fileline(), origp}; - sampledp->dtypeFrom(origp); - UASSERT(m_pExpr, "Should be under assertion"); - AstAssign* const assignp = new AstAssign{m_pExpr->fileline(), precondp, sampledp}; - m_pExpr->addPrecondp(assignp); - - AstVarRef* const precondReadp - = new AstVarRef{preVarp->fileline(), preVarp, VAccess::READ}; - precondReadp->user1(true); - nodep->replaceWith(precondReadp); - VL_DO_DANGLING(pushDeletep(nodep), nodep); } } void visit(AstMemberSel* nodep) override { @@ -500,32 +469,11 @@ private: void visit(AstNodeCoverOrAssert* nodep) override { if (nodep->sentreep()) return; // Already processed - VL_RESTORER(m_hasSExpr); - VL_RESTORER(m_hasUnsupp); - clearAssertInfo(); - m_pExpr = new AstPExpr{nodep->propp()->fileline()}; - m_pExpr->dtypeFrom(nodep->propp()); // Find Clocking's buried under nodep->exprsp iterateChildren(nodep); if (!nodep->immediate()) nodep->sentreep(newSenTree(nodep)); - if (m_hasSExpr && m_hasUnsupp) { - if (VN_IS(m_hasUnsupp, Implication)) { - m_hasUnsupp->v3warn(E_UNSUPPORTED, - "Unsupported: Implication with sequence expression"); - } else { - m_hasUnsupp->v3warn(E_UNSUPPORTED, - "Unsupported: Disable iff with sequence expression"); - } - if (m_pExpr) VL_DO_DANGLING(pushDeletep(m_pExpr), m_pExpr); - } else if (m_pExpr && m_pExpr->precondp()) { - m_pExpr->condp(VN_AS(nodep->propp()->unlinkFrBackWithNext(), NodeExpr)); - nodep->propp(m_pExpr); - iterateAndNextNull(m_pExpr->precondp()); - } else if (m_pExpr) { - VL_DO_DANGLING(pushDeletep(m_pExpr), m_pExpr); - } clearAssertInfo(); } void visit(AstFalling* nodep) override { @@ -564,10 +512,6 @@ private: if (sentreep) VL_DO_DANGLING(pushDeletep(sentreep->unlinkFrBack()), sentreep); nodep->sentreep(newSenTree(nodep)); } - void visit(AstLogNot* nodep) override { - if (m_inSExpr) nodep->v3error("Syntax error: unexpected 'not' in sequence expression"); - iterateChildren(nodep); - } void visit(AstPast* nodep) override { if (nodep->sentreep()) return; // Already processed iterateChildren(nodep); @@ -633,7 +577,6 @@ private: void visit(AstImplication* nodep) override { if (nodep->sentreep()) return; // Already processed - m_hasUnsupp = nodep; iterateChildren(nodep); @@ -685,7 +628,6 @@ private: } if (AstNodeExpr* const disablep = nodep->disablep()) { m_disablep = disablep; - m_hasUnsupp = disablep; if (VN_IS(nodep->backp(), Cover)) { blockp = new AstAnd{disablep->fileline(), new AstNot{disablep->fileline(), disablep->unlinkFrBack()}, @@ -699,17 +641,19 @@ private: nodep->replaceWith(blockp); VL_DO_DANGLING(pushDeletep(nodep), nodep); } - void visit(AstSExpr* nodep) override { - VL_RESTORER(m_inSExpr); - m_inSExpr = true; - m_hasSExpr = true; + void visit(AstPExpr* nodep) override { + VL_RESTORER(m_inPExpr); + m_inPExpr = true; - UASSERT_OBJ(m_pExpr, nodep, "Should be under assertion"); - m_pExpr->addPrecondp(nodep->delayp()->unlinkFrBack()); + if (AstLogNot* const notp = VN_CAST(nodep->backp(), LogNot)) { + notp->replaceWith(nodep->unlinkFrBack()); + VL_DO_DANGLING(pushDeletep(notp), notp); + iterate(nodep); + } else { + iterateChildren(nodep); + } iterateChildren(nodep); - nodep->replaceWith(nodep->exprp()->unlinkFrBack()); - VL_DO_DANGLING(pushDeletep(nodep), nodep); } void visit(AstNodeModule* nodep) override { VL_RESTORER(m_defaultClockingp); diff --git a/src/V3AssertProp.cpp b/src/V3AssertProp.cpp new file mode 100644 index 000000000..922f10fba --- /dev/null +++ b/src/V3AssertProp.cpp @@ -0,0 +1,264 @@ +// -*- mode: C++; c-file-style: "cc-mode" -*- +//************************************************************************* +// DESCRIPTION: Verilator: Implementation of assertion properties +// +// Code available from: https://verilator.org +// +//************************************************************************* +// +// Copyright 2005-2025 by Wilson Snyder. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0 +// +//************************************************************************* +// Each sequence is translated into a decision tree in form of deterministic +// finite automaton (DFA) with bipartite structure. Each cycle delay is connected +// with an expression that depending on an evaluation result, proceeds to the next +// evaluation state. The structure is rooted with original sequence expression for +// simplifying further transformation back to AST. +// +// The graph consists of the following nodes: +// +// DfaStmtVertex: Statements to be executed to traverse from one state to another +// DfaExprVertex: Property expression that is checked and based on that a branch +// is taken. +// DfaConditionEdge: Branch edge that connects statements and expressions. +// +// Properties steps: +// Ensemble a property decision tree from sequence expressions. +// Transform property decision tree into AST, remove source sequence expression +// Property blocks are wrapped with AstPExpr that are transformed +// further by V3AssertPre and V3Assert. +// +//************************************************************************* + +#include "V3PchAstNoMT.h" // VL_MT_DISABLED_CODE_UNIT + +#include "V3AssertProp.h" + +#include "V3Graph.h" + +VL_DEFINE_DEBUG_FUNCTIONS; + +//###################################################################### +// Data structures (graph types) + +class DfaVertex VL_NOT_FINAL : public V3GraphVertex { + VL_RTTI_IMPL(DfaVertex, V3GraphVertex) + // STATE + AstNode* const m_nodep; // Underlying node + +public: + // CONSTRUCTORS + explicit DfaVertex(V3Graph* graphp, AstNode* nodep) VL_MT_DISABLED : V3GraphVertex{graphp}, + m_nodep{nodep} {} + AstNode* nodep() const { return m_nodep; } + string name() const override VL_MT_STABLE { + return cvtToHex(m_nodep) + "\\n " + cvtToStr(m_nodep->typeName()) + "\\n"s + + m_nodep->fileline()->ascii(); + }; + string dotShape() const override { + if (inEmpty()) return "tripleoctagon"; + if (outEmpty()) return "doubleoctagon"; + return "oval"; + } + bool isStart() const { return inEmpty(); } +}; + +class DfaStmtVertex final : public DfaVertex { + VL_RTTI_IMPL(DfaStmtVertex, V3GraphEdge) +public: + // CONSTRUCTORS + explicit DfaStmtVertex(V3Graph* graphp, AstNodeStmt* stmtp) VL_MT_DISABLED + : DfaVertex{graphp, stmtp} {} + string dotColor() const override { return "green"; } +}; + +class DfaExprVertex final : public DfaVertex { + VL_RTTI_IMPL(DfaExprVertex, V3GraphEdge) +public: + // CONSTRUCTORS + explicit DfaExprVertex(V3Graph* graphp, AstNodeExpr* exprp) VL_MT_DISABLED + : DfaVertex{graphp, exprp} {} + string dotColor() const override { return "blue"; } +}; + +class DfaConditionEdge final : public V3GraphEdge { + VL_RTTI_IMPL(DfaConditionEdge, V3GraphEdge) + // STATE + const bool m_ifBranch; // Whether this branch is taken for fulfilled condition + +public: + // CONSTRUCTORS + explicit DfaConditionEdge(V3Graph* graphp, DfaVertex* fromp, DfaVertex* top, + bool ifBranch) VL_MT_DISABLED : V3GraphEdge{graphp, fromp, top, 1}, + m_ifBranch{ifBranch} {} + ~DfaConditionEdge() override = default; + + bool ifBranch() const { return m_ifBranch; } + string dotColor() const override { return m_ifBranch ? "green" : "red"; } +}; + +// Parse properties and ensemble a property tree graph +class AssertPropBuildVisitor final : public VNVisitorConst { + // STATE + V3Graph& m_graph; // Property tree + DfaVertex* m_lastVtxp = nullptr; // Last encountered vertex + bool m_underSExpr = false; // Is under sequence expression, for creating a start node + size_t m_underLogNots = 0; // Number of 'not' operators before sequence + + DfaStmtVertex* makeClause(AstSExpr* nodep, bool pass) { + return new DfaStmtVertex{ + &m_graph, + new AstPExprClause{nodep->fileline(), m_underLogNots % 2 == 0 ? pass : !pass}}; + } + + // VISITORS + void visit(AstNodeCoverOrAssert* nodep) override { iterateChildrenConst(nodep); } + void visit(AstLogNot* nodep) override { + VL_RESTORER(m_underLogNots); + ++m_underLogNots; + iterateChildrenConst(nodep); + } + void visit(AstSExpr* nodep) override { + + if (VN_IS(nodep->exprp(), SExpr)) { + VL_RESTORER(m_underSExpr); + m_underSExpr = true; + iterateConst(nodep->exprp()); + } else { + DfaExprVertex* const exprVtxp + = new DfaExprVertex{&m_graph, nodep->exprp()->unlinkFrBack()}; + new DfaConditionEdge{&m_graph, exprVtxp, makeClause(nodep, true), true}; + new DfaConditionEdge{&m_graph, exprVtxp, makeClause(nodep, false), false}; + m_lastVtxp = exprVtxp; + } + + DfaExprVertex* const startVtxp + = m_underSExpr ? nullptr : new DfaExprVertex{&m_graph, nodep}; + + DfaStmtVertex* const dlyVtxp + = new DfaStmtVertex{&m_graph, nodep->delayp()->unlinkFrBack()}; + + if (AstSExpr* const sexprp = VN_CAST(nodep->preExprp(), SExpr)) { + UASSERT_OBJ(!sexprp->preExprp() && !VN_IS(sexprp->exprp(), SExpr), sexprp, + "Incorrect sexpr tree"); + DfaStmtVertex* const sdlyVtxp + = new DfaStmtVertex{&m_graph, sexprp->delayp()->unlinkFrBack()}; + DfaExprVertex* const exprVtxp + = new DfaExprVertex{&m_graph, sexprp->exprp()->unlinkFrBack()}; + + if (startVtxp) new DfaConditionEdge{&m_graph, startVtxp, sdlyVtxp, true}; + new DfaConditionEdge{&m_graph, sdlyVtxp, exprVtxp, true}; + new DfaConditionEdge{&m_graph, exprVtxp, dlyVtxp, true}; + new DfaConditionEdge{&m_graph, dlyVtxp, m_lastVtxp, true}; + new DfaConditionEdge{&m_graph, exprVtxp, makeClause(nodep, false), false}; + + // This case only occurs when multi-delay sequence starts with an expression, + // don't set last as this is never a last expression. + } else if (nodep->preExprp()) { + DfaExprVertex* const preVtxp + = new DfaExprVertex{&m_graph, nodep->preExprp()->unlinkFrBack()}; + if (startVtxp) new DfaConditionEdge{&m_graph, startVtxp, preVtxp, true}; + new DfaConditionEdge{&m_graph, preVtxp, dlyVtxp, true}; + new DfaConditionEdge{&m_graph, dlyVtxp, m_lastVtxp, true}; + new DfaConditionEdge{&m_graph, preVtxp, makeClause(nodep, false), false}; + m_lastVtxp = preVtxp; + } else { + if (startVtxp) new DfaConditionEdge{&m_graph, startVtxp, dlyVtxp, true}; + new DfaConditionEdge{&m_graph, dlyVtxp, m_lastVtxp, true}; + m_lastVtxp = dlyVtxp; + } + } + void visit(AstNode* nodep) override { iterateChildrenConst(nodep); } + void visit(AstConstPool* nodep) override {} + +public: + // CONSTRUCTORS + explicit AssertPropBuildVisitor(AstNetlist* nodep, V3Graph& graph) + : m_graph{graph} { + iterateConst(nodep); + if (dumpGraphLevel() >= 6) m_graph.dumpDotFilePrefixedAlways("properties", true); + } + ~AssertPropBuildVisitor() override = default; +}; + +// Transform property graph into AST +class AssertPropTransformer final { + // STATE + V3Graph& m_graph; // Property tree + AstPExpr* m_pexprp = nullptr; // Currently built property sequence + AstBegin* m_current = nullptr; // Currently built block + + V3GraphVertex* processVtx(V3GraphVertex* vtxp) { + if (DfaStmtVertex* const stmtp = vtxp->cast()) return processVtx(stmtp); + if (DfaExprVertex* const exprp = vtxp->cast()) return processVtx(exprp); + // TODO use C++17 std::variant and std::visit + v3fatalSrc("Unexpected vertex type"); + return nullptr; + } + V3GraphVertex* processVtx(DfaStmtVertex* vtxp) { + UASSERT_OBJ(!vtxp->isStart(), vtxp->nodep(), + "Starting node should be a property expression"); + UASSERT_OBJ(m_current, vtxp->nodep(), "Should be under a block"); + m_current->addStmtsp(vtxp->nodep()); + return processEdge(vtxp->outEdges().frontp()); + } + V3GraphVertex* processVtx(DfaExprVertex* vtxp) { + AstNode* const nodep = vtxp->nodep(); + if (vtxp->isStart()) { + AstBegin* const bodyp = new AstBegin{nodep->fileline(), "", nullptr, true}; + m_pexprp = new AstPExpr{nodep->fileline(), bodyp, nodep->dtypep()}; + UASSERT_OBJ(vtxp->outSize1(), nodep, "Starting node must have one out edge"); + m_current = m_pexprp->bodyp(); + return processEdge(vtxp->outEdges().frontp()); + } + UASSERT_OBJ(vtxp->outEdges().size() == 2, nodep, "Each expression must have two branches"); + AstBegin* const passsp = new AstBegin{nodep->fileline(), "", nullptr, true}; + AstNode* const failsp = vtxp->outEdges().backp()->top()->as()->nodep(); + + AstSampled* const sampledp + = new AstSampled{nodep->fileline(), VN_AS(vtxp->nodep(), NodeExpr)}; + sampledp->dtypeFrom(vtxp->nodep()); + AstIf* const ifp = new AstIf{nodep->fileline(), sampledp, passsp, failsp}; + m_current->addStmtsp(ifp); + m_current = passsp; + return processEdge(vtxp->outEdges().frontp()); + } + V3GraphVertex* processEdge(V3GraphEdge* edgep) { + if (edgep) return processVtx(edgep->top()); + return nullptr; + } + +public: + // CONSTRUCTORS + explicit AssertPropTransformer(V3Graph& graph) + : m_graph{graph} { + for (V3GraphVertex& vtx : m_graph.vertices()) { + if (DfaVertex* const dVtxp = vtx.cast()) { + if (dVtxp->isStart()) { + VL_RESTORER(m_pexprp); + processVtx(&vtx); + AstSExpr* const propp = VN_AS(dVtxp->nodep(), SExpr); + propp->replaceWith(m_pexprp); + VL_DO_DANGLING(propp->deleteTree(), propp); + } + } + } + } +}; + +//###################################################################### +// Top AssertProp class + +void V3AssertProp::assertPropAll(AstNetlist* nodep) { + UINFO(2, __FUNCTION__ << ":"); + { + V3Graph graph; + { AssertPropBuildVisitor{nodep, graph}; } + AssertPropTransformer{graph}; + } + V3Global::dumpCheckGlobalTree("assertproperties", 0, dumpTreeEitherLevel() >= 3); +} diff --git a/src/V3AssertProp.h b/src/V3AssertProp.h new file mode 100644 index 000000000..2ec4ca1f7 --- /dev/null +++ b/src/V3AssertProp.h @@ -0,0 +1,32 @@ +// -*- mode: C++; c-file-style: "cc-mode" -*- +//************************************************************************* +// DESCRIPTION: Verilator: Implementation of assertion properties +// +// Code available from: https://verilator.org +// +//************************************************************************* +// +// Copyright 2005-2025 by Wilson Snyder. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0 +// +//************************************************************************* + +#ifndef VERILATOR_V3ASSERTPROP_H_ +#define VERILATOR_V3ASSERTPROP_H_ + +#include "config_build.h" +#include "verilatedos.h" + +class AstNetlist; + +//============================================================================ + +class V3AssertProp final { +public: + static void assertPropAll(AstNetlist* nodep) VL_MT_DISABLED; +}; + +#endif // Guard diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index e8448a0bf..749b1e0a5 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -1778,11 +1778,13 @@ public: }; class AstPExpr final : public AstNodeExpr { // Property expression - // @astgen op1 := precondp : List[AstNode] - // @astgen op2 := condp : Optional[AstNodeExpr] + // @astgen op1 := bodyp : AstBegin public: - explicit AstPExpr(FileLine* fl) - : ASTGEN_SUPER_PExpr(fl) {} + explicit AstPExpr(FileLine* fl, AstBegin* bodyp, AstNodeDType* dtypep) + : ASTGEN_SUPER_PExpr(fl) { + this->bodyp(bodyp); + this->dtypep(dtypep); + } ASTGEN_MEMBERS_AstPExpr; string emitVerilog() override { V3ERROR_NA_RETURN(""); } string emitC() override { V3ERROR_NA_RETURN(""); } @@ -2005,11 +2007,19 @@ public: }; class AstSExpr final : public AstNodeExpr { // Sequence expression - // @astgen op1 := delayp : AstDelay - // @astgen op2 := exprp : AstNodeExpr + // @astgen op1 := preExprp: Optional[AstNodeExpr] + // @astgen op2 := delayp : AstNodeStmt + // @astgen op3 := exprp : AstNodeExpr public: - explicit AstSExpr(FileLine* fl, AstDelay* delayp, AstNodeExpr* exprp) + explicit AstSExpr(FileLine* fl, AstNodeExpr* preExprp, AstNodeStmt* delayp, AstNodeExpr* exprp) : ASTGEN_SUPER_SExpr(fl) { + this->preExprp(preExprp); + this->delayp(delayp); + this->exprp(exprp); + } + explicit AstSExpr(FileLine* fl, AstNodeStmt* delayp, AstNodeExpr* exprp) + : ASTGEN_SUPER_SExpr(fl) { + this->preExprp(nullptr); this->delayp(delayp); this->exprp(exprp); } diff --git a/src/V3AstNodeStmt.h b/src/V3AstNodeStmt.h index 1369bdefa..9f97c54d2 100644 --- a/src/V3AstNodeStmt.h +++ b/src/V3AstNodeStmt.h @@ -821,6 +821,17 @@ public: } bool off() const { return m_off; } }; +class AstPExprClause final : public AstNodeStmt { + const bool m_pass; // True if will be replaced by passing assertion clause, false for + // assertion failure clause + +public: + ASTGEN_MEMBERS_AstPExprClause; + explicit AstPExprClause(FileLine* fl, bool pass = true) + : ASTGEN_SUPER_PExprClause(fl) + , m_pass{pass} {} + bool pass() const { return m_pass; } +}; class AstPrintTimeScale final : public AstNodeStmt { // Parents: stmtlist string m_name; // Parent module name diff --git a/src/V3EmitV.cpp b/src/V3EmitV.cpp index f8818749b..32418a44c 100644 --- a/src/V3EmitV.cpp +++ b/src/V3EmitV.cpp @@ -365,6 +365,7 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst { void visit(AstSFormat* nodep) override { visitNodeDisplay(nodep, nodep->lhsp(), nodep->fmtp()->text(), nodep->fmtp()->exprsp()); } + void visit(AstToStringN* nodep) override { iterateConst(nodep->lhsp()); } void visit(AstSFormatF* nodep) override { visitNodeDisplay(nodep, nullptr, nodep->text(), nodep->exprsp()); } @@ -803,9 +804,6 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst { puts(";\n"); } void visit(AstNodeCoverOrAssert* nodep) override { - if (AstPExpr* const pexprp = VN_CAST(nodep->propp(), PExpr)) { - iterateAndNextConstNull(pexprp); - } putfs(nodep, nodep->verilogKwd() + " "); if (nodep->type() == VAssertType::OBSERVED_DEFERRED_IMMEDIATE) { puts("#0 "); @@ -816,14 +814,10 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst { } iterateConstNull(nodep->sentreep()); puts("("); - if (const AstPExpr* const pexprp = VN_CAST(nodep->propp(), PExpr)) { - iterateAndNextConstNull(pexprp->condp()); + if (AstSampled* const sampledp = VN_CAST(nodep->propp(), Sampled)) { + iterateAndNextConstNull(sampledp->exprp()); } else { - if (AstSampled* const sampledp = VN_CAST(nodep->propp(), Sampled)) { - iterateAndNextConstNull(sampledp->exprp()); - } else { - iterateAndNextConstNull(nodep->propp()); - } + iterateAndNextConstNull(nodep->propp()); } if (!VN_IS(nodep, Restrict)) { puts(") begin\n"); @@ -1056,16 +1050,15 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst { iterateConstNull(nodep->propp()); puts("\n"); } - void visit(AstPExpr* nodep) override { - iterateAndNextConstNull(nodep->precondp()); // condp emitted by AstNodeCoverOrAssert - } + void visit(AstPExpr* nodep) override { iterateConst(nodep->bodyp()); } void visit(AstSExpr* nodep) override { + iterateConstNull(nodep->preExprp()); { VL_RESTORER(m_suppressSemi); m_suppressSemi = true; - iterateConstNull(nodep->delayp()); + iterateConst(nodep->delayp()); } - iterateConstNull(nodep->exprp()); + iterateConst(nodep->exprp()); } // Terminals diff --git a/src/V3Width.cpp b/src/V3Width.cpp index 0865243f4..c4d00710a 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -215,6 +215,9 @@ class WidthVisitor final : public VNVisitor { V3TaskConnectState m_taskConnectState; // State to cache V3Task::taskConnects WidthVP* m_vup = nullptr; // Current node state bool m_underFork = false; // Visiting under a fork + bool m_underSExpr = false; // Visiting under a sequence expression + AstNode* m_seqUnsupp = nullptr; // Property has unsupported node + bool m_hasSExpr = false; // Property has a sequence expression const AstCell* m_cellp = nullptr; // Current cell for arrayed instantiations const AstEnumItem* m_enumItemp = nullptr; // Current enum item AstNodeFTask* m_ftaskp = nullptr; // Current function/task @@ -1539,6 +1542,7 @@ class WidthVisitor final : public VNVisitor { } void visit(AstImplication* nodep) override { + m_seqUnsupp = nodep; if (m_vup->prelim()) { iterateCheckBool(nodep, "LHS", nodep->lhsp(), BOTH); iterateCheckBool(nodep, "RHS", nodep->rhsp(), BOTH); @@ -1557,9 +1561,15 @@ class WidthVisitor final : public VNVisitor { } } void visit(AstSExpr* nodep) override { + VL_RESTORER(m_underSExpr); + m_underSExpr = true; + m_hasSExpr = true; if (m_vup->prelim()) { - iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH); + if (nodep->preExprp()) { + iterateCheckBool(nodep, "preExprp", nodep->preExprp(), BOTH); + } iterate(nodep->delayp()); + iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH); nodep->dtypeSetBit(); } } @@ -5338,6 +5348,8 @@ class WidthVisitor final : public VNVisitor { } void visit(AstPropSpec* nodep) override { + VL_RESTORER(m_seqUnsupp); + VL_RESTORER(m_hasSExpr); if (m_vup->prelim()) { // First stage evaluation iterateCheckBool(nodep, "Property", nodep->propp(), BOTH); userIterateAndNext(nodep->sensesp(), nullptr); @@ -5346,6 +5358,20 @@ class WidthVisitor final : public VNVisitor { BOTH); // it's like an if() condition. } nodep->dtypeSetBit(); + if (m_hasSExpr) { + if (VN_IS(m_seqUnsupp, Implication)) { + m_seqUnsupp->v3warn(E_UNSUPPORTED, + "Unsupported: Implication with sequence expression"); + AstConst* const newp = new AstConst{nodep->fileline(), 0}; + newp->dtypeFrom(nodep); + nodep->replaceWith(newp); + VL_DO_DANGLING(pushDeletep(nodep), nodep); + } else if (nodep->disablep()) { + nodep->disablep()->v3warn(E_UNSUPPORTED, + "Unsupported: Disable iff with sequence expression"); + VL_DO_DANGLING(pushDeletep(nodep->disablep()->unlinkFrBack()), nodep); + } + } } } @@ -7008,6 +7034,13 @@ class WidthVisitor final : public VNVisitor { if (m_vup->prelim()) { iterateCheckBool(nodep, "LHS", nodep->op1p(), BOTH); nodep->dtypeSetBit(); + if (m_underSExpr) { + nodep->v3error("Unexpected 'not' in sequence expression context"); + AstConst* const newp = new AstConst{nodep->fileline(), 0}; + newp->dtypeFrom(nodep); + nodep->replaceWith(newp); + VL_DO_DANGLING(pushDeletep(nodep), nodep); + } } } void visit_log_and_or(AstNodeBiop* nodep) { diff --git a/src/Verilator.cpp b/src/Verilator.cpp index 892df9a1d..226b49129 100644 --- a/src/Verilator.cpp +++ b/src/Verilator.cpp @@ -20,6 +20,7 @@ #include "V3ActiveTop.h" #include "V3Assert.h" #include "V3AssertPre.h" +#include "V3AssertProp.h" #include "V3Ast.h" #include "V3Begin.h" #include "V3Branch.h" @@ -240,6 +241,8 @@ static void process() { // Assertion insertion // After we've added block coverage, but before other nasty transforms + V3AssertProp::assertPropAll(v3Global.rootp()); + // V3AssertPre::assertPreAll(v3Global.rootp()); // V3Assert::assertAll(v3Global.rootp()); diff --git a/src/verilog.y b/src/verilog.y index 32622b103..c77cc7f40 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6534,7 +6534,8 @@ pexpr: // IEEE: property_expr (The name pexpr is important as regex // // IEEE: '(' pexpr ')' // // Expanded below // - yNOT pexpr %prec prNEGATION { $$ = new AstLogNot{$1, $2}; } + yNOT pexpr + { $$ = new AstLogNot{$1, $2}; } | ySTRONG '(' sexpr ')' { $$ = $3; BBUNSUP($2, "Unsupported: strong (in property expression)"); } | yWEAK '(' sexpr ')' @@ -6624,7 +6625,7 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg cycle_delay_range ~p~sexpr %prec yP_POUNDPOUND { $$ = new AstSExpr{$1, $1, $2}; } | ~p~sexpr cycle_delay_range sexpr %prec prPOUNDPOUND_MULTI - { $$ = $1; BBUNSUP($2->fileline(), "Unsupported: ## (in sequence expression)"); DEL($2, $3); } + { $$ = new AstSExpr{$2, $1, $2, $3}; } // // // IEEE: expression_or_dist [ boolean_abbrev ] // // Note expression_or_dist includes "expr"! diff --git a/test_regress/t/t_debug_emitv.out b/test_regress/t/t_debug_emitv.out index a5071f8e0..e09dc1e14 100644 --- a/test_regress/t/t_debug_emitv.out +++ b/test_regress/t/t_debug_emitv.out @@ -277,6 +277,7 @@ module Vt_debug_emitv_t; str = $sformatf("cyc=%~", cyc); ; $display("str = %@", str); + $display("struct = %@", ps); $display("%% [%t] [%^] to=%o td=%d", $time, $realtime, $time, $time); $sscanf(40'h666f6f3d35, "foo=%d", i); @@ -365,9 +366,6 @@ module Vt_debug_emitv_t; property p1; @( clk) sum[0] endproperty - property p2; - @(posedge clk) disable iff (cyc == 'sh1) ##1 sum[0] - endproperty assert property (@( clk) (! ##1 in) ) begin end diff --git a/test_regress/t/t_debug_emitv.v b/test_regress/t/t_debug_emitv.v index 0b3a79f68..e7915f47d 100644 --- a/test_regress/t/t_debug_emitv.v +++ b/test_regress/t/t_debug_emitv.v @@ -218,6 +218,7 @@ module t (/*AUTOARG*/ str = $sformatf("cyc=%d", cyc); $display("str = %s", str); + $display("struct = %p", ps); $display("%% [%t] [%t] to=%o td=%d", $time, $realtime, $time, $time); $sscanf("foo=5", "foo=%d", i); $printtimescale; @@ -276,9 +277,6 @@ module t (/*AUTOARG*/ property p1; @(clk) sum[0] endproperty - property p2; - @(posedge clk) disable iff (cyc == 1) ##1 sum[0] - endproperty assert property (@(clk) not ##1 in); diff --git a/test_regress/t/t_expect.out b/test_regress/t/t_expect.out index 5f7f2d122..8a378f4bc 100644 --- a/test_regress/t/t_expect.out +++ b/test_regress/t/t_expect.out @@ -1,19 +1,10 @@ -%Error-UNSUPPORTED: t/t_expect.v:19:32: Unsupported: ## (in sequence expression) - 19 | expect (@(posedge clk) a ##1 b) a = 110; - | ^~ - ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest %Error-UNSUPPORTED: t/t_expect.v:19:7: Unsupported: expect 19 | expect (@(posedge clk) a ##1 b) a = 110; | ^~~~~~ -%Error-UNSUPPORTED: t/t_expect.v:21:32: Unsupported: ## (in sequence expression) - 21 | expect (@(posedge clk) a ##1 b) else a = 299; - | ^~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest %Error-UNSUPPORTED: t/t_expect.v:21:7: Unsupported: expect 21 | expect (@(posedge clk) a ##1 b) else a = 299; | ^~~~~~ -%Error-UNSUPPORTED: t/t_expect.v:23:32: Unsupported: ## (in sequence expression) - 23 | expect (@(posedge clk) a ##1 b) a = 300; else a = 399; - | ^~ %Error-UNSUPPORTED: t/t_expect.v:23:7: Unsupported: expect 23 | expect (@(posedge clk) a ##1 b) a = 300; else a = 399; | ^~~~~~ diff --git a/test_regress/t/t_property_sexpr.out b/test_regress/t/t_property_sexpr.out index 7f65a6dfc..0c9ae3f6a 100644 --- a/test_regress/t/t_property_sexpr.out +++ b/test_regress/t/t_property_sexpr.out @@ -1,140 +1,134 @@ -[4] single delay with const stmt, fileline:115 -[5] concurrent assert else, fileline:167 -[6] single delay with const stmt, fileline:115 -[7] concurrent assert stmt, fileline:166 -[8] single delay with const stmt, fileline:115 -[9] concurrent assert else, fileline:167 -[11] concurrent assert else, fileline:167 -[12] single delay with var stmt, fileline:118 -[13] concurrent assert else, fileline:167 -[14] single delay with var else, fileline:119 -[15] concurrent assert stmt, fileline:166 -[16] single delay with var stmt, fileline:118 -[17] concurrent assert else, fileline:167 -[18] single delay with var else, fileline:119 -[19] concurrent assert else, fileline:167 -[20] single delay with var stmt, fileline:118 -[21] concurrent assert else, fileline:167 -[23] concurrent assert stmt, fileline:166 -[25] concurrent assert else, fileline:167 -[26] single multi-cycle delay with var else, fileline:123 -[27] concurrent assert else, fileline:167 -[28] single multi-cycle delay with var stmt, fileline:122 -[29] concurrent assert else, fileline:167 -[30] single multi-cycle delay with var else, fileline:123 -[31] concurrent assert stmt, fileline:166 -[33] concurrent assert else, fileline:167 -[34] single delay with var brackets 1 else, fileline:127 -[35] concurrent assert else, fileline:167 -[36] single delay with var brackets 1 stmt, fileline:126 -[37] concurrent assert else, fileline:167 -[38] single delay with var brackets 1 else, fileline:127 -[39] concurrent assert stmt, fileline:166 -[40] single delay with var brackets 1 stmt, fileline:126 -[41] concurrent assert else, fileline:167 -[43] concurrent assert else, fileline:167 -[44] single delay with var brackets 2 stmt, fileline:130 -[45] concurrent assert else, fileline:167 -[46] single delay with var brackets 2 else, fileline:131 -[47] concurrent assert stmt, fileline:166 -[48] single delay with var brackets 2 stmt, fileline:130 -[49] concurrent assert else, fileline:167 -[50] single delay with var brackets 2 else, fileline:131 -[51] concurrent assert else, fileline:167 -[53] concurrent assert else, fileline:167 -[54] single delay with negated var else, fileline:135 -[55] concurrent assert stmt, fileline:166 -[56] single delay with negated var stmt, fileline:134 -[57] concurrent assert else, fileline:167 -[58] single delay with negated var else, fileline:135 -[59] concurrent assert else, fileline:167 -[60] single delay with negated var else, fileline:135 -[61] concurrent assert else, fileline:167 -[63] concurrent assert stmt, fileline:166 -[64] single delay with negated var else, fileline:139 -[65] concurrent assert else, fileline:167 -[66] single delay with negated var stmt, fileline:138 -[67] concurrent assert else, fileline:167 -[68] single delay with negated var else, fileline:139 -[69] concurrent assert else, fileline:167 -[70] single delay with negated var stmt, fileline:138 -[71] concurrent assert stmt, fileline:166 -[73] concurrent assert else, fileline:167 -[74] single delay with negated var brackets stmt, fileline:142 -[75] concurrent assert else, fileline:167 -[76] single delay with negated var brackets else, fileline:144 -[77] concurrent assert else, fileline:167 -[78] single delay with negated var brackets stmt, fileline:142 -[79] concurrent assert stmt, fileline:166 -[80] single delay with negated var brackets else, fileline:144 -[81] concurrent assert else, fileline:167 -[83] concurrent assert else, fileline:167 -[84] single delay with negated var brackets else, fileline:148 -[85] concurrent assert else, fileline:167 -[87] concurrent assert stmt, fileline:166 -[88] single delay with negated var brackets else, fileline:148 -[89] concurrent assert else, fileline:167 -[91] concurrent assert else, fileline:167 -[93] concurrent assert else, fileline:167 -[94] single delay with nested not else, fileline:152 -[95] concurrent assert stmt, fileline:166 -[96] single delay with nested not stmt, fileline:151 -[97] concurrent assert else, fileline:167 -[98] single delay with nested not else, fileline:152 -[99] concurrent assert else, fileline:167 -[100] single delay with nested not stmt, fileline:151 -[101] concurrent assert else, fileline:167 -[103] concurrent assert stmt, fileline:166 -[105] concurrent assert else, fileline:167 -[107] concurrent assert else, fileline:167 -[109] concurrent assert else, fileline:167 -[111] concurrent assert stmt, fileline:166 -[113] concurrent assert else, fileline:167 -[114] property, fileline:162 -[115] concurrent assert else, fileline:167 -[116] property, fileline:163 -[117] concurrent assert else, fileline:167 -[118] property, fileline:162 -[119] concurrent assert stmt, fileline:166 -[120] property, fileline:163 -[121] concurrent assert else, fileline:167 -[123] concurrent assert else, fileline:167 -[125] concurrent assert else, fileline:167 -[127] concurrent assert stmt, fileline:166 -[129] concurrent assert else, fileline:167 -[131] concurrent assert else, fileline:167 -[133] concurrent assert else, fileline:167 -[135] concurrent assert stmt, fileline:166 -[137] concurrent assert else, fileline:167 -[139] concurrent assert else, fileline:167 -[141] concurrent assert else, fileline:167 -[143] concurrent assert stmt, fileline:166 -[145] concurrent assert else, fileline:167 -[147] concurrent assert else, fileline:167 -[149] concurrent assert else, fileline:167 -[151] concurrent assert stmt, fileline:166 -[153] concurrent assert else, fileline:167 -[155] concurrent assert else, fileline:167 -[157] concurrent assert else, fileline:167 -[159] concurrent assert stmt, fileline:166 -[161] concurrent assert else, fileline:167 -[163] concurrent assert else, fileline:167 -[165] concurrent assert else, fileline:167 -[167] concurrent assert stmt, fileline:166 -[169] concurrent assert else, fileline:167 -[171] concurrent assert else, fileline:167 -[173] concurrent assert else, fileline:167 -[175] concurrent assert stmt, fileline:166 -[177] concurrent assert else, fileline:167 -[179] concurrent assert else, fileline:167 -[181] concurrent assert else, fileline:167 -[183] concurrent assert stmt, fileline:166 -[185] concurrent assert else, fileline:167 -[187] concurrent assert else, fileline:167 -[189] concurrent assert else, fileline:167 -[191] concurrent assert stmt, fileline:166 -[193] concurrent assert else, fileline:167 -[195] concurrent assert else, fileline:167 -[197] concurrent assert else, fileline:167 -[199] concurrent assert stmt, fileline:166 +[2] triggered e1 +[4] triggered e1 +[4] single delay with const stmt, fileline:99 +[6] triggered e1 +[6] single delay with const stmt, fileline:99 +[8] triggered e2 +[10] triggered e2 +[10] single delay with var stmt, fileline:102 +[12] triggered e2 +[12] single delay with var else, fileline:103 +[14] triggered e2 +[14] single delay with var stmt, fileline:102 +[16] triggered e2 +[16] single delay with var else, fileline:103 +[18] triggered e2 +[18] single delay with var stmt, fileline:102 +[20] triggered e3 +[22] triggered e3 +[22] stmt1, fileline:106 +[22] stmt2, fileline:107 +[24] triggered e3 +[24] else1, fileline:110 +[24] else2, fileline:111 +[26] triggered e3 +[26] stmt1, fileline:106 +[26] stmt2, fileline:107 +[28] triggered e3 +[28] else1, fileline:110 +[28] else2, fileline:111 +[30] triggered e4 +[32] triggered e4 +[34] triggered e4 +[34] single multi-cycle delay with var stmt, fileline:115 +[36] triggered e4 +[36] single multi-cycle delay with var else, fileline:116 +[38] triggered e4 +[38] single multi-cycle delay with var stmt, fileline:115 +[40] triggered e5 +[42] triggered e5 +[42] single delay with var brackets 1 stmt, fileline:119 +[44] triggered e5 +[44] single delay with var brackets 1 else, fileline:120 +[46] triggered e5 +[46] single delay with var brackets 1 stmt, fileline:119 +[48] triggered e5 +[48] single delay with var brackets 1 else, fileline:120 +[50] triggered e6 +[52] triggered e6 +[52] single delay with var brackets 2 else, fileline:124 +[54] triggered e6 +[54] single delay with var brackets 2 stmt, fileline:123 +[56] triggered e6 +[56] single delay with var brackets 2 else, fileline:124 +[58] triggered e6 +[58] single delay with var brackets 2 stmt, fileline:123 +[60] triggered e7 +[62] triggered e7 +[62] single delay with and var stmt, fileline:127 +[64] triggered e7 +[64] single delay with and var else, fileline:128 +[66] triggered e7 +[66] single delay with and var else, fileline:128 +[68] triggered e7 +[68] single delay with and var else, fileline:128 +[70] triggered e8 +[72] triggered e8 +[72] single delay with negated var stmt, fileline:131 +[74] triggered e8 +[74] single delay with negated var else, fileline:132 +[76] triggered e8 +[76] single delay with negated var stmt, fileline:131 +[78] triggered e8 +[78] single delay with negated var else, fileline:132 +[80] triggered e9 +[82] triggered e9 +[82] single delay with negated var brackets else, fileline:137 +[84] triggered e9 +[84] single delay with negated var brackets stmt, fileline:135 +[86] triggered e9 +[86] single delay with negated var brackets else, fileline:137 +[88] triggered e9 +[88] single delay with negated var brackets stmt, fileline:135 +[90] triggered e10 +[92] triggered e10 +[94] triggered e10 +[94] single delay with negated var brackets else, fileline:141 +[96] triggered e10 +[98] triggered e10 +[98] single delay with negated var brackets else, fileline:141 +[100] triggered e11 +[102] triggered e11 +[102] single delay with nested not stmt, fileline:144 +[104] triggered e11 +[104] single delay with nested not else, fileline:145 +[106] triggered e11 +[106] single delay with nested not stmt, fileline:144 +[108] triggered e11 +[108] single delay with nested not else, fileline:145 +[110] triggered e12 +[112] triggered e12 +[114] triggered e12 +[114] stmt, fileline: 148 +[116] triggered e12 +[116] else, fileline: 150 +[118] triggered e12 +[118] stmt, fileline: 148 +[120] triggered e13 +[122] triggered e13 +[122] property, fileline:161 +[124] triggered e13 +[124] property, fileline:160 +[126] triggered e13 +[126] property, fileline:161 +[128] triggered e13 +[128] property, fileline:160 +[130] triggered e14 +[132] triggered e14 +[132] else, fileline: 166 +[134] triggered e14 +[134] stmt, fileline: 164 +[136] triggered e14 +[136] else, fileline: 166 +[138] triggered e14 +[138] else, fileline: 166 +[140] triggered e15 +[140] else, fileline: 171 +[142] triggered e15 +[144] triggered e15 +[144] else, fileline: 171 +[144] else, fileline: 171 +[146] triggered e15 +[148] triggered e15 +[148] else, fileline: 171 *-* All Finished *-* diff --git a/test_regress/t/t_property_sexpr.v b/test_regress/t/t_property_sexpr.v index 7dd5a3801..5bbb48f90 100644 --- a/test_regress/t/t_property_sexpr.v +++ b/test_regress/t/t_property_sexpr.v @@ -4,6 +4,9 @@ // without warranty, 2025 by Antmicro. // SPDX-License-Identifier: CC0-1.0 +`define STRINGIFY(x) `"x`" +`define TRIGGER(e) ->e; $display("[%0t] triggered %s", $time, `STRINGIFY(e)) + module t ( /*AUTOARG*/ // Inputs clk @@ -11,7 +14,7 @@ module t ( /*AUTOARG*/ input clk; - bit [3:0] val = 0; + bit [1:0] val = 0; event e1; event e2; event e3; @@ -24,92 +27,73 @@ module t ( /*AUTOARG*/ event e10; event e11; event e12; + event e13; + event e14; + event e15; + integer cyc = 1; - always @(negedge clk) begin - val <= 4'(cyc % 4); - - if (cyc >= 0 && cyc <= 4) begin - ->e1; + always @(posedge clk) begin + ++val; + ++cyc; `ifdef TEST_VERBOSE - $display("[%0t] triggered e1", $time); + $display("[%0t] cyc=%0d val=%0d", $time, cyc, val); `endif - end - if (cyc >= 5 && cyc <= 10) begin - ->e2; -`ifdef TEST_VERBOSE - $display("[%0t] triggered e2", $time); -`endif - end - if (cyc >= 11 && cyc <= 15) begin - ->e3; -`ifdef TEST_VERBOSE - $display("[%0t] triggered e3", $time); -`endif - end - if (cyc >= 16 && cyc <= 20) begin - ->e4; -`ifdef TEST_VERBOSE - $display("[%0t] triggered e4", $time); -`endif - end - if (cyc >= 21 && cyc <= 25) begin - ->e5; -`ifdef TEST_VERBOSE - $display("[%0t] triggered e5", $time); -`endif - end - if (cyc >= 26 && cyc <= 30) begin - ->e6; -`ifdef TEST_VERBOSE - $display("[%0t] triggered e6", $time); -`endif - end - if (cyc >= 31 && cyc <= 35) begin - ->e7; -`ifdef TEST_VERBOSE - $display("[%0t] triggered e7", $time); -`endif - end - if (cyc >= 36 && cyc <= 40) begin - ->e8; -`ifdef TEST_VERBOSE - $display("[%0t] triggered e8", $time); -`endif - end - if (cyc >= 41 && cyc <= 45) begin - ->e9; -`ifdef TEST_VERBOSE - $display("[%0t] triggered e9", $time); -`endif - end - if (cyc >= 46 && cyc <= 50) begin - ->e10; -`ifdef TEST_VERBOSE - $display("[%0t] triggered e10", $time); -`endif - end - if (cyc >= 51 && cyc <= 55) begin - ->e11; -`ifdef TEST_VERBOSE - $display("[%0t] triggered e11", $time); -`endif - end - if (cyc >= 56 && cyc <= 60) begin - ->e12; -`ifdef TEST_VERBOSE - $display("[%0t] triggered e12", $time); -`endif - end -`ifdef TEST_VERBOSE - $display("cyc=%0d val=%0d", cyc, val); -`endif - cyc <= cyc + 1; if (cyc == 100) begin $write("*-* All Finished *-*\n"); $finish; end end + always @(negedge clk) begin + if (cyc >= 0 && cyc <= 4) begin + `TRIGGER(e1); + end + if (cyc >= 5 && cyc <= 10) begin + `TRIGGER(e2); + end + if (cyc >= 11 && cyc <= 15) begin + `TRIGGER(e3); + end + if (cyc >= 16 && cyc <= 20) begin + `TRIGGER(e4); + end + if (cyc >= 21 && cyc <= 25) begin + `TRIGGER(e5); + end + if (cyc >= 26 && cyc <= 30) begin + `TRIGGER(e6); + end + if (cyc >= 31 && cyc <= 35) begin + `TRIGGER(e7); + end + if (cyc >= 36 && cyc <= 40) begin + `TRIGGER(e8); + end + if (cyc >= 41 && cyc <= 45) begin + `TRIGGER(e9); + end + if (cyc >= 46 && cyc <= 50) begin + `TRIGGER(e10); + end + if (cyc >= 51 && cyc <= 55) begin + `TRIGGER(e11); + end + if (cyc >= 56 && cyc <= 60) begin + `TRIGGER(e12); + end + if (cyc >= 61 && cyc <= 65) begin + `TRIGGER(e13); + end + if (cyc >= 66 && cyc <= 70) begin + `TRIGGER(e14); + end + if (cyc >= 71 && cyc <= 75) begin + `TRIGGER(e15); + end + end + + + assert property (@(e1) ##1 1); assert property (@(e1) ##1 1) $display("[%0t] single delay with const stmt, fileline:%0d", $time, `__LINE__); @@ -118,51 +102,71 @@ module t ( /*AUTOARG*/ $display("[%0t] single delay with var stmt, fileline:%0d", $time, `__LINE__); else $display("[%0t] single delay with var else, fileline:%0d", $time, `__LINE__); - assert property (@(e3) ##2 val[0]) + assert property (@(e3) ##1 val[0]) begin + $display("[%0t] stmt1, fileline:%0d", $time, `__LINE__); + $display("[%0t] stmt2, fileline:%0d", $time, `__LINE__); + end + else begin + $display("[%0t] else1, fileline:%0d", $time, `__LINE__); + $display("[%0t] else2, fileline:%0d", $time, `__LINE__); + end + + assert property (@(e4) ##2 val[0]) $display("[%0t] single multi-cycle delay with var stmt, fileline:%0d", $time, `__LINE__); else $display("[%0t] single multi-cycle delay with var else, fileline:%0d", $time, `__LINE__); - assert property (@(e4) ##1 (val[0])) + assert property (@(e5) ##1 (val[0])) $display("[%0t] single delay with var brackets 1 stmt, fileline:%0d", $time, `__LINE__); else $display("[%0t] single delay with var brackets 1 else, fileline:%0d", $time, `__LINE__); - assert property (@(e5) (##1 (val[0]))) + assert property (@(e6) (##1 (val[0]))) $display("[%0t] single delay with var brackets 2 stmt, fileline:%0d", $time, `__LINE__); else $display("[%0t] single delay with var brackets 2 else, fileline:%0d", $time, `__LINE__); - assert property (@(e6) (##1 val[0] && val[1])) + assert property (@(e7) (##1 val[0] && val[1])) + $display("[%0t] single delay with and var stmt, fileline:%0d", $time, `__LINE__); + else $display("[%0t] single delay with and var else, fileline:%0d", $time, `__LINE__); + + assert property (@(e8) not not not ##1 val[0]) $display("[%0t] single delay with negated var stmt, fileline:%0d", $time, `__LINE__); else $display("[%0t] single delay with negated var else, fileline:%0d", $time, `__LINE__); - assert property (@(e7) not ##1 val[0]) - $display("[%0t] single delay with negated var stmt, fileline:%0d", $time, `__LINE__); - else $display("[%0t] single delay with negated var else, fileline:%0d", $time, `__LINE__); - - assume property (@(e8) not (##1 val[0])) + assume property (@(e9) not (##1 val[0])) $display("[%0t] single delay with negated var brackets stmt, fileline:%0d", $time, `__LINE__); else $display("[%0t] single delay with negated var brackets else, fileline:%0d", $time, `__LINE__); - assume property (@(e9) not (##1 val[0])) + assume property (@(e10) not (##1 val[0])) else $display("[%0t] single delay with negated var brackets else, fileline:%0d", $time, `__LINE__); - assert property (@(e10) not (not ##1 val[0])) + assert property (@(e11) not (not ##1 val[0])) $display("[%0t] single delay with nested not stmt, fileline:%0d", $time, `__LINE__); else $display("[%0t] single delay with nested not else, fileline:%0d", $time, `__LINE__); - restrict property (@(e11) ##1 val[0]); - - restrict property (@(e11) not ##1 val[0]); + assert property (@(e12) not (not ##2 val[0] && val[0])) + $display("[%0t] stmt, fileline:%d", $time, `__LINE__); + else + $display("[%0t] else, fileline:%d", $time, `__LINE__); +`ifdef VERILATOR + restrict property (@(e12) ##1 val[0]); + restrict property (@(e12) not ##1 val[0]); +`endif property prop; - @(e12) not ##1 val[0] + @(e13) not ##1 val[0] endproperty assert property (prop) $display("[%0t] property, fileline:%0d", $time, `__LINE__); else $display("[%0t] property, fileline:%0d", $time, `__LINE__); - assert property (@(posedge clk) not (not ##2 val[0] && val[1])) - $display("[%0t] concurrent assert stmt, fileline:%0d", $time, `__LINE__); - else $display("[%0t] concurrent assert else, fileline:%0d", $time, `__LINE__); + assert property (@(e14) val[0] ##2 val[1]) + $display("[%0t] stmt, fileline:%d", $time, `__LINE__); + else + $display("[%0t] else, fileline:%d", $time, `__LINE__); + + assert property (@(e15) val[0] ##1 val[1] ##1 val[0]) + $display("[%0t] stmt, fileline:%d", $time, `__LINE__); + else + $display("[%0t] else, fileline:%d", $time, `__LINE__); endmodule diff --git a/test_regress/t/t_property_sexpr_bad.out b/test_regress/t/t_property_sexpr_bad.out index 7b7051080..3279f25dd 100644 --- a/test_regress/t/t_property_sexpr_bad.out +++ b/test_regress/t/t_property_sexpr_bad.out @@ -1,6 +1,6 @@ -%Error: t/t_property_sexpr_bad.v:20:39: Syntax error: unexpected 'not' in sequence expression +%Error: t/t_property_sexpr_bad.v:20:39: Unexpected 'not' in sequence expression context : ... note: In instance 't' - 20 | assert property (@(posedge clk) ##1 not val) $display("[%0t] single delay with negated var stmt, fileline:%d", $time, 20); + 20 | assert property (@(posedge clk) ##1 not val); | ^~~ ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. %Error: Exiting due to diff --git a/test_regress/t/t_property_sexpr_bad.v b/test_regress/t/t_property_sexpr_bad.v index 86936c100..d5f82cce3 100644 --- a/test_regress/t/t_property_sexpr_bad.v +++ b/test_regress/t/t_property_sexpr_bad.v @@ -12,10 +12,10 @@ module t ( /*AUTOARG*/ input clk; bit val; - always @(negedge clk) begin + always @(posedge clk) begin $write("*-* All Finished *-*\n"); $finish; end - assert property (@(posedge clk) ##1 not val) $display("[%0t] single delay with negated var stmt, fileline:%d", $time, `__LINE__); + assert property (@(posedge clk) ##1 not val); endmodule diff --git a/test_regress/t/t_property_sexpr_cov.dat.out b/test_regress/t/t_property_sexpr_cov.dat.out new file mode 100644 index 000000000..7850e7b1c --- /dev/null +++ b/test_regress/t/t_property_sexpr_cov.dat.out @@ -0,0 +1,5 @@ +# SystemC::Coverage-3 +C 'ft/t_property_sexpr_cov.vl44n3tuserpagev_user/tocoverhtop.t' 2 +C 'ft/t_property_sexpr_cov.vl47n3tuserpagev_user/tocoverhtop.t' 2 +C 'ft/t_property_sexpr_cov.vl50n3tuserpagev_user/tocoverhtop.t' 3 +C 'ft/t_property_sexpr_cov.vl53n3tuserpagev_user/tocoverhtop.t' 25 diff --git a/test_regress/t/t_property_sexpr_cov.out b/test_regress/t/t_property_sexpr_cov.out index 2397081f7..d72891980 100644 --- a/test_regress/t/t_property_sexpr_cov.out +++ b/test_regress/t/t_property_sexpr_cov.out @@ -1,31 +1,33 @@ [4] cover property, fileline:45 -[7] concurrent cover, fileline:51 +[4] cover property, fileline:48 +[7] concurrent cover, fileline:54 [8] cover property, fileline:45 -[12] not cover property, fileline:48 -[15] concurrent cover, fileline:51 -[18] not cover property, fileline:48 -[20] not cover property, fileline:48 -[23] concurrent cover, fileline:51 -[31] concurrent cover, fileline:51 -[39] concurrent cover, fileline:51 -[47] concurrent cover, fileline:51 -[55] concurrent cover, fileline:51 -[63] concurrent cover, fileline:51 -[71] concurrent cover, fileline:51 -[79] concurrent cover, fileline:51 -[87] concurrent cover, fileline:51 -[95] concurrent cover, fileline:51 -[103] concurrent cover, fileline:51 -[111] concurrent cover, fileline:51 -[119] concurrent cover, fileline:51 -[127] concurrent cover, fileline:51 -[135] concurrent cover, fileline:51 -[143] concurrent cover, fileline:51 -[151] concurrent cover, fileline:51 -[159] concurrent cover, fileline:51 -[167] concurrent cover, fileline:51 -[175] concurrent cover, fileline:51 -[183] concurrent cover, fileline:51 -[191] concurrent cover, fileline:51 -[199] concurrent cover, fileline:51 +[8] cover property, fileline:48 +[12] not cover property, fileline:51 +[15] concurrent cover, fileline:54 +[18] not cover property, fileline:51 +[20] not cover property, fileline:51 +[23] concurrent cover, fileline:54 +[31] concurrent cover, fileline:54 +[39] concurrent cover, fileline:54 +[47] concurrent cover, fileline:54 +[55] concurrent cover, fileline:54 +[63] concurrent cover, fileline:54 +[71] concurrent cover, fileline:54 +[79] concurrent cover, fileline:54 +[87] concurrent cover, fileline:54 +[95] concurrent cover, fileline:54 +[103] concurrent cover, fileline:54 +[111] concurrent cover, fileline:54 +[119] concurrent cover, fileline:54 +[127] concurrent cover, fileline:54 +[135] concurrent cover, fileline:54 +[143] concurrent cover, fileline:54 +[151] concurrent cover, fileline:54 +[159] concurrent cover, fileline:54 +[167] concurrent cover, fileline:54 +[175] concurrent cover, fileline:54 +[183] concurrent cover, fileline:54 +[191] concurrent cover, fileline:54 +[199] concurrent cover, fileline:54 *-* All Finished *-* diff --git a/test_regress/t/t_property_sexpr_cov.py b/test_regress/t/t_property_sexpr_cov.py index d48d60eb6..9ca3456b4 100755 --- a/test_regress/t/t_property_sexpr_cov.py +++ b/test_regress/t/t_property_sexpr_cov.py @@ -14,5 +14,6 @@ test.scenarios('simulator') test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing', '--coverage-user']) test.execute(expect_filename=test.golden_filename) +test.files_identical(test.obj_dir + "/coverage.dat", "t/t_property_sexpr_cov.dat.out") test.passes() diff --git a/test_regress/t/t_property_sexpr_cov.v b/test_regress/t/t_property_sexpr_cov.v index 57506da30..a23742ba2 100644 --- a/test_regress/t/t_property_sexpr_cov.v +++ b/test_regress/t/t_property_sexpr_cov.v @@ -41,6 +41,9 @@ module t ( /*AUTOARG*/ end end + cover property (@(e1) ##1 val[0]) + $display("[%0t] cover property, fileline:%0d", $time, `__LINE__); + cover property (@(e1) ##1 val[0]) $display("[%0t] cover property, fileline:%0d", $time, `__LINE__); diff --git a/test_regress/t/t_property_sexpr_multi.py b/test_regress/t/t_property_sexpr_multi.py new file mode 100755 index 000000000..722b56945 --- /dev/null +++ b/test_regress/t/t_property_sexpr_multi.py @@ -0,0 +1,18 @@ +#!/usr/bin/env python3 +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2025 by Wilson Snyder. 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-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', '--dumpi-V3AssertProp 6']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_property_sexpr_multi.v b/test_regress/t/t_property_sexpr_multi.v new file mode 100644 index 000000000..45586fb01 --- /dev/null +++ b/test_regress/t/t_property_sexpr_multi.v @@ -0,0 +1,249 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed into the Public Domain, for any use, +// without warranty, 2025 by Antmicro. +// SPDX-License-Identifier: CC0-1.0 + +`define STRINGIFY(x) `"x`" +`define TRIGGER(e) ->e; $display("[cyc=%0d, val=%0d] triggered %s", cyc, val, `STRINGIFY(e)) + +`define stop $stop +`define checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got='h%p exp='h%p\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0) +`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); + +module t ( /*AUTOARG*/ + // Inputs + clk +); + + input clk; + + bit [1:0] val = 0; + event e1; + event e2; + event e3; + event e4; + event e5; + event e6; + event e7; + event e8; + event e9; + event e10; + event e11; + event e12; + integer cyc = 1; + + typedef struct { + bit fails; + bit passs; + } result_t; + + result_t results [int]; + result_t expected [int]; + + localparam MAX = 66; + always @(posedge clk) begin + ++val; + ++cyc; + + if (cyc == MAX + 1) begin + expected[6] = '{1, 0}; + expected[7] = '{1, 0}; + expected[8] = '{1, 1}; + + expected[11] = '{1, 0}; + expected[12] = '{1, 0}; + expected[13] = '{1, 0}; + expected[15] = '{1, 0}; + expected[16] = '{1, 1}; + expected[17] = '{1, 0}; + + expected[20] = '{1, 0}; + expected[21] = '{1, 0}; + expected[23] = '{1, 0}; + expected[24] = '{1, 0}; + expected[25] = '{1, 0}; + expected[27] = '{1, 1}; + + expected[29] = '{1, 0}; + expected[30] = '{1, 0}; + + expected[32] = '{1, 0}; + expected[33] = '{1, 0}; + + expected[35] = '{1, 0}; + expected[36] = '{1, 0}; + + expected[39] = '{1, 1}; + expected[40] = '{0, 1}; + expected[41] = '{0, 1}; + + expected[43] = '{1, 0}; + expected[44] = '{1, 0}; + expected[45] = '{1, 0}; + + expected[48] = '{0, 1}; + expected[49] = '{0, 1}; + expected[51] = '{1, 1}; + + expected[52] = '{0, 1}; + expected[54] = '{0, 1}; + expected[55] = '{1, 1}; + expected[56] = '{0, 1}; + + expected[58] = '{1, 0}; + expected[59] = '{1, 1}; + expected[60] = '{1, 0}; + + expected[62] = '{0, 1}; + expected[63] = '{0, 1}; + expected[64] = '{0, 1}; + expected[66] = '{0, 1}; + `checkh(results, expected); + $write("*-* All Finished *-*\n"); + $finish; + end + end + + always @(negedge clk) begin + if (cyc >= 5 && cyc <= 9) begin + `TRIGGER(e1); + end + if (cyc >= 10 && cyc <= 18) begin + `TRIGGER(e2); + end + if (cyc >= 19 && cyc <= 27) begin + `TRIGGER(e3); + end + if (cyc >= 28 && cyc <= 30) begin + `TRIGGER(e4); + end + if (cyc >= 31 && cyc <= 33) begin + `TRIGGER(e5); + end + if (cyc >= 34 && cyc <= 36) begin + `TRIGGER(e6); + end + if (cyc >= 37 && cyc <= 41) begin + `TRIGGER(e7); + end + if (cyc >= 42 && cyc <= 46) begin + `TRIGGER(e8); + end + if (cyc >= 47 && cyc <= 51) begin + `TRIGGER(e9); + end + if (cyc >= 52 && cyc <= 56) begin + `TRIGGER(e10); + end + if (cyc >= 57 && cyc <= 61) begin + `TRIGGER(e11); + end + if (cyc >= 62 && cyc <= MAX) begin + `TRIGGER(e12); + end + end + + assert property (@(e1) ##1 1 ##1 1); + + assert property (@(e1) val == 0 ##1 val == 1 ##1 val == 2 ##1 val == 3) + results[cyc].passs = 1; + else + results[cyc].fails = 1; + + assert property (@(e2) ##1 val == 1 ##2 val == 3) + results[cyc].passs = 1; + else + results[cyc].fails = 1; + + assert property (@(e3) ##1 val == 1 ##2 val == 3 ##3 val == 2) + results[cyc].passs = 1; + else + results[cyc].fails = 1; + + // Test failure at each step + assert property (@(e4) cyc == 28 ##1 cyc == 0 ##1 cyc == 30) + results[cyc].passs = 1; + else + results[cyc].fails = 1; + + assert property (@(e5) cyc == 31 ##1 cyc == 32 ##1 cyc == 0) + results[cyc].passs = 1; + else + results[cyc].fails = 1; + + assert property (@(e6) ##1 cyc == 34 ##1 cyc == 0) + results[cyc].passs = 1; + else + results[cyc].fails = 1; + + assert property (@(e7) not ##1 val == 1 ##1 val == 2) + results[cyc].passs = 1; + else + results[cyc].fails = 1; + + assert property (@(e8) not not ##1 val == 1 ##1 val == 2) + results[cyc].passs = 1; + else + results[cyc].fails = 1; + + assert property (@(e9) not not not ##1 val == 1 ##1 val == 2) + results[cyc].passs = 1; + else + results[cyc].fails = 1; + + assert property (@(e10) not val == 0 ##1 val == 1 ##1 val == 2) + results[cyc].passs = 1; + else + results[cyc].fails = 1; + + assert property (@(e11) not not val == 0 ##1 val == 1 ##1 val == 2) + results[cyc].passs = 1; + else + results[cyc].fails = 1; + + assert property (@(e12) not not not val == 0 ##1 val == 1 ##1 val == 2) + results[cyc].passs = 1; + else + results[cyc].fails = 1; + + empty_body_tests empty_body_tests(.clk(clk)); +endmodule + +module empty_body_tests(input clk); + event e; + int cyc = 0; + bit[7:0] hit = 0; + always @(posedge clk) begin + ++cyc; + if (cyc < 5) ->e; + else `checkd(hit, 'b1111111); + end + + assert property (@(e) ##1 1 ##1 1); + assert property (@(e) 1 ##1 1 ##1 1); + assert property (@(e) 1 ##1 1); + + assert property (@(e) ##1 1 ##1 1) begin + hit |= 'b1; + end + assert property (@(e) 1 ##1 1 ##1 1) begin + hit |= 'b10; + end + assert property (@(e) 1 ##1 1) begin + hit |= 'b100; + end + + assert property (@(e) ##1 1 ##1 0) else begin + hit |= 'b1000; + end + assert property (@(e) ##1 0) else begin + hit |= 'b10000; + end + assert property (@(e) 1 ##1 1 ##1 0) else begin + hit |= 'b100000; + end + assert property (@(e) 1 ##1 0) else begin + hit |= 'b1000000; + end +endmodule diff --git a/test_regress/t/t_property_sexpr_parse_unsup.out b/test_regress/t/t_property_sexpr_parse_unsup.out index 0230880e0..4c017ae88 100644 --- a/test_regress/t/t_property_sexpr_parse_unsup.out +++ b/test_regress/t/t_property_sexpr_parse_unsup.out @@ -1,35 +1,23 @@ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:29:39: Unsupported: ## (in sequence expression) - 29 | assert property (@(posedge clk) val ##1 val) $display("[%0t] var with single delay stmt, fileline:%d", $time, 29); - | ^~ - ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:30:43: Unsupported: ## (in sequence expression) - 30 | assert property (@(posedge clk) ##1 val ##2 val) $display("[%0t] sequence stmt, fileline:%d", $time, 30); - | ^~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:71:14: Unsupported: sequence match items - 71 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:75:14: Unsupported: sequence match items + 75 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; | ^ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:71:29: Unsupported: ## range cycle delay range expression - 71 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:75:29: Unsupported: ## range cycle delay range expression + 75 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; | ^~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:70:13: Unsupported: property variable declaration - 70 | integer l_b; +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:74:13: Unsupported: property variable declaration + 74 | integer l_b; | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:88:16: Unsupported: sequence match items - 88 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:16: Unsupported: sequence match items + 92 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; | ^ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:88:51: Unsupported: [-> boolean abbrev expression - 88 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:51: Unsupported: [-> boolean abbrev expression + 92 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:88:54: Unsupported: boolean abbrev (in sequence expression) - 88 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:54: Unsupported: boolean abbrev (in sequence expression) + 92 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; | ^ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:88:35: Unsupported: ## (in sequence expression) - 88 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; - | ^~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:86:14: Unsupported: property variable declaration - 86 | realtime l_t; +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:90:14: Unsupported: property variable declaration + 90 | realtime l_t; | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:31: Unsupported: ## (in sequence expression) - 92 | assert property (@clk not a ##1 b); - | ^~ %Error: Exiting due to diff --git a/test_regress/t/t_property_sexpr_unsup.out b/test_regress/t/t_property_sexpr_unsup.out index 367002cf4..67f822d29 100644 --- a/test_regress/t/t_property_sexpr_unsup.out +++ b/test_regress/t/t_property_sexpr_unsup.out @@ -1,35 +1,50 @@ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:32:41: Unsupported: Implication with sequence expression - 32 | assert property (@(posedge clk) ##1 1 |-> 1) $display("[%0t] single delay with const implication stmt, fileline:%d", $time, 32); +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:29:41: Unsupported: Implication with sequence expression + : ... note: In instance 't' + 29 | assert property (@(posedge clk) ##1 1 |-> 1) $display("[%0t] single delay with const implication stmt, fileline:%d", $time, 29); | ^~~ ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:34:41: Unsupported: Implication with sequence expression - 34 | assert property (@(posedge clk) ##1 1 |-> not (val)) $display("[%0t] single delay implication with negated var stmt, fileline:%d", $time, 34); +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:31:41: Unsupported: Implication with sequence expression + : ... note: In instance 't' + 31 | assert property (@(posedge clk) ##1 1 |-> not (val)) $display("[%0t] single delay implication with negated var stmt, fileline:%d", $time, 31); | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:36:37: Unsupported: Implication with sequence expression - 36 | assert property (@(posedge clk) 1 |-> ##1 val) $display("[%0t] single delay implication with negated var stmt, fileline:%d", $time, 36); +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:33:37: Unsupported: Implication with sequence expression + : ... note: In instance 't' + 33 | assert property (@(posedge clk) 1 |-> ##1 val) $display("[%0t] single delay implication with negated var stmt, fileline:%d", $time, 33); | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:38:45: Unsupported: Implication with sequence expression - 38 | assert property (@(posedge clk) (##1 val) |-> (not val)) $display("[%0t] single delay with negated implication stmt, fileline:%d", $time, 38); +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:35:45: Unsupported: Implication with sequence expression + : ... note: In instance 't' + 35 | assert property (@(posedge clk) (##1 val) |-> (not val)) $display("[%0t] single delay with negated implication stmt, fileline:%d", $time, 35); | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:40:45: Unsupported: Implication with sequence expression - 40 | assert property (@(posedge clk) ##1 (val) |-> not (val)) $display("[%0t] single delay with negated implication brackets stmt, fileline:%d", $time, 40); +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:37:45: Unsupported: Implication with sequence expression + : ... note: In instance 't' + 37 | assert property (@(posedge clk) ##1 (val) |-> not (val)) $display("[%0t] single delay with negated implication brackets stmt, fileline:%d", $time, 37); | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:44:41: Unsupported: Implication with sequence expression - 44 | assert property (@(posedge clk) ##1 1 |-> 0) $display("[%0t] disable iff with cond implication stmt, fileline:%d", $time, 44); +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:41:41: Unsupported: Implication with sequence expression + : ... note: In instance 't' + 41 | assert property (@(posedge clk) ##1 1 |-> 0) $display("[%0t] disable iff with cond implication stmt, fileline:%d", $time, 41); | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:46:45: Unsupported: Implication with sequence expression - 46 | assert property (@(posedge clk) (##1 val) |-> (##1 val)) $display("[%0t] two delays implication stmt, fileline:%d", $time, 46); +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:43:45: Unsupported: Implication with sequence expression + : ... note: In instance 't' + 43 | assert property (@(posedge clk) (##1 val) |-> (##1 val)) $display("[%0t] two delays implication stmt, fileline:%d", $time, 43); | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:48:52: Unsupported: Disable iff with sequence expression +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:45:52: Unsupported: Disable iff with sequence expression : ... note: In instance 't' - 48 | assert property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 48); + 45 | assert property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 45); | ^~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:50:52: Unsupported: Disable iff with sequence expression +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:47:52: Unsupported: Disable iff with sequence expression : ... note: In instance 't' - 50 | assume property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 50); + 47 | assume property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 47); | ^~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:52:51: Unsupported: Disable iff with sequence expression +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:49:51: Unsupported: Disable iff with sequence expression : ... note: In instance 't' - 52 | cover property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 52); + 49 | cover property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 49); | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:52:37: Unsupported: Disable iff with sequence expression + : ... note: In instance 't' + 52 | @(posedge clk) disable iff (cyc != 5) ##1 0; + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:56:18: Unsupported: Implication with sequence expression + : ... note: In instance 't' + 56 | ##1 cyc == 4 |-> 1; + | ^~~ %Error: Exiting due to diff --git a/test_regress/t/t_property_sexpr_unsup.v b/test_regress/t/t_property_sexpr_unsup.v index 91654e717..da27da6c0 100644 --- a/test_regress/t/t_property_sexpr_unsup.v +++ b/test_regress/t/t_property_sexpr_unsup.v @@ -25,10 +25,7 @@ module t ( /*AUTOARG*/ end end end -`ifdef PARSING_TIME - assert property (@(posedge clk) val ##1 val) $display("[%0t] var with single delay stmt, fileline:%d", $time, `__LINE__); - assert property (@(posedge clk) ##1 val ##2 val) $display("[%0t] sequence stmt, fileline:%d", $time, `__LINE__); -`else + assert property (@(posedge clk) ##1 1 |-> 1) $display("[%0t] single delay with const implication stmt, fileline:%d", $time, `__LINE__); assert property (@(posedge clk) ##1 1 |-> not (val)) $display("[%0t] single delay implication with negated var stmt, fileline:%d", $time, `__LINE__); @@ -50,7 +47,14 @@ module t ( /*AUTOARG*/ assume property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, `__LINE__); cover property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, `__LINE__); -`endif + + property prop_disableiff; + @(posedge clk) disable iff (cyc != 5) ##1 0; + endproperty + + property prop_implication; + ##1 cyc == 4 |-> 1; + endproperty endmodule // Test parsing only diff --git a/test_regress/t/t_sequence_sexpr_unsup.out b/test_regress/t/t_sequence_sexpr_unsup.out index 1f9d09780..a74f6a345 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.out +++ b/test_regress/t/t_sequence_sexpr_unsup.out @@ -66,152 +66,131 @@ 68 | ## [+] b; | ^~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:71:4: Unsupported: sequence - 71 | sequence s_cycdelay_int; + 71 | sequence s_cycdelay_id; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:72:9: Unsupported: ## (in sequence expression) - 72 | a ## 1 b; +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:72:9: Unsupported: ## id cycle delay range expression + 72 | a ## DELAY b; | ^~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:74:4: Unsupported: sequence - 74 | sequence s_cycdelay_id; + 74 | sequence s_cycdelay_pid; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:75:9: Unsupported: ## id cycle delay range expression - 75 | a ## DELAY b; - | ^~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:75:9: Unsupported: ## (in sequence expression) - 75 | a ## DELAY b; +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:75:9: Unsupported: ## () cycle delay range expression + 75 | a ## ( DELAY ) b; | ^~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:77:4: Unsupported: sequence - 77 | sequence s_cycdelay_pid; + 77 | sequence s_cycdelay_range; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:78:9: Unsupported: ## () cycle delay range expression - 78 | a ## ( DELAY ) b; - | ^~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:78:9: Unsupported: ## (in sequence expression) - 78 | a ## ( DELAY ) b; +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:78:9: Unsupported: ## range cycle delay range expression + 78 | a ## [1:2] b; | ^~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:80:4: Unsupported: sequence - 80 | sequence s_cycdelay_range; + 80 | sequence s_cycdelay_star; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:81:9: Unsupported: ## range cycle delay range expression - 81 | a ## [1:2] b; - | ^~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:81:9: Unsupported: ## (in sequence expression) - 81 | a ## [1:2] b; +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:81:9: Unsupported: ## [*] cycle delay range expression + 81 | a ## [*] b; | ^~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:83:4: Unsupported: sequence - 83 | sequence s_cycdelay_star; + 83 | sequence s_cycdelay_plus; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:84:9: Unsupported: ## [*] cycle delay range expression - 84 | a ## [*] b; +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:84:9: Unsupported: ## [+] cycle delay range expression + 84 | a ## [+] b; | ^~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:84:9: Unsupported: ## (in sequence expression) - 84 | a ## [*] b; - | ^~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:86:4: Unsupported: sequence - 86 | sequence s_cycdelay_plus; +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:87:4: Unsupported: sequence + 87 | sequence s_booleanabbrev_brastar_int; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:87:9: Unsupported: ## [+] cycle delay range expression - 87 | a ## [+] b; - | ^~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:87:9: Unsupported: ## (in sequence expression) - 87 | a ## [+] b; +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:88:9: Unsupported: [*] boolean abbrev expression + 88 | a [* 1 ]; | ^~ +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:88:12: Unsupported: boolean abbrev (in sequence expression) + 88 | a [* 1 ]; + | ^ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:90:4: Unsupported: sequence - 90 | sequence s_booleanabbrev_brastar_int; + 90 | sequence s_booleanabbrev_brastar; | ^~~~~~~~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:91:9: Unsupported: [*] boolean abbrev expression - 91 | a [* 1 ]; + 91 | a [*]; + | ^~ +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:91:9: Unsupported: boolean abbrev (in sequence expression) + 91 | a [*]; | ^~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:91:12: Unsupported: boolean abbrev (in sequence expression) - 91 | a [* 1 ]; - | ^ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:93:4: Unsupported: sequence - 93 | sequence s_booleanabbrev_brastar; + 93 | sequence s_booleanabbrev_plus; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:94:9: Unsupported: [*] boolean abbrev expression - 94 | a [*]; - | ^~ +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:94:9: Unsupported: [+] boolean abbrev expression + 94 | a [+]; + | ^~~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:94:9: Unsupported: boolean abbrev (in sequence expression) - 94 | a [*]; - | ^~ + 94 | a [+]; + | ^~~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:96:4: Unsupported: sequence - 96 | sequence s_booleanabbrev_plus; + 96 | sequence s_booleanabbrev_eq; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:97:9: Unsupported: [+] boolean abbrev expression - 97 | a [+]; - | ^~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:97:9: Unsupported: boolean abbrev (in sequence expression) - 97 | a [+]; - | ^~~ +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:97:9: Unsupported: [= boolean abbrev expression + 97 | a [= 1]; + | ^~ +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:97:12: Unsupported: boolean abbrev (in sequence expression) + 97 | a [= 1]; + | ^ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:99:4: Unsupported: sequence - 99 | sequence s_booleanabbrev_eq; + 99 | sequence s_booleanabbrev_eq_range; | ^~~~~~~~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:100:9: Unsupported: [= boolean abbrev expression - 100 | a [= 1]; + 100 | a [= 1:2]; | ^~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:100:12: Unsupported: boolean abbrev (in sequence expression) - 100 | a [= 1]; + 100 | a [= 1:2]; | ^ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:102:4: Unsupported: sequence - 102 | sequence s_booleanabbrev_eq_range; + 102 | sequence s_booleanabbrev_minusgt; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:103:9: Unsupported: [= boolean abbrev expression - 103 | a [= 1:2]; - | ^~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:103:12: Unsupported: boolean abbrev (in sequence expression) - 103 | a [= 1:2]; - | ^ +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:103:9: Unsupported: [-> boolean abbrev expression + 103 | a [-> 1]; + | ^~~ +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:103:13: Unsupported: boolean abbrev (in sequence expression) + 103 | a [-> 1]; + | ^ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:105:4: Unsupported: sequence - 105 | sequence s_booleanabbrev_minusgt; + 105 | sequence s_booleanabbrev_minusgt_range; | ^~~~~~~~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:106:9: Unsupported: [-> boolean abbrev expression - 106 | a [-> 1]; + 106 | a [-> 1:2]; | ^~~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:106:13: Unsupported: boolean abbrev (in sequence expression) - 106 | a [-> 1]; + 106 | a [-> 1:2]; | ^ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:108:4: Unsupported: sequence - 108 | sequence s_booleanabbrev_minusgt_range; +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:109:4: Unsupported: sequence + 109 | sequence p_arg_seqence(sequence inseq); | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:109:9: Unsupported: [-> boolean abbrev expression - 109 | a [-> 1:2]; - | ^~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:109:13: Unsupported: boolean abbrev (in sequence expression) - 109 | a [-> 1:2]; - | ^ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:112:4: Unsupported: sequence - 112 | sequence p_arg_seqence(sequence inseq); - | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:112:27: Unsupported: sequence argument data type - 112 | sequence p_arg_seqence(sequence inseq); +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:109:27: Unsupported: sequence argument data type + 109 | sequence p_arg_seqence(sequence inseq); | ^~~~~~~~ +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:113:4: Unsupported: sequence + 113 | sequence s_firstmatch_a; + | ^~~~~~~~ +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:114:7: Unsupported: first_match (in sequence expression) + 114 | first_match (a); + | ^~~~~~~~~~~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:116:4: Unsupported: sequence - 116 | sequence s_firstmatch_a; + 116 | sequence s_firstmatch_ab; | ^~~~~~~~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:117:7: Unsupported: first_match (in sequence expression) - 117 | first_match (a); + 117 | first_match (a, res0 = 1); | ^~~~~~~~~~~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:119:4: Unsupported: sequence - 119 | sequence s_firstmatch_ab; + 119 | sequence s_firstmatch_abc; | ^~~~~~~~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:120:7: Unsupported: first_match (in sequence expression) - 120 | first_match (a, res0 = 1); + 120 | first_match (a, res0 = 1, res1 = 2); | ^~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:122:4: Unsupported: sequence - 122 | sequence s_firstmatch_abc; - | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:123:7: Unsupported: first_match (in sequence expression) - 123 | first_match (a, res0 = 1, res1 = 2); - | ^~~~~~~~~~~ -%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:126:10: Ignoring unsupported: cover sequence - 126 | cover sequence (s_a) $display(""); +%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:123:10: Ignoring unsupported: cover sequence + 123 | cover sequence (s_a) $display(""); | ^~~~~~~~ ... For warning description see https://verilator.org/warn/COVERIGN?v=latest ... Use "/* verilator lint_off COVERIGN */" and lint_on around source to disable this message. -%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:127:10: Ignoring unsupported: cover sequence - 127 | cover sequence (@(posedge a) disable iff (b) s_a) $display(""); +%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:124:10: Ignoring unsupported: cover sequence + 124 | cover sequence (@(posedge a) disable iff (b) s_a) $display(""); | ^~~~~~~~ -%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:128:10: Ignoring unsupported: cover sequence - 128 | cover sequence (disable iff (b) s_a) $display(""); +%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:125:10: Ignoring unsupported: cover sequence + 125 | cover sequence (disable iff (b) s_a) $display(""); | ^~~~~~~~ %Error: Exiting due to diff --git a/test_regress/t/t_sequence_sexpr_unsup.v b/test_regress/t/t_sequence_sexpr_unsup.v index 662f1f1c1..d2ffb3a48 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.v +++ b/test_regress/t/t_sequence_sexpr_unsup.v @@ -68,9 +68,6 @@ module t (/*AUTOARG*/ ## [+] b; endsequence - sequence s_cycdelay_int; - a ## 1 b; - endsequence sequence s_cycdelay_id; a ## DELAY b; endsequence