Support named properties (#3667)

This commit is contained in:
Ryszard Rozak 2022-11-01 23:53:47 +01:00 committed by GitHub
parent 0b0b642241
commit bac98df46b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
25 changed files with 594 additions and 72 deletions

View File

@ -15,6 +15,7 @@
//*************************************************************************
// Pre steps:
// Attach clocks to each assertion
// Substitute property references by property body (IEEE Std 1800-2012, section 16.12.1).
//*************************************************************************
#include "config_build.h"
@ -24,6 +25,7 @@
#include "V3Ast.h"
#include "V3Global.h"
#include "V3Task.h"
VL_DEFINE_DEBUG_FUNCTIONS;
@ -67,6 +69,72 @@ private:
m_senip = nullptr;
m_disablep = nullptr;
}
AstPropSpec* getPropertyExprp(const AstProperty* const propp) {
// The only statements possible in AstProperty are AstPropSpec (body)
// and AstVar (arguments).
AstNode* propExprp = propp->stmtsp();
while (VN_IS(propExprp, Var)) propExprp = propExprp->nextp();
return VN_CAST(propExprp, PropSpec);
}
void replaceVarRefsWithExprRecurse(AstNode* const nodep, const AstVar* varp,
AstNode* const exprp) {
if (!nodep) return;
if (const AstVarRef* varrefp = VN_CAST(nodep, VarRef)) {
if (varp == varrefp->varp()) nodep->replaceWith(exprp->cloneTree(false));
}
replaceVarRefsWithExprRecurse(nodep->op1p(), varp, exprp);
replaceVarRefsWithExprRecurse(nodep->op2p(), varp, exprp);
replaceVarRefsWithExprRecurse(nodep->op3p(), varp, exprp);
replaceVarRefsWithExprRecurse(nodep->op4p(), varp, exprp);
}
AstPropSpec* substitutePropertyCall(AstPropSpec* nodep) {
if (AstFuncRef* const funcrefp = VN_CAST(nodep->propp(), FuncRef)) {
if (AstProperty* const propp = VN_CAST(funcrefp->taskp(), Property)) {
AstPropSpec* propExprp = getPropertyExprp(propp);
// Substitute inner property call befory copying in order to not doing the same for
// each call of outer property call.
propExprp = substitutePropertyCall(propExprp);
// Clone subtree after substitution. It is needed, because property might be called
// multiple times with different arguments.
propExprp = propExprp->cloneTree(false);
// Substitute formal arguments with actual arguments
const V3TaskConnects tconnects = V3Task::taskConnects(funcrefp, propp->stmtsp());
for (const auto& tconnect : tconnects) {
const AstVar* const portp = tconnect.first;
AstArg* const argp = tconnect.second;
AstNode* const pinp = argp->exprp()->unlinkFrBack();
replaceVarRefsWithExprRecurse(propExprp, portp, pinp);
}
// Handle case with 2 disable iff statement (IEEE 1800-2017 16.12.1)
if (nodep->disablep() && propExprp->disablep()) {
nodep->v3error("disable iff expression before property call and in its "
"body is not legal");
}
// If disable iff is in outer property, move it to inner
if (nodep->disablep()) {
AstNode* const disablep = nodep->disablep()->unlinkFrBack();
propExprp->disablep(disablep);
}
if (nodep->sensesp() && propExprp->sensesp()) {
nodep->v3warn(E_UNSUPPORTED,
"Unsupported: Clock event before property call and in its body");
pushDeletep(propExprp->sensesp()->unlinkFrBack());
}
// If clock event is in outer property, move it to inner
if (nodep->sensesp()) {
AstSenItem* const sensesp = nodep->sensesp();
sensesp->unlinkFrBack();
propExprp->sensesp(sensesp);
}
// Now substitute property reference with property body
nodep->replaceWith(propExprp);
return propExprp;
}
}
return nodep;
}
// VISITORS
//========== Statements
@ -162,7 +230,8 @@ private:
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
void visit(AstPropClocked* nodep) override {
void visit(AstPropSpec* nodep) override {
nodep = substitutePropertyCall(nodep);
// No need to iterate the body, once replace will get iterated
iterateAndNextNull(nodep->sensesp());
if (m_senip)
@ -189,6 +258,11 @@ private:
// Reset defaults
m_seniDefaultp = nullptr;
}
void visit(AstProperty* nodep) override {
// The body will be visited when will be substituted in place of property reference
// (AstFuncRef)
VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep);
}
void visit(AstNode* nodep) override { iterateChildren(nodep); }
public:

