Implement multi-expression inline sequences
Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>
This commit is contained in:
Bartłomiej Chmiel
parent
ea75163567
commit
61a1dd9531
|
|
@ -43,6 +43,7 @@ set(HEADERS
|
|||
V3ActiveTop.h
|
||||
V3Assert.h
|
||||
V3AssertPre.h
|
||||
V3AssertProperties.h
|
||||
V3Ast.h
|
||||
V3AstAttr.h
|
||||
V3AstInlines.h
|
||||
|
|
@ -207,6 +208,7 @@ set(COMMON_SOURCES
|
|||
V3ActiveTop.cpp
|
||||
V3Assert.cpp
|
||||
V3AssertPre.cpp
|
||||
V3AssertProperties.cpp
|
||||
V3Ast.cpp
|
||||
V3AstNodes.cpp
|
||||
V3Begin.cpp
|
||||
|
|
|
|||
|
|
@ -232,6 +232,7 @@ RAW_OBJS_PCH_ASTNOMT = \
|
|||
V3ActiveTop.o \
|
||||
V3Assert.o \
|
||||
V3AssertPre.o \
|
||||
V3AssertProperties.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,17 @@ class AssertVisitor final : public VNVisitor {
|
|||
return ifp;
|
||||
}
|
||||
|
||||
static AstNode* assertBody(AstNodeCoverOrAssert* nodep, AstNodeExpr* propp, AstNode* passsp,
|
||||
AstNode* assertBody(AstNodeCoverOrAssert* nodep, AstNode* 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* bodyp = nullptr;
|
||||
if (VString::startsWith(propp->name(), "__Vassert")) {
|
||||
AstFork* const forkp = new AstFork{nodep->fileline(), VJoinType::JOIN_NONE};
|
||||
forkp->addForksp(new AstBegin{nodep->fileline(), "", propp, true});
|
||||
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 +331,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 +378,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 +633,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,19 +653,32 @@ class AssertVisitor final : public VNVisitor {
|
|||
m_inSampled = false;
|
||||
iterateChildren(nodep);
|
||||
}
|
||||
void visit(AstPExpr* nodep) override {
|
||||
{
|
||||
VL_RESTORER(m_inSampled);
|
||||
m_inSampled = false;
|
||||
iterateAndNextNull(nodep->precondp());
|
||||
}
|
||||
iterate(nodep->condp());
|
||||
if (!m_inRestrict) {
|
||||
void visit(AstPExprClause* nodep) override {
|
||||
if (m_underAssert) {
|
||||
if (nodep->passs() && m_passsp) {
|
||||
// Cover adds COVERINC by AstNode::addNext, thus need to clone next too.
|
||||
nodep->replaceWith(m_passsp->cloneTree(true));
|
||||
VL_DO_DANGLING(pushDeletep(nodep), nodep);
|
||||
} else if (!nodep->passs() && 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));
|
||||
VL_DO_DANGLING(pushDeletep(nodep), nodep);
|
||||
} else {
|
||||
VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep);
|
||||
}
|
||||
}
|
||||
}
|
||||
void visit(AstPExpr* nodep) override {
|
||||
m_inSampled = false;
|
||||
if (m_underAssert) {
|
||||
iterateChildren(nodep);
|
||||
nodep->replaceWith(nodep->bodyp()->unlinkFrBack());
|
||||
VL_DO_DANGLING(pushDeletep(nodep), nodep);
|
||||
} else if (m_inRestrict) {
|
||||
VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep);
|
||||
}
|
||||
}
|
||||
|
||||
//========== Statements
|
||||
void visit(AstDisplay* nodep) override {
|
||||
|
|
|
|||
|
|
@ -56,15 +56,13 @@ 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_hasPExpr = false; // True if assert has AstPExpr inside
|
||||
bool m_inPExpr = false; // True if in AstPExpr
|
||||
|
||||
// METHODS
|
||||
|
||||
|
|
@ -343,7 +341,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 +417,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,17 +471,15 @@ private:
|
|||
void visit(AstNodeCoverOrAssert* nodep) override {
|
||||
if (nodep->sentreep()) return; // Already processed
|
||||
|
||||
VL_RESTORER(m_hasSExpr);
|
||||
VL_RESTORER(m_hasPExpr);
|
||||
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 (m_hasPExpr && m_hasUnsupp) {
|
||||
if (VN_IS(m_hasUnsupp, Implication)) {
|
||||
m_hasUnsupp->v3warn(E_UNSUPPORTED,
|
||||
"Unsupported: Implication with sequence expression");
|
||||
|
|
@ -518,13 +487,7 @@ private:
|
|||
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);
|
||||
VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep);
|
||||
}
|
||||
clearAssertInfo();
|
||||
}
|
||||
|
|
@ -564,10 +527,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);
|
||||
|
|
@ -699,17 +658,20 @@ 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;
|
||||
m_hasPExpr = 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,280 @@
|
|||
// -*- mode: C++; c-file-style: "cc-mode" -*-
|
||||
//*************************************************************************
|
||||
// DESCRIPTION: Verilator: Transform sequences into 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
|
||||
//
|
||||
//*************************************************************************
|
||||
// Properties steps:
|
||||
// Ensemble a property decision tree from sequence expressions.
|
||||
// Property decision tree is a tree rooted with source sequence
|
||||
// expression. It has a bipartite structure
|
||||
// (Expr -> Stmt -> Expr ...).
|
||||
// Transform property decision tree into AST, remove source sequence
|
||||
// expression
|
||||
// Each property is wrapped with AstPExpr that is transformed
|
||||
// further by V3AssertPre and V3Assert.
|
||||
//
|
||||
//*************************************************************************
|
||||
|
||||
#include "V3PchAstNoMT.h" // VL_MT_DISABLED_CODE_UNIT
|
||||
|
||||
#include "V3AssertProperties.h"
|
||||
|
||||
#include "V3Graph.h"
|
||||
#include "V3UniqueNames.h"
|
||||
|
||||
VL_DEFINE_DEBUG_FUNCTIONS;
|
||||
|
||||
namespace {
|
||||
|
||||
//######################################################################
|
||||
// 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; }
|
||||
// LCOV_EXCL_START // Debug code
|
||||
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";
|
||||
}
|
||||
// LCOV_EXCL_STOP
|
||||
bool isStart() const { return inEmpty(); }
|
||||
};
|
||||
|
||||
class StmtVertex final : public DfaVertex {
|
||||
VL_RTTI_IMPL(StmtVertex, V3GraphEdge)
|
||||
public:
|
||||
// CONSTRUCTORS
|
||||
explicit StmtVertex(V3Graph* graphp, AstNodeStmt* stmtp) VL_MT_DISABLED
|
||||
: DfaVertex{graphp, stmtp} {}
|
||||
// LCOV_EXCL_START // Debug code
|
||||
string dotColor() const override { return "green"; }
|
||||
// LCOV_EXCL_STOP
|
||||
};
|
||||
|
||||
class ExprVertex final : public DfaVertex {
|
||||
VL_RTTI_IMPL(ExprVertex, V3GraphEdge)
|
||||
public:
|
||||
// CONSTRUCTORS
|
||||
explicit ExprVertex(V3Graph* graphp, AstNodeExpr* exprp) VL_MT_DISABLED
|
||||
: DfaVertex{graphp, exprp} {}
|
||||
// LCOV_EXCL_START // Debug code
|
||||
string dotColor() const override { return "blue"; }
|
||||
// LCOV_EXCL_STOP
|
||||
};
|
||||
|
||||
class ConditionEdge final : public V3GraphEdge {
|
||||
VL_RTTI_IMPL(ConditionEdge, V3GraphEdge)
|
||||
// STATE
|
||||
const bool m_ifBranch; // Whether this branch is taken for fulfilled condition
|
||||
|
||||
public:
|
||||
// CONSTRUCTORS
|
||||
explicit ConditionEdge(V3Graph* graphp, DfaVertex* fromp, DfaVertex* top,
|
||||
bool ifBranch) VL_MT_DISABLED : V3GraphEdge{graphp, fromp, top, 1},
|
||||
m_ifBranch{ifBranch} {}
|
||||
~ConditionEdge() override = default;
|
||||
|
||||
bool ifBranch() const { return m_ifBranch; }
|
||||
// LCOV_EXCL_START // Debug code
|
||||
string dotColor() const override { return m_ifBranch ? "green" : "red"; }
|
||||
// LCOV_EXCL_STOP
|
||||
};
|
||||
|
||||
// Parse properties and ensemble a property tree graph
|
||||
class AssertPropertiesParser final : public VNVisitorConst {
|
||||
// STATE
|
||||
std::unique_ptr<V3Graph> m_graphp = std::make_unique<V3Graph>(); // Property tree
|
||||
DfaVertex* m_lastp = nullptr; // Last encountered vertex
|
||||
bool m_underSExpr
|
||||
= false; // Whether it is under sequence expression for creating a start node
|
||||
size_t m_underLogNots = 0; // Number of not operators before sequence
|
||||
|
||||
// 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 {
|
||||
const auto makeClause = [this, nodep](bool pass) {
|
||||
return new StmtVertex{
|
||||
m_graphp.get(),
|
||||
new AstPExprClause{nodep->fileline(), m_underLogNots % 2 == 0 ? pass : !pass}};
|
||||
};
|
||||
|
||||
if (VN_IS(nodep->exprp(), SExpr)) {
|
||||
VL_RESTORER(m_underSExpr);
|
||||
m_underSExpr = true;
|
||||
iterateConst(nodep->exprp());
|
||||
} else {
|
||||
ExprVertex* const exprVtxp
|
||||
= new ExprVertex{m_graphp.get(), nodep->exprp()->unlinkFrBack()};
|
||||
new ConditionEdge{m_graphp.get(), exprVtxp, makeClause(true), true};
|
||||
new ConditionEdge{m_graphp.get(), exprVtxp, makeClause(false), false};
|
||||
m_lastp = exprVtxp;
|
||||
}
|
||||
|
||||
ExprVertex* const startp = m_underSExpr ? nullptr : new ExprVertex{m_graphp.get(), nodep};
|
||||
|
||||
StmtVertex* const dlyVtxp
|
||||
= new StmtVertex{m_graphp.get(), 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");
|
||||
StmtVertex* const sdlyVtxp
|
||||
= new StmtVertex{m_graphp.get(), sexprp->delayp()->unlinkFrBack()};
|
||||
ExprVertex* const exprVtxp
|
||||
= new ExprVertex{m_graphp.get(), sexprp->exprp()->unlinkFrBack()};
|
||||
|
||||
if (startp) new ConditionEdge{m_graphp.get(), startp, sdlyVtxp, true};
|
||||
new ConditionEdge{m_graphp.get(), sdlyVtxp, exprVtxp, true};
|
||||
new ConditionEdge{m_graphp.get(), exprVtxp, dlyVtxp, true};
|
||||
new ConditionEdge{m_graphp.get(), dlyVtxp, m_lastp, true};
|
||||
new ConditionEdge{m_graphp.get(), exprVtxp, makeClause(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()) {
|
||||
ExprVertex* const preVtxp
|
||||
= new ExprVertex{m_graphp.get(), nodep->preExprp()->unlinkFrBack()};
|
||||
if (startp) new ConditionEdge{m_graphp.get(), startp, preVtxp, true};
|
||||
new ConditionEdge{m_graphp.get(), preVtxp, dlyVtxp, true};
|
||||
new ConditionEdge{m_graphp.get(), dlyVtxp, m_lastp, true};
|
||||
new ConditionEdge{m_graphp.get(), preVtxp, makeClause(false), false};
|
||||
m_lastp = preVtxp;
|
||||
} else {
|
||||
if (startp) new ConditionEdge{m_graphp.get(), startp, dlyVtxp, true};
|
||||
new ConditionEdge{m_graphp.get(), dlyVtxp, m_lastp, true};
|
||||
m_lastp = dlyVtxp;
|
||||
}
|
||||
}
|
||||
void visit(AstNode* nodep) override { iterateChildrenConst(nodep); }
|
||||
void visit(AstConstPool* nodep) override {}
|
||||
|
||||
public:
|
||||
// CONSTRUCTORS
|
||||
explicit AssertPropertiesParser(AstNetlist* nodep) {
|
||||
iterateConst(nodep);
|
||||
if (dumpGraphLevel() >= 6) m_graphp->dumpDotFilePrefixedAlways("properties", true);
|
||||
}
|
||||
std::unique_ptr<V3Graph> graphp() { return std::move(m_graphp); }
|
||||
~AssertPropertiesParser() override = default;
|
||||
};
|
||||
|
||||
// Transform property graph into AST
|
||||
class AssertPropertiesTransformer final {
|
||||
// STATE
|
||||
V3UniqueNames m_assertCycleDelayNames{"__Vassert"}; // Names for assertion properties
|
||||
const std::unique_ptr<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 (StmtVertex* const stmtp = vtxp->cast<StmtVertex>()) return processVtx(stmtp);
|
||||
if (ExprVertex* const exprp = vtxp->cast<ExprVertex>()) return processVtx(exprp);
|
||||
// TODO use C++17 std::variant and std::visit
|
||||
// LCOV_EXCL_START
|
||||
assert(0);
|
||||
VL_UNREACHABLE;
|
||||
return nullptr;
|
||||
// LCOV_EXCL_STOP
|
||||
}
|
||||
V3GraphVertex* processVtx(StmtVertex* 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(ExprVertex* vtxp) {
|
||||
AstNode* const nodep = vtxp->nodep();
|
||||
if (vtxp->isStart()) {
|
||||
AstBegin* const bodyp = new AstBegin{
|
||||
nodep->fileline(), m_assertCycleDelayNames.get(nodep) + "__block", nullptr, true};
|
||||
m_pexprp = new AstPExpr{nodep->fileline(), bodyp, nodep->dtypep()};
|
||||
UASSERT_OBJ(vtxp->outSize1() && vtxp->outEdges().frontp()->is<ConditionEdge>(), nodep,
|
||||
"Incorrect property graph");
|
||||
m_current = m_pexprp->bodyp();
|
||||
return processEdge(vtxp->outEdges().frontp());
|
||||
}
|
||||
UASSERT_OBJ(vtxp->outEdges().size() > 0 && vtxp->outEdges().size() <= 2, nodep,
|
||||
"Incorrect edges");
|
||||
AstBegin* const passsp = new AstBegin{
|
||||
nodep->fileline(), m_assertCycleDelayNames.get(nodep) + "__block_pass", nullptr, true};
|
||||
AstNode* const failsp = [vtxp]() -> AstNode* {
|
||||
if (!vtxp->outSize1()) {
|
||||
V3GraphVertex* const failVtxp = vtxp->outEdges().backp()->top();
|
||||
return failVtxp->as<StmtVertex>()->nodep();
|
||||
}
|
||||
return nullptr;
|
||||
}();
|
||||
|
||||
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 AssertPropertiesTransformer(std::unique_ptr<V3Graph> graph)
|
||||
: m_graph{std::move(graph)} {
|
||||
for (V3GraphVertex& vtx : m_graph->vertices()) {
|
||||
if (DfaVertex* const dVtxp = vtx.cast<ExprVertex>()) {
|
||||
if (dVtxp->isStart()) {
|
||||
VL_RESTORER(m_pexprp);
|
||||
processVtx(&vtx);
|
||||
AstSExpr* const propp = VN_AS(dVtxp->nodep(), SExpr);
|
||||
propp->replaceWith(m_pexprp);
|
||||
propp->deleteTree();
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
} //namespace
|
||||
|
||||
//######################################################################
|
||||
// Top AssertProperties class
|
||||
|
||||
void V3AssertProperties::assertPropertiesAll(AstNetlist* nodep) {
|
||||
UINFO(2, __FUNCTION__ << ":");
|
||||
{
|
||||
std::unique_ptr<V3Graph> graphp = AssertPropertiesParser{nodep}.graphp();
|
||||
AssertPropertiesTransformer{std::move(graphp)};
|
||||
}
|
||||
V3Global::dumpCheckGlobalTree("assertproperties", 0, dumpTreeEitherLevel() >= 3);
|
||||
}
|
||||
|
|
@ -0,0 +1,32 @@
|
|||
// -*- mode: C++; c-file-style: "cc-mode" -*-
|
||||
//*************************************************************************
|
||||
// DESCRIPTION: Verilator: Transform sequences into 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_V3ASSERTPROPERTIES_H_
|
||||
#define VERILATOR_V3ASSERTPROPERTIES_H_
|
||||
|
||||
#include "config_build.h"
|
||||
#include "verilatedos.h"
|
||||
|
||||
class AstNetlist;
|
||||
|
||||
//============================================================================
|
||||
|
||||
class V3AssertProperties final {
|
||||
public:
|
||||
static void assertPropertiesAll(AstNetlist* nodep) VL_MT_DISABLED;
|
||||
};
|
||||
|
||||
#endif // Guard
|
||||
|
|
@ -1764,11 +1764,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(""); }
|
||||
|
|
@ -1986,11 +1988,19 @@ public:
|
|||
};
|
||||
class AstSExpr final : public AstNodeExpr {
|
||||
// Sequence expression
|
||||
// @astgen op1 := delayp : AstDelay
|
||||
// @astgen op2 := exprp : AstNodeExpr
|
||||
// @astgen op1 := preExprp: Optional[AstNodeExpr]
|
||||
// @astgen op2 := delayp : AstNodeStmt<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);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -821,6 +821,16 @@ public:
|
|||
}
|
||||
bool off() const { return m_off; }
|
||||
};
|
||||
class AstPExprClause final : public AstNodeStmt {
|
||||
const bool m_passs;
|
||||
|
||||
public:
|
||||
ASTGEN_MEMBERS_AstPExprClause;
|
||||
explicit AstPExprClause(FileLine* fl, bool passs = true)
|
||||
: ASTGEN_SUPER_PExprClause(fl)
|
||||
, m_passs{passs} {}
|
||||
bool passs() const { return m_passs; }
|
||||
};
|
||||
class AstPrintTimeScale final : public AstNodeStmt {
|
||||
// Parents: stmtlist
|
||||
string m_name; // Parent module name
|
||||
|
|
|
|||
|
|
@ -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());
|
||||
}
|
||||
|
|
@ -799,9 +800,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,15 +810,11 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
|
|||
}
|
||||
iterateConstNull(nodep->sentreep());
|
||||
puts("(");
|
||||
if (const AstPExpr* const pexprp = VN_CAST(nodep->propp(), PExpr)) {
|
||||
iterateAndNextConstNull(pexprp->condp());
|
||||
} else {
|
||||
if (AstSampled* const sampledp = VN_CAST(nodep->propp(), Sampled)) {
|
||||
iterateAndNextConstNull(sampledp->exprp());
|
||||
} else {
|
||||
iterateAndNextConstNull(nodep->propp());
|
||||
}
|
||||
}
|
||||
if (!VN_IS(nodep, Restrict)) {
|
||||
puts(") begin\n");
|
||||
iterateAndNextConstNull(nodep->passsp());
|
||||
|
|
@ -1052,16 +1046,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,7 @@ 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
|
||||
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
|
||||
|
|
@ -1557,9 +1558,14 @@ class WidthVisitor final : public VNVisitor {
|
|||
}
|
||||
}
|
||||
void visit(AstSExpr* nodep) override {
|
||||
VL_RESTORER(m_underSExpr);
|
||||
m_underSExpr = 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();
|
||||
}
|
||||
}
|
||||
|
|
@ -7008,6 +7014,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 "V3AssertProperties.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
|
||||
V3AssertProperties::assertPropertiesAll(v3Global.rootp());
|
||||
//
|
||||
V3AssertPre::assertPreAll(v3Global.rootp());
|
||||
//
|
||||
V3Assert::assertAll(v3Global.rootp());
|
||||
|
|
|
|||
|
|
@ -6534,7 +6534,7 @@ 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 ')'
|
||||
|
|
@ -6622,9 +6622,15 @@ sexpr<nodeExprp>: // ==IEEE: sequence_expr (The name sexpr is important as reg
|
|||
// // IEEE: "sequence_expr cycle_delay_range sequence_expr { cycle_delay_range sequence_expr }"
|
||||
// // Both rules basically mean we can repeat sequences, so make it simpler:
|
||||
cycle_delay_range ~p~sexpr %prec yP_POUNDPOUND
|
||||
{ $$ = new AstSExpr{$<fl>1, $1, $2}; }
|
||||
{ $$ = new AstSExpr{$<fl>1, $1, $2};
|
||||
if (VN_IS($2, LogNot)) {
|
||||
BBUNSUP($2->fileline(), "Unexpected not in sequence expression context");
|
||||
}
|
||||
}
|
||||
| ~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"!
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
| ^~~~~~
|
||||
|
|
|
|||
|
|
@ -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,5 @@
|
|||
%Error: t/t_property_sexpr_bad.v:20:39: Syntax error: unexpected 'not' in sequence expression
|
||||
: ... note: In instance 't'
|
||||
20 | assert property (@(posedge clk) ##1 not val) $display("[%0t] single delay with negated var stmt, fileline:%d", $time, 20);
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_bad.v:20:39: Unexpected not in sequence expression context
|
||||
20 | assert property (@(posedge clk) ##1 not val);
|
||||
| ^~~
|
||||
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
|
||||
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
|
||||
%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'])
|
||||
|
||||
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);
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:67:14: Unsupported: sequence match items
|
||||
67 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
|
||||
| ^
|
||||
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:30:43: Unsupported: ## (in sequence expression)
|
||||
30 | assert property (@(posedge clk) ##1 val ##2 val) $display("[%0t] sequence stmt, fileline:%d", $time, 30);
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:67:29: Unsupported: ## range cycle delay range expression
|
||||
67 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:71:14: Unsupported: sequence match items
|
||||
71 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
|
||||
| ^
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:71:29: Unsupported: ## range cycle delay range expression
|
||||
71 | ($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:66:13: Unsupported: property variable declaration
|
||||
66 | 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:84:16: Unsupported: sequence match items
|
||||
84 | (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:84:51: Unsupported: [-> boolean abbrev expression
|
||||
84 | (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:84:54: Unsupported: boolean abbrev (in sequence expression)
|
||||
84 | (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:82:14: Unsupported: property variable declaration
|
||||
82 | 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,35 @@
|
|||
%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
|
||||
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
|
||||
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
|
||||
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
|
||||
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
|
||||
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
|
||||
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
|
||||
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: 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,6 @@ 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
|
||||
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:109:27: Unsupported: sequence argument data type
|
||||
109 | sequence p_arg_seqence(sequence inseq);
|
||||
| ^~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:112:27: Unsupported: sequence argument data type
|
||||
112 | sequence p_arg_seqence(sequence inseq);
|
||||
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:113:4: Unsupported: sequence
|
||||
113 | sequence s_firstmatch_a;
|
||||
| ^~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:114:7: Unsupported: first_match (in sequence expression)
|
||||
114 | first_match (a);
|
||||
| ^~~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:116:4: Unsupported: sequence
|
||||
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
|
||||
|
|
|
|||
Loading…
Reference in New Issue