Support `s_until` and `s_until_with` (IEEE1800-2023 16.12.12) (#7722)
Signed-off-by: Artur Bieniek <abieniek@antmicro.com>
This commit is contained in:
Artur Bieniek
GitHub
parent
96336395d6
commit
a3827182c0
|
|
@ -253,8 +253,7 @@ class AssertVisitor final : public VNVisitor {
|
|||
}
|
||||
}
|
||||
AstSampled* newSampledExpr(AstNodeExpr* nodep) {
|
||||
AstSampled* const sampledp = new AstSampled{nodep->fileline(), nodep};
|
||||
sampledp->dtypeFrom(nodep);
|
||||
AstSampled* const sampledp = new AstSampled{nodep->fileline(), nodep, nodep->dtypep()};
|
||||
return sampledp;
|
||||
}
|
||||
AstVarRef* newMonitorNumVarRefp(const AstNode* nodep, VAccess access) {
|
||||
|
|
|
|||
|
|
@ -182,8 +182,7 @@ struct BuildResult final {
|
|||
};
|
||||
|
||||
static AstNodeExpr* sampled(AstNodeExpr* exprp) {
|
||||
AstSampled* const sp = new AstSampled{exprp->fileline(), exprp};
|
||||
sp->dtypeFrom(exprp);
|
||||
AstSampled* const sp = new AstSampled{exprp->fileline(), exprp, exprp->dtypep()};
|
||||
return sp;
|
||||
}
|
||||
|
||||
|
|
@ -838,13 +837,14 @@ class SvaNfaBuilder final {
|
|||
BuildResult buildUntil(AstUntil* nodep, SvaStateVertex* entryVtxp, bool isTopLevelStep) {
|
||||
FileLine* const flp = nodep->fileline();
|
||||
if (!isTopLevelStep) {
|
||||
nodep->v3warn(E_UNSUPPORTED, "Unsupported: 'until' in complex property expression");
|
||||
nodep->v3warn(E_UNSUPPORTED, "Unsupported: '" << nodep->verilogKwd()
|
||||
<< "' in complex property expression");
|
||||
return BuildResult::failWithError();
|
||||
}
|
||||
if (nodep->isStrong()) {
|
||||
nodep->v3warn(E_UNSUPPORTED, "Unsupported: s_until"
|
||||
<< (nodep->isOverlapping() ? "_with" : "")
|
||||
<< " (in property expresion)");
|
||||
<< " (in property expression)");
|
||||
return BuildResult::failWithError();
|
||||
}
|
||||
AstNodeExpr* const lhsp = nodep->lhsp();
|
||||
|
|
@ -853,7 +853,8 @@ class SvaNfaBuilder final {
|
|||
return ep->exists([](const AstNodeExpr* np) { return np->isMultiCycleSva(); });
|
||||
};
|
||||
if (hasSeq(lhsp) || hasSeq(rhsp)) {
|
||||
nodep->v3warn(E_UNSUPPORTED, "Unsupported: 'until' in complex property expression");
|
||||
nodep->v3warn(E_UNSUPPORTED, "Unsupported: '" << nodep->verilogKwd()
|
||||
<< "' in complex property expression");
|
||||
return BuildResult::failWithError();
|
||||
}
|
||||
|
||||
|
|
@ -1926,16 +1927,16 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
|
||||
// Bare `assert property (p until q)` with boolean operands stays on
|
||||
// V3AssertPre's AstLoop lowering, which preserves per-attempt action-block
|
||||
// firings that this NFA's single-bit aggregated state cannot. NFA still
|
||||
// owns strong forms, sequence operands, and any embedding inside a
|
||||
// multi-cycle context (implication consequent, or/and operands, etc.).
|
||||
// firings that this NFA's single-bit aggregated state cannot. Strong bare
|
||||
// forms are also lowered there. NFA still owns sequence operands and any
|
||||
// embedding inside a multi-cycle context (implication consequent, or/and
|
||||
// operands, etc.).
|
||||
static bool isBareTopLevelUntil(AstNode* propp) {
|
||||
AstNode* p = propp;
|
||||
if (AstPropSpec* const specp = VN_CAST(p, PropSpec)) p = specp->propp();
|
||||
while (AstLogNot* const notp = VN_CAST(p, LogNot)) p = notp->lhsp();
|
||||
AstUntil* const untilp = VN_CAST(p, Until);
|
||||
if (!untilp) return false;
|
||||
if (untilp->isStrong()) return false;
|
||||
const auto hasSeq = [](const AstNodeExpr* ep) {
|
||||
return ep->exists([](const AstNodeExpr* np) { return np->isMultiCycleSva(); });
|
||||
};
|
||||
|
|
|
|||
|
|
@ -366,8 +366,8 @@ private:
|
|||
if (skewp->num().is1Step()) {
|
||||
// #1step means the value that is sampled is always the signal's last value
|
||||
// before the clock edge (IEEE 1800-2023 14.4)
|
||||
AstSampled* const sampledp = new AstSampled{flp, exprp->cloneTreePure(false)};
|
||||
sampledp->dtypeFrom(exprp);
|
||||
AstSampled* const sampledp
|
||||
= new AstSampled{flp, exprp->cloneTreePure(false), exprp->dtypep()};
|
||||
AstAssign* const assignp = new AstAssign{flp, refp, sampledp};
|
||||
m_clockingp->addNextHere(new AstAlways{
|
||||
flp, VAlwaysKwd::ALWAYS,
|
||||
|
|
@ -413,7 +413,7 @@ private:
|
|||
}
|
||||
}
|
||||
void visit(AstDelay* nodep) override {
|
||||
m_hasCycleDelay = true;
|
||||
m_hasCycleDelay |= nodep->isCycleDelay();
|
||||
// Only cycle delays are relevant in this stage; also only process once
|
||||
if (!nodep->isCycleDelay()) {
|
||||
if (m_inSynchDrive) {
|
||||
|
|
@ -844,7 +844,7 @@ private:
|
|||
|
||||
// Assertion condition check
|
||||
AstLoop* const loopp = new AstLoop{flp};
|
||||
AstNodeExpr* const condp = new AstSampled{flp, nodep->exprp()->unlinkFrBack()};
|
||||
AstNodeExpr* const condp = new AstSampled{flp, nodep->exprp()->unlinkFrBack(), nullptr};
|
||||
loopp->addStmtsp(new AstLoopTest{flp, loopp, new AstLogNot{flp, condp}});
|
||||
loopp->addStmtsp(new AstEventControl{flp, sentreep, nullptr});
|
||||
|
||||
|
|
@ -1298,17 +1298,121 @@ private:
|
|||
}
|
||||
void visit(AstUntil* nodep) override {
|
||||
FileLine* const flp = nodep->fileline();
|
||||
if (m_pexprp) {
|
||||
nodep->v3warn(E_UNSUPPORTED, "Unsupported: 'until' in complex property expression");
|
||||
nodep->replaceWith(new AstConst{flp, AstConst::BitFalse{}});
|
||||
VL_DO_DANGLING(pushDeletep(nodep), nodep);
|
||||
return;
|
||||
}
|
||||
UASSERT_OBJ(
|
||||
!m_pexprp, nodep,
|
||||
"'" << nodep->verilogKwd()
|
||||
<< "' in complex property expression should have been rejected by V3AssertNfa");
|
||||
if (nodep->isStrong()) {
|
||||
nodep->v3warn(E_UNSUPPORTED, "Unsupported: s_until"
|
||||
<< (nodep->isOverlapping() ? "_with" : "")
|
||||
<< " (in property expresion)");
|
||||
nodep->replaceWith(new AstConst{flp, AstConst::BitFalse{}});
|
||||
// p s_until q / p s_until_with q: q must eventually be true. Until then, p must
|
||||
// be true on every sampled tick. For s_until, check q first: when q is true on
|
||||
// this tick, p is not required. For s_until_with, p must be true on the q tick too.
|
||||
AstNodeExpr* const rawLhsp = nodep->lhsp()->unlinkFrBack();
|
||||
AstNodeExpr* const rawRhsp = nodep->rhsp()->unlinkFrBack();
|
||||
AstSampled* const lhsp = new AstSampled{flp, rawLhsp, rawLhsp->dtypep()};
|
||||
AstSampled* const rhsp = new AstSampled{flp, rawRhsp, rawRhsp->dtypep()};
|
||||
AstNodeExpr* finalCondp = rhsp->cloneTreePure(false);
|
||||
if (nodep->isOverlapping()) {
|
||||
finalCondp = new AstLogAnd{flp, lhsp->cloneTreePure(false), finalCondp};
|
||||
}
|
||||
|
||||
// Track active assertion attempts. Only the count is needed to emit final failures.
|
||||
AstVar* const activep = new AstVar{flp, VVarType::MODULETEMP, m_activeNames.get(""),
|
||||
nodep->findBasicDType(VBasicDTypeKwd::UINT32)};
|
||||
activep->lifetime(VLifetime::STATIC_EXPLICIT);
|
||||
m_modp->addStmtsp(activep);
|
||||
|
||||
AstVar* const donep
|
||||
= new AstVar{flp, VVarType::BLOCKTEMP, "__VassertDone", nodep->findBitDType()};
|
||||
donep->lifetime(VLifetime::AUTOMATIC_EXPLICIT);
|
||||
auto setDone = [&]() {
|
||||
return new AstAssign{flp, new AstVarRef{flp, donep, VAccess::WRITE},
|
||||
new AstConst{flp, AstConst::BitTrue{}}};
|
||||
};
|
||||
|
||||
AstLoop* const loopp = new AstLoop{flp};
|
||||
AstAssign* const decrementVar = new AstAssign{
|
||||
flp, new AstVarRef{flp, activep, VAccess::WRITE},
|
||||
new AstSub{flp, new AstVarRef{flp, activep, VAccess::READ}, new AstConst{flp, 1}}};
|
||||
loopp->addStmtsp(new AstLoopTest{
|
||||
flp, loopp, new AstLogNot{flp, new AstVarRef{flp, donep, VAccess::READ}}});
|
||||
{
|
||||
AstBegin* const passp = new AstBegin{flp, "", nullptr, true};
|
||||
passp->addStmtsp(new AstPExprClause{flp});
|
||||
passp->addStmtsp(decrementVar);
|
||||
passp->addStmtsp(setDone());
|
||||
AstNodeExpr* passCondp = rhsp;
|
||||
if (nodep->isOverlapping()) {
|
||||
passCondp = new AstLogAnd{flp, lhsp->cloneTreePure(false), passCondp};
|
||||
}
|
||||
loopp->addStmtsp(new AstIf{flp, passCondp, passp});
|
||||
}
|
||||
{
|
||||
AstBegin* const failp = new AstBegin{flp, "", nullptr, true};
|
||||
failp->addStmtsp(new AstPExprClause{flp, false});
|
||||
failp->addStmtsp(decrementVar->cloneTree(false));
|
||||
failp->addStmtsp(setDone());
|
||||
loopp->addStmtsp(new AstIf{
|
||||
flp,
|
||||
new AstLogAnd{flp,
|
||||
new AstLogNot{flp, new AstVarRef{flp, donep, VAccess::READ}},
|
||||
new AstLogNot{flp, lhsp}},
|
||||
failp});
|
||||
}
|
||||
AstDelay* const delayp = new AstDelay{flp, new AstConst{flp, 1}, false};
|
||||
delayp->timeunit(m_modp->timeunit());
|
||||
loopp->addStmtsp(new AstIf{
|
||||
flp, new AstLogNot{flp, new AstVarRef{flp, donep, VAccess::READ}}, delayp});
|
||||
|
||||
// Main assertion block
|
||||
AstBegin* const bodyp = new AstBegin{flp, "", nullptr, true};
|
||||
bodyp->addStmtsp(donep);
|
||||
bodyp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, donep, VAccess::WRITE},
|
||||
new AstConst{flp, AstConst::BitFalse{}}});
|
||||
FileLine* const flp = activep->fileline();
|
||||
bodyp->addStmtsp(
|
||||
new AstAssign{flp, new AstVarRef{flp, activep, VAccess::WRITE},
|
||||
new AstAdd{flp, new AstVarRef{flp, activep, VAccess::READ},
|
||||
new AstConst{flp, 1}}});
|
||||
bodyp->addStmtsp(loopp);
|
||||
|
||||
// Validate assertion condition for each active assert
|
||||
AstVar* const activeCountp = new AstVar{flp, VVarType::BLOCKTEMP, "__VassertCount",
|
||||
nodep->findBasicDType(VBasicDTypeKwd::UINT32)};
|
||||
activeCountp->lifetime(VLifetime::AUTOMATIC_EXPLICIT);
|
||||
|
||||
AstAssign* const initActiveCountp
|
||||
= new AstAssign{flp, new AstVarRef{flp, activeCountp, VAccess::WRITE},
|
||||
new AstVarRef{flp, activep, VAccess::READ}};
|
||||
AstLoop* const finalLoopp = new AstLoop{flp};
|
||||
finalLoopp->addStmtsp(
|
||||
new AstLoopTest{flp, finalLoopp,
|
||||
new AstNeq{flp, new AstVarRef{flp, activeCountp, VAccess::READ},
|
||||
new AstConst{flp, 0}}});
|
||||
finalLoopp->addStmtsp(new AstIf{flp, finalCondp, new AstPExprClause{flp},
|
||||
new AstPExprClause{flp, false}});
|
||||
finalLoopp->addStmtsp(
|
||||
new AstAssign{flp, new AstVarRef{flp, activeCountp, VAccess::WRITE},
|
||||
new AstSub{flp, new AstVarRef{flp, activeCountp, VAccess::READ},
|
||||
new AstConst{flp, 1}}});
|
||||
|
||||
// Final assertion block
|
||||
AstBegin* const finalp = new AstBegin{flp, "", nullptr, true};
|
||||
finalp->addStmtsp(activeCountp);
|
||||
finalp->addStmtsp(initActiveCountp);
|
||||
finalp->addStmtsp(finalLoopp);
|
||||
|
||||
AstPExpr* const pexprp = new AstPExpr{flp, bodyp, finalp, nodep->dtypep()};
|
||||
VL_RESTORER(m_pexprp);
|
||||
VL_RESTORER(m_hasCycleDelay);
|
||||
m_pexprp = pexprp;
|
||||
m_hasCycleDelay = false;
|
||||
iterate(bodyp);
|
||||
iterate(finalp);
|
||||
|
||||
UASSERT_OBJ(!m_hasCycleDelay, nodep,
|
||||
"s_until cycle delay should have been handled by V3AssertNfa");
|
||||
|
||||
nodep->replaceWith(pexprp);
|
||||
VL_DO_DANGLING(pushDeletep(nodep), nodep);
|
||||
return;
|
||||
}
|
||||
|
|
@ -1367,8 +1471,8 @@ private:
|
|||
iterateNull(nodep->disablep());
|
||||
if (!VN_AS(nodep->backp(), NodeCoverOrAssert)->immediate()) {
|
||||
const AstNodeDType* const propDtp = nodep->propp()->dtypep();
|
||||
nodep->propp(new AstSampled{nodep->fileline(), nodep->propp()->unlinkFrBack()});
|
||||
nodep->propp()->dtypeFrom(propDtp);
|
||||
nodep->propp(new AstSampled{nodep->fileline(), nodep->propp()->unlinkFrBack(),
|
||||
propDtp->dtypep()});
|
||||
}
|
||||
iterate(nodep->propp());
|
||||
}
|
||||
|
|
|
|||
|
|
@ -2519,9 +2519,10 @@ class AstSampled final : public AstNodeExpr {
|
|||
// Verilog $sampled
|
||||
// @astgen op1 := exprp : AstNode<AstNodeExpr|AstPropSpec>
|
||||
public:
|
||||
AstSampled(FileLine* fl, AstNode* exprp)
|
||||
AstSampled(FileLine* fl, AstNode* exprp, AstNodeDType* dtypep)
|
||||
: ASTGEN_SUPER_Sampled(fl) {
|
||||
this->exprp(exprp);
|
||||
this->dtypep(dtypep);
|
||||
}
|
||||
ASTGEN_MEMBERS_AstSampled;
|
||||
string emitVerilog() override { return "$sampled(%l)"; }
|
||||
|
|
@ -2906,6 +2907,9 @@ public:
|
|||
string emitVerilog() override { V3ERROR_NA_RETURN(""); }
|
||||
string emitC() override { V3ERROR_NA_RETURN(""); }
|
||||
string emitSimpleOperator() override { V3ERROR_NA_RETURN(""); }
|
||||
string verilogKwd() const override {
|
||||
return (isStrong() ? "s_" : string()) + "until" + (isOverlapping() ? "_with" : "");
|
||||
}
|
||||
bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
|
||||
int instrCount() const override { return widthInstrs(); }
|
||||
bool sameNode(const AstNode* /*samep*/) const override { return true; }
|
||||
|
|
|
|||
|
|
@ -210,7 +210,7 @@ class SliceVisitor final : public VNVisitor {
|
|||
UINFO(9, " cloneSliceSel(" << elements << "," << elemIdx << ") " << nodep);
|
||||
AstNodeExpr* const exprp = VN_AS(snodep->exprp(), NodeExpr);
|
||||
AstNodeExpr* const selp = cloneAndSel(exprp, elements, elemIdx, needPure);
|
||||
return new AstSampled{nodep->fileline(), selp};
|
||||
return new AstSampled{nodep->fileline(), selp, nullptr};
|
||||
} else if (AstExprStmt* const snodep = VN_CAST(nodep, ExprStmt)) {
|
||||
UINFO(9, " cloneExprStmt(" << elements << "," << elemIdx << ") " << nodep);
|
||||
AstNodeExpr* const resultSelp
|
||||
|
|
|
|||
|
|
@ -1714,6 +1714,13 @@ class WidthVisitor final : public VNVisitor {
|
|||
}
|
||||
|
||||
void visit(AstUntil* nodep) override {
|
||||
if (nodep->isStrong()
|
||||
&& (v3Global.opt.timing().isSetFalse() || !v3Global.opt.timing().isSetTrue())) {
|
||||
nodep->v3warn(E_NOTIMING, nodep->verilogKwd() << " requires --timing");
|
||||
nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}});
|
||||
VL_DO_DANGLING(nodep->deleteTree(), nodep);
|
||||
return;
|
||||
}
|
||||
assertAtExpr(nodep);
|
||||
if (m_vup->prelim()) {
|
||||
iterateCheckBool(nodep, "LHS", nodep->lhsp(), BOTH);
|
||||
|
|
|
|||
|
|
@ -4531,7 +4531,7 @@ system_f_or_t_expr_call<nodeExprp>: // IEEE: part of system_tf_call (can be tas
|
|||
| yD_ROSE '(' expr ',' expr ')' { $$ = new AstRose{$1, $3, GRAMMARP->createSenTreeChanged($1, $5)}; }
|
||||
| yD_ROSE_GCLK '(' expr ')' { $$ = new AstRose{$1, $3, GRAMMARP->createGlobalClockSenTree($1)}; }
|
||||
| yD_RTOI '(' expr ')' { $$ = new AstRToIS{$1, $3}; }
|
||||
| yD_SAMPLED '(' expr ')' { $$ = new AstSampled{$1, $3}; }
|
||||
| yD_SAMPLED '(' expr ')' { $$ = new AstSampled{$1, $3, $3->dtypep()}; }
|
||||
| yD_SFORMATF '(' exprDispList ')' { $$ = new AstSFormatF{$1, AstSFormatF::ExprFormat{}, $3, 'd', false}; }
|
||||
| yD_SHORTREALTOBITS '(' expr ')' { $$ = new AstRealToBits{$1, $3}; UNSUPREAL($1); }
|
||||
| yD_SIGNED '(' expr ')' { $$ = new AstSigned{$1, $3}; }
|
||||
|
|
|
|||
|
|
@ -51,4 +51,12 @@
|
|||
: ... note: In instance 't'
|
||||
38 | assert property (@(e) s_eventually 1'h1);
|
||||
| ^~~~~~~~~~~~
|
||||
%Error-NOTIMING: t/t_notiming.v:39:31: s_until requires --timing
|
||||
: ... note: In instance 't'
|
||||
39 | assert property (@(e) 1'h1 s_until 1'h1);
|
||||
| ^~~~~~~
|
||||
%Error-NOTIMING: t/t_notiming.v:40:31: s_until_with requires --timing
|
||||
: ... note: In instance 't'
|
||||
40 | assert property (@(e) 1'h1 s_until_with 1'h1);
|
||||
| ^~~~~~~~~~~~
|
||||
%Error: Exiting due to
|
||||
|
|
|
|||
|
|
@ -36,6 +36,8 @@ module t;
|
|||
s.get();
|
||||
end
|
||||
assert property (@(e) s_eventually 1'h1);
|
||||
assert property (@(e) 1'h1 s_until 1'h1);
|
||||
assert property (@(e) 1'h1 s_until_with 1'h1);
|
||||
endmodule
|
||||
|
||||
`ifdef VERILATOR_TIMING
|
||||
|
|
|
|||
|
|
@ -1,16 +1,16 @@
|
|||
%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:72:14: Logical operator IMPLICATION expects 1 bit on the RHS, but RHS's CMETHODHARD 'at' generates 8 bits.
|
||||
%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:80:14: Logical operator IMPLICATION expects 1 bit on the RHS, but RHS's CMETHODHARD 'at' generates 8 bits.
|
||||
: ... note: In instance 't.ieee'
|
||||
72 | $rose(a) |-> q[0];
|
||||
80 | $rose(a) |-> q[0];
|
||||
| ^~~
|
||||
... For warning description see https://verilator.org/warn/WIDTHTRUNC?v=latest
|
||||
... Use "/* verilator lint_off WIDTHTRUNC */" and lint_on around source to disable this message.
|
||||
%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:77:29: Logical operator SEXPR expects 1 bit on the exprp, but exprp's CMETHODHARD 'at' generates 8 bits.
|
||||
%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:85:29: Logical operator SEXPR expects 1 bit on the exprp, but exprp's CMETHODHARD 'at' generates 8 bits.
|
||||
: ... note: In instance 't.ieee'
|
||||
77 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
|
||||
85 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
|
||||
| ^~
|
||||
%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:98:31: Logical operator SEXPR expects 1 bit on the exprp, but exprp's VARREF 'b' generates 32 bits.
|
||||
: ... note: In instance 't.ieee'
|
||||
98 | assert property (@clk not a ##1 b);
|
||||
%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:106:31: Logical operator SEXPR expects 1 bit on the exprp, but exprp's VARREF 'b' generates 32 bits.
|
||||
: ... note: In instance 't.ieee'
|
||||
106 | assert property (@clk not a ##1 b);
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:47:39: Unsupported: 'until' in complex property expression
|
||||
: ... note: In instance 't'
|
||||
|
|
@ -21,16 +21,32 @@
|
|||
: ... note: In instance 't'
|
||||
49 | assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, 49);
|
||||
| ^~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:51:39: Unsupported: s_until (in property expresion)
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:51:44: Unsupported: s_until (in property expression)
|
||||
: ... note: In instance 't'
|
||||
51 | assert property (@(posedge clk) val s_until !val) $display("[%0t] s_until, fileline:%d", $time, 51);
|
||||
51 | assert property (@(posedge clk) ##1 (val s_until val)) $display("[%0t] s_until in sequence, fileline:%d", $time, 51);
|
||||
| ^~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:53:39: Unsupported: s_until (in property expression)
|
||||
: ... note: In instance 't'
|
||||
53 | assert property (@(posedge clk) val s_until val s_until val) $display("[%0t] nested s_until, fileline:%d", $time, 53);
|
||||
| ^~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:53:39: Unsupported: s_until_with (in property expresion)
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:39: Unsupported: s_until (in property expression)
|
||||
: ... note: In instance 't'
|
||||
53 | assert property (@(posedge clk) val s_until_with val) $display("[%0t] s_until_with, fileline:%d", $time, 53);
|
||||
55 | assert property (@(posedge clk) val s_until (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, 55);
|
||||
| ^~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:57:44: Unsupported: s_until_with (in property expression)
|
||||
: ... note: In instance 't'
|
||||
57 | assert property (@(posedge clk) ##1 (val s_until_with val)) $display("[%0t] s_until_with in sequence, fileline:%d", $time, 57);
|
||||
| ^~~~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:59:39: Unsupported: s_until_with (in property expression)
|
||||
: ... note: In instance 't'
|
||||
59 | assert property (@(posedge clk) val s_until_with val s_until_with val) $display("[%0t] nested s_until_with, fileline:%d", $time, 59);
|
||||
| ^~~~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:40: Unsupported: 'until' in complex property expression
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:61:39: Unsupported: s_until_with (in property expression)
|
||||
: ... note: In instance 't'
|
||||
55 | assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, 55);
|
||||
61 | assert property (@(posedge clk) val s_until_with (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, 61);
|
||||
| ^~~~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:63:40: Unsupported: 'until' in complex property expression
|
||||
: ... note: In instance 't'
|
||||
63 | assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, 63);
|
||||
| ^~~~~
|
||||
%Error: Exiting due to
|
||||
|
|
|
|||
|
|
@ -7,16 +7,32 @@
|
|||
: ... note: In instance 't'
|
||||
49 | assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, 49);
|
||||
| ^~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:51:39: Unsupported: s_until (in property expresion)
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:51:44: Unsupported: s_until (in property expression)
|
||||
: ... note: In instance 't'
|
||||
51 | assert property (@(posedge clk) val s_until !val) $display("[%0t] s_until, fileline:%d", $time, 51);
|
||||
51 | assert property (@(posedge clk) ##1 (val s_until val)) $display("[%0t] s_until in sequence, fileline:%d", $time, 51);
|
||||
| ^~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:53:39: Unsupported: s_until (in property expression)
|
||||
: ... note: In instance 't'
|
||||
53 | assert property (@(posedge clk) val s_until val s_until val) $display("[%0t] nested s_until, fileline:%d", $time, 53);
|
||||
| ^~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:53:39: Unsupported: s_until_with (in property expresion)
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:39: Unsupported: s_until (in property expression)
|
||||
: ... note: In instance 't'
|
||||
53 | assert property (@(posedge clk) val s_until_with val) $display("[%0t] s_until_with, fileline:%d", $time, 53);
|
||||
55 | assert property (@(posedge clk) val s_until (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, 55);
|
||||
| ^~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:57:44: Unsupported: s_until_with (in property expression)
|
||||
: ... note: In instance 't'
|
||||
57 | assert property (@(posedge clk) ##1 (val s_until_with val)) $display("[%0t] s_until_with in sequence, fileline:%d", $time, 57);
|
||||
| ^~~~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:59:39: Unsupported: s_until_with (in property expression)
|
||||
: ... note: In instance 't'
|
||||
59 | assert property (@(posedge clk) val s_until_with val s_until_with val) $display("[%0t] nested s_until_with, fileline:%d", $time, 59);
|
||||
| ^~~~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:40: Unsupported: 'until' in complex property expression
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:61:39: Unsupported: s_until_with (in property expression)
|
||||
: ... note: In instance 't'
|
||||
55 | assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, 55);
|
||||
61 | assert property (@(posedge clk) val s_until_with (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, 61);
|
||||
| ^~~~~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:63:40: Unsupported: 'until' in complex property expression
|
||||
: ... note: In instance 't'
|
||||
63 | assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, 63);
|
||||
| ^~~~~
|
||||
%Error: Exiting due to
|
||||
|
|
|
|||
|
|
@ -48,9 +48,17 @@ module t ( /*AUTOARG*/
|
|||
|
||||
assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, `__LINE__);
|
||||
|
||||
assert property (@(posedge clk) val s_until !val) $display("[%0t] s_until, fileline:%d", $time, `__LINE__);
|
||||
assert property (@(posedge clk) ##1 (val s_until val)) $display("[%0t] s_until in sequence, fileline:%d", $time, `__LINE__);
|
||||
|
||||
assert property (@(posedge clk) val s_until_with val) $display("[%0t] s_until_with, fileline:%d", $time, `__LINE__);
|
||||
assert property (@(posedge clk) val s_until val s_until val) $display("[%0t] nested s_until, fileline:%d", $time, `__LINE__);
|
||||
|
||||
assert property (@(posedge clk) val s_until (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, `__LINE__);
|
||||
|
||||
assert property (@(posedge clk) ##1 (val s_until_with val)) $display("[%0t] s_until_with in sequence, fileline:%d", $time, `__LINE__);
|
||||
|
||||
assert property (@(posedge clk) val s_until_with val s_until_with val) $display("[%0t] nested s_until_with, fileline:%d", $time, `__LINE__);
|
||||
|
||||
assert property (@(posedge clk) val s_until_with (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, `__LINE__);
|
||||
|
||||
assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, `__LINE__);
|
||||
|
||||
|
|
|
|||
|
|
@ -46,6 +46,40 @@ module t ( /*AUTOARG*/
|
|||
results[5].passs++;
|
||||
else results[5].fails++;
|
||||
|
||||
assert property (@(posedge clk) 0 s_until 1)
|
||||
results[6].passs++;
|
||||
else results[6].fails++;
|
||||
|
||||
assert property (@(posedge clk) cyc < 5 s_until cyc >= 5)
|
||||
results[7].passs++;
|
||||
else results[7].fails++;
|
||||
|
||||
assert property (@(posedge clk) cyc % 3 == 0 s_until cyc % 5 == 0)
|
||||
results[8].passs++;
|
||||
else results[8].fails++;
|
||||
|
||||
// Check that s_until accepts immediately when RHS is true, even if LHS is false.
|
||||
assert property (@(posedge clk) cyc % 2 == 0 s_until 1)
|
||||
results[9].passs++;
|
||||
else results[9].fails++;
|
||||
|
||||
// Check that s_until_with requires LHS when RHS is true on the same tick.
|
||||
assert property (@(posedge clk) 0 s_until_with 1)
|
||||
results[10].passs++;
|
||||
else results[10].fails++;
|
||||
|
||||
assert property (@(posedge clk) 1 s_until_with cyc >= 5)
|
||||
results[11].passs++;
|
||||
else results[11].fails++;
|
||||
|
||||
assert property (@(posedge clk) cyc <= 5 s_until_with cyc >= 5)
|
||||
results[12].passs++;
|
||||
else results[12].fails++;
|
||||
|
||||
assert property (@(posedge clk) cyc < 5 s_until_with cyc >= 5)
|
||||
results[13].passs++;
|
||||
else results[13].fails++;
|
||||
|
||||
always @(edge clk) begin
|
||||
++cyc;
|
||||
if (cyc == MAX) begin
|
||||
|
|
@ -54,6 +88,14 @@ module t ( /*AUTOARG*/
|
|||
expected[3] = '{0, 7};
|
||||
expected[4] = '{5, 2};
|
||||
expected[5] = '{2, 5};
|
||||
expected[6] = '{0, 7};
|
||||
expected[7] = '{0, 7};
|
||||
expected[8] = '{5, 2};
|
||||
expected[9] = '{0, 7};
|
||||
expected[10] = '{7, 0};
|
||||
expected[11] = '{0, 7};
|
||||
expected[12] = '{4, 3};
|
||||
expected[13] = '{7, 0};
|
||||
`checkh(results, expected);
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
|
|
|
|||
|
|
@ -52,4 +52,12 @@
|
|||
38 | assert property (@(e) s_eventually 1'h1);
|
||||
| ^~~~~~~~~~~~
|
||||
... For error description see https://verilator.org/warn/NOTIMING?v=latest
|
||||
%Error-NOTIMING: t/t_notiming.v:39:31: s_until requires --timing
|
||||
: ... note: In instance 't'
|
||||
39 | assert property (@(e) 1'h1 s_until 1'h1);
|
||||
| ^~~~~~~
|
||||
%Error-NOTIMING: t/t_notiming.v:40:31: s_until_with requires --timing
|
||||
: ... note: In instance 't'
|
||||
40 | assert property (@(e) 1'h1 s_until_with 1'h1);
|
||||
| ^~~~~~~~~~~~
|
||||
%Error: Exiting due to
|
||||
|
|
|
|||
Loading…
Reference in New Issue