View File

@ -453,6 +453,8 @@ public:
TIME,
// Closer to a class type, but limited usage
STRING,
// Property / Sequence argument type
UNTYPED,
// Internal types for mid-steps
SCOPEPTR,
CHARPTR,
@ -485,6 +487,7 @@ public:
"shortint",
"time",
"string",
"untyped",
"VerilatedScope*",
"char*",
"VlMTaskState",
@ -501,11 +504,12 @@ public:
}
const char* dpiType() const {
static const char* const names[]
= {"%E-unk", "svBit", "char", "void*", "char",
"int", "%E-integer", "svLogic", "long long", "double",
"short", "%E-time", "const char*", "dpiScope", "const char*",
"%E-mtaskstate", "%E-triggervec", "%E-dly-sched", "%E-trig-sched", "%E-dyn-sched",
"%E-fork", "IData", "QData", "%E-logic-implct", " MAX"};
= {"%E-unk", "svBit", "char", "void*", "char",
"int", "%E-integer", "svLogic", "long long", "double",
"short", "%E-time", "const char*", "%E-untyped", "dpiScope",
"const char*", "%E-mtaskstate", "%E-triggervec", "%E-dly-sched", "%E-trig-sched",
"%E-dyn-sched", "%E-fork", "IData", "QData", "%E-logic-implct",
" MAX"};
return names[m_e];
}
static void selfTest() {
@ -582,7 +586,7 @@ public:
return (m_e == EVENT || m_e == STRING || m_e == SCOPEPTR || m_e == CHARPTR
|| m_e == MTASKSTATE || m_e == TRIGGERVEC || m_e == DELAY_SCHEDULER
|| m_e == TRIGGER_SCHEDULER || m_e == DYNAMIC_TRIGGER_SCHEDULER || m_e == FORK_SYNC
|| m_e == DOUBLE);
|| m_e == DOUBLE || m_e == UNTYPED);
}
bool isDouble() const VL_MT_SAFE { return m_e == DOUBLE; }
bool isEvent() const { return m_e == EVENT; }

View File

@ -465,6 +465,7 @@ public:
int right() const { return littleEndian() ? hi() : lo(); }
inline bool littleEndian() const;
bool implicit() const { return keyword() == VBasicDTypeKwd::LOGIC_IMPLICIT; }
bool untyped() const { return keyword() == VBasicDTypeKwd::UNTYPED; }
VNumRange declRange() const { return isRanged() ? VNumRange{left(), right()} : VNumRange{}; }
void cvtRangeConst(); // Convert to smaller representation
bool isCompound() const override { return isString(); }

View File

