Support `s_eventually` (#7291) (#7508)

This commit is contained in:
Bartłomiej Chmiel 2026-05-04 15:57:03 +02:00 committed by GitHub
parent bc1acc8aa3
commit 4e349971d3
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
44 changed files with 717 additions and 261 deletions

View File

@ -150,6 +150,7 @@ class AssertVisitor final : public VNVisitor {
bool m_inRestrict = false; // True inside restrict assertion
AstNode* m_passsp = nullptr; // Current pass statement
AstNode* m_failsp = nullptr; // Current fail statement
AstFinal* m_finalp = nullptr; // Current final block
// Map from (expression, senTree) to AstAlways that computes delayed values of the expression
std::unordered_map<VNRef<AstNodeExpr>, std::unordered_map<VNRef<AstSenTree>, AstAlways*>>
m_modExpr2Sen2DelayedAlwaysp;
@ -302,6 +303,14 @@ class AssertVisitor final : public VNVisitor {
if (AstPExpr* const pexprp = VN_CAST(propp, PExpr)) {
AstFork* const forkp = new AstFork{nodep->fileline(), VJoinType::JOIN_NONE};
forkp->addForksp(pexprp->bodyp()->unlinkFrBack());
if (AstNodeStmt* const finalp = pexprp->finalp()) {
if (!m_finalp) {
m_finalp = new AstFinal{m_modp->fileline(), finalp->unlinkFrBack()};
m_modp->addStmtsp(m_finalp);
} else {
m_finalp->addStmtsp(finalp->unlinkFrBack());
}
}
VL_DO_DANGLING2(pushDeletep(pexprp), pexprp, propp);
bodyp = forkp;
} else {

View File

@ -67,9 +67,11 @@ private:
V3UniqueNames m_nonConsRepNames{"__VnonConsRep"}; // Nonconsecutive rep name generator
V3UniqueNames m_disableCntNames{"__VdisableCnt"}; // Disable condition counter name generator
V3UniqueNames m_propVarNames{"__Vpropvar"}; // Property-local variable name generator
V3UniqueNames m_activeNames{"__VassertsActive"}; // Active asserts map 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
bool m_hasCycleDelay = false; // True if node has cycle delay beneath
std::vector<AstVarXRef*> m_xrefsp; // list of xrefs that need name fixup
std::vector<AstSequence*> m_seqsToCleanup; // Sequences to clean up after traversal
@ -411,6 +413,7 @@ private:
}
}
void visit(AstDelay* nodep) override {
m_hasCycleDelay = true;
// Only cycle delays are relevant in this stage; also only process once
if (!nodep->isCycleDelay()) {
if (m_inSynchDrive) {
@ -792,6 +795,121 @@ private:
nodep->replaceWith(exprp);
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
static AstAssocArrayDType* getProcessAssocArrayType(FileLine* const flp) {
// Type of __VassertsActive___x[std::process]
AstNodeDType* valp
= v3Global.rootp()->typeTablep()->findBasicDType(flp, VBasicDTypeKwd::BIT);
AstClassRefDType* keyp
= new AstClassRefDType{flp, v3Global.rootp()->stdPackageClassp(), nullptr};
keyp->classOrPackagep(v3Global.rootp()->stdPackageClassp());
v3Global.rootp()->typeTablep()->addTypesp(keyp);
AstAssocArrayDType* const typep = new AstAssocArrayDType{flp, valp, keyp};
typep->dtypep(typep);
v3Global.rootp()->typeTablep()->addTypesp(typep);
return typep;
}
static AstStmtExpr* getProcessAssocArrayDelete(AstVarRef* const refp) {
// Constructs refp.delete(std::process::self()) statement
FileLine* const flp = refp->fileline();
refp->classOrPackagep(v3Global.rootp()->stdPackageClassp());
AstCMethodHard* const deletep = new AstCMethodHard{
flp, refp, VCMethod::ASSOC_ERASE, v3Global.rootp()->stdPackageProcessSelfp(flp)};
deletep->dtypep(refp->findVoidDType());
return new AstStmtExpr{flp, deletep};
}
static AstNodeExpr* getProcessAssocArraySize(AstVarRef* const refp) {
// Constructs refp.size() statement
refp->classOrPackagep(v3Global.rootp()->stdPackageClassp());
AstCMethodHard* const sizep
= new AstCMethodHard{refp->fileline(), refp, VCMethod::ASSOC_SIZE};
sizep->dtypep(refp->findBasicDType(VBasicDTypeKwd::UINT32));
return sizep;
}
void visit(AstSEventually* nodep) override {
UASSERT(v3Global.rootp()->stdPackagep(), "Should be imported");
AstSenTree* const sentreep = newSenTree(nodep);
if (!sentreep->sensesp()) {
VL_DO_DANGLING(pushDeletep(sentreep), sentreep);
nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}});
VL_DO_DANGLING(pushDeletep(nodep), nodep);
return;
}
FileLine* const flp = nodep->fileline();
// Track active assertions
AstVar* const activep = new AstVar{flp, VVarType::MODULETEMP, m_activeNames.get(""),
getProcessAssocArrayType(flp)};
activep->lifetime(VLifetime::STATIC_EXPLICIT);
m_modp->addStmtsp(activep);
// Assertion condition check
AstLoop* const loopp = new AstLoop{flp};
AstNodeExpr* const condp = new AstSampled{flp, nodep->exprp()->unlinkFrBack()};
loopp->addStmtsp(new AstLoopTest{flp, loopp, new AstLogNot{flp, condp}});
loopp->addStmtsp(new AstEventControl{flp, sentreep, nullptr});
// Add assertion to the active set
AstAssocSel* const selp = new AstAssocSel{flp, new AstVarRef{flp, activep, VAccess::WRITE},
v3Global.rootp()->stdPackageProcessSelfp(flp)};
AstAssign* const incrementp = new AstAssign{flp, selp, new AstConst{flp, 1}};
AstPExprClause* const clausep = new AstPExprClause{flp};
AstStmtExpr* const deletep
= getProcessAssocArrayDelete(new AstVarRef{flp, activep, VAccess::WRITE});
// Main assertion block
AstBegin* const bodyp = new AstBegin{flp, "", nullptr, true};
bodyp->addStmtsp(incrementp);
bodyp->addStmtsp(loopp);
bodyp->addStmtsp(clausep);
bodyp->addStmtsp(deletep);
// 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},
getProcessAssocArraySize(new AstVarRef{flp, activep, VAccess::READ})};
AstLoop* const finalLoopp = new AstLoop{flp};
AstIf* const finalBodypCondp
= new AstIf{flp, condp->cloneTreePure(false), new AstPExprClause{flp},
new AstPExprClause{flp, false}};
finalLoopp->addStmtsp(
new AstLoopTest{flp, finalLoopp,
new AstNeq{flp, new AstVarRef{flp, activeCountp, VAccess::READ},
new AstConst{flp, 0}}});
finalLoopp->addStmtsp(finalBodypCondp);
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);
m_pexprp = new AstPExpr{flp, bodyp, finalp, nodep->dtypep()};
VL_RESTORER(m_hasCycleDelay);
m_hasCycleDelay = false;
iterate(bodyp);
iterate(finalp);
if (m_hasCycleDelay) {
nodep->v3warn(E_UNSUPPORTED, "Unsupported: cycle delay in s_eventually");
nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}});
VL_DO_DANGLING(pushDeletep(nodep), nodep);
VL_DO_DANGLING(m_pexprp->deleteTree(), m_pexprp);
return;
}
nodep->replaceWith(m_pexprp);
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
void visit(AstStable* nodep) override {
if (nodep->user1SetOnce()) return;
iterateChildren(nodep);
@ -1272,6 +1390,17 @@ private:
m_pexprp = nodep;
if (m_disablep) {
const AstSampled* sampledp = nullptr;
if (m_disablep->exists([&sampledp](const AstSampled* const sp) {
sampledp = sp;
return true;
})) {
sampledp->v3warn(E_UNSUPPORTED,
"Unsupported: $sampled inside disabled condition of a sequence");
m_disablep = new AstConst{m_disablep->fileline(), AstConst::BitFalse{}};
// always a copy is used, so remove it now
pushDeletep(m_disablep);
}
FileLine* const flp = nodep->fileline();
// Add counter which counts times the condition turned true
AstVar* const disableCntp

View File

@ -1898,10 +1898,18 @@ public:
class AstPExpr final : public AstNodeExpr {
// Property expression
// @astgen op1 := bodyp : AstBegin
// @astgen op2 := finalp : Optional[AstNodeStmt]
public:
explicit AstPExpr(FileLine* fl, AstBegin* bodyp, AstNodeDType* dtypep)
: ASTGEN_SUPER_PExpr(fl) {
this->bodyp(bodyp);
this->finalp(nullptr);
this->dtypep(dtypep);
}
explicit AstPExpr(FileLine* fl, AstBegin* bodyp, AstNodeStmt* finalp, AstNodeDType* dtypep)
: ASTGEN_SUPER_PExpr(fl) {
this->bodyp(bodyp);
this->finalp(finalp);
this->dtypep(dtypep);
}
ASTGEN_MEMBERS_AstPExpr;
@ -2226,6 +2234,19 @@ public:
bool unbounded() const { return m_unbounded; }
bool isMultiCycleSva() const override { return true; }
};
class AstSEventually final : public AstNodeExpr {
// s_eventually
// @astgen op1 := exprp : AstNodeExpr
public:
explicit AstSEventually(FileLine* fl, AstNodeExpr* exprp)
: ASTGEN_SUPER_SEventually(fl) {
this->exprp(exprp);
}
ASTGEN_MEMBERS_AstSEventually;
string emitVerilog() override { V3ERROR_NA_RETURN(""); }
string emitC() override { V3ERROR_NA_RETURN(""); }
bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
};
class AstSExpr final : public AstNodeExpr {
// Sequence expression
// @astgen op1 := preExprp: Optional[AstNodeExpr]

View File

@ -1263,6 +1263,7 @@ class AstNetlist final : public AstNode {
// @astgen ptr := m_constPoolp : AstConstPool // Reference to constant pool, for faster lookup
// @astgen ptr := m_dollarUnitPkgp : Optional[AstPackage] // $unit
// @astgen ptr := m_stdPackagep : Optional[AstPackage] // SystemVerilog std package
// @astgen ptr := m_stdPackageClassp : Optional[AstClass] // SystemVerilog std process class
// @astgen ptr := m_evalp : Optional[AstCFunc] // The '_eval' function
// @astgen ptr := m_evalNbap : Optional[AstCFunc] // The '_eval__nba' function
// @astgen ptr := m_dpiExportTriggerp : Optional[AstVarScope] // DPI export trigger variable
@ -1304,6 +1305,9 @@ public:
void nbaEventTriggerp(AstVarScope* const varScopep) { m_nbaEventTriggerp = varScopep; }
void stdPackagep(AstPackage* const packagep) { m_stdPackagep = packagep; }
AstPackage* stdPackagep() const { return m_stdPackagep; }
void stdPackageClassp(AstClass* const classp) { m_stdPackageClassp = classp; }
AstClass* stdPackageClassp() const { return m_stdPackageClassp; }
AstFuncRef* stdPackageProcessSelfp(FileLine*) const;
AstTopScope* topScopep() const { return m_topScopep; }
void createTopScope(AstScope* scopep);
VTimescale timeunit() const { return m_timeunit; }

View File

@ -2703,6 +2703,18 @@ AstVarScope* AstNetlist::stlFirstIterationp() {
AstVarScope* const vscp = m_stlFirstIterationp;
return vscp;
}
AstFuncRef* AstNetlist::stdPackageProcessSelfp(FileLine* flp) const {
UASSERT(v3Global.rootp()->stdPackageClassp(), "'std' should be imported");
AstFunc* selfp = nullptr;
for (AstNode* itemp = v3Global.rootp()->stdPackageClassp()->stmtsp(); itemp;
itemp = itemp->nextp()) {
if (itemp->name() == "self") selfp = VN_AS(itemp, Func);
}
UASSERT(selfp, "'std::process::self' should be found");
AstFuncRef* const processSelfp = new AstFuncRef{flp, selfp};
processSelfp->classOrPackagep(v3Global.rootp()->stdPackageClassp());
return processSelfp;
}
void AstNodeModule::dump(std::ostream& str) const {
this->AstNode::dump(str);
str << " L" << level();

View File

@ -157,6 +157,7 @@ void V3Global::removeStd() {
UINFO(3, "Removing unused std:: package");
if (AstNodeModule* stdp = v3Global.rootp()->stdPackagep()) {
v3Global.rootp()->stdPackagep(nullptr);
v3Global.rootp()->stdPackageClassp(nullptr);
VL_DO_DANGLING(stdp->unlinkFrBack()->deleteTree(), stdp);
}
}

View File

@ -161,12 +161,6 @@ class LinkJumpVisitor final : public VNVisitor {
if (AstNode* const refp = nodep->op4p()) addPrefixToBlocksRecurse(prefix, refp);
if (AstNode* const refp = nodep->nextp()) addPrefixToBlocksRecurse(prefix, refp);
}
static AstNode* getMemberp(const AstNodeModule* const nodep, const std::string& name) {
for (AstNode* itemp = nodep->stmtsp(); itemp; itemp = itemp->nextp()) {
if (itemp->name() == name) return itemp;
}
return nullptr;
}
bool existsBlockAbove(const std::string& name) const {
for (const AstNodeBlock* const stackp : vlstd::reverse_view(m_blockStack)) {
if (stackp->name() == name) return true;
@ -175,14 +169,11 @@ class LinkJumpVisitor final : public VNVisitor {
}
static AstStmtExpr* getQueuePushProcessSelfp(AstVarRef* const queueRefp) {
// Constructs queue.push_back(std::process::self()) statement
FileLine* const fl = queueRefp->fileline();
AstClass* const processClassp
= VN_AS(getMemberp(v3Global.rootp()->stdPackagep(), "process"), Class);
AstFunc* const selfMethodp = VN_AS(getMemberp(processClassp, "self"), Func);
AstFuncRef* const processSelfp = new AstFuncRef{fl, selfMethodp};
processSelfp->classOrPackagep(processClassp);
FileLine* const flp = queueRefp->fileline();
return new AstStmtExpr{
fl, new AstMethodCall{fl, queueRefp, "push_back", new AstArg{fl, "", processSelfp}}};
flp,
new AstMethodCall{flp, queueRefp, "push_back",
new AstArg{flp, "", v3Global.rootp()->stdPackageProcessSelfp(flp)}}};
}
static AstStmtExpr* getQueuePushProcessSelfp(FileLine* const fl, AstVar* const processQueuep) {
AstPackage* const topPkgp = v3Global.rootp()->dollarUnitPkgAddp();
@ -192,13 +183,18 @@ class LinkJumpVisitor final : public VNVisitor {
}
static AstStmtExpr* getQueueKillStmtp(FileLine* const fl, AstVar* const processQueuep) {
AstPackage* const topPkgp = v3Global.rootp()->dollarUnitPkgAddp();
AstClass* const processClassp
= VN_AS(getMemberp(v3Global.rootp()->stdPackagep(), "process"), Class);
AstVarRef* const queueRefp = new AstVarRef{fl, topPkgp, processQueuep, VAccess::READWRITE};
AstTaskRef* const killQueueCall
= new AstTaskRef{fl, VN_AS(getMemberp(processClassp, "killQueue"), Task),
new AstArg{fl, "", queueRefp}};
killQueueCall->classOrPackagep(processClassp);
AstTaskRef* killQueueCall = nullptr;
for (AstNode* itemp = v3Global.rootp()->stdPackageClassp()->stmtsp(); itemp;
itemp = itemp->nextp()) {
if (itemp->name() == "killQueue") {
killQueueCall
= new AstTaskRef{fl, VN_AS(itemp, Task), new AstArg{fl, "", queueRefp}};
break;
}
}
UASSERT(killQueueCall, "Should be found");
killQueueCall->classOrPackagep(v3Global.rootp()->stdPackageClassp());
return new AstStmtExpr{fl, killQueueCall};
}
static void prependStmtsp(AstNodeFTask* const nodep, AstNode* const stmtp) {
@ -238,12 +234,11 @@ class LinkJumpVisitor final : public VNVisitor {
}
AstVar* getProcessQueuep(AstNode* const nodep, FileLine* const fl) {
AstPackage* const topPkgp = v3Global.rootp()->dollarUnitPkgAddp();
AstClass* const processClassp
= VN_AS(getMemberp(v3Global.rootp()->stdPackagep(), "process"), Class);
AstVar* const processQueuep = new AstVar{
fl, VVarType::VAR, m_queueNames.get(nodep->name()), VFlagChildDType{},
new AstQueueDType{fl, VFlagChildDType{},
new AstClassRefDType{fl, processClassp, nullptr}, nullptr}};
new AstQueueDType{
fl, VFlagChildDType{},
new AstClassRefDType{fl, v3Global.rootp()->stdPackageClassp(), nullptr}, nullptr}};
processQueuep->lifetime(VLifetime::STATIC_EXPLICIT);
processQueuep->processQueue(true);
topPkgp->addStmtsp(processQueuep);

View File

@ -80,6 +80,15 @@ void V3ParseImp::importIfInStd(FileLine* fileline, const string& id, bool doImpo
if (doImport) {
AstPackageImport* const impp = new AstPackageImport{stdpkgp->fileline(), stdpkgp, "*"};
unitPackage(stdpkgp->fileline())->addStmtsp(impp);
for (AstNode* itemp = v3Global.rootp()->stdPackagep()->stmtsp(); itemp;
itemp = itemp->nextp()) {
if (itemp->name() == "process") {
v3Global.rootp()->stdPackageClassp(VN_AS(itemp, Class));
UASSERT_OBJ(v3Global.rootp()->stdPackageClassp(), v3Global.rootp(),
"'std' package class should be found");
break;
}
}
}
}
}

View File

@ -1728,6 +1728,18 @@ class WidthVisitor final : public VNVisitor {
if (nodep->seedp()) iterateCheckSigned32(nodep, "seed", nodep->seedp(), BOTH);
}
}
void visit(AstSEventually* nodep) override {
if (v3Global.opt.timing().isSetFalse() || !v3Global.opt.timing().isSetTrue()) {
nodep->v3warn(E_NOTIMING, "s_eventually requires --timing");
nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::WidthedValue{}, 1, 0});
VL_DO_DANGLING(nodep->deleteTree(), nodep);
return;
}
if (m_vup->prelim()) {
iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH);
nodep->dtypeSetBit();
}
}
void visit(AstSGotoRep* nodep) override {
assertAtExpr(nodep);
if (m_vup->prelim()) {

View File

@ -6778,7 +6778,10 @@ pexpr<nodeExprp>: // IEEE: property_expr (The name pexpr is important as regex
| yS_ALWAYS pexpr
{ $$ = new AstPropAlways{$1, $2, new AstUnbounded{$1}, new AstUnbounded{$1}, true}; }
| yS_EVENTUALLY pexpr
{ $$ = $2; BBUNSUP($1, "Unsupported: s_eventually (in property expression)"); }
{
$$ = new AstSEventually{$1, $2};
PARSEP->importIfInStd($1, "process", true);
}
| yS_EVENTUALLY anyrange pexpr %prec yS_EVENTUALLY
{ $$ = $3; BBUNSUP($1, "Unsupported: s_eventually[] (in property expression)"); DEL($2); }
| yEVENTUALLY anyrange pexpr %prec yS_EVENTUALLY

View File

@ -1,4 +1,4 @@
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"(E)","stdPackagep":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"UNLINKED","stlFirstIterationp":"UNLINKED",
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"(E)","stdPackagep":"UNLINKED","stdPackageClassp":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"UNLINKED","stlFirstIterationp":"UNLINKED",
"modulesp": [
{"type":"MODULE","name":"t","addr":"(F)","loc":"d,67:8,67:9","origName":"t","verilogName":"t","level":1,"timeunit":"1ps","inlinesp": [],
"stmtsp": [

View File

@ -1,4 +1,4 @@
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"UNLINKED","stlFirstIterationp":"UNLINKED",
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","stdPackageClassp":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"UNLINKED","stlFirstIterationp":"UNLINKED",
"modulesp": [
{"type":"MODULE","name":"test","addr":"(E)","loc":"d,21:8,21:12","origName":"test","verilogName":"test","level":1,"timeunit":"1ps","inlinesp": [],
"stmtsp": [

View File

@ -1,4 +1,4 @@
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"UNLINKED","stlFirstIterationp":"UNLINKED",
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","stdPackageClassp":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"UNLINKED","stlFirstIterationp":"UNLINKED",
"modulesp": [
{"type":"MODULE","name":"t","addr":"(E)","loc":"d,7:8,7:9","origName":"t","verilogName":"t","level":1,"timeunit":"1ps","inlinesp": [],
"stmtsp": [

View File

@ -1,4 +1,4 @@
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"(E)","stlFirstIterationp":"UNLINKED",
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","stdPackageClassp":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"(E)","stlFirstIterationp":"UNLINKED",
"modulesp": [
{"type":"MODULE","name":"$root","addr":"(F)","loc":"d,7:8,7:9","origName":"$root","verilogName":"$root","level":1,"modPublic":true,"timeunit":"1ps","inlinesp": [],
"stmtsp": [

View File

@ -1,4 +1,4 @@
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"(E)","stlFirstIterationp":"UNLINKED",
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","stdPackageClassp":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"(E)","stlFirstIterationp":"UNLINKED",
"modulesp": [
{"type":"MODULE","name":"$root","addr":"(F)","loc":"d,11:8,11:11","origName":"$root","verilogName":"$root","level":1,"modPublic":true,"timeunit":"1ps","inlinesp": [],
"stmtsp": [

View File

@ -1,4 +1,4 @@
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"(E)","stlFirstIterationp":"UNLINKED",
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","stdPackageClassp":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"(E)","stlFirstIterationp":"UNLINKED",
"modulesp": [
{"type":"MODULE","name":"$root","addr":"(F)","loc":"d,11:8,11:11","origName":"$root","verilogName":"$root","level":1,"modPublic":true,"timeunit":"1ps","inlinesp": [],
"stmtsp": [

View File

@ -1,4 +1,4 @@
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"(E)","stlFirstIterationp":"UNLINKED",
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","stdPackageClassp":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"(E)","stlFirstIterationp":"UNLINKED",
"modulesp": [
{"type":"MODULE","name":"$root","addr":"(F)","loc":"d,7:8,7:21","origName":"$root","verilogName":"$root","level":1,"modPublic":true,"timeunit":"1ps","inlinesp": [],
"stmtsp": [

View File

@ -1,4 +1,4 @@
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"UNLINKED","stlFirstIterationp":"UNLINKED",
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","stdPackageClassp":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"UNLINKED","stlFirstIterationp":"UNLINKED",
"modulesp": [
{"type":"MODULE","name":"m","addr":"(E)","loc":"d,7:8,7:9","origName":"m","verilogName":"m","level":1,"timeunit":"1ps","inlinesp": [],
"stmtsp": [

View File

@ -1,4 +1,4 @@
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"UNLINKED","stlFirstIterationp":"UNLINKED",
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","stdPackageClassp":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"UNLINKED","stlFirstIterationp":"UNLINKED",
"modulesp": [
{"type":"MODULE","name":"top","addr":"(E)","loc":"d,7:8,7:11","origName":"top","verilogName":"top","level":1,"timeunit":"1ps","inlinesp": [],
"stmtsp": [

View File

@ -1,4 +1,4 @@
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"UNLINKED","stlFirstIterationp":"UNLINKED",
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","stdPackageClassp":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"UNLINKED","stlFirstIterationp":"UNLINKED",
"modulesp": [
{"type":"MODULE","name":"m","addr":"(E)","loc":"d,12:8,12:9","origName":"m","verilogName":"m","level":1,"timeunit":"1ps","inlinesp": [],
"stmtsp": [

View File

@ -31,20 +31,24 @@
: ... note: In instance 't'
27 | initial #2 $stop;
| ^
%Error-NOTIMING: t/t_notiming.v:33:8: mailbox::put() requires --timing
: ... note: In instance 't'
33 | m.put(i);
| ^~~
%Error-NOTIMING: t/t_notiming.v:34:8: mailbox::get() requires --timing
: ... note: In instance 't'
34 | m.get(i);
| ^~~
%Error-NOTIMING: t/t_notiming.v:35:8: mailbox::peek() requires --timing
: ... note: In instance 't'
35 | m.peek(i);
| ^~~~
%Error-NOTIMING: t/t_notiming.v:36:8: semaphore::get() requires --timing
: ... note: In instance 't'
36 | s.get();
| ^~~
%Error-NOTIMING: t/t_notiming.v:33:10: mailbox::put() requires --timing
: ... note: In instance 't'
33 | m.put(i);
| ^~~
%Error-NOTIMING: t/t_notiming.v:34:10: mailbox::get() requires --timing
: ... note: In instance 't'
34 | m.get(i);
| ^~~
%Error-NOTIMING: t/t_notiming.v:35:10: mailbox::peek() requires --timing
: ... note: In instance 't'
35 | m.peek(i);
| ^~~~
%Error-NOTIMING: t/t_notiming.v:36:10: semaphore::get() requires --timing
: ... note: In instance 't'
36 | s.get();
| ^~~
%Error-NOTIMING: t/t_notiming.v:38:26: s_eventually requires --timing
: ... note: In instance 't'
38 | assert property (@(e) s_eventually 1'h1);
| ^~~~~~~~~~~~
%Error: Exiting due to

View File

@ -26,15 +26,16 @@ module t;
initial #1 ->e;
initial #2 $stop; // timeout
mailbox#(int) m = new;
semaphore s = new;
initial begin
int i;
m.put(i);
m.get(i);
m.peek(i);
s.get();
end
mailbox#(int) m = new;
semaphore s = new;
initial begin
int i;
m.put(i);
m.get(i);
m.peek(i);
s.get();
end
assert property (@(e) s_eventually 1'h1);
endmodule
`ifdef VERILATOR_TIMING

View File

@ -0,0 +1,6 @@
%Error-UNSUPPORTED: t/t_property_disable_iff_unsup.v:20:48: Unsupported: $sampled inside disabled condition of a sequence
: ... note: In instance 't'
20 | assert property (@(posedge clk) disable iff ($sampled(val)) s_eventually 1);
| ^~~~~~~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error: Exiting due to

View File

@ -0,0 +1,16 @@
#!/usr/bin/env python3
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# 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-FileCopyrightText: 2025 Wilson Snyder
# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
import vltest_bootstrap
test.scenarios('vlt')
test.lint(fails=True, verilator_flags2=['--timing'], expect_filename=test.golden_filename)
test.passes()

View File

@ -0,0 +1,21 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain.
// SPDX-FileCopyrightText: 2026 Antmicro
// SPDX-License-Identifier: CC0-1.0
module t ( /*AUTOARG*/
// Inputs
clk
);
input clk;
bit val;
always @(posedge clk) begin
$write("*-* All Finished *-*\n");
$finish;
end
assert property (@(posedge clk) disable iff ($sampled(val)) s_eventually 1);
endmodule

View File

@ -11,7 +11,7 @@ import vltest_bootstrap
test.scenarios('simulator')
test.compile()
test.compile(timing_loop=True, verilator_flags2=['--timing'])
test.execute()

View File

@ -1,13 +1,18 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain.
// SPDX-FileCopyrightText: 2025 Wilson Snyder
// SPDX-FileCopyrightText: 2026 Wilson Snyder
// SPDX-License-Identifier: CC0-1.0
// verilog_format: off
`define stop $stop
`define checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0x exp=%0x (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0);
`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
`define PROPERTY_CHECK(msg) \
$display("[%0t] stmt, %s, fileline:%d", $time, msg, `__LINE__); \
else \
$display("[%0t] else, %s, fileline:%d", $time, msg, `__LINE__); \
// verilog_format: on
module t (
@ -53,7 +58,6 @@ module t (
always @(negedge clk) begin
if (cyc == 10) -> test.e;
end
endmodule
module Test(input clk,
@ -82,4 +86,5 @@ module Test(input clk,
assert property ( @e not a )
else count_hits_event = count_hits_event + 1;
endmodule

View File

@ -0,0 +1,68 @@
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:26:13: Unsupported: strong (in property expression)
26 | strong(a);
| ^
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:30:11: Unsupported: weak (in property expression)
30 | weak(a);
| ^
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:58:7: Unsupported: nexttime (in property expression)
58 | nexttime a;
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:62:7: Unsupported: nexttime[] (in property expression)
62 | nexttime [2] a;
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:66:7: Unsupported: s_nexttime (in property expression)
66 | s_nexttime a;
| ^~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:70:7: Unsupported: s_nexttime[] (in property expression)
70 | s_nexttime [2] a;
| ^~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:74:7: Unsupported: nexttime (in property expression)
74 | nexttime always a;
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:78:7: Unsupported: nexttime[] (in property expression)
78 | nexttime [2] always a;
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:82:7: Unsupported: nexttime[] (in property expression)
82 | nexttime [2] always a;
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:86:7: Unsupported: nexttime (in property expression)
86 | nexttime s_eventually a;
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:90:16: Unsupported: s_eventually[] (in property expression)
90 | nexttime s_eventually [2:$] always a;
| ^~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:90:7: Unsupported: nexttime (in property expression)
90 | nexttime s_eventually [2:$] always a;
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:94:17: Unsupported: accept_on (in property expression)
94 | accept_on (a) b;
| ^
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:98:22: Unsupported: sync_accept_on (in property expression)
98 | sync_accept_on (a) b;
| ^
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:102:17: Unsupported: reject_on (in property expression)
102 | reject_on (a) b;
| ^
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:106:22: Unsupported: sync_reject_on (in property expression)
106 | sync_reject_on (a) b;
| ^
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:109:27: Unsupported: property argument data type
109 | property p_arg_propery(property inprop);
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:112:27: Unsupported: sequence argument data type
112 | property p_arg_seqence(sequence inseq);
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:117:7: Unsupported: property case expression
117 | case (a) endcase
| ^~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:120:7: Unsupported: property case expression
120 | case (a) default: b; endcase
| ^~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:123:7: Unsupported: property case expression
123 | if (a) b
| ^~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:126:7: Unsupported: property case expression
126 | if (a) b else c
| ^~
%Error: Exiting due to

View File

@ -0,0 +1,20 @@
#!/usr/bin/env python3
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# 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-FileCopyrightText: 2025 Wilson Snyder
# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
import vltest_bootstrap
test.scenarios('vlt')
test.top_filename = "t/t_property_pexpr_unsup.v"
test.lint(expect_filename=test.golden_filename,
verilator_flags2=['-DPARSING_TIME', '--assert', '--timing', '--error-limit 1000'],
fails=True)
test.passes()

View File

@ -1,71 +1,26 @@
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:23:11: Unsupported: strong (in property expression)
23 | strong(a);
| ^
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:130:22: Unsupported: Unclocked assertion
: ... note: In instance 't'
130 | assert property ((s_eventually a) implies (s_eventually a));
| ^~~~~~~~~~~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:27:9: Unsupported: weak (in property expression)
27 | weak(a);
| ^
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:51:5: Unsupported: nexttime (in property expression)
51 | nexttime a;
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:55:5: Unsupported: nexttime[] (in property expression)
55 | nexttime [2] a;
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:59:5: Unsupported: s_nexttime (in property expression)
59 | s_nexttime a;
| ^~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:63:5: Unsupported: s_nexttime[] (in property expression)
63 | s_nexttime [2] a;
| ^~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:67:5: Unsupported: nexttime (in property expression)
67 | nexttime always a;
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:71:5: Unsupported: nexttime[] (in property expression)
71 | nexttime [2] always a;
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:75:5: Unsupported: nexttime[] (in property expression)
75 | nexttime [2] always a;
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:79:14: Unsupported: s_eventually (in property expression)
79 | nexttime s_eventually a;
| ^~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:79:5: Unsupported: nexttime (in property expression)
79 | nexttime s_eventually a;
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:83:14: Unsupported: s_eventually[] (in property expression)
83 | nexttime s_eventually [2:$] always a;
| ^~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:83:5: Unsupported: nexttime (in property expression)
83 | nexttime s_eventually [2:$] always a;
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:87:15: Unsupported: accept_on (in property expression)
87 | accept_on (a) b;
| ^
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:91:20: Unsupported: sync_accept_on (in property expression)
91 | sync_accept_on (a) b;
| ^
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:95:15: Unsupported: reject_on (in property expression)
95 | reject_on (a) b;
| ^
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:99:20: Unsupported: sync_reject_on (in property expression)
99 | sync_reject_on (a) b;
| ^
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:102:26: Unsupported: property argument data type
102 | property p_arg_propery(property inprop);
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:105:26: Unsupported: sequence argument data type
105 | property p_arg_seqence(sequence inseq);
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:110:5: Unsupported: property case expression
110 | case (a) endcase
| ^~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:113:5: Unsupported: property case expression
113 | case (a) default: b; endcase
| ^~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:116:5: Unsupported: property case expression
116 | if (a) b
| ^~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:119:5: Unsupported: property case expression
119 | if (a) b else c
| ^~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:130:47: Unsupported: Unclocked assertion
: ... note: In instance 't'
130 | assert property ((s_eventually a) implies (s_eventually a));
| ^~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:130:4: Unsupported: Unclocked assertion
: ... note: In instance 't'
130 | assert property ((s_eventually a) implies (s_eventually a));
| ^~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:132:22: Unsupported: Unclocked assertion
: ... note: In instance 't'
132 | assert property ((s_eventually a) iff (s_eventually a));
| ^~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:132:43: Unsupported: Unclocked assertion
: ... note: In instance 't'
132 | assert property ((s_eventually a) iff (s_eventually a));
| ^~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:132:4: Unsupported: Unclocked assertion
: ... note: In instance 't'
132 | assert property ((s_eventually a) iff (s_eventually a));
| ^~~~~~
%Error: Exiting due to

View File

@ -12,7 +12,7 @@ import vltest_bootstrap
test.scenarios('vlt')
test.compile(expect_filename=test.golden_filename,
verilator_flags2=['--assert --error-limit 1000'],
verilator_flags2=['--timing', '--error-limit 1000'],
fails=test.vlt_all)
test.passes()

View File

@ -1,128 +1,140 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain.
// SPDX-FileCopyrightText: 2023 Wilson Snyder
// SPDX-FileCopyrightText: 2026 Wilson Snyder
// SPDX-License-Identifier: CC0-1.0
module t (
input clk
);
module t (/*AUTOARG*/
// Inputs
clk
);
int a;
int b;
int c;
int cyc = 0;
input clk;
bit a;
bit b;
bit c;
int cyc = 0;
always @(posedge clk) begin
cyc <= cyc + 1;
end
always @(posedge clk) begin
cyc <= cyc + 1;
end
// NOTE this grammar hasn't been checked with other simulators,
// is here just to avoid uncovered code lines in the grammar.
property p_strong;
strong(a);
endproperty
`ifdef PARSING_TIME
// NOTE this grammar hasn't been checked with other simulators,
// is here just to avoid uncovered code lines in the grammar.
property p_strong;
strong(a);
endproperty
property p_weak;
weak(a);
endproperty
property p_weak;
weak(a);
endproperty
property p_suntil;
a s_until b;
endproperty
property p_until;
a until b;
endproperty
property p_untilwith;
a until_with b;
endproperty
property p_suntil;
a s_until b;
endproperty
property p_suntilwith;
a s_until_with b;
endproperty
property p_untilwith;
a until_with b;
endproperty
property p_poundminuspound1;
a #-# b;
endproperty
property p_suntilwith;
a s_until_with b;
endproperty
property p_poundeqpound;
a #=# b;
endproperty
property p_poundminuspound1;
a #-# b;
endproperty
property p_nexttime;
nexttime a;
endproperty
property p_poundeqpound;
a #=# b;
endproperty
property p_nexttime2;
nexttime [2] a;
endproperty
property p_nexttime;
nexttime a;
endproperty
property p_snexttime;
s_nexttime a;
endproperty
property p_nexttime2;
nexttime [2] a;
endproperty
property p_snexttime2;
s_nexttime [2] a;
endproperty
property p_snexttime;
s_nexttime a;
endproperty
property p_nexttime_always;
nexttime always a;
endproperty
property p_snexttime2;
s_nexttime [2] a;
endproperty
property p_nexttime_always2;
nexttime [2] always a;
endproperty
property p_nexttime_always;
nexttime always a;
endproperty
property p_nexttime_eventually2;
nexttime [2] always a;
endproperty
property p_nexttime_always2;
nexttime [2] always a;
endproperty
property p_nexttime_seventually;
nexttime s_eventually a;
endproperty
property p_nexttime_eventually2;
nexttime [2] always a;
endproperty
property p_nexttime_seventually2;
nexttime s_eventually [2:$] always a;
endproperty
property p_nexttime_seventually;
nexttime s_eventually a;
endproperty
property p_accepton;
accept_on (a) b;
endproperty
property p_nexttime_seventually2;
nexttime s_eventually [2:$] always a;
endproperty
property p_syncaccepton;
sync_accept_on (a) b;
endproperty
property p_accepton;
accept_on (a) b;
endproperty
property p_rejecton;
reject_on (a) b;
endproperty
property p_syncaccepton;
sync_accept_on (a) b;
endproperty
property p_syncrejecton;
sync_reject_on (a) b;
endproperty
property p_rejecton;
reject_on (a) b;
endproperty
property p_arg_propery(property inprop);
inprop;
endproperty
property p_arg_seqence(sequence inseq);
inseq;
endproperty
property p_syncrejecton;
sync_reject_on (a) b;
endproperty
property p_case_1;
case (a) endcase
endproperty
property p_case_2;
case (a) default: b; endcase
endproperty
property p_if;
if (a) b
endproperty
property p_ifelse;
if (a) b else c
endproperty
property p_arg_propery(property inprop);
inprop;
endproperty
property p_arg_seqence(sequence inseq);
inseq;
endproperty
always @(posedge clk) begin
if (cyc == 10) begin
$write("*-* All Finished *-*\n");
$finish;
end
end
property p_case_1;
case (a) endcase
endproperty
property p_case_2;
case (a) default: b; endcase
endproperty
property p_if;
if (a) b
endproperty
property p_ifelse;
if (a) b else c
endproperty
`endif
assert property ((s_eventually a) implies (s_eventually a));
assert property ((s_eventually a) iff (s_eventually a));
always @(posedge clk) begin
if (cyc == 10) begin
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule

View File

@ -0,0 +1,4 @@
[4] stmt, s_eventually before final
*-* All Finished *-*
[5] else, s_eventually during final
[5] else, s_eventually after final

View File

@ -0,0 +1,18 @@
#!/usr/bin/env python3
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# 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-FileCopyrightText: 2026 Wilson Snyder
# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
import vltest_bootstrap
test.scenarios('simulator')
test.compile(timing_loop=True, verilator_flags2=['--timing'])
test.execute(expect_filename=test.golden_filename)
test.passes()

View File

@ -0,0 +1,34 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain.
// SPDX-FileCopyrightText: 2026 Antmicro
// SPDX-License-Identifier: CC0-1.0
// verilog_format: off
`define PROPERTY_CHECK(msg) \
$display("[%0t] stmt, %s", $time, msg); \
else \
$display("[%0t] else, %s", $time, msg); \
// verilog_format: on
module t;
bit clk = 0;
initial forever #1 clk = ~clk;
localparam MAX = 4;
integer cyc = 1;
assert property (@(negedge clk) disable iff (cyc < MAX - 1) s_eventually (cyc == MAX - 1)) `PROPERTY_CHECK("s_eventually before final")
assert property (@(negedge clk) disable iff (cyc < MAX - 1) s_eventually (cyc == MAX)) `PROPERTY_CHECK("s_eventually during final")
assert property (@(negedge clk) disable iff (cyc < MAX - 1) s_eventually (cyc == MAX + 1)) `PROPERTY_CHECK("s_eventually after final")
always @(posedge clk) begin
++cyc;
if (cyc == MAX) begin
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule

View File

@ -0,0 +1,18 @@
#!/usr/bin/env python3
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# 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-FileCopyrightText: 2026 Wilson Snyder
# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
import vltest_bootstrap
test.scenarios('simulator')
test.compile(timing_loop=True, verilator_flags2=['--timing'])
test.execute()
test.passes()

View File

@ -0,0 +1,34 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain.
// SPDX-FileCopyrightText: 2026 Antmicro
// SPDX-License-Identifier: CC0-1.0
// verilog_format: off
`define PROPERTY_CHECK(msg) \
$display("[%0t] stmt, %s", $time, msg); \
else \
$display("[%0t] else, %s", $time, msg); \
// verilog_format: on
module t;
bit clk = 0;
initial forever #1 clk = ~clk;
localparam MAX = 1000;
integer cyc = 0;
integer passed = 0;
assert property (@(negedge clk) s_eventually 1)
++passed;
always @(posedge clk) begin
++cyc;
if (cyc == MAX) begin
$display("%d", passed);
if (passed != 999) $stop;
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule

View File

@ -0,0 +1,14 @@
%Error-UNSUPPORTED: t/t_property_s_eventually_unsup.v:14:20: Unsupported: Unclocked assertion
: ... note: In instance 't'
14 | assert property (s_eventually ##1 1);
| ^~~~~~~~~~~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_property_s_eventually_unsup.v:14:3: Unsupported: Unclocked assertion
: ... note: In instance 't'
14 | assert property (s_eventually ##1 1);
| ^~~~~~
%Error-UNSUPPORTED: t/t_property_s_eventually_unsup.v:15:35: Unsupported: cycle delay in s_eventually
: ... note: In instance 't'
15 | assert property (@(negedge clk) s_eventually ##1 1);
| ^~~~~~~~~~~~
%Error: Exiting due to

View File

@ -0,0 +1,16 @@
#!/usr/bin/env python3
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# 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-FileCopyrightText: 2026 Wilson Snyder
# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
import vltest_bootstrap
test.scenarios('simulator')
test.lint(expect_filename=test.golden_filename, verilator_flags2=['--timing'], fails=True)
test.passes()

View File

@ -0,0 +1,24 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain.
// SPDX-FileCopyrightText: 2026 Antmicro
// SPDX-License-Identifier: CC0-1.0
module t;
bit clk = 0;
initial forever #1 clk = ~clk;
localparam MAX = 3;
integer cyc = 1;
assert property (s_eventually ##1 1);
assert property (@(negedge clk) s_eventually ##1 1);
always @(posedge clk) begin
++cyc;
if (cyc == MAX) begin
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule

View File

@ -11,8 +11,6 @@ import vltest_bootstrap
test.scenarios('vlt')
test.lint(fails=True,
verilator_flags2=['--assert', '--timing'],
expect_filename=test.golden_filename)
test.lint(fails=True, verilator_flags2=['--timing'], expect_filename=test.golden_filename)
test.passes()

View File

@ -11,22 +11,10 @@
%Error-UNSUPPORTED: t/t_property_unsup.v:90:50: Unsupported: eventually[] (in property expression)
90 | assert property ((eventually[0: 1] a) implies (eventually[0: 1] a));
| ^~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_unsup.v:92:21: Unsupported: s_eventually (in property expression)
92 | assert property ((s_eventually a) implies (s_eventually a));
| ^~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_unsup.v:92:46: Unsupported: s_eventually (in property expression)
92 | assert property ((s_eventually a) implies (s_eventually a));
| ^~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_unsup.v:112:21: Unsupported: eventually[] (in property expression)
112 | assert property ((eventually[0: 1] a) iff (eventually[0: 1] a));
| ^~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_unsup.v:112:46: Unsupported: eventually[] (in property expression)
112 | assert property ((eventually[0: 1] a) iff (eventually[0: 1] a));
| ^~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_unsup.v:114:21: Unsupported: s_eventually (in property expression)
114 | assert property ((s_eventually a) iff (s_eventually a));
| ^~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_unsup.v:114:42: Unsupported: s_eventually (in property expression)
114 | assert property ((s_eventually a) iff (s_eventually a));
| ^~~~~~~~~~~~
%Error: Exiting due to

View File

@ -31,20 +31,25 @@
: ... note: In instance 't'
27 | initial #2 $stop;
| ^
%Error-NEEDTIMINGOPT: t/t_notiming.v:33:8: Use --timing or --no-timing to specify how mailbox::put() should be handled
: ... note: In instance 't'
33 | m.put(i);
| ^~~
%Error-NEEDTIMINGOPT: t/t_notiming.v:34:8: Use --timing or --no-timing to specify how mailbox::get() should be handled
: ... note: In instance 't'
34 | m.get(i);
| ^~~
%Error-NEEDTIMINGOPT: t/t_notiming.v:35:8: Use --timing or --no-timing to specify how mailbox::peek() should be handled
: ... note: In instance 't'
35 | m.peek(i);
| ^~~~
%Error-NEEDTIMINGOPT: t/t_notiming.v:36:8: Use --timing or --no-timing to specify how semaphore::get() should be handled
: ... note: In instance 't'
36 | s.get();
| ^~~
%Error-NEEDTIMINGOPT: t/t_notiming.v:33:10: Use --timing or --no-timing to specify how mailbox::put() should be handled
: ... note: In instance 't'
33 | m.put(i);
| ^~~
%Error-NEEDTIMINGOPT: t/t_notiming.v:34:10: Use --timing or --no-timing to specify how mailbox::get() should be handled
: ... note: In instance 't'
34 | m.get(i);
| ^~~
%Error-NEEDTIMINGOPT: t/t_notiming.v:35:10: Use --timing or --no-timing to specify how mailbox::peek() should be handled
: ... note: In instance 't'
35 | m.peek(i);
| ^~~~
%Error-NEEDTIMINGOPT: t/t_notiming.v:36:10: Use --timing or --no-timing to specify how semaphore::get() should be handled
: ... note: In instance 't'
36 | s.get();
| ^~~
%Error-NOTIMING: t/t_notiming.v:38:26: s_eventually requires --timing
: ... note: In instance 't'
38 | assert property (@(e) s_eventually 1'h1);
| ^~~~~~~~~~~~
... For error description see https://verilator.org/warn/NOTIMING?v=latest
%Error: Exiting due to

View File

@ -1,4 +1,4 @@
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"UNLINKED","stlFirstIterationp":"UNLINKED",
{"type":"NETLIST","name":"$root","addr":"(B)","loc":"a,0:0,0:0","timeunit":"1ps","timeprecision":"1ps","typeTablep":"(C)","constPoolp":"(D)","dollarUnitPkgp":"UNLINKED","stdPackagep":"UNLINKED","stdPackageClassp":"UNLINKED","evalp":"UNLINKED","evalNbap":"UNLINKED","dpiExportTriggerp":"UNLINKED","delaySchedulerp":"UNLINKED","nbaEventp":"UNLINKED","nbaEventTriggerp":"UNLINKED","topScopep":"UNLINKED","stlFirstIterationp":"UNLINKED",
"modulesp": [
{"type":"MODULE","name":"mh2","addr":"(E)","loc":"d,18:8,18:11","origName":"mh2","verilogName":"mh2","level":1,"timeunit":"1ps","inlinesp": [],
"stmtsp": [