luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Support multi-expression sequences (#6639)

This commit is contained in:
Bartłomiej Chmiel 2025-11-06 14:42:27 +01:00 committed by GitHub
parent f7e12e9219
commit 5adecb9fa3
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
30 changed files with 1107 additions and 553 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/CMakeLists.txt
View File

@ -43,6 +43,7 @@ set(HEADERS
V3ActiveTop.h V3ActiveTop.h
V3Assert.h V3Assert.h
V3AssertPre.h V3AssertPre.h
V3AssertProp.h
V3Ast.h V3Ast.h
V3AstAttr.h V3AstAttr.h
V3AstInlines.h V3AstInlines.h
@ -207,6 +208,7 @@ set(COMMON_SOURCES
V3ActiveTop.cpp V3ActiveTop.cpp
V3Assert.cpp V3Assert.cpp
V3AssertPre.cpp V3AssertPre.cpp
V3AssertProp.cpp
V3Ast.cpp V3Ast.cpp
V3AstNodes.cpp V3AstNodes.cpp
V3Begin.cpp V3Begin.cpp

1
src/Makefile_obj.in
View File

@ -232,6 +232,7 @@ RAW_OBJS_PCH_ASTNOMT = \
V3ActiveTop.o \ V3ActiveTop.o \
V3Assert.o \ V3Assert.o \
V3AssertPre.o \ V3AssertPre.o \
V3AssertProp.o \
V3Begin.o \ V3Begin.o \
V3Branch.o \ V3Branch.o \
V3CCtors.o \ V3CCtors.o \

70
src/V3Assert.cpp
View File

@ -143,6 +143,9 @@ class AssertVisitor final : public VNVisitor {
VDouble0 m_statPastVars; // Statistic tracking VDouble0 m_statPastVars; // Statistic tracking
bool m_inSampled = false; // True inside a sampled expression bool m_inSampled = false; // True inside a sampled expression
bool m_inRestrict = false; // True inside restrict assertion 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 // METHODS
static AstNodeExpr* assertOnCond(FileLine* fl, VAssertType type, static AstNodeExpr* assertOnCond(FileLine* fl, VAssertType type,
@ -288,25 +291,18 @@ class AssertVisitor final : public VNVisitor {
return ifp; return ifp;
} }
static AstNode* assertBody(AstNodeCoverOrAssert* nodep, AstNodeExpr* propp, AstNode* passsp, AstNode* assertBody(AstNodeCoverOrAssert* nodep, AstNode* propp, AstNode* passsp,
AstNode* failsp) { AstNode* failsp) {
if (AstPExpr* const pExpr = VN_CAST(propp, PExpr)) { AstNode* bodyp = nullptr;
AstNodeExpr* const condp = pExpr->condp(); if (AstPExpr* const pexprp = VN_CAST(propp, PExpr)) {
UASSERT_OBJ(condp, pExpr, "Should have condition"); AstFork* const forkp = new AstFork{nodep->fileline(), VJoinType::JOIN_NONE};
AstIf* const ifp = assertCond(nodep, condp->unlinkFrBack(), passsp, failsp); forkp->addForksp(pexprp->bodyp()->unlinkFrBack());
VL_DO_DANGLING(pushDeletep(pexprp), pexprp);
AstNode* const precondps = pExpr->precondp(); bodyp = forkp;
UASSERT_OBJ(precondps, pExpr, "Should have precondition"); } else {
precondps->unlinkFrBackWithNext()->addNext(ifp); bodyp = assertCond(nodep, VN_AS(propp, NodeExpr), passsp, failsp);
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;
} }
return newIfAssertOn(bodyp, nodep->directive(), nodep->type());
AstIf* const ifp = assertCond(nodep, propp, passsp, failsp);
return newIfAssertOn(ifp, nodep->directive(), nodep->type());
} }
AstNodeStmt* newFireAssertUnchecked(const AstNodeStmt* nodep, const string& message, AstNodeStmt* newFireAssertUnchecked(const AstNodeStmt* nodep, const string& message,
@ -336,7 +332,6 @@ class AssertVisitor final : public VNVisitor {
{ AssertDeFuture{nodep->propp(), m_modp, m_modPastNum++}; } { AssertDeFuture{nodep->propp(), m_modp, m_modPastNum++}; }
iterateChildren(nodep); iterateChildren(nodep);
AstNodeExpr* const propp = VN_AS(nodep->propp()->unlinkFrBackWithNext(), NodeExpr);
AstSenTree* const sentreep = nodep->sentreep(); AstSenTree* const sentreep = nodep->sentreep();
const string& message = nodep->name(); const string& message = nodep->name();
AstNode* passsp = nodep->passsp(); AstNode* passsp = nodep->passsp();
@ -384,7 +379,15 @@ class AssertVisitor final : public VNVisitor {
nodep->v3fatalSrc("Unknown node type"); 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) { if (sentreep) {
bodysp = new AstAlways{nodep->fileline(), VAlwaysKwd::ALWAYS, sentreep, bodysp}; bodysp = new AstAlways{nodep->fileline(), VAlwaysKwd::ALWAYS, sentreep, bodysp};
} }
@ -631,7 +634,7 @@ class AssertVisitor final : public VNVisitor {
} }
void visit(AstVarRef* nodep) override { void visit(AstVarRef* nodep) override {
iterateChildren(nodep); iterateChildren(nodep);
if (m_inSampled && !VString::startsWith(nodep->name(), "__VpropPrecond")) { if (m_inSampled && !VString::startsWith(nodep->name(), "__VcycleDly")) {
if (!nodep->access().isReadOnly()) { if (!nodep->access().isReadOnly()) {
nodep->v3warn(E_UNSUPPORTED, nodep->v3warn(E_UNSUPPORTED,
"Unsupported: Write to variable in sampled expression"); "Unsupported: Write to variable in sampled expression");
@ -651,16 +654,27 @@ class AssertVisitor final : public VNVisitor {
m_inSampled = false; m_inSampled = false;
iterateChildren(nodep); 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 { void visit(AstPExpr* nodep) override {
{ if (m_underAssert) {
VL_RESTORER(m_inSampled); VL_RESTORER(m_inSampled);
m_inSampled = false; m_inSampled = false;
iterateAndNextNull(nodep->precondp()); iterateChildren(nodep);
} } else if (m_inRestrict) {
iterate(nodep->condp());
if (!m_inRestrict) {
VL_DO_DANGLING(pushDeletep(nodep), nodep);
} else {
VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep); VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep);
} }
} }

80
src/V3AssertPre.cpp
View File

@ -56,15 +56,11 @@ private:
AstNodeExpr* m_disablep = nullptr; // Last disable AstNodeExpr* m_disablep = nullptr; // Last disable
// Other: // Other:
V3UniqueNames m_cycleDlyNames{"__VcycleDly"}; // Cycle delay counter name generator 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_inAssign = false; // True if in an AssignNode
bool m_inAssignDlyLhs = false; // True if in AssignDly's LHS bool m_inAssignDlyLhs = false; // True if in AssignDly's LHS
bool m_inSynchDrive = false; // True if in synchronous drive bool m_inSynchDrive = false; // True if in synchronous drive
std::vector<AstVarXRef*> m_xrefsp; // list of xrefs that need name fixup std::vector<AstVarXRef*> m_xrefsp; // list of xrefs that need name fixup
AstNodeExpr* m_hasUnsupp = nullptr; // True if assert has unsupported construct inside bool m_inPExpr = false; // True if in AstPExpr
AstPExpr* m_pExpr = nullptr; // Current AstPExpr
bool m_hasSExpr = false; // True if assert has AstSExpr inside
bool m_inSExpr = false; // True if in AstSExpr
// METHODS // METHODS
@ -343,7 +339,7 @@ private:
} }
AstSenItem* sensesp = nullptr; AstSenItem* sensesp = nullptr;
if (!m_defaultClockingp) { if (!m_defaultClockingp) {
if (!m_pExpr && !m_inSExpr) { if (!m_inPExpr) {
nodep->v3error("Usage of cycle delays requires default clocking" nodep->v3error("Usage of cycle delays requires default clocking"
" (IEEE 1800-2023 14.11)"); " (IEEE 1800-2023 14.11)");
VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep); VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep);
@ -419,33 +415,6 @@ private:
} }
} }
nodep->user1(true); 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 { void visit(AstMemberSel* nodep) override {
@ -500,32 +469,11 @@ private:
void visit(AstNodeCoverOrAssert* nodep) override { void visit(AstNodeCoverOrAssert* nodep) override {
if (nodep->sentreep()) return; // Already processed if (nodep->sentreep()) return; // Already processed
VL_RESTORER(m_hasSExpr);
VL_RESTORER(m_hasUnsupp);
clearAssertInfo(); clearAssertInfo();
m_pExpr = new AstPExpr{nodep->propp()->fileline()};
m_pExpr->dtypeFrom(nodep->propp());
// Find Clocking's buried under nodep->exprsp // Find Clocking's buried under nodep->exprsp
iterateChildren(nodep); iterateChildren(nodep);
if (!nodep->immediate()) nodep->sentreep(newSenTree(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(); clearAssertInfo();
} }
void visit(AstFalling* nodep) override { void visit(AstFalling* nodep) override {
@ -564,10 +512,6 @@ private:
if (sentreep) VL_DO_DANGLING(pushDeletep(sentreep->unlinkFrBack()), sentreep); if (sentreep) VL_DO_DANGLING(pushDeletep(sentreep->unlinkFrBack()), sentreep);
nodep->sentreep(newSenTree(nodep)); 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 { void visit(AstPast* nodep) override {
if (nodep->sentreep()) return; // Already processed if (nodep->sentreep()) return; // Already processed
iterateChildren(nodep); iterateChildren(nodep);
@ -633,7 +577,6 @@ private:
void visit(AstImplication* nodep) override { void visit(AstImplication* nodep) override {
if (nodep->sentreep()) return; // Already processed if (nodep->sentreep()) return; // Already processed
m_hasUnsupp = nodep;
iterateChildren(nodep); iterateChildren(nodep);
@ -685,7 +628,6 @@ private:
} }
if (AstNodeExpr* const disablep = nodep->disablep()) { if (AstNodeExpr* const disablep = nodep->disablep()) {
m_disablep = disablep; m_disablep = disablep;
m_hasUnsupp = disablep;
if (VN_IS(nodep->backp(), Cover)) { if (VN_IS(nodep->backp(), Cover)) {
blockp = new AstAnd{disablep->fileline(), blockp = new AstAnd{disablep->fileline(),
new AstNot{disablep->fileline(), disablep->unlinkFrBack()}, new AstNot{disablep->fileline(), disablep->unlinkFrBack()},
@ -699,17 +641,19 @@ private:
nodep->replaceWith(blockp); nodep->replaceWith(blockp);
VL_DO_DANGLING(pushDeletep(nodep), nodep); VL_DO_DANGLING(pushDeletep(nodep), nodep);
} }
void visit(AstSExpr* nodep) override { void visit(AstPExpr* nodep) override {
VL_RESTORER(m_inSExpr); VL_RESTORER(m_inPExpr);
m_inSExpr = true; m_inPExpr = true;
m_hasSExpr = true;
UASSERT_OBJ(m_pExpr, nodep, "Should be under assertion"); if (AstLogNot* const notp = VN_CAST(nodep->backp(), LogNot)) {
m_pExpr->addPrecondp(nodep->delayp()->unlinkFrBack()); notp->replaceWith(nodep->unlinkFrBack());
VL_DO_DANGLING(pushDeletep(notp), notp);
iterate(nodep);
} else {
iterateChildren(nodep);
}
iterateChildren(nodep); iterateChildren(nodep);
nodep->replaceWith(nodep->exprp()->unlinkFrBack());
VL_DO_DANGLING(pushDeletep(nodep), nodep);
} }
void visit(AstNodeModule* nodep) override { void visit(AstNodeModule* nodep) override {
VL_RESTORER(m_defaultClockingp); VL_RESTORER(m_defaultClockingp);

264
src/V3AssertProp.cpp Normal file
View File

@ -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<DfaStmtVertex>()) return processVtx(stmtp);
if (DfaExprVertex* const exprp = vtxp->cast<DfaExprVertex>()) 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<DfaStmtVertex>()->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<DfaExprVertex>()) {
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);
}

32
src/V3AssertProp.h Normal file
View File

@ -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

24
src/V3AstNodeExpr.h
View File

@ -1778,11 +1778,13 @@ public:
}; };
class AstPExpr final : public AstNodeExpr { class AstPExpr final : public AstNodeExpr {
// Property expression // Property expression
// @astgen op1 := precondp : List[AstNode] // @astgen op1 := bodyp : AstBegin
// @astgen op2 := condp : Optional[AstNodeExpr]
public: public:
explicit AstPExpr(FileLine* fl) explicit AstPExpr(FileLine* fl, AstBegin* bodyp, AstNodeDType* dtypep)
: ASTGEN_SUPER_PExpr(fl) {} : ASTGEN_SUPER_PExpr(fl) {
this->bodyp(bodyp);
this->dtypep(dtypep);
}
ASTGEN_MEMBERS_AstPExpr; ASTGEN_MEMBERS_AstPExpr;
string emitVerilog() override { V3ERROR_NA_RETURN(""); } string emitVerilog() override { V3ERROR_NA_RETURN(""); }
string emitC() override { V3ERROR_NA_RETURN(""); } string emitC() override { V3ERROR_NA_RETURN(""); }
@ -2005,11 +2007,19 @@ public:
}; };
class AstSExpr final : public AstNodeExpr { class AstSExpr final : public AstNodeExpr {
// Sequence expression // Sequence expression
// @astgen op1 := delayp : AstDelay // @astgen op1 := preExprp: Optional[AstNodeExpr]
// @astgen op2 := exprp : AstNodeExpr // @astgen op2 := delayp : AstNodeStmt<AstDelay|AstBegin>
// @astgen op3 := exprp : AstNodeExpr
public: public:
explicit AstSExpr(FileLine* fl, AstDelay* delayp, AstNodeExpr* exprp) explicit AstSExpr(FileLine* fl, AstNodeExpr* preExprp, AstNodeStmt* delayp, AstNodeExpr* exprp)
: ASTGEN_SUPER_SExpr(fl) { : 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->delayp(delayp);
this->exprp(exprp); this->exprp(exprp);
} }

11
src/V3AstNodeStmt.h
View File

@ -821,6 +821,17 @@ public:
} }
bool off() const { return m_off; } 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 { class AstPrintTimeScale final : public AstNodeStmt {
// Parents: stmtlist // Parents: stmtlist
string m_name; // Parent module name string m_name; // Parent module name

23
src/V3EmitV.cpp
View File

@ -365,6 +365,7 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
void visit(AstSFormat* nodep) override { void visit(AstSFormat* nodep) override {
visitNodeDisplay(nodep, nodep->lhsp(), nodep->fmtp()->text(), nodep->fmtp()->exprsp()); visitNodeDisplay(nodep, nodep->lhsp(), nodep->fmtp()->text(), nodep->fmtp()->exprsp());
} }
void visit(AstToStringN* nodep) override { iterateConst(nodep->lhsp()); }
void visit(AstSFormatF* nodep) override { void visit(AstSFormatF* nodep) override {
visitNodeDisplay(nodep, nullptr, nodep->text(), nodep->exprsp()); visitNodeDisplay(nodep, nullptr, nodep->text(), nodep->exprsp());
} }
@ -803,9 +804,6 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
puts(";\n"); puts(";\n");
} }
void visit(AstNodeCoverOrAssert* nodep) override { void visit(AstNodeCoverOrAssert* nodep) override {
if (AstPExpr* const pexprp = VN_CAST(nodep->propp(), PExpr)) {
iterateAndNextConstNull(pexprp);
}
putfs(nodep, nodep->verilogKwd() + " "); putfs(nodep, nodep->verilogKwd() + " ");
if (nodep->type() == VAssertType::OBSERVED_DEFERRED_IMMEDIATE) { if (nodep->type() == VAssertType::OBSERVED_DEFERRED_IMMEDIATE) {
puts("#0 "); puts("#0 ");
@ -816,14 +814,10 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
} }
iterateConstNull(nodep->sentreep()); iterateConstNull(nodep->sentreep());
puts("("); puts("(");
if (const AstPExpr* const pexprp = VN_CAST(nodep->propp(), PExpr)) { if (AstSampled* const sampledp = VN_CAST(nodep->propp(), Sampled)) {
iterateAndNextConstNull(pexprp->condp()); iterateAndNextConstNull(sampledp->exprp());
} else { } else {
if (AstSampled* const sampledp = VN_CAST(nodep->propp(), Sampled)) { iterateAndNextConstNull(nodep->propp());
iterateAndNextConstNull(sampledp->exprp());
} else {
iterateAndNextConstNull(nodep->propp());
}
} }
if (!VN_IS(nodep, Restrict)) { if (!VN_IS(nodep, Restrict)) {
puts(") begin\n"); puts(") begin\n");
@ -1056,16 +1050,15 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
iterateConstNull(nodep->propp()); iterateConstNull(nodep->propp());
puts("\n"); puts("\n");
} }
void visit(AstPExpr* nodep) override { void visit(AstPExpr* nodep) override { iterateConst(nodep->bodyp()); }
iterateAndNextConstNull(nodep->precondp()); // condp emitted by AstNodeCoverOrAssert
}
void visit(AstSExpr* nodep) override { void visit(AstSExpr* nodep) override {
iterateConstNull(nodep->preExprp());
{ {
VL_RESTORER(m_suppressSemi); VL_RESTORER(m_suppressSemi);
m_suppressSemi = true; m_suppressSemi = true;
iterateConstNull(nodep->delayp()); iterateConst(nodep->delayp());
} }
iterateConstNull(nodep->exprp()); iterateConst(nodep->exprp());
} }
// Terminals // Terminals

35
src/V3Width.cpp
View File

@ -215,6 +215,9 @@ class WidthVisitor final : public VNVisitor {
V3TaskConnectState m_taskConnectState; // State to cache V3Task::taskConnects V3TaskConnectState m_taskConnectState; // State to cache V3Task::taskConnects
WidthVP* m_vup = nullptr; // Current node state WidthVP* m_vup = nullptr; // Current node state
bool m_underFork = false; // Visiting under a fork 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 AstCell* m_cellp = nullptr; // Current cell for arrayed instantiations
const AstEnumItem* m_enumItemp = nullptr; // Current enum item const AstEnumItem* m_enumItemp = nullptr; // Current enum item
AstNodeFTask* m_ftaskp = nullptr; // Current function/task AstNodeFTask* m_ftaskp = nullptr; // Current function/task
@ -1539,6 +1542,7 @@ class WidthVisitor final : public VNVisitor {
} }
void visit(AstImplication* nodep) override { void visit(AstImplication* nodep) override {
m_seqUnsupp = nodep;
if (m_vup->prelim()) { if (m_vup->prelim()) {
iterateCheckBool(nodep, "LHS", nodep->lhsp(), BOTH); iterateCheckBool(nodep, "LHS", nodep->lhsp(), BOTH);
iterateCheckBool(nodep, "RHS", nodep->rhsp(), BOTH); iterateCheckBool(nodep, "RHS", nodep->rhsp(), BOTH);
@ -1557,9 +1561,15 @@ class WidthVisitor final : public VNVisitor {
} }
} }
void visit(AstSExpr* nodep) override { void visit(AstSExpr* nodep) override {
VL_RESTORER(m_underSExpr);
m_underSExpr = true;
m_hasSExpr = true;
if (m_vup->prelim()) { if (m_vup->prelim()) {
iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH); if (nodep->preExprp()) {
iterateCheckBool(nodep, "preExprp", nodep->preExprp(), BOTH);
}
iterate(nodep->delayp()); iterate(nodep->delayp());
iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH);
nodep->dtypeSetBit(); nodep->dtypeSetBit();
} }
} }
@ -5338,6 +5348,8 @@ class WidthVisitor final : public VNVisitor {
} }
void visit(AstPropSpec* nodep) override { void visit(AstPropSpec* nodep) override {
VL_RESTORER(m_seqUnsupp);
VL_RESTORER(m_hasSExpr);
if (m_vup->prelim()) { // First stage evaluation if (m_vup->prelim()) { // First stage evaluation
iterateCheckBool(nodep, "Property", nodep->propp(), BOTH); iterateCheckBool(nodep, "Property", nodep->propp(), BOTH);
userIterateAndNext(nodep->sensesp(), nullptr); userIterateAndNext(nodep->sensesp(), nullptr);
@ -5346,6 +5358,20 @@ class WidthVisitor final : public VNVisitor {
BOTH); // it's like an if() condition. BOTH); // it's like an if() condition.
} }
nodep->dtypeSetBit(); 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()) { if (m_vup->prelim()) {
iterateCheckBool(nodep, "LHS", nodep->op1p(), BOTH); iterateCheckBool(nodep, "LHS", nodep->op1p(), BOTH);
nodep->dtypeSetBit(); 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) { void visit_log_and_or(AstNodeBiop* nodep) {

3
src/Verilator.cpp
View File

@ -20,6 +20,7 @@
#include "V3ActiveTop.h" #include "V3ActiveTop.h"
#include "V3Assert.h" #include "V3Assert.h"
#include "V3AssertPre.h" #include "V3AssertPre.h"
#include "V3AssertProp.h"
#include "V3Ast.h" #include "V3Ast.h"
#include "V3Begin.h" #include "V3Begin.h"
#include "V3Branch.h" #include "V3Branch.h"
@ -240,6 +241,8 @@ static void process() {
// Assertion insertion // Assertion insertion
// After we've added block coverage, but before other nasty transforms // After we've added block coverage, but before other nasty transforms
V3AssertProp::assertPropAll(v3Global.rootp());
//
V3AssertPre::assertPreAll(v3Global.rootp()); V3AssertPre::assertPreAll(v3Global.rootp());
// //
V3Assert::assertAll(v3Global.rootp()); V3Assert::assertAll(v3Global.rootp());

5
src/verilog.y
View File

@ -6534,7 +6534,8 @@ pexpr<nodeExprp>: // IEEE: property_expr (The name pexpr is important as regex
// // IEEE: '(' pexpr ')' // // IEEE: '(' pexpr ')'
// // Expanded below // // Expanded below
// //
yNOT pexpr %prec prNEGATION { $$ = new AstLogNot{$1, $2}; } yNOT pexpr
{ $$ = new AstLogNot{$1, $2}; }
| ySTRONG '(' sexpr ')' | ySTRONG '(' sexpr ')'
{ $$ = $3; BBUNSUP($2, "Unsupported: strong (in property expression)"); } { $$ = $3; BBUNSUP($2, "Unsupported: strong (in property expression)"); }
| yWEAK '(' sexpr ')' | yWEAK '(' sexpr ')'
@ -6624,7 +6625,7 @@ sexpr<nodeExprp>: // ==IEEE: sequence_expr (The name sexpr is important as reg
cycle_delay_range ~p~sexpr %prec yP_POUNDPOUND cycle_delay_range ~p~sexpr %prec yP_POUNDPOUND
{ $$ = new AstSExpr{$<fl>1, $1, $2}; } { $$ = new AstSExpr{$<fl>1, $1, $2}; }
| ~p~sexpr cycle_delay_range sexpr %prec prPOUNDPOUND_MULTI | ~p~sexpr cycle_delay_range sexpr %prec prPOUNDPOUND_MULTI
{ $$ = $1; BBUNSUP($2->fileline(), "Unsupported: ## (in sequence expression)"); DEL($2, $3); } { $$ = new AstSExpr{$<fl>2, $1, $2, $3}; }
// //
// // IEEE: expression_or_dist [ boolean_abbrev ] // // IEEE: expression_or_dist [ boolean_abbrev ]
// // Note expression_or_dist includes "expr"! // // Note expression_or_dist includes "expr"!

4
test_regress/t/t_debug_emitv.out
View File

@ -277,6 +277,7 @@ module Vt_debug_emitv_t;
str = $sformatf("cyc=%~", cyc); str = $sformatf("cyc=%~", cyc);
; ;
$display("str = %@", str); $display("str = %@", str);
$display("struct = %@", ps);
$display("%% [%t] [%^] to=%o td=%d", $time, $display("%% [%t] [%^] to=%o td=%d", $time,
$realtime, $time, $time); $realtime, $time, $time);
$sscanf(40'h666f6f3d35, "foo=%d", i); $sscanf(40'h666f6f3d35, "foo=%d", i);
@ -365,9 +366,6 @@ module Vt_debug_emitv_t;
property p1; property p1;
@( clk) sum[0] @( clk) sum[0]
endproperty endproperty
property p2;
@(posedge clk) disable iff (cyc == 'sh1) ##1 sum[0]
endproperty
assert property (@( clk) (! ##1 in) assert property (@( clk) (! ##1 in)
) begin ) begin
end end

4
test_regress/t/t_debug_emitv.v
View File

@ -218,6 +218,7 @@ module t (/*AUTOARG*/
str = $sformatf("cyc=%d", cyc); str = $sformatf("cyc=%d", cyc);
$display("str = %s", str); $display("str = %s", str);
$display("struct = %p", ps);
$display("%% [%t] [%t] to=%o td=%d", $time, $realtime, $time, $time); $display("%% [%t] [%t] to=%o td=%d", $time, $realtime, $time, $time);
$sscanf("foo=5", "foo=%d", i); $sscanf("foo=5", "foo=%d", i);
$printtimescale; $printtimescale;
@ -276,9 +277,6 @@ module t (/*AUTOARG*/
property p1; property p1;
@(clk) sum[0] @(clk) sum[0]
endproperty endproperty
property p2;
@(posedge clk) disable iff (cyc == 1) ##1 sum[0]
endproperty
assert property (@(clk) not ##1 in); assert property (@(clk) not ##1 in);

11
test_regress/t/t_expect.out
View File

@ -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 %Error-UNSUPPORTED: t/t_expect.v:19:7: Unsupported: expect
19 | expect (@(posedge clk) a ##1 b) a = 110; 19 | expect (@(posedge clk) a ##1 b) a = 110;
| ^~~~~~ | ^~~~~~
%Error-UNSUPPORTED: t/t_expect.v:21:32: Unsupported: ## (in sequence expression) ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
21 | expect (@(posedge clk) a ##1 b) else a = 299;
| ^~
%Error-UNSUPPORTED: t/t_expect.v:21:7: Unsupported: expect %Error-UNSUPPORTED: t/t_expect.v:21:7: Unsupported: expect
21 | expect (@(posedge clk) a ##1 b) else a = 299; 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 %Error-UNSUPPORTED: t/t_expect.v:23:7: Unsupported: expect
23 | expect (@(posedge clk) a ##1 b) a = 300; else a = 399; 23 | expect (@(posedge clk) a ##1 b) a = 300; else a = 399;
| ^~~~~~ | ^~~~~~

272
test_regress/t/t_property_sexpr.out
View File

@ -1,140 +1,134 @@
[4] single delay with const stmt, fileline:115 [2] triggered e1
[5] concurrent assert else, fileline:167 [4] triggered e1
[6] single delay with const stmt, fileline:115 [4] single delay with const stmt, fileline:99
[7] concurrent assert stmt, fileline:166 [6] triggered e1
[8] single delay with const stmt, fileline:115 [6] single delay with const stmt, fileline:99
[9] concurrent assert else, fileline:167 [8] triggered e2
[11] concurrent assert else, fileline:167 [10] triggered e2
[12] single delay with var stmt, fileline:118 [10] single delay with var stmt, fileline:102
[13] concurrent assert else, fileline:167 [12] triggered e2
[14] single delay with var else, fileline:119 [12] single delay with var else, fileline:103
[15] concurrent assert stmt, fileline:166 [14] triggered e2
[16] single delay with var stmt, fileline:118 [14] single delay with var stmt, fileline:102
[17] concurrent assert else, fileline:167 [16] triggered e2
[18] single delay with var else, fileline:119 [16] single delay with var else, fileline:103
[19] concurrent assert else, fileline:167 [18] triggered e2
[20] single delay with var stmt, fileline:118 [18] single delay with var stmt, fileline:102
[21] concurrent assert else, fileline:167 [20] triggered e3
[23] concurrent assert stmt, fileline:166 [22] triggered e3
[25] concurrent assert else, fileline:167 [22] stmt1, fileline:106
[26] single multi-cycle delay with var else, fileline:123 [22] stmt2, fileline:107
[27] concurrent assert else, fileline:167 [24] triggered e3
[28] single multi-cycle delay with var stmt, fileline:122 [24] else1, fileline:110
[29] concurrent assert else, fileline:167 [24] else2, fileline:111
[30] single multi-cycle delay with var else, fileline:123 [26] triggered e3
[31] concurrent assert stmt, fileline:166 [26] stmt1, fileline:106
[33] concurrent assert else, fileline:167 [26] stmt2, fileline:107
[34] single delay with var brackets 1 else, fileline:127 [28] triggered e3
[35] concurrent assert else, fileline:167 [28] else1, fileline:110
[36] single delay with var brackets 1 stmt, fileline:126 [28] else2, fileline:111
[37] concurrent assert else, fileline:167 [30] triggered e4
[38] single delay with var brackets 1 else, fileline:127 [32] triggered e4
[39] concurrent assert stmt, fileline:166 [34] triggered e4
[40] single delay with var brackets 1 stmt, fileline:126 [34] single multi-cycle delay with var stmt, fileline:115
[41] concurrent assert else, fileline:167 [36] triggered e4
[43] concurrent assert else, fileline:167 [36] single multi-cycle delay with var else, fileline:116
[44] single delay with var brackets 2 stmt, fileline:130 [38] triggered e4
[45] concurrent assert else, fileline:167 [38] single multi-cycle delay with var stmt, fileline:115
[46] single delay with var brackets 2 else, fileline:131 [40] triggered e5
[47] concurrent assert stmt, fileline:166 [42] triggered e5
[48] single delay with var brackets 2 stmt, fileline:130 [42] single delay with var brackets 1 stmt, fileline:119
[49] concurrent assert else, fileline:167 [44] triggered e5
[50] single delay with var brackets 2 else, fileline:131 [44] single delay with var brackets 1 else, fileline:120
[51] concurrent assert else, fileline:167 [46] triggered e5
[53] concurrent assert else, fileline:167 [46] single delay with var brackets 1 stmt, fileline:119
[54] single delay with negated var else, fileline:135 [48] triggered e5
[55] concurrent assert stmt, fileline:166 [48] single delay with var brackets 1 else, fileline:120
[56] single delay with negated var stmt, fileline:134 [50] triggered e6
[57] concurrent assert else, fileline:167 [52] triggered e6
[58] single delay with negated var else, fileline:135 [52] single delay with var brackets 2 else, fileline:124
[59] concurrent assert else, fileline:167 [54] triggered e6
[60] single delay with negated var else, fileline:135 [54] single delay with var brackets 2 stmt, fileline:123
[61] concurrent assert else, fileline:167 [56] triggered e6
[63] concurrent assert stmt, fileline:166 [56] single delay with var brackets 2 else, fileline:124
[64] single delay with negated var else, fileline:139 [58] triggered e6
[65] concurrent assert else, fileline:167 [58] single delay with var brackets 2 stmt, fileline:123
[66] single delay with negated var stmt, fileline:138 [60] triggered e7
[67] concurrent assert else, fileline:167 [62] triggered e7
[68] single delay with negated var else, fileline:139 [62] single delay with and var stmt, fileline:127
[69] concurrent assert else, fileline:167 [64] triggered e7
[70] single delay with negated var stmt, fileline:138 [64] single delay with and var else, fileline:128
[71] concurrent assert stmt, fileline:166 [66] triggered e7
[73] concurrent assert else, fileline:167 [66] single delay with and var else, fileline:128
[74] single delay with negated var brackets stmt, fileline:142 [68] triggered e7
[75] concurrent assert else, fileline:167 [68] single delay with and var else, fileline:128
[76] single delay with negated var brackets else, fileline:144 [70] triggered e8
[77] concurrent assert else, fileline:167 [72] triggered e8
[78] single delay with negated var brackets stmt, fileline:142 [72] single delay with negated var stmt, fileline:131
[79] concurrent assert stmt, fileline:166 [74] triggered e8
[80] single delay with negated var brackets else, fileline:144 [74] single delay with negated var else, fileline:132
[81] concurrent assert else, fileline:167 [76] triggered e8
[83] concurrent assert else, fileline:167 [76] single delay with negated var stmt, fileline:131
[84] single delay with negated var brackets else, fileline:148 [78] triggered e8
[85] concurrent assert else, fileline:167 [78] single delay with negated var else, fileline:132
[87] concurrent assert stmt, fileline:166 [80] triggered e9
[88] single delay with negated var brackets else, fileline:148 [82] triggered e9
[89] concurrent assert else, fileline:167 [82] single delay with negated var brackets else, fileline:137
[91] concurrent assert else, fileline:167 [84] triggered e9
[93] concurrent assert else, fileline:167 [84] single delay with negated var brackets stmt, fileline:135
[94] single delay with nested not else, fileline:152 [86] triggered e9
[95] concurrent assert stmt, fileline:166 [86] single delay with negated var brackets else, fileline:137
[96] single delay with nested not stmt, fileline:151 [88] triggered e9
[97] concurrent assert else, fileline:167 [88] single delay with negated var brackets stmt, fileline:135
[98] single delay with nested not else, fileline:152 [90] triggered e10
[99] concurrent assert else, fileline:167 [92] triggered e10
[100] single delay with nested not stmt, fileline:151 [94] triggered e10
[101] concurrent assert else, fileline:167 [94] single delay with negated var brackets else, fileline:141
[103] concurrent assert stmt, fileline:166 [96] triggered e10
[105] concurrent assert else, fileline:167 [98] triggered e10
[107] concurrent assert else, fileline:167 [98] single delay with negated var brackets else, fileline:141
[109] concurrent assert else, fileline:167 [100] triggered e11
[111] concurrent assert stmt, fileline:166 [102] triggered e11
[113] concurrent assert else, fileline:167 [102] single delay with nested not stmt, fileline:144
[114] property, fileline:162 [104] triggered e11
[115] concurrent assert else, fileline:167 [104] single delay with nested not else, fileline:145
[116] property, fileline:163 [106] triggered e11
[117] concurrent assert else, fileline:167 [106] single delay with nested not stmt, fileline:144
[118] property, fileline:162 [108] triggered e11
[119] concurrent assert stmt, fileline:166 [108] single delay with nested not else, fileline:145
[120] property, fileline:163 [110] triggered e12
[121] concurrent assert else, fileline:167 [112] triggered e12
[123] concurrent assert else, fileline:167 [114] triggered e12
[125] concurrent assert else, fileline:167 [114] stmt, fileline: 148
[127] concurrent assert stmt, fileline:166 [116] triggered e12
[129] concurrent assert else, fileline:167 [116] else, fileline: 150
[131] concurrent assert else, fileline:167 [118] triggered e12
[133] concurrent assert else, fileline:167 [118] stmt, fileline: 148
[135] concurrent assert stmt, fileline:166 [120] triggered e13
[137] concurrent assert else, fileline:167 [122] triggered e13
[139] concurrent assert else, fileline:167 [122] property, fileline:161
[141] concurrent assert else, fileline:167 [124] triggered e13
[143] concurrent assert stmt, fileline:166 [124] property, fileline:160
[145] concurrent assert else, fileline:167 [126] triggered e13
[147] concurrent assert else, fileline:167 [126] property, fileline:161
[149] concurrent assert else, fileline:167 [128] triggered e13
[151] concurrent assert stmt, fileline:166 [128] property, fileline:160
[153] concurrent assert else, fileline:167 [130] triggered e14
[155] concurrent assert else, fileline:167 [132] triggered e14
[157] concurrent assert else, fileline:167 [132] else, fileline: 166
[159] concurrent assert stmt, fileline:166 [134] triggered e14
[161] concurrent assert else, fileline:167 [134] stmt, fileline: 164
[163] concurrent assert else, fileline:167 [136] triggered e14
[165] concurrent assert else, fileline:167 [136] else, fileline: 166
[167] concurrent assert stmt, fileline:166 [138] triggered e14
[169] concurrent assert else, fileline:167 [138] else, fileline: 166
[171] concurrent assert else, fileline:167 [140] triggered e15
[173] concurrent assert else, fileline:167 [140] else, fileline: 171
[175] concurrent assert stmt, fileline:166 [142] triggered e15
[177] concurrent assert else, fileline:167 [144] triggered e15
[179] concurrent assert else, fileline:167 [144] else, fileline: 171
[181] concurrent assert else, fileline:167 [144] else, fileline: 171
[183] concurrent assert stmt, fileline:166 [146] triggered e15
[185] concurrent assert else, fileline:167 [148] triggered e15
[187] concurrent assert else, fileline:167 [148] else, fileline: 171
[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
*-* All Finished *-* *-* All Finished *-*

196
test_regress/t/t_property_sexpr.v
View File

@ -4,6 +4,9 @@
// without warranty, 2025 by Antmicro. // without warranty, 2025 by Antmicro.
// SPDX-License-Identifier: CC0-1.0 // SPDX-License-Identifier: CC0-1.0
`define STRINGIFY(x) `"x`"
`define TRIGGER(e) ->e; $display("[%0t] triggered %s", $time, `STRINGIFY(e))
module t ( /*AUTOARG*/ module t ( /*AUTOARG*/
// Inputs // Inputs
clk clk
@ -11,7 +14,7 @@ module t ( /*AUTOARG*/
input clk; input clk;
bit [3:0] val = 0; bit [1:0] val = 0;
event e1; event e1;
event e2; event e2;
event e3; event e3;
@ -24,92 +27,73 @@ module t ( /*AUTOARG*/
event e10; event e10;
event e11; event e11;
event e12; event e12;
event e13;
event e14;
event e15;
integer cyc = 1; integer cyc = 1;
always @(negedge clk) begin always @(posedge clk) begin
val <= 4'(cyc % 4); ++val;
++cyc;
if (cyc >= 0 && cyc <= 4) begin
->e1;
`ifdef TEST_VERBOSE `ifdef TEST_VERBOSE
$display("[%0t] triggered e1", $time); $display("[%0t] cyc=%0d val=%0d", $time, cyc, val);
`endif `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 if (cyc == 100) begin
$write("*-* All Finished *-*\n"); $write("*-* All Finished *-*\n");
$finish; $finish;
end end
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) assert property (@(e1) ##1 1)
$display("[%0t] single delay with const stmt, fileline:%0d", $time, `__LINE__); $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__); $display("[%0t] single delay with var stmt, fileline:%0d", $time, `__LINE__);
else $display("[%0t] single delay with var else, 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__); $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__); 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__); $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__); 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__); $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__); 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__); $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__); else $display("[%0t] single delay with negated var else, fileline:%0d", $time, `__LINE__);
assert property (@(e7) not ##1 val[0]) assume property (@(e9) 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]))
$display("[%0t] single delay with negated var brackets stmt, fileline:%0d", $time, `__LINE__); $display("[%0t] single delay with negated var brackets stmt, fileline:%0d", $time, `__LINE__);
else else
$display("[%0t] single delay with negated var brackets else, fileline:%0d", $time, `__LINE__); $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 else
$display("[%0t] single delay with negated var brackets else, fileline:%0d", $time, `__LINE__); $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__); $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__); else $display("[%0t] single delay with nested not else, fileline:%0d", $time, `__LINE__);
restrict property (@(e11) ##1 val[0]); assert property (@(e12) not (not ##2 val[0] && val[0]))
$display("[%0t] stmt, fileline:%d", $time, `__LINE__);
restrict property (@(e11) not ##1 val[0]); 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; property prop;
@(e12) not ##1 val[0] @(e13) not ##1 val[0]
endproperty endproperty
assert property (prop) $display("[%0t] property, fileline:%0d", $time, `__LINE__); assert property (prop) $display("[%0t] property, fileline:%0d", $time, `__LINE__);
else $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])) assert property (@(e14) val[0] ##2 val[1])
$display("[%0t] concurrent assert stmt, fileline:%0d", $time, `__LINE__); $display("[%0t] stmt, fileline:%d", $time, `__LINE__);
else $display("[%0t] concurrent assert else, fileline:%0d", $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 endmodule

4
test_regress/t/t_property_sexpr_bad.out
View File

@ -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' : ... 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. ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
%Error: Exiting due to %Error: Exiting due to

4
test_regress/t/t_property_sexpr_bad.v
View File

@ -12,10 +12,10 @@ module t ( /*AUTOARG*/
input clk; input clk;
bit val; bit val;
always @(negedge clk) begin always @(posedge clk) begin
$write("*-* All Finished *-*\n"); $write("*-* All Finished *-*\n");
$finish; $finish;
end 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 endmodule

5
test_regress/t/t_property_sexpr_cov.dat.out Normal file
View File

@ -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

58
test_regress/t/t_property_sexpr_cov.out
View File

@ -1,31 +1,33 @@
[4] cover property, fileline:45 [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 [8] cover property, fileline:45
[12] not cover property, fileline:48 [8] cover property, fileline:48
[15] concurrent cover, fileline:51 [12] not cover property, fileline:51
[18] not cover property, fileline:48 [15] concurrent cover, fileline:54
[20] not cover property, fileline:48 [18] not cover property, fileline:51
[23] concurrent cover, fileline:51 [20] not cover property, fileline:51
[31] concurrent cover, fileline:51 [23] concurrent cover, fileline:54
[39] concurrent cover, fileline:51 [31] concurrent cover, fileline:54
[47] concurrent cover, fileline:51 [39] concurrent cover, fileline:54
[55] concurrent cover, fileline:51 [47] concurrent cover, fileline:54
[63] concurrent cover, fileline:51 [55] concurrent cover, fileline:54
[71] concurrent cover, fileline:51 [63] concurrent cover, fileline:54
[79] concurrent cover, fileline:51 [71] concurrent cover, fileline:54
[87] concurrent cover, fileline:51 [79] concurrent cover, fileline:54
[95] concurrent cover, fileline:51 [87] concurrent cover, fileline:54
[103] concurrent cover, fileline:51 [95] concurrent cover, fileline:54
[111] concurrent cover, fileline:51 [103] concurrent cover, fileline:54
[119] concurrent cover, fileline:51 [111] concurrent cover, fileline:54
[127] concurrent cover, fileline:51 [119] concurrent cover, fileline:54
[135] concurrent cover, fileline:51 [127] concurrent cover, fileline:54
[143] concurrent cover, fileline:51 [135] concurrent cover, fileline:54
[151] concurrent cover, fileline:51 [143] concurrent cover, fileline:54
[159] concurrent cover, fileline:51 [151] concurrent cover, fileline:54
[167] concurrent cover, fileline:51 [159] concurrent cover, fileline:54
[175] concurrent cover, fileline:51 [167] concurrent cover, fileline:54
[183] concurrent cover, fileline:51 [175] concurrent cover, fileline:54
[191] concurrent cover, fileline:51 [183] concurrent cover, fileline:54
[199] concurrent cover, fileline:51 [191] concurrent cover, fileline:54
[199] concurrent cover, fileline:54
*-* All Finished *-* *-* All Finished *-*

1
test_regress/t/t_property_sexpr_cov.py
View File

@ -14,5 +14,6 @@ test.scenarios('simulator')
test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing', '--coverage-user']) test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing', '--coverage-user'])
test.execute(expect_filename=test.golden_filename) test.execute(expect_filename=test.golden_filename)
test.files_identical(test.obj_dir + "/coverage.dat", "t/t_property_sexpr_cov.dat.out")
test.passes() test.passes()

3
test_regress/t/t_property_sexpr_cov.v
View File

@ -41,6 +41,9 @@ module t ( /*AUTOARG*/
end end
end end
cover property (@(e1) ##1 val[0])
$display("[%0t] cover property, fileline:%0d", $time, `__LINE__);
cover property (@(e1) ##1 val[0]) cover property (@(e1) ##1 val[0])
$display("[%0t] cover property, fileline:%0d", $time, `__LINE__); $display("[%0t] cover property, fileline:%0d", $time, `__LINE__);

18
test_regress/t/t_property_sexpr_multi.py Executable file
View File

@ -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()

249
test_regress/t/t_property_sexpr_multi.v Normal file
View File

@ -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

42
test_regress/t/t_property_sexpr_parse_unsup.out
View File

@ -1,35 +1,23 @@
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:29:39: Unsupported: ## (in sequence expression) %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:75:14: Unsupported: sequence match items
29 | assert property (@(posedge clk) val ##1 val) $display("[%0t] var with single delay stmt, fileline:%d", $time, 29); 75 | ($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: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:71:29: Unsupported: ## range cycle delay range expression ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
71 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; %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 %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:74:13: Unsupported: property variable declaration
70 | integer l_b; 74 | integer l_b;
| ^~~ | ^~~
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:88:16: Unsupported: sequence match items %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:16: Unsupported: sequence match items
88 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; 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 %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:51: Unsupported: [-> boolean abbrev expression
88 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; 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) %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:54: Unsupported: boolean abbrev (in sequence expression)
88 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; 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) %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:90:14: Unsupported: property variable declaration
88 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; 90 | realtime l_t;
| ^~
%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:92:31: Unsupported: ## (in sequence expression)
92 | assert property (@clk not a ##1 b);
| ^~
%Error: Exiting due to %Error: Exiting due to

55
test_regress/t/t_property_sexpr_unsup.out
View File

@ -1,35 +1,50 @@
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:32:41: Unsupported: Implication with sequence expression %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:29: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); : ... 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 ... 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 %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:31: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); : ... 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 %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:33: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); : ... 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 %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:35: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); : ... 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 %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:37: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); : ... 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 %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:41: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); : ... 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 %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:43: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); : ... 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' : ... 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' : ... 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' : ... 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 %Error: Exiting due to

14
test_regress/t/t_property_sexpr_unsup.v
View File

@ -25,10 +25,7 @@ module t ( /*AUTOARG*/
end end
end 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 |-> 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__); 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__); 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__); 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 endmodule
// Test parsing only // Test parsing only

167
test_regress/t/t_sequence_sexpr_unsup.out
View File

@ -66,152 +66,131 @@
68 | ## [+] b; 68 | ## [+] b;
| ^~ | ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:71:4: Unsupported: sequence %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) %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:72:9: Unsupported: ## id cycle delay range expression
72 | a ## 1 b; 72 | a ## DELAY b;
| ^~ | ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:74:4: Unsupported: sequence %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 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:75:9: Unsupported: ## () cycle delay range expression
75 | a ## DELAY b; 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:77:4: Unsupported: sequence %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 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:78:9: Unsupported: ## range cycle delay range expression
78 | a ## ( DELAY ) b; 78 | a ## [1:2] 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:80:4: Unsupported: sequence %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 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:81:9: Unsupported: ## [*] cycle delay range expression
81 | a ## [1:2] b; 81 | a ## [*] 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:83:4: Unsupported: sequence %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 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:84:9: Unsupported: ## [+] cycle delay range expression
84 | a ## [*] b; 84 | a ## [+] b;
| ^~ | ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:84:9: Unsupported: ## (in sequence expression) %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:87:4: Unsupported: sequence
84 | a ## [*] b; 87 | sequence s_booleanabbrev_brastar_int;
| ^~
%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:9: Unsupported: ## [+] cycle delay range expression %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:88:9: Unsupported: [*] boolean abbrev expression
87 | a ## [+] b; 88 | a [* 1 ];
| ^~
%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:12: Unsupported: boolean abbrev (in sequence expression)
88 | a [* 1 ];
| ^
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:90:4: Unsupported: sequence %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 %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 %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 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:94:9: Unsupported: [+] boolean abbrev expression
94 | a [*]; 94 | a [+];
| ^~ | ^~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:94:9: Unsupported: boolean abbrev (in sequence expression) %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 %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 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:97:9: Unsupported: [= boolean abbrev expression
97 | a [+]; 97 | a [= 1];
| ^~~ | ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:97:9: Unsupported: boolean abbrev (in sequence expression) %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:97:12: Unsupported: boolean abbrev (in sequence expression)
97 | a [+]; 97 | a [= 1];
| ^~~ | ^
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:99:4: Unsupported: sequence %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 %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) %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 %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 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:103:9: Unsupported: [-> boolean abbrev expression
103 | a [= 1:2]; 103 | a [-> 1];
| ^~ | ^~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:103:12: Unsupported: boolean abbrev (in sequence expression) %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:103:13: Unsupported: boolean abbrev (in sequence expression)
103 | a [= 1:2]; 103 | a [-> 1];
| ^ | ^
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:105:4: Unsupported: sequence %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 %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) %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 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:109:4: Unsupported: sequence
108 | sequence s_booleanabbrev_minusgt_range; 109 | sequence p_arg_seqence(sequence inseq);
| ^~~~~~~~ | ^~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:109:9: Unsupported: [-> boolean abbrev expression %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:109:27: Unsupported: sequence argument data type
109 | a [-> 1:2]; 109 | sequence p_arg_seqence(sequence inseq);
| ^~~
%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: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 %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) %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 %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) %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 %Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:123:10: Ignoring unsupported: cover sequence
122 | sequence s_firstmatch_abc; 123 | cover sequence (s_a) $display("");
| ^~~~~~~~
%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("");
| ^~~~~~~~ | ^~~~~~~~
... For warning description see https://verilator.org/warn/COVERIGN?v=latest ... 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. ... 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 %Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:124:10: Ignoring unsupported: cover sequence
127 | cover sequence (@(posedge a) disable iff (b) s_a) $display(""); 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 %Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:125:10: Ignoring unsupported: cover sequence
128 | cover sequence (disable iff (b) s_a) $display(""); 125 | cover sequence (disable iff (b) s_a) $display("");
| ^~~~~~~~ | ^~~~~~~~
%Error: Exiting due to %Error: Exiting due to

3
test_regress/t/t_sequence_sexpr_unsup.v
View File

@ -68,9 +68,6 @@ module t (/*AUTOARG*/
## [+] b; ## [+] b;
endsequence endsequence
sequence s_cycdelay_int;
a ## 1 b;
endsequence
sequence s_cycdelay_id; sequence s_cycdelay_id;
a ## DELAY b; a ## DELAY b;
endsequence endsequence