From bac98df46b00171025e10544e10a6100b4c20196 Mon Sep 17 00:00:00 2001 From: Ryszard Rozak Date: Tue, 1 Nov 2022 23:53:47 +0100 Subject: [PATCH] Support named properties (#3667) --- src/V3AssertPre.cpp | 76 ++++++++++- src/V3Ast.h | 16 ++- src/V3AstNodeDType.h | 1 + src/V3AstNodeOther.h | 16 ++- src/V3LinkInc.cpp | 2 +- src/V3ParseGrammar.cpp | 9 +- src/V3Width.cpp | 38 +++++- src/verilog.l | 2 +- src/verilog.y | 123 ++++++++++-------- test_regress/t/t_assert_clock_event_unsup.out | 5 + test_regress/t/t_assert_clock_event_unsup.pl | 20 +++ test_regress/t/t_assert_clock_event_unsup.v | 37 ++++++ test_regress/t/t_assert_disable_bad.out | 5 + test_regress/t/t_assert_disable_bad.pl | 20 +++ test_regress/t/t_assert_disable_bad.v | 28 ++++ test_regress/t/t_assert_named_property.pl | 22 ++++ test_regress/t/t_assert_named_property.v | 66 ++++++++++ test_regress/t/t_assert_property_untyped.pl | 22 ++++ test_regress/t/t_assert_property_untyped.v | 38 ++++++ .../t/t_assert_property_untyped_unsup.out | 5 + .../t/t_assert_property_untyped_unsup.pl | 20 +++ .../t/t_assert_property_untyped_unsup.v | 33 +++++ .../t/t_assert_recursive_property_unsup.out | 6 + .../t/t_assert_recursive_property_unsup.pl | 20 +++ .../t/t_assert_recursive_property_unsup.v | 36 +++++ 25 files changed, 594 insertions(+), 72 deletions(-) create mode 100644 test_regress/t/t_assert_clock_event_unsup.out create mode 100755 test_regress/t/t_assert_clock_event_unsup.pl create mode 100644 test_regress/t/t_assert_clock_event_unsup.v create mode 100644 test_regress/t/t_assert_disable_bad.out create mode 100755 test_regress/t/t_assert_disable_bad.pl create mode 100644 test_regress/t/t_assert_disable_bad.v create mode 100755 test_regress/t/t_assert_named_property.pl create mode 100644 test_regress/t/t_assert_named_property.v create mode 100755 test_regress/t/t_assert_property_untyped.pl create mode 100644 test_regress/t/t_assert_property_untyped.v create mode 100644 test_regress/t/t_assert_property_untyped_unsup.out create mode 100755 test_regress/t/t_assert_property_untyped_unsup.pl create mode 100644 test_regress/t/t_assert_property_untyped_unsup.v create mode 100644 test_regress/t/t_assert_recursive_property_unsup.out create mode 100755 test_regress/t/t_assert_recursive_property_unsup.pl create mode 100644 test_regress/t/t_assert_recursive_property_unsup.v diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index bb0ae8b27..528efcd96 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -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: diff --git a/src/V3Ast.h b/src/V3Ast.h index 0253e20fe..c38b73ce2 100644 --- a/src/V3Ast.h +++ b/src/V3Ast.h @@ -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; } diff --git a/src/V3AstNodeDType.h b/src/V3AstNodeDType.h index 010a78d20..a69c0ad8d 100644 --- a/src/V3AstNodeDType.h +++ b/src/V3AstNodeDType.h @@ -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(); } diff --git a/src/V3AstNodeOther.h b/src/V3AstNodeOther.h index a0b3e991f..7343024d4 100644 --- a/src/V3AstNodeOther.h +++ b/src/V3AstNodeOther.h @@ -1593,7 +1593,7 @@ public: return pragType() == static_cast(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: diff --git a/src/V3LinkInc.cpp b/src/V3LinkInc.cpp index 7c12c4e28..56a7512a8 100644 --- a/src/V3LinkInc.cpp +++ b/src/V3LinkInc.cpp @@ -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) { diff --git a/src/V3ParseGrammar.cpp b/src/V3ParseGrammar.cpp index 7781f6eb8..8d495716a 100644 --- a/src/V3ParseGrammar.cpp +++ b/src/V3ParseGrammar.cpp @@ -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); } diff --git a/src/V3Width.cpp b/src/V3Width.cpp index e5a7050fd..caebfdcd0 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -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?"); diff --git a/src/verilog.l b/src/verilog.l index b2cf6533f..b0a6d01e3 100644 --- a/src/verilog.l +++ b/src/verilog.l @@ -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"); } } diff --git a/src/verilog.y b/src/verilog.y index c73dad6e4..d7668fffe 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -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 m_pinStack; // Queue of pin numbers being parsed @@ -719,7 +721,7 @@ BISONPRE_VERSION(3.7,%define api.header.include {"V3ParseBison.h"}) %token yUNSIGNED "unsigned" //UNSUP %token yUNTIL "until" //UNSUP %token yUNTIL_WITH "until_with" -//UNSUP %token yUNTYPED "untyped" +%token yUNTYPED "untyped" %token yVAR "var" %token yVECTORED "vectored" %token yVIRTUAL__CLASS "virtual-then-class" @@ -1182,7 +1184,7 @@ package_or_generate_item_declaration: // ==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: // IEEE: clocking_declaration (INCOMPLE //************************************************ // Asserts -//UNSUPassertion_item_declaration: // ==IEEE: assertion_item_declaration -//UNSUP property_declaration { $$ = $1; } +assertion_item_declaration: // ==IEEE: assertion_item_declaration + property_declaration { $$ = $1; } //UNSUP | sequence_declaration { $$ = $1; } //UNSUP | let_declaration { $$ = $1; } -//UNSUP ; + ; assertion_item: // ==IEEE: assertion_item concurrent_assertion_item { $$ = $1; } @@ -5411,66 +5413,75 @@ elseStmtBlock: // Part of concurrent_assertion_statement | yELSE stmtBlock { $$ = $2; } ; -//UNSUPproperty_declaration: // ==IEEE: property_declaration -//UNSUP property_declarationFront property_port_listE ';' property_declarationBody -//UNSUP yENDPROPERTY endLabelE -//UNSUP { SYMP->popScope($$); } -//UNSUP ; +property_declaration: // ==IEEE: property_declaration + property_declarationFront property_port_listE ';' property_declarationBody + yENDPROPERTY endLabelE + { $$ = $1; + $$->addStmtsp($2); + $$->addStmtsp($4); + SYMP->popScope($$); + GRAMMARP->endLabel($6, $$, $6); + GRAMMARP->m_insideProperty = false; + GRAMMARP->m_typedPropertyPort = false; } + ; -//UNSUPproperty_declarationFront: // IEEE: part of property_declaration -//UNSUP yPROPERTY idAny/*property_identifier*/ -//UNSUP { SYMP->pushNew($$); } -//UNSUP ; +property_declarationFront: // IEEE: part of property_declaration + yPROPERTY idAny/*property_identifier*/ + { $$ = new AstProperty{$1, *$2, nullptr}; + GRAMMARP->m_insideProperty = true; + SYMP->pushNewUnderNodeOrCurrent($$, nullptr); } + ; -//UNSUPproperty_port_listE: // IEEE: [ ( [ property_port_list ] ) ] -//UNSUP /* empty */ { $$ = nullptr; } -//UNSUP | '(' {VARRESET_LIST(""); VARIO("input"); } property_port_list ')' -//UNSUP { VARRESET_NONLIST(""); } -//UNSUP ; +property_port_listE: // IEEE: [ ( [ property_port_list ] ) ] + /* empty */ { $$ = nullptr; } + | '(' property_port_list ')' { $$ = $2; } + ; -//UNSUPproperty_port_list: // ==IEEE: property_port_list -//UNSUP property_port_item { $$ = $1; } -//UNSUP | property_port_list ',' property_port_item { } -//UNSUP ; +property_port_list: // ==IEEE: property_port_list + property_port_item { $$ = $1; } + | property_port_list ',' property_port_item { $$ = addNextNull($1, $3); } + ; -//UNSUPproperty_port_item: // IEEE: property_port_item/sequence_port_item +property_port_item: // 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: // IEEE: part of property_port_item/sequence_port_item/checker_port_direction -//UNSUP portSig variable_dimensionListE { VARDONE($1, $1, $2, ""); PINNUMINC(); } +property_port_itemAssignment: // IEEE: part of property_port_item/sequence_port_item/checker_port_direction + id variable_dimensionListE { $$ = VARDONEA($1, *$1, $2, nullptr); } //UNSUP | portSig variable_dimensionListE '=' property_actual_arg //UNSUP { VARDONE($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: // IEEE: part of property_declaration +property_declarationBody: // 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: // Part of concurrent_assertion_statement //UNSUP property_port_listE { $$ = $1; } //UNSUP ; -//UNSUPproperty_formal_typeNoDt: // IEEE: property_formal_type (w/o implicit) -//UNSUP sequence_formal_typeNoDt { $$ = $1; } +property_formal_typeNoDt: // IEEE: property_formal_type (w/o implicit) + sequence_formal_typeNoDt { $$ = $1; } //UNSUP | yPROPERTY { } -//UNSUP ; + ; -//UNSUPsequence_formal_typeNoDt: // ==IEEE: sequence_formal_type (w/o data_type_or_implicit) -//UNSUP // // IEEE: data_type_or_implicit -//UNSUP // // implicit expanded where used +sequence_formal_typeNoDt: // ==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: // IEEE: part of sequence_declaration //UNSUP // // 1800-2012 makes ';' optional @@ -5524,11 +5535,11 @@ property_spec: // 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: // ==IEEE: property_statement_spec diff --git a/test_regress/t/t_assert_clock_event_unsup.out b/test_regress/t/t_assert_clock_event_unsup.out new file mode 100644 index 000000000..56484ebb6 --- /dev/null +++ b/test_regress/t/t_assert_clock_event_unsup.out @@ -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 diff --git a/test_regress/t/t_assert_clock_event_unsup.pl b/test_regress/t/t_assert_clock_event_unsup.pl new file mode 100755 index 000000000..f201521f0 --- /dev/null +++ b/test_regress/t/t_assert_clock_event_unsup.pl @@ -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; diff --git a/test_regress/t/t_assert_clock_event_unsup.v b/test_regress/t/t_assert_clock_event_unsup.v new file mode 100644 index 000000000..6737ff316 --- /dev/null +++ b/test_regress/t/t_assert_clock_event_unsup.v @@ -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 diff --git a/test_regress/t/t_assert_disable_bad.out b/test_regress/t/t_assert_disable_bad.out new file mode 100644 index 000000000..a53fbe9d1 --- /dev/null +++ b/test_regress/t/t_assert_disable_bad.out @@ -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 diff --git a/test_regress/t/t_assert_disable_bad.pl b/test_regress/t/t_assert_disable_bad.pl new file mode 100755 index 000000000..f201521f0 --- /dev/null +++ b/test_regress/t/t_assert_disable_bad.pl @@ -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; diff --git a/test_regress/t/t_assert_disable_bad.v b/test_regress/t/t_assert_disable_bad.v new file mode 100644 index 000000000..cb0f84b7d --- /dev/null +++ b/test_regress/t/t_assert_disable_bad.v @@ -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 diff --git a/test_regress/t/t_assert_named_property.pl b/test_regress/t/t_assert_named_property.pl new file mode 100755 index 000000000..c505d6263 --- /dev/null +++ b/test_regress/t/t_assert_named_property.pl @@ -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; diff --git a/test_regress/t/t_assert_named_property.v b/test_regress/t/t_assert_named_property.v new file mode 100644 index 000000000..63e4f6a33 --- /dev/null +++ b/test_regress/t/t_assert_named_property.v @@ -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 diff --git a/test_regress/t/t_assert_property_untyped.pl b/test_regress/t/t_assert_property_untyped.pl new file mode 100755 index 000000000..c505d6263 --- /dev/null +++ b/test_regress/t/t_assert_property_untyped.pl @@ -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; diff --git a/test_regress/t/t_assert_property_untyped.v b/test_regress/t/t_assert_property_untyped.v new file mode 100644 index 000000000..29fbd99c2 --- /dev/null +++ b/test_regress/t/t_assert_property_untyped.v @@ -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 diff --git a/test_regress/t/t_assert_property_untyped_unsup.out b/test_regress/t/t_assert_property_untyped_unsup.out new file mode 100644 index 000000000..e9985890c --- /dev/null +++ b/test_regress/t/t_assert_property_untyped_unsup.out @@ -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 diff --git a/test_regress/t/t_assert_property_untyped_unsup.pl b/test_regress/t/t_assert_property_untyped_unsup.pl new file mode 100755 index 000000000..f201521f0 --- /dev/null +++ b/test_regress/t/t_assert_property_untyped_unsup.pl @@ -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; diff --git a/test_regress/t/t_assert_property_untyped_unsup.v b/test_regress/t/t_assert_property_untyped_unsup.v new file mode 100644 index 000000000..9784c48fc --- /dev/null +++ b/test_regress/t/t_assert_property_untyped_unsup.v @@ -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 diff --git a/test_regress/t/t_assert_recursive_property_unsup.out b/test_regress/t/t_assert_recursive_property_unsup.out new file mode 100644 index 000000000..fbca8fd7c --- /dev/null +++ b/test_regress/t/t_assert_recursive_property_unsup.out @@ -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 diff --git a/test_regress/t/t_assert_recursive_property_unsup.pl b/test_regress/t/t_assert_recursive_property_unsup.pl new file mode 100755 index 000000000..f201521f0 --- /dev/null +++ b/test_regress/t/t_assert_recursive_property_unsup.pl @@ -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; diff --git a/test_regress/t/t_assert_recursive_property_unsup.v b/test_regress/t/t_assert_recursive_property_unsup.v new file mode 100644 index 000000000..b6d91ad47 --- /dev/null +++ b/test_regress/t/t_assert_recursive_property_unsup.v @@ -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