Compare commits
4 Commits
100c831474
...
9d74984163
| Author | SHA1 | Date |
|---|---|---|
|
|
9d74984163 | |
|
|
5adecb9fa3 | |
|
|
f7e12e9219 | |
|
|
47b52800bf |
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -232,6 +232,7 @@ RAW_OBJS_PCH_ASTNOMT = \
|
|||
V3ActiveTop.o \
|
||||
V3Assert.o \
|
||||
V3AssertPre.o \
|
||||
V3AssertProp.o \
|
||||
V3Begin.o \
|
||||
V3Branch.o \
|
||||
V3CCtors.o \
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<AstVarXRef*> 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);
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
|
@ -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
|
||||
|
|
@ -902,6 +902,8 @@ public:
|
|||
// isUnlikely handles $stop or similar statement which means an above IF
|
||||
// statement is unlikely to be taken
|
||||
virtual bool isUnlikely() const { return false; }
|
||||
// Is an IEEE system function (versus internally-generated)
|
||||
virtual bool isSystemFunc() const { return false; }
|
||||
virtual int instrCount() const { return 0; }
|
||||
// Iff node is identical to another node
|
||||
virtual bool isSame(const AstNode* samep) const {
|
||||
|
|
|
|||
|
|
@ -134,6 +134,7 @@ public:
|
|||
bool cleanRhs() const override { return false; }
|
||||
bool sizeMattersLhs() const override { return false; }
|
||||
bool sizeMattersRhs() const override { return false; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
int instrCount() const override { return INSTR_COUNT_DBL_TRIG; }
|
||||
void numberOperate(V3Number&, const V3Number&, const V3Number&) override { V3ERROR_NA; }
|
||||
};
|
||||
|
|
@ -172,6 +173,7 @@ public:
|
|||
bool cleanRhs() const override { return false; }
|
||||
bool sizeMattersLhs() const override { return false; }
|
||||
bool sizeMattersRhs() const override { return false; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
int instrCount() const override { return INSTR_COUNT_DBL_TRIG; }
|
||||
bool doubleFlavor() const override { return true; }
|
||||
};
|
||||
|
|
@ -347,6 +349,7 @@ protected:
|
|||
|
||||
public:
|
||||
ASTGEN_MEMBERS_AstNodeTermop;
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstNodeTriop VL_NOT_FINAL : public AstNodeExpr {
|
||||
// Ternary expression
|
||||
|
|
@ -403,6 +406,7 @@ public:
|
|||
bool sizeMattersLhs() const override { return false; }
|
||||
bool sizeMattersRhs() const override { return false; }
|
||||
bool sizeMattersThs() const override { return false; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
int instrCount() const override { return INSTR_COUNT_DBL_TRIG; }
|
||||
void numberOperate(V3Number& out, const V3Number& lhs, const V3Number& rhs,
|
||||
const V3Number& ths) override {
|
||||
|
|
@ -449,6 +453,7 @@ public:
|
|||
bool cleanOut() const override { return true; }
|
||||
bool cleanLhs() const override { return false; }
|
||||
bool sizeMattersLhs() const override { return false; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
int instrCount() const override { return INSTR_COUNT_DBL_TRIG; }
|
||||
bool doubleFlavor() const override { return true; }
|
||||
};
|
||||
|
|
@ -1350,6 +1355,7 @@ public:
|
|||
int instrCount() const override { return widthInstrs() * 64; }
|
||||
bool isPredictOptimizable() const override { return false; }
|
||||
bool isPure() override { return false; } // SPECIAL: $display has 'visual' ordering
|
||||
bool isSystemFunc() const override { return true; }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
};
|
||||
class AstFOpen final : public AstNodeExpr {
|
||||
|
|
@ -1372,6 +1378,7 @@ public:
|
|||
bool isOutputter() override { return true; }
|
||||
bool isUnlikely() const override { return true; }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstFOpenMcd final : public AstNodeExpr {
|
||||
// @astgen op2 := filenamep : AstNodeExpr
|
||||
|
|
@ -1415,6 +1422,7 @@ public:
|
|||
bool isOutputter() override { return true; } // SPECIAL: makes output
|
||||
bool cleanOut() const override { return false; }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstFRewind final : public AstNodeExpr {
|
||||
// @astgen op1 := filep : Optional[AstNode]
|
||||
|
|
@ -1462,6 +1470,7 @@ public:
|
|||
}
|
||||
string text() const { return m_text; } // * = Text to display
|
||||
void text(const string& text) { m_text = text; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstFSeek final : public AstNodeExpr {
|
||||
// @astgen op1 := filep : AstNode // file (must be a VarRef)
|
||||
|
|
@ -1484,6 +1493,7 @@ public:
|
|||
bool isOutputter() override { return true; } // SPECIAL: makes output
|
||||
bool cleanOut() const override { return false; }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstFTell final : public AstNodeExpr {
|
||||
// @astgen op1 := filep : AstNode // file (must be a VarRef)
|
||||
|
|
@ -1503,6 +1513,7 @@ public:
|
|||
bool isUnlikely() const override { return true; }
|
||||
bool cleanOut() const override { return false; }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstFalling final : public AstNodeExpr {
|
||||
// Verilog $falling_gclk
|
||||
|
|
@ -1519,6 +1530,7 @@ public:
|
|||
bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
|
||||
int instrCount() const override { return widthInstrs(); }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstFell final : public AstNodeExpr {
|
||||
// Verilog $fell
|
||||
|
|
@ -1537,6 +1549,7 @@ public:
|
|||
bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
|
||||
int instrCount() const override { return widthInstrs(); }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstFuture final : public AstNodeExpr {
|
||||
// Verilog $future_gclk
|
||||
|
|
@ -1555,6 +1568,7 @@ public:
|
|||
bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
|
||||
int instrCount() const override { return widthInstrs(); }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstGatePin final : public AstNodeExpr {
|
||||
// Possibly expand a gate primitive input pin value to match the range of the gate primitive
|
||||
|
|
@ -1764,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(""); }
|
||||
|
|
@ -1835,6 +1851,7 @@ public:
|
|||
bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
|
||||
int instrCount() const override { return widthInstrs(); }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstPatMember final : public AstNodeExpr {
|
||||
// Verilog '{a} or '{a{b}}
|
||||
|
|
@ -1923,6 +1940,7 @@ public:
|
|||
bool isGateOptimizable() const override { return false; }
|
||||
bool isPredictOptimizable() const override { return false; }
|
||||
bool isPure() override { return !seedp(); }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
int instrCount() const override { return INSTR_COUNT_PLI; }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
bool combinable(const AstRand* samep) const {
|
||||
|
|
@ -1947,6 +1965,7 @@ public:
|
|||
bool cleanOut() const override { return false; }
|
||||
bool isGateOptimizable() const override { return false; }
|
||||
bool isPredictOptimizable() const override { return false; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
int instrCount() const override { return INSTR_COUNT_PLI; }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
};
|
||||
|
|
@ -1965,6 +1984,7 @@ public:
|
|||
bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
|
||||
int instrCount() const override { return widthInstrs(); }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstRose final : public AstNodeExpr {
|
||||
// Verilog $rose
|
||||
|
|
@ -1983,14 +2003,23 @@ public:
|
|||
bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
|
||||
int instrCount() const override { return widthInstrs(); }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstSExpr final : public AstNodeExpr {
|
||||
// Sequence expression
|
||||
// @astgen op1 := delayp : AstDelay
|
||||
// @astgen op2 := exprp : AstNodeExpr
|
||||
// @astgen op1 := preExprp: Optional[AstNodeExpr]
|
||||
// @astgen op2 := delayp : AstNodeStmt<AstDelay|AstBegin>
|
||||
// @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);
|
||||
}
|
||||
|
|
@ -2055,6 +2084,7 @@ public:
|
|||
string emitVerilog() override { V3ERROR_NA_RETURN(""); }
|
||||
string emitC() override { V3ERROR_NA_RETURN(""); }
|
||||
bool cleanOut() const override { V3ERROR_NA_RETURN(true); }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstSScanF final : public AstNodeExpr {
|
||||
// @astgen op1 := exprsp : List[AstNode] // VarRefs for results
|
||||
|
|
@ -2086,6 +2116,7 @@ public:
|
|||
string text() const { return m_text; } // * = Text to display
|
||||
VTimescale timeunit() const { return m_timeunit; }
|
||||
void timeunit(const VTimescale& flag) { m_timeunit = flag; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstSampled final : public AstNodeExpr {
|
||||
// Verilog $sampled
|
||||
|
|
@ -2102,6 +2133,7 @@ public:
|
|||
bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
|
||||
int instrCount() const override { return 0; }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstScopeName final : public AstNodeExpr {
|
||||
// For display %m and DPI context imports
|
||||
|
|
@ -2228,6 +2260,7 @@ public:
|
|||
bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
|
||||
int instrCount() const override { return widthInstrs(); }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstStackTraceF final : public AstNodeExpr {
|
||||
// $stacktrace used as function
|
||||
|
|
@ -2263,6 +2296,7 @@ public:
|
|||
bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
|
||||
int instrCount() const override { return widthInstrs(); }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstStructSel final : public AstNodeExpr {
|
||||
// Unpacked struct/union member access
|
||||
|
|
@ -2330,6 +2364,7 @@ public:
|
|||
bool isUnlikely() const override { return true; }
|
||||
bool cleanOut() const override { return true; }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstTestPlusArgs final : public AstNodeExpr {
|
||||
// Search expression. If nullptr then this is a $test$plusargs instead of $value$plusargs.
|
||||
|
|
@ -2346,6 +2381,7 @@ public:
|
|||
bool isGateOptimizable() const override { return false; }
|
||||
bool isPredictOptimizable() const override { return false; }
|
||||
// but isPure() true
|
||||
bool isSystemFunc() const override { return true; }
|
||||
bool cleanOut() const override { return true; }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
};
|
||||
|
|
@ -2380,6 +2416,7 @@ public:
|
|||
string emitC() override { V3ERROR_NA_RETURN(""); }
|
||||
string emitSimpleOperator() override { V3ERROR_NA_RETURN(""); }
|
||||
bool cleanOut() const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
int instrCount() const override { return widthInstrs(); }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
};
|
||||
|
|
@ -2396,6 +2433,7 @@ public:
|
|||
string emitC() override { V3ERROR_NA_RETURN(""); }
|
||||
string emitSimpleOperator() override { V3ERROR_NA_RETURN(""); }
|
||||
bool cleanOut() const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
int instrCount() const override { return widthInstrs(); }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
VTimescale timeunit() const { return m_timeunit; }
|
||||
|
|
@ -2450,6 +2488,7 @@ public:
|
|||
bool isGateOptimizable() const override { return false; }
|
||||
bool isPredictOptimizable() const override { return false; }
|
||||
bool isPure() override { return !outp(); }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
bool cleanOut() const override { return true; }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
};
|
||||
|
|
@ -2553,6 +2592,7 @@ public:
|
|||
bool cleanRhs() const override { return true; }
|
||||
bool sizeMattersLhs() const override { return false; }
|
||||
bool sizeMattersRhs() const override { return false; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
int instrCount() const override { return widthInstrs() * 20; }
|
||||
bool isPure() override { return false; }
|
||||
};
|
||||
|
|
@ -2731,6 +2771,7 @@ public:
|
|||
bool cleanRhs() const override { return true; }
|
||||
bool sizeMattersLhs() const override { return false; }
|
||||
bool sizeMattersRhs() const override { return false; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
int instrCount() const override { return widthInstrs() * 64; }
|
||||
AstNode* strgp() const { return lhsp(); }
|
||||
AstNode* filep() const { return rhsp(); }
|
||||
|
|
@ -2751,6 +2792,7 @@ public:
|
|||
bool cleanRhs() const override { return true; }
|
||||
bool sizeMattersLhs() const override { return false; }
|
||||
bool sizeMattersRhs() const override { return false; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
int instrCount() const override { return widthInstrs() * 64; }
|
||||
bool isPredictOptimizable() const override { return false; }
|
||||
bool isPure() override { return false; } // SPECIAL: $display has 'visual' ordering
|
||||
|
|
@ -3667,6 +3709,7 @@ public:
|
|||
bool isGateOptimizable() const override { return false; }
|
||||
bool isPredictOptimizable() const override { return false; }
|
||||
bool isPure() override { return false; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
int instrCount() const override { return INSTR_COUNT_PLI; }
|
||||
};
|
||||
|
||||
|
|
@ -4452,6 +4495,7 @@ public:
|
|||
bool sizeMattersRhs() const override { return false; }
|
||||
bool sizeMattersThs() const override { return false; }
|
||||
bool sizeMattersFhs() const override { return false; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
int instrCount() const override { return widthInstrs() * 16; }
|
||||
};
|
||||
|
||||
|
|
@ -4466,6 +4510,7 @@ public:
|
|||
string emitVerilog() override { return "%f$inferred_disable"; }
|
||||
string emitC() override { V3ERROR_NA_RETURN(""); }
|
||||
bool cleanOut() const override { return true; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
};
|
||||
class AstTime final : public AstNodeTermop {
|
||||
|
|
@ -4482,6 +4527,7 @@ public:
|
|||
bool cleanOut() const override { return true; }
|
||||
bool isGateOptimizable() const override { return false; }
|
||||
bool isPredictOptimizable() const override { return false; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
int instrCount() const override { return INSTR_COUNT_TIME; }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
void dump(std::ostream& str = std::cout) const override;
|
||||
|
|
@ -4503,6 +4549,7 @@ public:
|
|||
bool cleanOut() const override { return true; }
|
||||
bool isGateOptimizable() const override { return false; }
|
||||
bool isPredictOptimizable() const override { return false; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
int instrCount() const override { return INSTR_COUNT_TIME; }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
void dump(std::ostream& str = std::cout) const override;
|
||||
|
|
@ -4795,6 +4842,7 @@ public:
|
|||
bool cleanLhs() const override { return false; } // Eliminated before matters
|
||||
bool sizeMattersLhs() const override { return false; } // Eliminated before matters
|
||||
int instrCount() const override { return INSTR_COUNT_DBL; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstCAwait final : public AstNodeUniop {
|
||||
// Emit C++'s co_await expression
|
||||
|
|
@ -4867,6 +4915,7 @@ public:
|
|||
bool cleanLhs() const override { return true; }
|
||||
bool sizeMattersLhs() const override { return false; }
|
||||
int instrCount() const override { return widthInstrs() * 16; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstCastWrap final : public AstNodeUniop {
|
||||
// A cast which has been expanded and the LHSP does all the lifting
|
||||
|
|
@ -4896,6 +4945,7 @@ public:
|
|||
bool cleanLhs() const override { return true; }
|
||||
bool sizeMattersLhs() const override { return false; }
|
||||
int instrCount() const override { return widthInstrs() * 16; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstCvtPackString final : public AstNodeUniop {
|
||||
// Convert to Verilator Packed String (aka verilog "string")
|
||||
|
|
@ -4977,6 +5027,7 @@ public:
|
|||
int instrCount() const override { return widthInstrs() * 16; }
|
||||
bool isPredictOptimizable() const override { return false; }
|
||||
bool isPure() override { return false; } // SPECIAL: $display has 'visual' ordering
|
||||
bool isSystemFunc() const override { return true; }
|
||||
AstNode* filep() const { return lhsp(); }
|
||||
};
|
||||
class AstFGetC final : public AstNodeUniop {
|
||||
|
|
@ -4995,6 +5046,7 @@ public:
|
|||
bool isPredictOptimizable() const override { return false; }
|
||||
bool isPure() override { return false; } // SPECIAL: $display has 'visual' ordering
|
||||
AstNode* filep() const { return lhsp(); }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstISToRD final : public AstNodeUniop {
|
||||
// $itor where lhs is signed
|
||||
|
|
@ -5012,6 +5064,7 @@ public:
|
|||
bool cleanLhs() const override { return true; }
|
||||
bool sizeMattersLhs() const override { return false; }
|
||||
int instrCount() const override { return INSTR_COUNT_DBL; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstIToRD final : public AstNodeUniop {
|
||||
// $itor where lhs is unsigned
|
||||
|
|
@ -5028,6 +5081,7 @@ public:
|
|||
bool cleanLhs() const override { return true; }
|
||||
bool sizeMattersLhs() const override { return false; }
|
||||
int instrCount() const override { return INSTR_COUNT_DBL; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstIsUnbounded final : public AstNodeUniop {
|
||||
// True if is unbounded ($)
|
||||
|
|
@ -5046,6 +5100,7 @@ public:
|
|||
bool cleanOut() const override { return false; }
|
||||
bool cleanLhs() const override { return false; }
|
||||
bool sizeMattersLhs() const override { return false; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstIsUnknown final : public AstNodeUniop {
|
||||
// True if any unknown bits
|
||||
|
|
@ -5061,6 +5116,7 @@ public:
|
|||
bool cleanOut() const override { return false; }
|
||||
bool cleanLhs() const override { return false; }
|
||||
bool sizeMattersLhs() const override { return false; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstLenN final : public AstNodeUniop {
|
||||
// Length of a string
|
||||
|
|
@ -5191,6 +5247,7 @@ public:
|
|||
bool cleanLhs() const override { return true; }
|
||||
bool sizeMattersLhs() const override { return false; }
|
||||
int instrCount() const override { return widthInstrs() * 4; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstOneHot0 final : public AstNodeUniop {
|
||||
// True if only single bit, or no bits set in vector
|
||||
|
|
@ -5207,6 +5264,7 @@ public:
|
|||
bool cleanLhs() const override { return true; }
|
||||
bool sizeMattersLhs() const override { return false; }
|
||||
int instrCount() const override { return widthInstrs() * 3; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstRToIRoundS final : public AstNodeUniop {
|
||||
// Convert real to integer, with arbitrary sized output (not just "integer" format)
|
||||
|
|
@ -5225,6 +5283,7 @@ public:
|
|||
bool cleanLhs() const override { return false; }
|
||||
bool sizeMattersLhs() const override { return false; }
|
||||
int instrCount() const override { return INSTR_COUNT_DBL; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstRToIS final : public AstNodeUniop {
|
||||
// $rtoi(lhs)
|
||||
|
|
@ -5241,6 +5300,7 @@ public:
|
|||
bool cleanLhs() const override { return false; } // Eliminated before matters
|
||||
bool sizeMattersLhs() const override { return false; } // Eliminated before matters
|
||||
int instrCount() const override { return INSTR_COUNT_DBL; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstRealToBits final : public AstNodeUniop {
|
||||
public:
|
||||
|
|
@ -5256,6 +5316,7 @@ public:
|
|||
bool cleanLhs() const override { return false; } // Eliminated before matters
|
||||
bool sizeMattersLhs() const override { return false; } // Eliminated before matters
|
||||
int instrCount() const override { return INSTR_COUNT_DBL; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstRedAnd final : public AstNodeUniop {
|
||||
public:
|
||||
|
|
@ -5337,6 +5398,7 @@ public:
|
|||
bool cleanLhs() const override { return false; } // Eliminated before matters
|
||||
bool sizeMattersLhs() const override { return true; } // Eliminated before matters
|
||||
int instrCount() const override { return 0; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
class AstTimeImport final : public AstNodeUniop {
|
||||
// Take a constant that represents a time and needs conversion based on time units
|
||||
|
|
@ -5419,6 +5481,7 @@ public:
|
|||
bool cleanLhs() const override { return false; } // Eliminated before matters
|
||||
bool sizeMattersLhs() const override { return true; } // Eliminated before matters
|
||||
int instrCount() const override { return 0; }
|
||||
bool isSystemFunc() const override { return true; }
|
||||
};
|
||||
|
||||
// === AstNodeSystemUniopD ===
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -24,6 +24,7 @@
|
|||
#include "V3Clock.h"
|
||||
|
||||
#include "V3Const.h"
|
||||
#include "V3Sched.h"
|
||||
|
||||
VL_DEFINE_DEBUG_FUNCTIONS;
|
||||
|
||||
|
|
@ -62,7 +63,7 @@ class ClockVisitor final : public VNVisitor {
|
|||
// NODE STATE
|
||||
|
||||
// STATE
|
||||
AstCFunc* const m_evalp = nullptr; // The '_eval' function
|
||||
AstCFunc* m_sampleCFuncp = nullptr; // The CFunc to populate with sampled value assignments
|
||||
|
||||
// VISITORS
|
||||
void visit(AstCoverToggle* nodep) override {
|
||||
|
|
@ -98,19 +99,20 @@ class ClockVisitor final : public VNVisitor {
|
|||
//========== Move sampled assignments
|
||||
void visit(AstVarScope* nodep) override {
|
||||
AstVar* const varp = nodep->varp();
|
||||
if (varp->valuep() && varp->name().substr(0, strlen("__Vsampled")) == "__Vsampled") {
|
||||
FileLine* const flp = nodep->fileline();
|
||||
AstNodeExpr* const rhsp = VN_AS(varp->valuep()->unlinkFrBack(), NodeExpr);
|
||||
AstVarRef* const lhsp = new AstVarRef{flp, nodep, VAccess::WRITE};
|
||||
AstAssign* const assignp = new AstAssign{flp, lhsp, rhsp};
|
||||
if (AstNode* const stmtsp = m_evalp->stmtsp()) {
|
||||
stmtsp->addHereThisAsNext(assignp);
|
||||
} else {
|
||||
m_evalp->addStmtsp(assignp);
|
||||
}
|
||||
varp->direction(VDirection::NONE); // Restore defaults
|
||||
varp->primaryIO(false);
|
||||
if (!varp->valuep()) return;
|
||||
if (!VString::startsWith(varp->name(), "__Vsampled")) return;
|
||||
|
||||
// Create the containing function on first encounter
|
||||
if (!m_sampleCFuncp) {
|
||||
m_sampleCFuncp = V3Sched::util::makeSubFunction(v3Global.rootp(), "_sample", false);
|
||||
}
|
||||
|
||||
FileLine* const flp = nodep->fileline();
|
||||
AstNodeExpr* const rhsp = VN_AS(varp->valuep()->unlinkFrBack(), NodeExpr);
|
||||
AstVarRef* const lhsp = new AstVarRef{flp, nodep, VAccess::WRITE};
|
||||
m_sampleCFuncp->addStmtsp(new AstAssign{flp, lhsp, rhsp});
|
||||
varp->direction(VDirection::NONE); // Restore defaults
|
||||
varp->primaryIO(false);
|
||||
}
|
||||
|
||||
//--------------------
|
||||
|
|
@ -118,9 +120,15 @@ class ClockVisitor final : public VNVisitor {
|
|||
|
||||
public:
|
||||
// CONSTRUCTORS
|
||||
explicit ClockVisitor(AstNetlist* netlistp)
|
||||
: m_evalp{netlistp->evalp()} {
|
||||
explicit ClockVisitor(AstNetlist* netlistp) {
|
||||
iterate(netlistp);
|
||||
// If we need a sample function, call it at the begining of eval
|
||||
if (m_sampleCFuncp) {
|
||||
V3Sched::util::splitCheck(m_sampleCFuncp);
|
||||
AstCCall* const callp = new AstCCall{m_sampleCFuncp->fileline(), m_sampleCFuncp};
|
||||
callp->dtypeSetVoid();
|
||||
netlistp->evalp()->stmtsp()->addHereThisAsNext(callp->makeStmt());
|
||||
}
|
||||
}
|
||||
~ClockVisitor() override = default;
|
||||
};
|
||||
|
|
|
|||
|
|
@ -141,7 +141,7 @@ class CoverageVisitor final : public VNVisitor {
|
|||
const VNUser2InUse m_inuser2;
|
||||
V3UniqueNames m_exprTempNames; // For generating unique temporary variable names used by
|
||||
// expression coverage
|
||||
std::unordered_map<VNRef<AstFuncRef>, AstVar*> m_funcTemps;
|
||||
std::unordered_map<AstNodeExpr*, AstVar*> m_funcTemps;
|
||||
|
||||
// STATE - across all visitors
|
||||
int m_nextHandle = 0;
|
||||
|
|
@ -277,6 +277,7 @@ class CoverageVisitor final : public VNVisitor {
|
|||
VL_RESTORER(m_modp);
|
||||
VL_RESTORER(m_state);
|
||||
VL_RESTORER(m_exprTempNames);
|
||||
VL_RESTORER(m_funcTemps);
|
||||
createHandle(nodep);
|
||||
m_modp = nodep;
|
||||
m_state.m_inModOff
|
||||
|
|
@ -333,6 +334,7 @@ class CoverageVisitor final : public VNVisitor {
|
|||
void visit(AstNodeFTask* nodep) override {
|
||||
VL_RESTORER(m_ftaskp);
|
||||
VL_RESTORER(m_exprTempNames);
|
||||
VL_RESTORER(m_funcTemps);
|
||||
m_ftaskp = nodep;
|
||||
if (!nodep->dpiImport()) iterateProcedure(nodep);
|
||||
}
|
||||
|
|
@ -784,9 +786,10 @@ class CoverageVisitor final : public VNVisitor {
|
|||
comment += (first ? "" : " && ") + term.m_emitV
|
||||
+ "==" + (term.m_objective ? "1" : "0");
|
||||
AstNodeExpr* covExprp = nullptr;
|
||||
if (AstFuncRef* const frefp = VN_CAST(term.m_exprp, FuncRef)) {
|
||||
AstNodeDType* const dtypep = frefp->taskp()->fvarp()->dtypep();
|
||||
const auto pair = m_funcTemps.emplace(*frefp, nullptr);
|
||||
if (VN_IS(term.m_exprp, FuncRef) || term.m_exprp->isSystemFunc()) {
|
||||
AstNodeExpr* const frefp = term.m_exprp;
|
||||
AstNodeDType* const dtypep = frefp->dtypep();
|
||||
const auto pair = m_funcTemps.emplace(frefp, nullptr);
|
||||
AstVar* varp = pair.first->second;
|
||||
if (pair.second) {
|
||||
varp = new AstVar{fl, VVarType::MODULETEMP, m_exprTempNames.get(frefp),
|
||||
|
|
|
|||
|
|
@ -105,7 +105,7 @@ class EmitCSyms final : EmitCBaseVisitorConst {
|
|||
size_t m_funcNum = 0; // CFunc split function number
|
||||
V3OutCFile* m_ofpBase = nullptr; // Base (not split) C file
|
||||
AstCFile* m_ofpBaseFile = nullptr; // Base (not split) AstCFile
|
||||
std::unordered_map<int, bool> m_usesVfinal; // Split method uses __Vfinal
|
||||
std::vector<std::pair<size_t, bool>> m_usesVfinal; // Split file index + uses __Vfinal
|
||||
VDouble0 m_statVarScopeBytes; // Statistic tracking
|
||||
const std::string m_symsFileBase = v3Global.opt.makeDir() + "/" + symClassName();
|
||||
|
||||
|
|
@ -620,7 +620,7 @@ void EmitCSyms::checkSplit(bool usesVfinal) {
|
|||
puts(");\n");
|
||||
|
||||
// Create new split file
|
||||
m_usesVfinal[funcNum] = usesVfinal;
|
||||
m_usesVfinal.emplace_back(funcNum, usesVfinal);
|
||||
const std::string filename = m_symsFileBase + "__" + std::to_string(funcNum) + ".cpp";
|
||||
AstCFile* const cfilep = newCFile(filename, true /*slow*/, true /*source*/);
|
||||
cfilep->support(true);
|
||||
|
|
|
|||
|
|
@ -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());
|
||||
}
|
||||
|
|
@ -699,6 +700,10 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
|
|||
emitVerilogFormat(nodep, nodep->emitVerilog(), nodep->lhsp(), nodep->rhsp(),
|
||||
nodep->thsp());
|
||||
}
|
||||
void visit(AstNodeQuadop* nodep) override {
|
||||
emitVerilogFormat(nodep, nodep->emitVerilog(), nodep->lhsp(), nodep->rhsp(), nodep->thsp(),
|
||||
nodep->fhsp());
|
||||
}
|
||||
void visit(AstMemberSel* nodep) override {
|
||||
iterateConst(nodep->fromp());
|
||||
puts(".");
|
||||
|
|
@ -799,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 ");
|
||||
|
|
@ -812,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");
|
||||
|
|
@ -1052,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
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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());
|
||||
|
|
|
|||
|
|
@ -6534,7 +6534,8 @@ pexpr<nodeExprp>: // 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<nodeExprp>: // ==IEEE: sequence_expr (The name sexpr is important as reg
|
|||
cycle_delay_range ~p~sexpr %prec yP_POUNDPOUND
|
||||
{ $$ = new AstSExpr{$<fl>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{$<fl>2, $1, $2, $3}; }
|
||||
//
|
||||
// // IEEE: expression_or_dist [ boolean_abbrev ]
|
||||
// // Note expression_or_dist includes "expr"!
|
||||
|
|
|
|||
|
|
@ -0,0 +1,339 @@
|
|||
// // verilator_coverage annotation
|
||||
// DESCRIPTION: Verilator: Verilog Test module
|
||||
//
|
||||
// This file ONLY is placed under the Creative Commons Public Domain, for
|
||||
// any use, without warranty, 2024 by Wilson Snyder.
|
||||
// SPDX-License-Identifier: CC0-1.0
|
||||
|
||||
module t (/*AUTOARG*/
|
||||
// Inputs
|
||||
clk
|
||||
);
|
||||
|
||||
input clk;
|
||||
|
||||
int cyc, bump, result;
|
||||
logic foo;
|
||||
%000001 initial begin
|
||||
-000001 point: comment=block hier=top.t
|
||||
%000001 cyc = 0;
|
||||
-000001 point: comment=block hier=top.t
|
||||
%000001 foo = '1;
|
||||
-000001 point: comment=block hier=top.t
|
||||
end
|
||||
|
||||
|
||||
000010 always @(posedge clk) begin
|
||||
+000010 point: comment=block hier=top.t
|
||||
~000010 if (($time != 0) && foo) bump <= bump + 1;
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($realtime != 0) && foo) bump <= bump + 1;
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($stime != 0) && foo) bump <= bump + 1;
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($bitstoreal(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($bitstoreal(64'h7b) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($bitstoreal(64'h7b) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($itor(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($itor($signed(32'sh7b)) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($itor($signed(32'sh7b)) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($signed(3) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=((32'sh3 != 32'sh0)==0) => 0 hier=top.t
|
||||
+000010 point: comment=((32'sh3 != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($realtobits(1.23) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($realtobits(1.23) != 64'h0)==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($realtobits(1.23) != 64'h0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($rtoi(1.23) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($rtoi(1.23) != 32'sh0)==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($rtoi(1.23) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($unsigned(-3) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(((- 32'sh3) != 32'sh0)==0) => 0 hier=top.t
|
||||
+000010 point: comment=(((- 32'sh3) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($clog2(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($clog2(32'sh7b) != 32'sh0)==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($clog2(32'sh7b) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($ln(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($ln($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($ln($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($log10(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($log10($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($log10($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($exp(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($exp($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($exp($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($sqrt(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($sqrt($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($sqrt($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($pow(123, 2) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=((($itor($signed(32'sh7b)) ** $itor($signed(32'sh2))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=((($itor($signed(32'sh7b)) ** $itor($signed(32'sh2))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($floor(1.23) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($floor(1.23) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($floor(1.23) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($ceil(1.23) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($ceil(1.23) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($ceil(1.23) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($sin(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($sin($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($sin($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($cos(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($cos($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($cos($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($tan(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($tan($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($tan($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($asin(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($asin($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($asin($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($acos(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($acos($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($acos($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($atan(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($atan($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($atan($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($atan2(123, 2) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($atan2($itor($signed(32'sh7b)),$itor($signed(32'sh2))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($atan2($itor($signed(32'sh7b)),$itor($signed(32'sh2))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($hypot(123, 2) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($hypot($itor($signed(32'sh7b)),$itor($signed(32'sh2))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($hypot($itor($signed(32'sh7b)),$itor($signed(32'sh2))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($sinh(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($sinh($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($sinh($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($cosh(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($cosh($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($cosh($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($tanh(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($tanh($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($tanh($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($asinh(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($asinh($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($asinh($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($acosh(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($acosh($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($acosh($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($atanh(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($atanh($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($atanh($itor($signed(32'sh7b))) != $itor($signed(32'sh0)))==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($countbits(123, 2) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($countbits(32'sh7b, 32'sh2, , 32'sh2) != 32'sh0)==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($countbits(32'sh7b, 32'sh2, , 32'sh2) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($onehot(123) != 0) && foo) bump <= bump + 1;
|
||||
+000010 point: comment=(($onehot(32'sh7b) != 32'sh0)==0) => 0 hier=top.t
|
||||
-000000 point: comment=(($onehot(32'sh7b) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
-000000 point: comment=if hier=top.t
|
||||
+000010 point: comment=else hier=top.t
|
||||
~000010 if ($isunknown(foo) && foo) bump <= bump + 1;
|
||||
+000010 point: comment=($isunknown(foo)==0) => 0 hier=top.t
|
||||
-000000 point: comment=($isunknown(foo)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
-000000 point: comment=if hier=top.t
|
||||
+000010 point: comment=else hier=top.t
|
||||
~000010 if (($countones(123) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($countones(32'sh7b) != 32'sh0)==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($countones(32'sh7b) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($onehot0(123) != 0) && foo) bump <= bump + 1;
|
||||
+000010 point: comment=(($onehot0(32'sh7b) != 32'sh0)==0) => 0 hier=top.t
|
||||
-000000 point: comment=(($onehot0(32'sh7b) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
-000000 point: comment=if hier=top.t
|
||||
+000010 point: comment=else hier=top.t
|
||||
~000010 if (($sampled(foo) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($sampled(foo) != 32'sh0)==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($sampled(foo) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($fell(foo) != 0) && foo) bump <= bump + 1;
|
||||
+000010 point: comment=(($fell(foo) != 32'sh0)==0) => 0 hier=top.t
|
||||
-000000 point: comment=(($fell(foo) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
-000000 point: comment=if hier=top.t
|
||||
+000010 point: comment=else hier=top.t
|
||||
%000009 if (($changed(foo) != 0) && foo) bump <= bump + 1;
|
||||
-000009 point: comment=(((! $stable(foo)) != 32'sh0)==0) => 0 hier=top.t
|
||||
-000001 point: comment=(((! $stable(foo)) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
-000001 point: comment=if hier=top.t
|
||||
-000009 point: comment=else hier=top.t
|
||||
%000009 if (($rose(foo) != 0) && foo) bump <= bump + 1;
|
||||
-000009 point: comment=(($rose(foo) != 32'sh0)==0) => 0 hier=top.t
|
||||
-000001 point: comment=(($rose(foo) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
-000001 point: comment=if hier=top.t
|
||||
-000009 point: comment=else hier=top.t
|
||||
%000009 if (($stable(foo) != 0) && foo) bump <= bump + 1;
|
||||
-000001 point: comment=(($stable(foo) != 32'sh0)==0) => 0 hier=top.t
|
||||
-000009 point: comment=(($stable(foo) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
-000009 point: comment=if hier=top.t
|
||||
-000001 point: comment=else hier=top.t
|
||||
%000009 if (($past(foo) != 0) && foo) bump <= bump + 1;
|
||||
-000001 point: comment=(($past(foo) != 32'sh0)==0) => 0 hier=top.t
|
||||
-000009 point: comment=(($past(foo) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
-000009 point: comment=if hier=top.t
|
||||
-000001 point: comment=else hier=top.t
|
||||
~000010 if (($random != 0) && foo) bump <= bump + 1;
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($dist_erlang(result, 2, 3) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($dist_erlang(result, 32'sh2, 32'sh3) != 32'sh0)==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($dist_erlang(result, 32'sh2, 32'sh3) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($dist_normal(result, 2, 3) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($dist_normal(result, 32'sh2, 32'sh3) != 32'sh0)==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($dist_normal(result, 32'sh2, 32'sh3) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($dist_t(result, 2) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($dist_t(result, 32'sh2) != 32'sh0)==0) => 0 hier=top.t
|
||||
-000000 point: comment=(($dist_t(result, 32'sh2) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
-000000 point: comment=if hier=top.t
|
||||
+000010 point: comment=else hier=top.t
|
||||
~000010 if (($dist_chi_square(result, 2) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($dist_chi_square(result, 32'sh2) != 32'sh0)==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($dist_chi_square(result, 32'sh2) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($dist_exponential(result, 2) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($dist_exponential(result, 32'sh2) != 32'sh0)==0) => 0 hier=top.t
|
||||
-000000 point: comment=(($dist_exponential(result, 32'sh2) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($dist_poisson(result, 2) != 0) && foo) bump <= bump + 1;
|
||||
+000010 point: comment=(($dist_poisson(result, 32'sh2) != 32'sh0)==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($dist_poisson(result, 32'sh2) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($dist_uniform(result, 2, 3) != 0) && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(($dist_uniform(result, 32'sh2, 32'sh3) != 32'sh0)==0) => 0 hier=top.t
|
||||
+000010 point: comment=(($dist_uniform(result, 32'sh2, 32'sh3) != 32'sh0)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
~000010 if (($sformatf("abc") != "abc") && foo) bump <= bump + 1;
|
||||
+000010 point: comment=(($sformatf(%22abc%22);%0A != %22abc%22)==0) => 0 hier=top.t
|
||||
-000000 point: comment=(($sformatf(%22abc%22);%0A != %22abc%22)==1 && foo==1) => 1 hier=top.t
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
-000000 point: comment=if hier=top.t
|
||||
+000010 point: comment=else hier=top.t
|
||||
~000010 if (foo && foo) bump <= bump + 1;
|
||||
-000000 point: comment=(foo==0) => 0 hier=top.t
|
||||
+000010 point: comment=(foo==1) => 1 hier=top.t
|
||||
+000010 point: comment=if hier=top.t
|
||||
-000000 point: comment=else hier=top.t
|
||||
000010 cyc <= cyc + 1;
|
||||
+000010 point: comment=block hier=top.t
|
||||
%000009 if (cyc==9) begin
|
||||
-000001 point: comment=if hier=top.t
|
||||
-000009 point: comment=else hier=top.t
|
||||
%000001 $write("*-* All Finished *-*\n");
|
||||
-000001 point: comment=if hier=top.t
|
||||
%000001 $finish;
|
||||
-000001 point: comment=if hier=top.t
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
|
|
@ -0,0 +1,26 @@
|
|||
#!/usr/bin/env python3
|
||||
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
|
||||
#
|
||||
# Copyright 2024 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(verilator_flags2=["--cc --coverage-line --coverage-expr"])
|
||||
|
||||
test.execute()
|
||||
|
||||
test.run(cmd=[os.environ["VERILATOR_ROOT"] + "/bin/verilator_coverage",
|
||||
"--annotate-points",
|
||||
"--annotate", test.obj_dir + "/annotated",
|
||||
test.obj_dir + "/coverage.dat"],
|
||||
verilator_run=True) # yapf:disable
|
||||
|
||||
test.files_identical(test.obj_dir + "/annotated/t_cover_sys_line_expr.v", test.golden_filename)
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,81 @@
|
|||
// DESCRIPTION: Verilator: Verilog Test module
|
||||
//
|
||||
// This file ONLY is placed under the Creative Commons Public Domain, for
|
||||
// any use, without warranty, 2024 by Wilson Snyder.
|
||||
// SPDX-License-Identifier: CC0-1.0
|
||||
|
||||
module t (/*AUTOARG*/
|
||||
// Inputs
|
||||
clk
|
||||
);
|
||||
|
||||
input clk;
|
||||
|
||||
int cyc, bump, result;
|
||||
logic foo;
|
||||
initial begin
|
||||
cyc = 0;
|
||||
foo = '1;
|
||||
end
|
||||
|
||||
|
||||
always @(posedge clk) begin
|
||||
if (($time != 0) && foo) bump <= bump + 1;
|
||||
if (($realtime != 0) && foo) bump <= bump + 1;
|
||||
if (($stime != 0) && foo) bump <= bump + 1;
|
||||
if (($bitstoreal(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($itor(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($signed(3) != 0) && foo) bump <= bump + 1;
|
||||
if (($realtobits(1.23) != 0) && foo) bump <= bump + 1;
|
||||
if (($rtoi(1.23) != 0) && foo) bump <= bump + 1;
|
||||
if (($unsigned(-3) != 0) && foo) bump <= bump + 1;
|
||||
if (($clog2(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($ln(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($log10(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($exp(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($sqrt(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($pow(123, 2) != 0) && foo) bump <= bump + 1;
|
||||
if (($floor(1.23) != 0) && foo) bump <= bump + 1;
|
||||
if (($ceil(1.23) != 0) && foo) bump <= bump + 1;
|
||||
if (($sin(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($cos(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($tan(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($asin(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($acos(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($atan(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($atan2(123, 2) != 0) && foo) bump <= bump + 1;
|
||||
if (($hypot(123, 2) != 0) && foo) bump <= bump + 1;
|
||||
if (($sinh(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($cosh(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($tanh(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($asinh(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($acosh(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($atanh(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($countbits(123, 2) != 0) && foo) bump <= bump + 1;
|
||||
if (($onehot(123) != 0) && foo) bump <= bump + 1;
|
||||
if ($isunknown(foo) && foo) bump <= bump + 1;
|
||||
if (($countones(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($onehot0(123) != 0) && foo) bump <= bump + 1;
|
||||
if (($sampled(foo) != 0) && foo) bump <= bump + 1;
|
||||
if (($fell(foo) != 0) && foo) bump <= bump + 1;
|
||||
if (($changed(foo) != 0) && foo) bump <= bump + 1;
|
||||
if (($rose(foo) != 0) && foo) bump <= bump + 1;
|
||||
if (($stable(foo) != 0) && foo) bump <= bump + 1;
|
||||
if (($past(foo) != 0) && foo) bump <= bump + 1;
|
||||
if (($random != 0) && foo) bump <= bump + 1;
|
||||
if (($dist_erlang(result, 2, 3) != 0) && foo) bump <= bump + 1;
|
||||
if (($dist_normal(result, 2, 3) != 0) && foo) bump <= bump + 1;
|
||||
if (($dist_t(result, 2) != 0) && foo) bump <= bump + 1;
|
||||
if (($dist_chi_square(result, 2) != 0) && foo) bump <= bump + 1;
|
||||
if (($dist_exponential(result, 2) != 0) && foo) bump <= bump + 1;
|
||||
if (($dist_poisson(result, 2) != 0) && foo) bump <= bump + 1;
|
||||
if (($dist_uniform(result, 2, 3) != 0) && foo) bump <= bump + 1;
|
||||
if (($sformatf("abc") != "abc") && foo) bump <= bump + 1;
|
||||
if (foo && foo) bump <= bump + 1;
|
||||
cyc <= cyc + 1;
|
||||
if (cyc==9) begin
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
| ^~~~~~
|
||||
|
|
|
|||
|
|
@ -39,6 +39,7 @@ module t (/*AUTOARG*/
|
|||
$write("[%0t] cyc==%0d sum=%x\n", $time, cyc, w[CNT]);
|
||||
`endif
|
||||
if (w[CNT] !== `EXPECTED_SUM) $stop;
|
||||
$display("cyc: %0d $past(cyc): %0d", cyc, $past(cyc));
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
end
|
||||
|
|
@ -55,7 +56,7 @@ module sub (input clk, input [31:0] i, output [31:0] z);
|
|||
assign z = z_tmp;
|
||||
|
||||
always @(posedge z_tmp == 32'b11) begin
|
||||
$display("%m z_tmp[0]: %0d", z_tmp);
|
||||
$display("%m z_tmp: %0d, $past(z_tmp): $0d", z_tmp, $past(z_tmp));
|
||||
end
|
||||
|
||||
endmodule
|
||||
|
|
|
|||
|
|
@ -125,7 +125,7 @@ test.file_grep_not(test.obj_dir + "/" + test.vm_prefix + "_classes.mk", "vm_clas
|
|||
test.file_grep_not(test.obj_dir + "/" + test.vm_prefix + "_classes.mk", "vm_classes_2")
|
||||
|
||||
# Check combine count
|
||||
test.file_grep(test.stats, r'Node count, CFILE + (\d+)', (219 if test.vltmt else 205))
|
||||
test.file_grep(test.stats, r'Node count, CFILE + (\d+)', (239 if test.vltmt else 222))
|
||||
test.file_grep(test.stats, r'Makefile targets, VM_CLASSES_FAST + (\d+)', 2)
|
||||
test.file_grep(test.stats, r'Makefile targets, VM_CLASSES_SLOW + (\d+)', 2)
|
||||
|
||||
|
|
|
|||
|
|
@ -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 *-*
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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 *-*
|
||||
|
|
|
|||
|
|
@ -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()
|
||||
|
|
|
|||
|
|
@ -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__);
|
||||
|
||||
|
|
|
|||
|
|
@ -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()
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -0,0 +1 @@
|
|||
t_sys_file_basic.out
|
||||
|
|
@ -0,0 +1,26 @@
|
|||
#!/usr/bin/env python3
|
||||
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
|
||||
#
|
||||
# Copyright 2024 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.top_filename = "t/t_sys_file_basic.v"
|
||||
|
||||
test.unlink_ok(test.obj_dir + "/t_sys_file_basic_test.log")
|
||||
|
||||
test.compile(
|
||||
verilator_flags2=["--coverage-expr"],
|
||||
# Build without cached objects, see bug363
|
||||
make_flags=["VM_PARALLEL_BUILDS=0"],
|
||||
)
|
||||
|
||||
test.execute()
|
||||
test.files_identical(test.obj_dir + "/t_sys_file_basic_test.log", test.golden_filename)
|
||||
|
||||
test.passes()
|
||||
Loading…
Reference in New Issue