@ -1593,7 +1593,7 @@ public:
return pragType() == static_cast<const AstPragma*>(samep)->pragType();
}
};
class AstPropClocked final : public AstNode {
class AstPropSpec final : public AstNode {
// A clocked property
// Parents: ASSERT|COVER (property)
// Children: SENITEM, Properties
@ -1601,13 +1601,13 @@ class AstPropClocked final : public AstNode {
// @astgen op2 := disablep : Optional[AstNode]
// @astgen op3 := propp : AstNode
public:
AstPropClocked(FileLine* fl, AstSenItem* sensesp, AstNode* disablep, AstNode* propp)
: ASTGEN_SUPER_PropClocked(fl) {
AstPropSpec(FileLine* fl, AstSenItem* sensesp, AstNode* disablep, AstNode* propp)
: ASTGEN_SUPER_PropSpec(fl) {
this->sensesp(sensesp);
this->disablep(disablep);
this->propp(propp);
}
ASTGEN_MEMBERS_AstPropClocked;
ASTGEN_MEMBERS_AstPropSpec;
bool hasDType() const override {
return true;
} // Used under Cover, which expects a bool child
@ -2433,6 +2433,14 @@ public:
ASTGEN_MEMBERS_AstFunc;
bool hasDType() const override { return true; }
};
class AstProperty final : public AstNodeFTask {
// A property inside a module
public:
AstProperty(FileLine* fl, const string& name, AstNode* stmtp)
: ASTGEN_SUPER_Property(fl, name, stmtp) {}
ASTGEN_MEMBERS_AstProperty;
bool hasDType() const override { return true; }
};
class AstTask final : public AstNodeFTask {
// A task inside a module
public:

View File

@ -195,7 +195,7 @@ private:
void visit(AstLogEq* nodep) override { unsupported_visit(nodep); }
void visit(AstLogIf* nodep) override { unsupported_visit(nodep); }
void visit(AstNodeCond* nodep) override { unsupported_visit(nodep); }
void visit(AstPropClocked* nodep) override { unsupported_visit(nodep); }
void visit(AstPropSpec* nodep) override { unsupported_visit(nodep); }
void prepost_visit(AstNodeTriop* nodep) {
// Check if we are underneath a statement
if (!m_insStmtp) {

View File

@ -169,7 +169,14 @@ AstVar* V3ParseGrammar::createVariable(FileLine* fileline, const string& name,
dtypep = new AstBasicDType(fileline, VBasicDTypeKwd::DOUBLE);
}
if (!dtypep) { // Created implicitly
dtypep = new AstBasicDType(fileline, LOGIC_IMPLICIT);
if (m_insideProperty) {
if (m_typedPropertyPort) {
fileline->v3warn(E_UNSUPPORTED, "Untyped property port following a typed port");
}
dtypep = new AstBasicDType{fileline, VBasicDTypeKwd::UNTYPED};
} else {
dtypep = new AstBasicDType{fileline, LOGIC_IMPLICIT};
}
} else { // May make new variables with same type, so clone
dtypep = dtypep->cloneTree(false);
}

View File

@ -4027,7 +4027,7 @@ private:
return times;
}
void visit(AstPropClocked* nodep) override {
void visit(AstPropSpec* nodep) override {
if (m_vup->prelim()) { // First stage evaluation
iterateCheckBool(nodep, "Property", nodep->propp(), BOTH);
userIterateAndNext(nodep->sensesp(), nullptr);
@ -4940,8 +4940,13 @@ private:
m_funcp = VN_AS(nodep, Func);
UASSERT_OBJ(m_funcp, nodep, "FTask with function variable, but isn't a function");
nodep->dtypeFrom(nodep->fvarp()); // Which will get it from fvarp()->dtypep()
} else if (VN_IS(nodep, Property)) {
nodep->dtypeSetBit();
}
userIterateChildren(nodep, nullptr);
WidthVP* vup = nullptr;
if (VN_IS(nodep, Property)) vup = WidthVP(SELF, BOTH).p();
userIterateChildren(nodep, vup);
nodep->didWidth(true);
nodep->doingWidth(false);
m_funcp = nullptr;
@ -4951,6 +4956,34 @@ private:
// func
}
}
void visit(AstProperty* nodep) override {
if (nodep->didWidth()) return;
if (nodep->doingWidth()) {
UINFO(5, "Recursive property call: " << nodep);
nodep->v3warn(E_UNSUPPORTED,
"Unsupported: Recursive property call: " << nodep->prettyNameQ());
nodep->recursive(true);
nodep->didWidth(true);
return;
}
nodep->doingWidth(true);
m_ftaskp = nodep;
// Property call will be replaced by property body in V3AssertPre. Property body has bit
// dtype, so set it here too
nodep->dtypeSetBit();
for (AstNode* propStmtp = nodep->stmtsp(); propStmtp; propStmtp = propStmtp->nextp()) {
if (VN_IS(propStmtp, Var)) {
userIterate(propStmtp, nullptr);
} else if (VN_IS(propStmtp, PropSpec)) {
iterateCheckSizedSelf(nodep, "PropSpec", propStmtp, SELF, BOTH);
} else {
propStmtp->v3fatal("Invalid statement under AstProperty");
}
}
nodep->didWidth(true);
nodep->doingWidth(false);
m_ftaskp = nullptr;
}
void visit(AstReturn* nodep) override {
// IEEE: Assignment-like context
assertAtStatement(nodep);
@ -5718,6 +5751,7 @@ private:
UASSERT_OBJ(nodep->dtypep(), nodep,
"Under node " << nodep->prettyTypeName()
<< " has no dtype?? Missing Visitor func?");
if (expDTypep->basicp()->untyped() || nodep->dtypep()->basicp()->untyped()) return false;
UASSERT_OBJ(nodep->width() != 0, nodep,
"Under node " << nodep->prettyTypeName()
<< " has no expected width?? Missing Visitor func?");

View File

@ -598,7 +598,7 @@ vnum {vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
"unique0" { FL; return yUNIQUE0; }
"until" { ERROR_RSVD_WORD("SystemVerilog 2009"); }
"until_with" { ERROR_RSVD_WORD("SystemVerilog 2009"); }
"untyped" { ERROR_RSVD_WORD("SystemVerilog 2009"); }
"untyped" { FL; return yUNTYPED; }
"weak" { ERROR_RSVD_WORD("SystemVerilog 2009"); }
}

View File

@ -93,6 +93,8 @@ public:
string m_instModule; // Name of module referenced for instantiations
AstPin* m_instParamp = nullptr; // Parameters for instantiations
bool m_tracingParse = true; // Tracing disable for parser
bool m_insideProperty = false; // Is inside property declaration
bool m_typedPropertyPort = false; // True if typed property port occured on port lists
int m_pinNum = -1; // Pin number currently parsing
std::stack<int> m_pinStack; // Queue of pin numbers being parsed
@ -719,7 +721,7 @@ BISONPRE_VERSION(3.7,%define api.header.include {"V3ParseBison.h"})
%token<fl> yUNSIGNED "unsigned"
//UNSUP %token<fl> yUNTIL "until"
//UNSUP %token<fl> yUNTIL_WITH "until_with"
//UNSUP %token<fl> yUNTYPED "untyped"
%token<fl> yUNTYPED "untyped"
%token<fl> yVAR "var"
%token<fl> yVECTORED "vectored"
%token<fl> yVIRTUAL__CLASS "virtual-then-class"
@ -1182,7 +1184,7 @@ package_or_generate_item_declaration<nodep>: // ==IEEE: package_or_generate_i
// // local_parameter_declaration under parameter_declaration
| parameter_declaration ';' { $$ = $1; }
//UNSUP covergroup_declaration { $$ = $1; }
//UNSUP assertion_item_declaration { $$ = $1; }
| assertion_item_declaration { $$ = $1; }
| ';' { $$ = nullptr; }
;
@ -5308,11 +5310,11 @@ clocking_declaration<nodep>: // IEEE: clocking_declaration (INCOMPLE
//************************************************
// Asserts
//UNSUPassertion_item_declaration: // ==IEEE: assertion_item_declaration
//UNSUP property_declaration { $$ = $1; }
assertion_item_declaration<nodep>: // ==IEEE: assertion_item_declaration
property_declaration { $$ = $1; }
//UNSUP | sequence_declaration { $$ = $1; }
//UNSUP | let_declaration { $$ = $1; }
//UNSUP ;
;
assertion_item<nodep>: // ==IEEE: assertion_item
concurrent_assertion_item { $$ = $1; }
@ -5411,66 +5413,75 @@ elseStmtBlock<nodep>: // Part of concurrent_assertion_statement
| yELSE stmtBlock { $$ = $2; }
;
//UNSUPproperty_declaration<nodep>: // ==IEEE: property_declaration
//UNSUP property_declarationFront property_port_listE ';' property_declarationBody
//UNSUP yENDPROPERTY endLabelE
//UNSUP { SYMP->popScope($$); }
//UNSUP ;
property_declaration<nodeFTaskp>: // ==IEEE: property_declaration
property_declarationFront property_port_listE ';' property_declarationBody
yENDPROPERTY endLabelE
{ $$ = $1;
$$->addStmtsp($2);
$$->addStmtsp($4);
SYMP->popScope($$);
GRAMMARP->endLabel($<fl>6, $$, $6);
GRAMMARP->m_insideProperty = false;
GRAMMARP->m_typedPropertyPort = false; }
;
//UNSUPproperty_declarationFront<nodep>: // IEEE: part of property_declaration
//UNSUP yPROPERTY idAny/*property_identifier*/
//UNSUP { SYMP->pushNew($$); }
//UNSUP ;
property_declarationFront<nodeFTaskp>: // IEEE: part of property_declaration
yPROPERTY idAny/*property_identifier*/
{ $$ = new AstProperty{$1, *$2, nullptr};
GRAMMARP->m_insideProperty = true;
SYMP->pushNewUnderNodeOrCurrent($$, nullptr); }
;
//UNSUPproperty_port_listE<nodep>: // IEEE: [ ( [ property_port_list ] ) ]
//UNSUP /* empty */ { $$ = nullptr; }
//UNSUP | '(' {VARRESET_LIST(""); VARIO("input"); } property_port_list ')'
//UNSUP { VARRESET_NONLIST(""); }
//UNSUP ;
property_port_listE<nodep>: // IEEE: [ ( [ property_port_list ] ) ]
/* empty */ { $$ = nullptr; }
| '(' property_port_list ')' { $$ = $2; }
;
//UNSUPproperty_port_list<nodep>: // ==IEEE: property_port_list
//UNSUP property_port_item { $$ = $1; }
//UNSUP | property_port_list ',' property_port_item { }
//UNSUP ;
property_port_list<nodep>: // ==IEEE: property_port_list
property_port_item { $$ = $1; }
| property_port_list ',' property_port_item { $$ = addNextNull($1, $3); }
;
//UNSUPproperty_port_item<nodep>: // IEEE: property_port_item/sequence_port_item
property_port_item<nodep>: // IEEE: property_port_item/sequence_port_item
//UNSUP // // Merged in sequence_port_item
//UNSUP // // IEEE: property_lvar_port_direction ::= yINPUT
//UNSUP // // prop IEEE: [ yLOCAL [ yINPUT ] ] property_formal_type
//UNSUP // // id {variable_dimension} [ '=' property_actual_arg ]
//UNSUP // // seq IEEE: [ yLOCAL [ sequence_lvar_port_direction ] ] sequence_formal_type
//UNSUP // // id {variable_dimension} [ '=' sequence_actual_arg ]
//UNSUP property_port_itemFront property_port_itemAssignment { }
//UNSUP ;
property_port_itemFront property_port_itemAssignment { $$ = $2; }
;
//UNSUPproperty_port_itemFront: // IEEE: part of property_port_item/sequence_port_item
//UNSUP property_port_itemDirE property_formal_typeNoDt { VARDTYPE($2); }
property_port_itemFront: // IEEE: part of property_port_item/sequence_port_item
property_port_itemDirE property_formal_typeNoDt { VARDTYPE($2); }
//UNSUP // // data_type_or_implicit
//UNSUP | property_port_itemDirE data_type { VARDTYPE($2); }
| property_port_itemDirE data_type
{ VARDTYPE($2); GRAMMARP->m_typedPropertyPort = true; }
//UNSUP | property_port_itemDirE yVAR data_type { VARDTYPE($3); }
//UNSUP | property_port_itemDirE yVAR implicit_typeE { VARDTYPE($3); }
//UNSUP | property_port_itemDirE signingE rangeList { VARDTYPE(SPACED($2,$3)); }
//UNSUP | property_port_itemDirE /*implicit*/ { /*VARDTYPE-same*/ }
//UNSUP ;
| property_port_itemDirE implicit_typeE { VARDTYPE($2); }
;
//UNSUPproperty_port_itemAssignment<nodep>: // IEEE: part of property_port_item/sequence_port_item/checker_port_direction
//UNSUP portSig variable_dimensionListE { VARDONE($<fl>1, $1, $2, ""); PINNUMINC(); }
property_port_itemAssignment<nodep>: // IEEE: part of property_port_item/sequence_port_item/checker_port_direction
id variable_dimensionListE { $$ = VARDONEA($<fl>1, *$1, $2, nullptr); }
//UNSUP | portSig variable_dimensionListE '=' property_actual_arg
//UNSUP { VARDONE($<fl>1, $1, $2, $4); PINNUMINC(); }
//UNSUP ;
;
//UNSUPproperty_port_itemDirE:
//UNSUP /* empty */ { $$ = nullptr; }
//UNSUP | yLOCAL__ETC { }
//UNSUP | yLOCAL__ETC port_direction { }
//UNSUP ;
property_port_itemDirE:
/* empty */ { GRAMMARP->m_pinAnsi = true; VARIO(INPUT); }
//UNSUP | yLOCAL__ETC { GRAMMARP->m_pinAnsi = true; VARIO(INPUT); }
//UNSUP | yLOCAL__ETC yINPUT { GRAMMARP->m_pinAnsi = true; VARIO(INPUT); }
;
//UNSUPproperty_declarationBody<nodep>: // IEEE: part of property_declaration
property_declarationBody<nodep>: // IEEE: part of property_declaration
//UNSUP assertion_variable_declarationList property_statement_spec { }
//UNSUP // // IEEE-2012: Incorectly hasyCOVER ySEQUENCE then property_spec here.
//UNSUP // // Fixed in IEEE 1800-2017
//UNSUP | property_statement_spec { $$ = $1; }
//UNSUP ;
property_spec { $$ = $1; }
| property_spec ';' { $$ = $1; }
;
//UNSUPassertion_variable_declarationList: // IEEE: part of assertion_variable_declaration
//UNSUP assertion_variable_declaration { $$ = $1; }
@ -5498,19 +5509,19 @@ elseStmtBlock<nodep>: // Part of concurrent_assertion_statement
//UNSUP property_port_listE { $$ = $1; }
//UNSUP ;
//UNSUPproperty_formal_typeNoDt<nodep>: // IEEE: property_formal_type (w/o implicit)
//UNSUP sequence_formal_typeNoDt { $$ = $1; }
property_formal_typeNoDt<nodeDTypep>: // IEEE: property_formal_type (w/o implicit)
sequence_formal_typeNoDt { $$ = $1; }
//UNSUP | yPROPERTY { }
//UNSUP ;
;
//UNSUPsequence_formal_typeNoDt<nodep>: // ==IEEE: sequence_formal_type (w/o data_type_or_implicit)
//UNSUP // // IEEE: data_type_or_implicit
//UNSUP // // implicit expanded where used
sequence_formal_typeNoDt<nodeDTypep>: // ==IEEE: sequence_formal_type (w/o data_type_or_implicit)
// // IEEE: data_type_or_implicit
// // implicit expanded where used
//UNSUP ySEQUENCE { }
//UNSUP // // IEEE-2009: yEVENT
//UNSUP // // already part of data_type. Removed in 1800-2012.
//UNSUP | yUNTYPED { }
//UNSUP ;
// // IEEE-2009: yEVENT
// // already part of data_type. Removed in 1800-2012.
yUNTYPED { $$ = nullptr; GRAMMARP->m_typedPropertyPort = false; }
;
//UNSUPsequence_declarationBody<nodep>: // IEEE: part of sequence_declaration
//UNSUP // // 1800-2012 makes ';' optional
@ -5524,11 +5535,11 @@ property_spec<nodep>: // IEEE: property_spec
//UNSUP: This rule has been super-specialized to what is supported now
//UNSUP remove below
'@' '(' senitemEdge ')' yDISABLE yIFF '(' expr ')' pexpr
{ $$ = new AstPropClocked($1, $3, $8, $10); }
| '@' '(' senitemEdge ')' pexpr { $$ = new AstPropClocked($1, $3, nullptr, $5); }
{ $$ = new AstPropSpec{$1, $3, $8, $10}; }
| '@' '(' senitemEdge ')' pexpr { $$ = new AstPropSpec{$1, $3, nullptr, $5}; }
//UNSUP remove above
| yDISABLE yIFF '(' expr ')' pexpr { $$ = new AstPropClocked($4->fileline(), nullptr, $4, $6); }
| pexpr { $$ = new AstPropClocked($1->fileline(), nullptr, nullptr, $1); }
| yDISABLE yIFF '(' expr ')' pexpr { $$ = new AstPropSpec{$4->fileline(), nullptr, $4, $6}; }
| pexpr { $$ = new AstPropSpec{$1->fileline(), nullptr, nullptr, $1}; }
;
//UNSUPproperty_statement_spec<nodep>: // ==IEEE: property_statement_spec

View File

@ -0,0 +1,5 @@
%Error-UNSUPPORTED: t/t_assert_clock_event_unsup.v:26:7: Unsupported: Clock event before property call and in its body
26 | @(negedge clk)
| ^
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error: Exiting due to

View File

@ -0,0 +1,20 @@
#!/usr/bin/env perl
if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; }
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# Copyright 2022 by Antmicro Ltd. 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
scenarios(vlt => 1);
compile(
expect_filename=>$Self->{golden_filename},
verilator_flags2=> ['--assert'],
fails => 1,
);
ok(1);
1;

View File

@ -0,0 +1,37 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain, for
// any use, without warranty, 2022 by Antmicro Ltd.
// SPDX-License-Identifier: CC0-1.0
module t (/*AUTOARG*/
clk
);
input clk;
int cyc = 0;
logic val = 0;
always @(posedge clk) begin
cyc <= cyc + 1;
val = ~val;
end
property check(int cyc_mod_2, logic expected);
@(posedge clk)
cyc % 2 == cyc_mod_2 |=> val == expected;
endproperty
property check_if_1(int cyc_mod_2);
@(negedge clk)
check(cyc_mod_2, 1);
endproperty
assert property(check_if_1(1))
else begin
// Assertion should fail
$write("*-* All Finished *-*\n");
$finish;
end
endmodule

View File

@ -0,0 +1,5 @@
%Error: t/t_assert_disable_bad.v:27:38: disable iff expression before property call and in its body is not legal
: ... In instance t
27 | assert property (disable iff (val == 0) check(1, 1));
| ^~
%Error: Exiting due to

View File

@ -0,0 +1,20 @@
#!/usr/bin/env perl
if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; }
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# Copyright 2022 by Antmicro Ltd. 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
scenarios(vlt => 1);
compile(
expect_filename=>$Self->{golden_filename},
verilator_flags2=> ['--assert'],
fails => 1,
);
ok(1);
1;

View File

@ -0,0 +1,28 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain, for
// any use, without warranty, 2022 by Antmicro Ltd.
// SPDX-License-Identifier: CC0-1.0
module t (/*AUTOARG*/
clk
);
input clk;
int cyc = 0;
logic val = 0;
always @(posedge clk) begin
cyc <= cyc + 1;
val = ~val;
end
property check(int cyc_mod_2, logic expected);
@(posedge clk)
disable iff (cyc == 0) cyc % 2 == cyc_mod_2 |=> val == expected;
endproperty
// Test should fail due to duplicated disable iff statements
// (IEEE Std 1800-2012, section 16.12.1).
assert property (disable iff (val == 0) check(1, 1));
endmodule

View File

@ -0,0 +1,22 @@
#!/usr/bin/env perl
if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; }
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# Copyright 2022 by Antmicro Ltd. 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
scenarios(simulator => 1);
compile(
verilator_flags2 => ['--assert'],
);
execute(
check_finished => 1,
);
ok(1);
1;

View File

@ -0,0 +1,66 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain, for
// any use, without warranty, 2022 by Antmicro Ltd.
// SPDX-License-Identifier: CC0-1.0
module t (/*AUTOARG*/
clk
);
input clk;
int cyc = 0;
logic val = 0;
always @(posedge clk) begin
cyc <= cyc + 1;
val = ~val;
end
property check(int cyc_mod_2, logic expected);
@(posedge clk)
cyc % 2 == cyc_mod_2 |=> val == expected;
endproperty
property check_if_1(int cyc_mod_2);
check(cyc_mod_2, 1);
endproperty
property check_if_gt_5(int cyc);
@(posedge clk)
cyc > 5;
endproperty
property pass_assertion(int cyc);
disable iff (cyc <= 10)
cyc > 10;
endproperty
int expected_fails = 0;
assert property(check(0, 1))
else begin
// Assertion should pass
$display("Assert failed, but shouldn't");
$stop;
end
assert property(check(1, 1))
else begin
// Assertion should fail
expected_fails += 1;
end
assert property(check_if_1(1))
else begin
// Assertion should fail
expected_fails += 1;
end
assert property(disable iff (cyc < 5) check_if_gt_5(cyc + 1));
assert property(@(posedge clk) pass_assertion(cyc));
always @(posedge clk) begin
if (expected_fails == 2) begin
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule

View File

@ -0,0 +1,22 @@
#!/usr/bin/env perl
if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; }
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# Copyright 2022 by Antmicro Ltd. 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
scenarios(simulator => 1);
compile(
verilator_flags2 => ['--assert'],
);
execute(
check_finished => 1,
);
ok(1);
1;

View File

@ -0,0 +1,38 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain, for
// any use, without warranty, 2022 by Antmicro Ltd.
// SPDX-License-Identifier: CC0-1.0
module t (/*AUTOARG*/
clk
);
input clk;
int cyc = 0;
logic [4:0] val = 0;
always @(posedge clk) begin
cyc <= cyc + 1;
val = ~val;
end
property check(cyc_mod_2, untyped expected);
@(posedge clk)
cyc % 2 == cyc_mod_2 |=> val == expected;
endproperty
assert property(check(0, 5'b11111))
else begin
// Assertion should pass
$display("Assert failed, but shouldn't");
$stop;
end
always @(posedge clk) begin
if (cyc == 10) begin
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule

View File

@ -0,0 +1,5 @@
%Error-UNSUPPORTED: t/t_assert_property_untyped_unsup.v:20:52: Untyped property port following a typed port
20 | property check(cyc_mod_2, logic [4:0] expected, arg3, untyped arg4, arg5);
| ^~~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error: Exiting due to

View File

@ -0,0 +1,20 @@
#!/usr/bin/env perl
if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; }
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# Copyright 2022 by Antmicro Ltd. 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
scenarios(vlt => 1);
compile(
expect_filename=>$Self->{golden_filename},
verilator_flags2=> ['--assert'],
fails => 1,
);
ok(1);
1;

View File

@ -0,0 +1,33 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain, for
// any use, without warranty, 2022 by Antmicro Ltd.
// SPDX-License-Identifier: CC0-1.0
module t (/*AUTOARG*/
clk
);
input clk;
int cyc = 0;
logic [4:0] val = 0;
always @(posedge clk) begin
cyc <= cyc + 1;
val = ~val;
end
property check(cyc_mod_2, logic [4:0] expected, arg3, untyped arg4, arg5);
@(posedge clk)
cyc % 2 == cyc_mod_2 |=> val == expected;
endproperty
assert property(check(0, 5'b11111, 100, 25, 17));
always @(posedge clk) begin
if (cyc == 10) begin
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule

View File

@ -0,0 +1,6 @@
%Error-UNSUPPORTED: t/t_assert_recursive_property_unsup.v:20:4: Unsupported: Recursive property call: 'check'
: ... In instance t
20 | property check(int n);
| ^~~~~~~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error: Exiting due to

View File

@ -0,0 +1,20 @@
#!/usr/bin/env perl
if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; }
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# Copyright 2022 by Antmicro Ltd. 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
scenarios(vlt => 1);
compile(
expect_filename=>$Self->{golden_filename},
verilator_flags2=> ['--assert'],
fails => 1,
);
ok(1);
1;

View File

@ -0,0 +1,36 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain, for
// any use, without warranty, 2022 by Antmicro Ltd.
// SPDX-License-Identifier: CC0-1.0
module t (/*AUTOARG*/
clk
);
input clk;
int cyc = 0;
logic val = 0;
always @(posedge clk) begin
cyc <= cyc + 1;
val = ~val;
end
property check(int n);
disable iff (n == 0)
check(n - 1);
endproperty
assert property(@(posedge clk) check(1))
else begin
// Assertion should pass
$write("*-* Assertion failed *-*\n");
$stop;
end
always @(posedge clk) begin
$write("*-* All Finished *-*\n");
$finish;
end
endmodule