diff --git a/README.md b/README.md index 913777f2e..195329a37 100644 --- a/README.md +++ b/README.md @@ -259,11 +259,7 @@ for them: - The ``tri``, ``triand``, ``trior``, ``wand`` and ``wor`` net types -- The ``config`` keyword and library map files - -- The ``disable``, ``primitive`` and ``specify`` statements - -- Latched logic (is synthesized as logic with feedback loops) +- The ``config`` and ``disable`` keywords and library map files Verilog Attributes and non-standard features @@ -424,6 +420,11 @@ Verilog Attributes and non-standard features in an unconditional context (only if/case statements on parameters and constant values). The intended use for this is synthesis-time DRC. +- There is limited support for converting specify .. endspecify statements to + special ``$specify2``, ``$specify3``, and ``$specrule`` cells, for use in + blackboxes and whiteboxes. Use ``read_verilog -specify`` to enable this + functionality. (By default specify .. endspecify blocks are ignored.) + Non-standard or SystemVerilog features for formal verification ============================================================== diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc index dc39e5e08..04d1ee311 100644 --- a/backends/ilang/ilang_backend.cc +++ b/backends/ilang/ilang_backend.cc @@ -160,7 +160,10 @@ void ILANG_BACKEND::dump_cell(std::ostream &f, std::string indent, const RTLIL:: } f << stringf("%s" "cell %s %s\n", indent.c_str(), cell->type.c_str(), cell->name.c_str()); for (auto &it : cell->parameters) { - f << stringf("%s parameter%s %s ", indent.c_str(), (it.second.flags & RTLIL::CONST_FLAG_SIGNED) != 0 ? " signed" : "", it.first.c_str()); + f << stringf("%s parameter%s%s %s ", indent.c_str(), + (it.second.flags & RTLIL::CONST_FLAG_SIGNED) != 0 ? " signed" : "", + (it.second.flags & RTLIL::CONST_FLAG_REAL) != 0 ? " real" : "", + it.first.c_str()); dump_const(f, it.second); f << stringf("\n"); } diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index 9967482d6..9fd4ccbc8 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -183,8 +183,9 @@ bool is_reg_wire(RTLIL::SigSpec sig, std::string ®_name) return true; } -void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int offset = 0, bool no_decimal = false, bool set_signed = false, bool escape_comment = false) +void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int offset = 0, bool no_decimal = false, bool escape_comment = false) { + bool set_signed = (data.flags & RTLIL::CONST_FLAG_SIGNED) != 0; if (width < 0) width = data.bits.size() - offset; if (width == 0) { @@ -275,7 +276,8 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o } } } else { - f << stringf("\""); + if ((data.flags & RTLIL::CONST_FLAG_REAL) == 0) + f << stringf("\""); std::string str = data.decode_string(); for (size_t i = 0; i < str.size(); i++) { if (str[i] == '\n') @@ -293,7 +295,8 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o else f << str[i]; } - f << stringf("\""); + if ((data.flags & RTLIL::CONST_FLAG_REAL) == 0) + f << stringf("\""); } } @@ -373,7 +376,7 @@ void dump_attributes(std::ostream &f, std::string indent, dictsecond == Const(1, 1) || it->second == Const(1))) f << stringf(" 1 "); else - dump_const(f, it->second, -1, 0, false, false, attr2comment); + dump_const(f, it->second, -1, 0, false, attr2comment); f << stringf(" %s%c", attr2comment ? "*/" : "*)", term); } } @@ -1242,6 +1245,118 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell) return true; } + if (cell->type.in("$assert", "$assume", "$cover")) + { + f << stringf("%s" "always @* if (", indent.c_str()); + dump_sigspec(f, cell->getPort("\\EN")); + f << stringf(") %s(", cell->type.c_str()+1); + dump_sigspec(f, cell->getPort("\\A")); + f << stringf(");\n"); + return true; + } + + if (cell->type.in("$specify2", "$specify3")) + { + f << stringf("%s" "specify\n%s ", indent.c_str(), indent.c_str()); + + SigSpec en = cell->getPort("\\EN"); + if (en != State::S1) { + f << stringf("if ("); + dump_sigspec(f, cell->getPort("\\EN")); + f << stringf(") "); + } + + f << "("; + if (cell->type == "$specify3" && cell->getParam("\\EDGE_EN").as_bool()) + f << (cell->getParam("\\EDGE_POL").as_bool() ? "posedge ": "negedge "); + + dump_sigspec(f, cell->getPort("\\SRC")); + + f << " "; + if (cell->getParam("\\SRC_DST_PEN").as_bool()) + f << (cell->getParam("\\SRC_DST_POL").as_bool() ? "+": "-"); + f << (cell->getParam("\\FULL").as_bool() ? "*> ": "=> "); + + if (cell->type == "$specify3") { + f << "("; + dump_sigspec(f, cell->getPort("\\DST")); + f << " "; + if (cell->getParam("\\DAT_DST_PEN").as_bool()) + f << (cell->getParam("\\DAT_DST_POL").as_bool() ? "+": "-"); + f << ": "; + dump_sigspec(f, cell->getPort("\\DAT")); + f << ")"; + } else { + dump_sigspec(f, cell->getPort("\\DST")); + } + + bool bak_decimal = decimal; + decimal = 1; + + f << ") = ("; + dump_const(f, cell->getParam("\\T_RISE_MIN")); + f << ":"; + dump_const(f, cell->getParam("\\T_RISE_TYP")); + f << ":"; + dump_const(f, cell->getParam("\\T_RISE_MAX")); + f << ", "; + dump_const(f, cell->getParam("\\T_FALL_MIN")); + f << ":"; + dump_const(f, cell->getParam("\\T_FALL_TYP")); + f << ":"; + dump_const(f, cell->getParam("\\T_FALL_MAX")); + f << ");\n"; + + decimal = bak_decimal; + + f << stringf("%s" "endspecify\n", indent.c_str()); + return true; + } + + if (cell->type == "$specrule") + { + f << stringf("%s" "specify\n%s ", indent.c_str(), indent.c_str()); + + string spec_type = cell->getParam("\\TYPE").decode_string(); + f << stringf("%s(", spec_type.c_str()); + + if (cell->getParam("\\SRC_PEN").as_bool()) + f << (cell->getParam("\\SRC_POL").as_bool() ? "posedge ": "negedge "); + dump_sigspec(f, cell->getPort("\\SRC")); + + if (cell->getPort("\\SRC_EN") != State::S1) { + f << " &&& "; + dump_sigspec(f, cell->getPort("\\SRC_EN")); + } + + f << ", "; + if (cell->getParam("\\DST_PEN").as_bool()) + f << (cell->getParam("\\DST_POL").as_bool() ? "posedge ": "negedge "); + dump_sigspec(f, cell->getPort("\\DST")); + + if (cell->getPort("\\DST_EN") != State::S1) { + f << " &&& "; + dump_sigspec(f, cell->getPort("\\DST_EN")); + } + + bool bak_decimal = decimal; + decimal = 1; + + f << ", "; + dump_const(f, cell->getParam("\\T_LIMIT")); + + if (spec_type == "$setuphold" || spec_type == "$recrem" || spec_type == "$fullskew") { + f << ", "; + dump_const(f, cell->getParam("\\T_LIMIT2")); + } + + f << ");\n"; + decimal = bak_decimal; + + f << stringf("%s" "endspecify\n", indent.c_str()); + return true; + } + // FIXME: $_SR_[PN][PN]_, $_DLATCH_[PN]_, $_DLATCHSR_[PN][PN][PN]_ // FIXME: $sr, $dlatch, $memrd, $memwr, $fsm @@ -1264,8 +1379,7 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell) if (it != cell->parameters.begin()) f << stringf(","); f << stringf("\n%s .%s(", indent.c_str(), id(it->first).c_str()); - bool is_signed = (it->second.flags & RTLIL::CONST_FLAG_SIGNED) != 0; - dump_const(f, it->second, -1, 0, false, is_signed); + dump_const(f, it->second); f << stringf(")"); } f << stringf("\n%s" ")", indent.c_str()); @@ -1312,8 +1426,7 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell) if (defparam && cell->parameters.size() > 0) { for (auto it = cell->parameters.begin(); it != cell->parameters.end(); ++it) { f << stringf("%sdefparam %s.%s = ", indent.c_str(), cell_name.c_str(), id(it->first).c_str()); - bool is_signed = (it->second.flags & RTLIL::CONST_FLAG_SIGNED) != 0; - dump_const(f, it->second, -1, 0, false, is_signed); + dump_const(f, it->second); f << stringf(";\n"); } } diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc index 9f88b08c1..5623541b2 100644 --- a/frontends/ast/ast.cc +++ b/frontends/ast/ast.cc @@ -951,6 +951,9 @@ static AstModule* process_module(AstNode *ast, bool defer, AstNode *original_ast continue; if (child->type == AST_PARAMETER || child->type == AST_LOCALPARAM) continue; + if (child->type == AST_CELL && child->children.size() > 0 && child->children[0]->type == AST_CELLTYPE && + (child->children[0]->str == "$specify2" || child->children[0]->str == "$specify3" || child->children[0]->str == "$specrule")) + continue; blackbox_module = false; break; } @@ -1035,6 +1038,9 @@ static AstModule* process_module(AstNode *ast, bool defer, AstNode *original_ast child->delete_children(); child->children.push_back(AstNode::mkconst_int(0, false, 0)); new_children.push_back(child); + } else if (child->type == AST_CELL && child->children.size() > 0 && child->children[0]->type == AST_CELLTYPE && + (child->children[0]->str == "$specify2" || child->children[0]->str == "$specify3" || child->children[0]->str == "$specrule")) { + new_children.push_back(child); } else { delete child; } diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index d4515babf..379fed641 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -1492,10 +1492,12 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint) continue; } if (child->type == AST_PARASET) { + int extra_const_flags = 0; IdString paraname = child->str.empty() ? stringf("$%d", ++para_counter) : child->str; if (child->children[0]->type == AST_REALVALUE) { log_file_warning(filename, linenum, "Replacing floating point parameter %s.%s = %f with string.\n", log_id(cell), log_id(paraname), child->children[0]->realvalue); + extra_const_flags = RTLIL::CONST_FLAG_REAL; auto strnode = AstNode::mkconst_str(stringf("%f", child->children[0]->realvalue)); strnode->cloneInto(child->children[0]); delete strnode; @@ -1504,6 +1506,7 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint) log_file_error(filename, linenum, "Parameter %s.%s with non-constant value!\n", log_id(cell), log_id(paraname)); cell->parameters[paraname] = child->children[0]->asParaConst(); + cell->parameters[paraname].flags |= extra_const_flags; continue; } if (child->type == AST_ARGUMENT) { @@ -1523,9 +1526,29 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint) } for (auto &attr : attributes) { if (attr.second->type != AST_CONSTANT) - log_file_error(filename, linenum, "Attribute `%s' with non-constant value!\n", attr.first.c_str()); + log_file_error(filename, linenum, "Attribute `%s' with non-constant value.\n", attr.first.c_str()); cell->attributes[attr.first] = attr.second->asAttrConst(); } + if (cell->type.in("$specify2", "$specify3")) { + int src_width = GetSize(cell->getPort("\\SRC")); + int dst_width = GetSize(cell->getPort("\\DST")); + bool full = cell->getParam("\\FULL").as_bool(); + if (!full && src_width != dst_width) + log_file_error(filename, linenum, "Parallel specify SRC width does not match DST width.\n"); + if (cell->type == "$specify3") { + int dat_width = GetSize(cell->getPort("\\DAT")); + if (dat_width != dst_width) + log_file_error(filename, linenum, "Specify DAT width does not match DST width.\n"); + } + cell->setParam("\\SRC_WIDTH", Const(src_width)); + cell->setParam("\\DST_WIDTH", Const(dst_width)); + } + if (cell->type == "$specrule") { + int src_width = GetSize(cell->getPort("\\SRC")); + int dst_width = GetSize(cell->getPort("\\DST")); + cell->setParam("\\SRC_WIDTH", Const(src_width)); + cell->setParam("\\DST_WIDTH", Const(dst_width)); + } } break; diff --git a/frontends/ilang/ilang_lexer.l b/frontends/ilang/ilang_lexer.l index d8e01ae4d..4fd0ae855 100644 --- a/frontends/ilang/ilang_lexer.l +++ b/frontends/ilang/ilang_lexer.l @@ -53,6 +53,7 @@ USING_YOSYS_NAMESPACE "attribute" { return TOK_ATTRIBUTE; } "parameter" { return TOK_PARAMETER; } "signed" { return TOK_SIGNED; } +"real" { return TOK_REAL; } "wire" { return TOK_WIRE; } "memory" { return TOK_MEMORY; } "width" { return TOK_WIDTH; } diff --git a/frontends/ilang/ilang_parser.y b/frontends/ilang/ilang_parser.y index 7bb216dd0..0df792997 100644 --- a/frontends/ilang/ilang_parser.y +++ b/frontends/ilang/ilang_parser.y @@ -61,7 +61,7 @@ USING_YOSYS_NAMESPACE %token TOK_CELL TOK_CONNECT TOK_SWITCH TOK_CASE TOK_ASSIGN TOK_SYNC %token TOK_LOW TOK_HIGH TOK_POSEDGE TOK_NEGEDGE TOK_EDGE TOK_ALWAYS TOK_GLOBAL TOK_INIT %token TOK_UPDATE TOK_PROCESS TOK_END TOK_INVALID TOK_EOL TOK_OFFSET -%token TOK_PARAMETER TOK_ATTRIBUTE TOK_MEMORY TOK_SIZE TOK_SIGNED TOK_UPTO +%token TOK_PARAMETER TOK_ATTRIBUTE TOK_MEMORY TOK_SIZE TOK_SIGNED TOK_REAL TOK_UPTO %type sigspec_list_reversed %type sigspec sigspec_list @@ -241,6 +241,12 @@ cell_body: free($4); delete $5; } | + cell_body TOK_PARAMETER TOK_REAL TOK_ID constant EOL { + current_cell->parameters[$4] = *$5; + current_cell->parameters[$4].flags |= RTLIL::CONST_FLAG_REAL; + free($4); + delete $5; + } | cell_body TOK_CONNECT TOK_ID sigspec EOL { if (current_cell->hasPort($3)) rtlil_frontend_ilang_yyerror(stringf("ilang error: redefinition of cell port %s.", $3).c_str()); diff --git a/frontends/verilog/verilog_frontend.cc b/frontends/verilog/verilog_frontend.cc index 9e624d355..01e589efb 100644 --- a/frontends/verilog/verilog_frontend.cc +++ b/frontends/verilog/verilog_frontend.cc @@ -158,6 +158,9 @@ struct VerilogFrontend : public Frontend { log(" delete (* whitebox *) and (* lib_whitebox *) attributes from\n"); log(" all modules.\n"); log("\n"); + log(" -specify\n"); + log(" parse and import specify blocks\n"); + log("\n"); log(" -noopt\n"); log(" don't perform basic optimizations (such as const folding) in the\n"); log(" high-level front-end.\n"); @@ -228,6 +231,8 @@ struct VerilogFrontend : public Frontend { bool flag_nooverwrite = false; bool flag_overwrite = false; bool flag_defer = false; + bool flag_noblackbox = false; + bool flag_nowb = false; std::map defines_map; std::list include_dirs; std::list attributes; @@ -237,9 +242,8 @@ struct VerilogFrontend : public Frontend { formal_mode = false; norestrict_mode = false; assume_asserts_mode = false; - noblackbox_mode = false; lib_mode = false; - nowb_mode = false; + specify_mode = false; default_nettype_wire = true; args.insert(args.begin()+1, verilog_defaults.begin(), verilog_defaults.end()); @@ -340,7 +344,7 @@ struct VerilogFrontend : public Frontend { continue; } if (arg == "-noblackbox") { - noblackbox_mode = true; + flag_noblackbox = true; continue; } if (arg == "-lib") { @@ -349,7 +353,11 @@ struct VerilogFrontend : public Frontend { continue; } if (arg == "-nowb") { - nowb_mode = true; + flag_nowb = true; + continue; + } + if (arg == "-specify") { + specify_mode = true; continue; } if (arg == "-noopt") { @@ -450,7 +458,7 @@ struct VerilogFrontend : public Frontend { error_on_dpi_function(current_ast); AST::process(design, current_ast, flag_dump_ast1, flag_dump_ast2, flag_no_dump_ptr, flag_dump_vlog1, flag_dump_vlog2, flag_dump_rtlil, flag_nolatches, - flag_nomeminit, flag_nomem2reg, flag_mem2reg, noblackbox_mode, lib_mode, nowb_mode, flag_noopt, flag_icells, flag_nooverwrite, flag_overwrite, flag_defer, default_nettype_wire); + flag_nomeminit, flag_nomem2reg, flag_mem2reg, flag_noblackbox, lib_mode, flag_nowb, flag_noopt, flag_icells, flag_nooverwrite, flag_overwrite, flag_defer, default_nettype_wire); if (!flag_nopp) delete lexin; diff --git a/frontends/verilog/verilog_frontend.h b/frontends/verilog/verilog_frontend.h index ca40946cb..a7c9b2fe6 100644 --- a/frontends/verilog/verilog_frontend.h +++ b/frontends/verilog/verilog_frontend.h @@ -69,14 +69,11 @@ namespace VERILOG_FRONTEND // running in -assert-assumes mode extern bool assert_assumes_mode; - // running in -noblackbox mode - extern bool noblackbox_mode; - // running in -lib mode extern bool lib_mode; - // running in -nowb mode - extern bool nowb_mode; + // running in -specify mode + extern bool specify_mode; // lexer input stream extern std::istream *lexin; diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l index 08e556e8e..142d05d45 100644 --- a/frontends/verilog/verilog_lexer.l +++ b/frontends/verilog/verilog_lexer.l @@ -148,7 +148,7 @@ YOSYS_NAMESPACE_END "endfunction" { return TOK_ENDFUNCTION; } "task" { return TOK_TASK; } "endtask" { return TOK_ENDTASK; } -"specify" { return TOK_SPECIFY; } +"specify" { return specify_mode ? TOK_SPECIFY : TOK_IGNORED_SPECIFY; } "endspecify" { return TOK_ENDSPECIFY; } "specparam" { return TOK_SPECPARAM; } "package" { SV_KEYWORD(TOK_PACKAGE); } @@ -303,6 +303,12 @@ supply1 { return TOK_SUPPLY1; } return TOK_ID; } +"$"(setup|hold|setuphold|removal|recovery|recrem|skew|timeskew|fullskew|nochange) { + if (!specify_mode) REJECT; + frontend_verilog_yylval.string = new std::string(yytext); + return TOK_ID; +} + "$signed" { return TOK_TO_SIGNED; } "$unsigned" { return TOK_TO_UNSIGNED; } @@ -413,6 +419,17 @@ import[ \t\r\n]+\"(DPI|DPI-C)\"[ \t\r\n]+function[ \t\r\n]+ { "+:" { return TOK_POS_INDEXED; } "-:" { return TOK_NEG_INDEXED; } +[-+]?[=*]> { + if (!specify_mode) REJECT; + frontend_verilog_yylval.string = new std::string(yytext); + return TOK_SPECIFY_OPER; +} + +"&&&" { + if (!specify_mode) REJECT; + return TOK_SPECIFY_AND; +} + "/*" { BEGIN(COMMENT); } . /* ignore comment body */ \n /* ignore comment body */ diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y index 46b3a9025..d23009e60 100644 --- a/frontends/verilog/verilog_parser.y +++ b/frontends/verilog/verilog_parser.y @@ -59,7 +59,7 @@ namespace VERILOG_FRONTEND { std::vector case_type_stack; bool do_not_require_port_stubs; bool default_nettype_wire; - bool sv_mode, formal_mode, noblackbox_mode, lib_mode, nowb_mode; + bool sv_mode, formal_mode, lib_mode, specify_mode; bool noassert_mode, noassume_mode, norestrict_mode; bool assume_asserts_mode, assert_assumes_mode; bool current_wire_rand, current_wire_const; @@ -94,6 +94,20 @@ static void free_attr(std::map *al) delete al; } +struct specify_target { + char polarity_op; + AstNode *dst, *dat; +}; + +struct specify_triple { + AstNode *t_min, *t_avg, *t_max; +}; + +struct specify_rise_fall { + specify_triple rise; + specify_triple fall; +}; + %} %define api.prefix {frontend_verilog_yy} @@ -102,10 +116,15 @@ static void free_attr(std::map *al) std::string *string; struct YOSYS_NAMESPACE_PREFIX AST::AstNode *ast; std::map *al; + struct specify_target *specify_target_ptr; + struct specify_triple *specify_triple_ptr; + struct specify_rise_fall *specify_rise_fall_ptr; bool boolean; + char ch; } -%token TOK_STRING TOK_ID TOK_CONSTVAL TOK_REALVAL TOK_PRIMITIVE TOK_SVA_LABEL +%token TOK_STRING TOK_ID TOK_CONSTVAL TOK_REALVAL TOK_PRIMITIVE +%token TOK_SVA_LABEL TOK_SPECIFY_OPER %token TOK_ASSERT TOK_ASSUME TOK_RESTRICT TOK_COVER TOK_FINAL %token ATTR_BEGIN ATTR_END DEFATTR_BEGIN DEFATTR_END %token TOK_MODULE TOK_ENDMODULE TOK_PARAMETER TOK_LOCALPARAM TOK_DEFPARAM @@ -116,7 +135,8 @@ static void free_attr(std::map *al) %token TOK_BEGIN TOK_END TOK_IF TOK_ELSE TOK_FOR TOK_WHILE TOK_REPEAT %token TOK_DPI_FUNCTION TOK_POSEDGE TOK_NEGEDGE TOK_OR TOK_AUTOMATIC %token TOK_CASE TOK_CASEX TOK_CASEZ TOK_ENDCASE TOK_DEFAULT -%token TOK_FUNCTION TOK_ENDFUNCTION TOK_TASK TOK_ENDTASK TOK_SPECIFY TOK_ENDSPECIFY TOK_SPECPARAM +%token TOK_FUNCTION TOK_ENDFUNCTION TOK_TASK TOK_ENDTASK TOK_SPECIFY +%token TOK_IGNORED_SPECIFY TOK_ENDSPECIFY TOK_SPECPARAM TOK_SPECIFY_AND %token TOK_GENERATE TOK_ENDGENERATE TOK_GENVAR TOK_REAL %token TOK_SYNOPSYS_FULL_CASE TOK_SYNOPSYS_PARALLEL_CASE %token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED @@ -130,6 +150,12 @@ static void free_attr(std::map *al) %type opt_signed opt_property unique_case_attr %type attr case_attr +%type specify_target +%type specify_triple +%type specify_rise_fall +%type specify_if specify_condition specify_opt_arg +%type specify_edge + // operator precedence from low to high %left OP_LOR %left OP_LAND @@ -542,7 +568,7 @@ module_body: module_body_stmt: task_func_decl | specify_block |param_decl | localparam_decl | defparam_decl | specparam_declaration | wire_decl | assign_stmt | cell_stmt | - always_stmt | TOK_GENERATE module_gen_body TOK_ENDGENERATE | defattr | assert_property | checker_decl; + always_stmt | TOK_GENERATE module_gen_body TOK_ENDGENERATE | defattr | assert_property | checker_decl | ignored_specify_block; checker_decl: TOK_CHECKER TOK_ID ';' { @@ -700,15 +726,254 @@ task_func_body: task_func_body behavioral_stmt | /* empty */; -specify_block: - TOK_SPECIFY specify_item_opt TOK_ENDSPECIFY | - TOK_SPECIFY TOK_ENDSPECIFY ; +/*************************** specify parser ***************************/ -specify_item_opt: - specify_item_opt specify_item | - specify_item ; +specify_block: + TOK_SPECIFY specify_item_list TOK_ENDSPECIFY; + +specify_item_list: + specify_item specify_item_list | + /* empty */; specify_item: + specify_if '(' specify_edge expr TOK_SPECIFY_OPER specify_target ')' '=' specify_rise_fall ';' { + AstNode *en_expr = $1; + char specify_edge = $3; + AstNode *src_expr = $4; + string *oper = $5; + specify_target *target = $6; + specify_rise_fall *timing = $9; + + if (specify_edge != 0 && target->dat == nullptr) + frontend_verilog_yyerror("Found specify edge but no data spec.\n"); + + AstNode *cell = new AstNode(AST_CELL); + ast_stack.back()->children.push_back(cell); + cell->str = stringf("$specify$%d", autoidx++); + cell->children.push_back(new AstNode(AST_CELLTYPE)); + cell->children.back()->str = target->dat ? "$specify3" : "$specify2"; + + char oper_polarity = 0; + char oper_type = oper->at(0); + + if (oper->size() == 3) { + oper_polarity = oper->at(0); + oper_type = oper->at(1); + } + + cell->children.push_back(new AstNode(AST_PARASET, AstNode::mkconst_int(oper_type == '*', false, 1))); + cell->children.back()->str = "\\FULL"; + + cell->children.push_back(new AstNode(AST_PARASET, AstNode::mkconst_int(oper_polarity != 0, false, 1))); + cell->children.back()->str = "\\SRC_DST_PEN"; + + cell->children.push_back(new AstNode(AST_PARASET, AstNode::mkconst_int(oper_polarity == '+', false, 1))); + cell->children.back()->str = "\\SRC_DST_POL"; + + cell->children.push_back(new AstNode(AST_PARASET, timing->rise.t_min)); + cell->children.back()->str = "\\T_RISE_MIN"; + + cell->children.push_back(new AstNode(AST_PARASET, timing->rise.t_avg)); + cell->children.back()->str = "\\T_RISE_TYP"; + + cell->children.push_back(new AstNode(AST_PARASET, timing->rise.t_max)); + cell->children.back()->str = "\\T_RISE_MAX"; + + cell->children.push_back(new AstNode(AST_PARASET, timing->fall.t_min)); + cell->children.back()->str = "\\T_FALL_MIN"; + + cell->children.push_back(new AstNode(AST_PARASET, timing->fall.t_avg)); + cell->children.back()->str = "\\T_FALL_TYP"; + + cell->children.push_back(new AstNode(AST_PARASET, timing->fall.t_max)); + cell->children.back()->str = "\\T_FALL_MAX"; + + cell->children.push_back(new AstNode(AST_ARGUMENT, en_expr ? en_expr : AstNode::mkconst_int(1, false, 1))); + cell->children.back()->str = "\\EN"; + + cell->children.push_back(new AstNode(AST_ARGUMENT, src_expr)); + cell->children.back()->str = "\\SRC"; + + cell->children.push_back(new AstNode(AST_ARGUMENT, target->dst)); + cell->children.back()->str = "\\DST"; + + if (target->dat) + { + cell->children.push_back(new AstNode(AST_PARASET, AstNode::mkconst_int(specify_edge != 0, false, 1))); + cell->children.back()->str = "\\EDGE_EN"; + + cell->children.push_back(new AstNode(AST_PARASET, AstNode::mkconst_int(specify_edge == 'p', false, 1))); + cell->children.back()->str = "\\EDGE_POL"; + + cell->children.push_back(new AstNode(AST_PARASET, AstNode::mkconst_int(target->polarity_op != 0, false, 1))); + cell->children.back()->str = "\\DAT_DST_PEN"; + + cell->children.push_back(new AstNode(AST_PARASET, AstNode::mkconst_int(target->polarity_op == '+', false, 1))); + cell->children.back()->str = "\\DAT_DST_POL"; + + cell->children.push_back(new AstNode(AST_ARGUMENT, target->dat)); + cell->children.back()->str = "\\DAT"; + } + + delete oper; + delete target; + delete timing; + } | + TOK_ID '(' specify_edge expr specify_condition ',' specify_edge expr specify_condition ',' expr specify_opt_arg ')' ';' { + if (*$1 != "$setup" && *$1 != "$hold" && *$1 != "$setuphold" && *$1 != "$removal" && *$1 != "$recovery" && + *$1 != "$recrem" && *$1 != "$skew" && *$1 != "$timeskew" && *$1 != "$fullskew" && *$1 != "$nochange") + frontend_verilog_yyerror("Unsupported specify rule type: %s\n", $1->c_str()); + + AstNode *src_pen = AstNode::mkconst_int($3 != 0, false, 1); + AstNode *src_pol = AstNode::mkconst_int($3 == 'p', false, 1); + AstNode *src_expr = $4, *src_en = $5 ? $5 : AstNode::mkconst_int(1, false, 1); + + AstNode *dst_pen = AstNode::mkconst_int($7 != 0, false, 1); + AstNode *dst_pol = AstNode::mkconst_int($7 == 'p', false, 1); + AstNode *dst_expr = $8, *dst_en = $9 ? $9 : AstNode::mkconst_int(1, false, 1); + + AstNode *limit = $11; + AstNode *limit2 = $12; + + AstNode *cell = new AstNode(AST_CELL); + ast_stack.back()->children.push_back(cell); + cell->str = stringf("$specify$%d", autoidx++); + cell->children.push_back(new AstNode(AST_CELLTYPE)); + cell->children.back()->str = "$specrule"; + + cell->children.push_back(new AstNode(AST_PARASET, AstNode::mkconst_str(*$1))); + cell->children.back()->str = "\\TYPE"; + + cell->children.push_back(new AstNode(AST_PARASET, limit)); + cell->children.back()->str = "\\T_LIMIT"; + + cell->children.push_back(new AstNode(AST_PARASET, limit2 ? limit2 : AstNode::mkconst_int(0, true))); + cell->children.back()->str = "\\T_LIMIT2"; + + cell->children.push_back(new AstNode(AST_PARASET, src_pen)); + cell->children.back()->str = "\\SRC_PEN"; + + cell->children.push_back(new AstNode(AST_PARASET, src_pol)); + cell->children.back()->str = "\\SRC_POL"; + + cell->children.push_back(new AstNode(AST_PARASET, dst_pen)); + cell->children.back()->str = "\\DST_PEN"; + + cell->children.push_back(new AstNode(AST_PARASET, dst_pol)); + cell->children.back()->str = "\\DST_POL"; + + cell->children.push_back(new AstNode(AST_ARGUMENT, src_en)); + cell->children.back()->str = "\\SRC_EN"; + + cell->children.push_back(new AstNode(AST_ARGUMENT, src_expr)); + cell->children.back()->str = "\\SRC"; + + cell->children.push_back(new AstNode(AST_ARGUMENT, dst_en)); + cell->children.back()->str = "\\DST_EN"; + + cell->children.push_back(new AstNode(AST_ARGUMENT, dst_expr)); + cell->children.back()->str = "\\DST"; + + delete $1; + }; + +specify_opt_arg: + ',' expr { + $$ = $2; + } | + /* empty */ { + $$ = nullptr; + }; + +specify_if: + TOK_IF '(' expr ')' { + $$ = $3; + } | + /* empty */ { + $$ = nullptr; + }; + +specify_condition: + TOK_SPECIFY_AND expr { + $$ = $2; + } | + /* empty */ { + $$ = nullptr; + }; + +specify_target: + expr { + $$ = new specify_target; + $$->polarity_op = 0; + $$->dst = $1; + $$->dat = nullptr; + } | + '(' expr ':' expr ')'{ + $$ = new specify_target; + $$->polarity_op = 0; + $$->dst = $2; + $$->dat = $4; + } | + '(' expr TOK_NEG_INDEXED expr ')'{ + $$ = new specify_target; + $$->polarity_op = '-'; + $$->dst = $2; + $$->dat = $4; + } | + '(' expr TOK_POS_INDEXED expr ')'{ + $$ = new specify_target; + $$->polarity_op = '+'; + $$->dst = $2; + $$->dat = $4; + }; + +specify_edge: + TOK_POSEDGE { $$ = 'p'; } | + TOK_NEGEDGE { $$ = 'n'; } | + { $$ = 0; }; + +specify_rise_fall: + specify_triple { + $$ = new specify_rise_fall; + $$->rise = *$1; + $$->fall.t_min = $1->t_min->clone(); + $$->fall.t_avg = $1->t_avg->clone(); + $$->fall.t_max = $1->t_max->clone(); + delete $1; + } | + '(' specify_triple ',' specify_triple ')' { + $$ = new specify_rise_fall; + $$->rise = *$2; + $$->fall = *$4; + delete $2; + delete $4; + }; + +specify_triple: + expr { + $$ = new specify_triple; + $$->t_min = $1; + $$->t_avg = $1->clone(); + $$->t_max = $1->clone(); + } | + expr ':' expr ':' expr { + $$ = new specify_triple; + $$->t_min = $1; + $$->t_avg = $3; + $$->t_max = $5; + }; + +/******************** ignored specify parser **************************/ + +ignored_specify_block: + TOK_IGNORED_SPECIFY ignored_specify_item_opt TOK_ENDSPECIFY | + TOK_IGNORED_SPECIFY TOK_ENDSPECIFY ; + +ignored_specify_item_opt: + ignored_specify_item_opt ignored_specify_item | + ignored_specify_item ; + +ignored_specify_item: specparam_declaration // | pulsestyle_declaration // | showcancelled_declaration @@ -724,13 +989,13 @@ specparam_declaration: // and the 'non_opt_range' rule allows index ranges not allowed by 1364-2005 // exxxxtending this for SV specparam would change this anyhow specparam_range: - '[' constant_expression ':' constant_expression ']' ; + '[' ignspec_constant_expression ':' ignspec_constant_expression ']' ; list_of_specparam_assignments: specparam_assignment | list_of_specparam_assignments ',' specparam_assignment; specparam_assignment: - TOK_ID '=' constant_mintypmax_expression ; + ignspec_id '=' constant_mintypmax_expression ; /* pulsestyle_declaration : @@ -805,19 +1070,19 @@ opt_polarity_operator : // Good enough for the time being specify_input_terminal_descriptor : - TOK_ID ; + ignspec_id ; // Good enough for the time being specify_output_terminal_descriptor : - TOK_ID ; + ignspec_id ; system_timing_declaration : - TOK_ID '(' system_timing_args ')' ';' ; + ignspec_id '(' system_timing_args ')' ';' ; system_timing_arg : - TOK_POSEDGE TOK_ID | - TOK_NEGEDGE TOK_ID | - expr ; + TOK_POSEDGE ignspec_id | + TOK_NEGEDGE ignspec_id | + ignspec_expr ; system_timing_args : system_timing_arg | @@ -874,19 +1139,27 @@ tzx_path_delay_expression : */ path_delay_expression : - constant_expression; + ignspec_constant_expression; constant_mintypmax_expression : - constant_expression - | constant_expression ':' constant_expression ':' constant_expression + ignspec_constant_expression + | ignspec_constant_expression ':' ignspec_constant_expression ':' ignspec_constant_expression ; // for the time being this is OK, but we may write our own expr here. // as I'm not sure it is legal to use a full expr here (probably not) // On the other hand, other rules requiring constant expressions also use 'expr' // (such as param assignment), so we may leave this as-is, perhaps adding runtime checks for constant-ness -constant_expression: - expr ; +ignspec_constant_expression: + expr { delete $1; }; + +ignspec_expr: + expr { delete $1; }; + +ignspec_id: + TOK_ID { delete $1; }; + +/**********************************************************************/ param_signed: TOK_SIGNED { diff --git a/kernel/celltypes.h b/kernel/celltypes.h index 0da78c313..4e91eddda 100644 --- a/kernel/celltypes.h +++ b/kernel/celltypes.h @@ -85,6 +85,8 @@ struct CellTypes setup_internals_eval(); IdString A = "\\A", B = "\\B", EN = "\\EN", Y = "\\Y"; + IdString SRC = "\\SRC", DST = "\\DST", DAT = "\\DAT"; + IdString EN_SRC = "\\EN_SRC", EN_DST = "\\EN_DST"; setup_type("$tribuf", {A, EN}, {Y}, true); @@ -99,6 +101,9 @@ struct CellTypes setup_type("$allconst", pool(), {Y}, true); setup_type("$allseq", pool(), {Y}, true); setup_type("$equiv", {A, B}, {Y}, true); + setup_type("$specify2", {EN, SRC, DST}, pool(), true); + setup_type("$specify3", {EN, SRC, DST, DAT}, pool(), true); + setup_type("$specrule", {EN_SRC, EN_DST, SRC, DST}, pool(), true); } void setup_internals_eval() diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index dd6817873..147d378e5 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -1194,6 +1194,46 @@ namespace { return; } + if (cell->type.in("$specify2", "$specify3")) { + param_bool("\\FULL"); + param_bool("\\SRC_DST_PEN"); + param_bool("\\SRC_DST_POL"); + param("\\T_RISE_MIN"); + param("\\T_RISE_TYP"); + param("\\T_RISE_MAX"); + param("\\T_FALL_MIN"); + param("\\T_FALL_TYP"); + param("\\T_FALL_MAX"); + port("\\EN", 1); + port("\\SRC", param("\\SRC_WIDTH")); + port("\\DST", param("\\DST_WIDTH")); + if (cell->type == "$specify3") { + param_bool("\\EDGE_EN"); + param_bool("\\EDGE_POL"); + param_bool("\\DAT_DST_PEN"); + param_bool("\\DAT_DST_POL"); + port("\\DAT", param("\\DST_WIDTH")); + } + check_expected(); + return; + } + + if (cell->type == "$specrule") { + param("\\TYPE"); + param_bool("\\SRC_PEN"); + param_bool("\\SRC_POL"); + param_bool("\\DST_PEN"); + param_bool("\\DST_POL"); + param("\\T_LIMIT"); + param("\\T_LIMIT2"); + port("\\SRC_EN", 1); + port("\\DST_EN", 1); + port("\\SRC", param("\\SRC_WIDTH")); + port("\\DST", param("\\DST_WIDTH")); + check_expected(); + return; + } + if (cell->type == "$_BUF_") { check_gate("AY"); return; } if (cell->type == "$_NOT_") { check_gate("AY"); return; } if (cell->type == "$_AND_") { check_gate("ABY"); return; } diff --git a/kernel/rtlil.h b/kernel/rtlil.h index db5c33c73..0c3fa6f76 100644 --- a/kernel/rtlil.h +++ b/kernel/rtlil.h @@ -50,7 +50,7 @@ namespace RTLIL CONST_FLAG_NONE = 0, CONST_FLAG_STRING = 1, CONST_FLAG_SIGNED = 2, // only used for parameters - CONST_FLAG_REAL = 4 // unused -- to be used for parameters + CONST_FLAG_REAL = 4 // only used for parameters }; struct Const; diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex index e64919182..cb1bcf1be 100644 --- a/manual/CHAPTER_CellLib.tex +++ b/manual/CHAPTER_CellLib.tex @@ -465,6 +465,10 @@ Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$live}, {\tt \$fair} {\tt \$initstate}, {\tt \$anyconst}, {\tt \$anyseq}, {\tt \$allconst}, {\tt \$allseq} cells. \end{fixme} +\begin{fixme} +Add information about {\tt \$specify2}, {\tt \$specify3}, and {\tt \$specrule} cells. +\end{fixme} + \begin{fixme} Add information about {\tt \$slice} and {\tt \$concat} cells. \end{fixme} diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc index 618d32550..249939876 100644 --- a/passes/opt/opt_clean.cc +++ b/passes/opt/opt_clean.cc @@ -64,7 +64,7 @@ struct keep_cache_t bool query(Cell *cell) { - if (cell->type.in("$memwr", "$meminit", "$assert", "$assume", "$live", "$fair", "$cover")) + if (cell->type.in("$memwr", "$meminit", "$assert", "$assume", "$live", "$fair", "$cover", "$specify2", "$specify3", "$specrule")) return true; if (cell->has_keep_attr()) diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v index 8e43fe058..a424d3089 100644 --- a/techlibs/common/simlib.v +++ b/techlibs/common/simlib.v @@ -1271,6 +1271,181 @@ endmodule // -------------------------------------------------------- +module \$specify2 (EN, SRC, DST); + +parameter FULL = 0; +parameter SRC_WIDTH = 1; +parameter DST_WIDTH = 1; + +parameter SRC_DST_PEN = 0; +parameter SRC_DST_POL = 0; + +parameter T_RISE_MIN = 0; +parameter T_RISE_TYP = 0; +parameter T_RISE_MAX = 0; + +parameter T_FALL_MIN = 0; +parameter T_FALL_TYP = 0; +parameter T_FALL_MAX = 0; + +input EN; +input [SRC_WIDTH-1:0] SRC; +input [DST_WIDTH-1:0] DST; + +localparam SD = SRC_DST_PEN ? (SRC_DST_POL ? 1 : 2) : 0; + +`ifdef SIMLIB_SPECIFY +specify + if (EN && SD==0 && !FULL) (SRC => DST) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && SD==0 && FULL) (SRC *> DST) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && SD==1 && !FULL) (SRC +=> DST) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && SD==1 && FULL) (SRC +*> DST) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && SD==2 && !FULL) (SRC -=> DST) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && SD==2 && FULL) (SRC -*> DST) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); +endspecify +`endif + +endmodule + +// -------------------------------------------------------- + +module \$specify3 (EN, SRC, DST, DAT); + +parameter FULL = 0; +parameter SRC_WIDTH = 1; +parameter DST_WIDTH = 1; + +parameter EDGE_EN = 0; +parameter EDGE_POL = 0; + +parameter SRC_DST_PEN = 0; +parameter SRC_DST_POL = 0; + +parameter DAT_DST_PEN = 0; +parameter DAT_DST_POL = 0; + +parameter T_RISE_MIN = 0; +parameter T_RISE_TYP = 0; +parameter T_RISE_MAX = 0; + +parameter T_FALL_MIN = 0; +parameter T_FALL_TYP = 0; +parameter T_FALL_MAX = 0; + +input EN; +input [SRC_WIDTH-1:0] SRC; +input [DST_WIDTH-1:0] DST, DAT; + +localparam ED = EDGE_EN ? (EDGE_POL ? 1 : 2) : 0; +localparam SD = SRC_DST_PEN ? (SRC_DST_POL ? 1 : 2) : 0; +localparam DD = DAT_DST_PEN ? (DAT_DST_POL ? 1 : 2) : 0; + +`ifdef SIMLIB_SPECIFY +specify + // DD=0 + + if (EN && DD==0 && SD==0 && ED==0 && !FULL) ( SRC => (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==0 && SD==0 && ED==0 && FULL) ( SRC *> (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==0 && SD==0 && ED==1 && !FULL) (posedge SRC => (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==0 && SD==0 && ED==1 && FULL) (posedge SRC *> (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==0 && SD==0 && ED==2 && !FULL) (negedge SRC => (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==0 && SD==0 && ED==2 && FULL) (negedge SRC *> (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + + if (EN && DD==0 && SD==1 && ED==0 && !FULL) ( SRC +=> (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==0 && SD==1 && ED==0 && FULL) ( SRC +*> (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==0 && SD==1 && ED==1 && !FULL) (posedge SRC +=> (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==0 && SD==1 && ED==1 && FULL) (posedge SRC +*> (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==0 && SD==1 && ED==2 && !FULL) (negedge SRC +=> (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==0 && SD==1 && ED==2 && FULL) (negedge SRC +*> (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + + if (EN && DD==0 && SD==2 && ED==0 && !FULL) ( SRC -=> (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==0 && SD==2 && ED==0 && FULL) ( SRC -*> (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==0 && SD==2 && ED==1 && !FULL) (posedge SRC -=> (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==0 && SD==2 && ED==1 && FULL) (posedge SRC -*> (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==0 && SD==2 && ED==2 && !FULL) (negedge SRC -=> (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==0 && SD==2 && ED==2 && FULL) (negedge SRC -*> (DST : DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + + // DD=1 + + if (EN && DD==1 && SD==0 && ED==0 && !FULL) ( SRC => (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==1 && SD==0 && ED==0 && FULL) ( SRC *> (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==1 && SD==0 && ED==1 && !FULL) (posedge SRC => (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==1 && SD==0 && ED==1 && FULL) (posedge SRC *> (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==1 && SD==0 && ED==2 && !FULL) (negedge SRC => (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==1 && SD==0 && ED==2 && FULL) (negedge SRC *> (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + + if (EN && DD==1 && SD==1 && ED==0 && !FULL) ( SRC +=> (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==1 && SD==1 && ED==0 && FULL) ( SRC +*> (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==1 && SD==1 && ED==1 && !FULL) (posedge SRC +=> (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==1 && SD==1 && ED==1 && FULL) (posedge SRC +*> (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==1 && SD==1 && ED==2 && !FULL) (negedge SRC +=> (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==1 && SD==1 && ED==2 && FULL) (negedge SRC +*> (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + + if (EN && DD==1 && SD==2 && ED==0 && !FULL) ( SRC -=> (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==1 && SD==2 && ED==0 && FULL) ( SRC -*> (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==1 && SD==2 && ED==1 && !FULL) (posedge SRC -=> (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==1 && SD==2 && ED==1 && FULL) (posedge SRC -*> (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==1 && SD==2 && ED==2 && !FULL) (negedge SRC -=> (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==1 && SD==2 && ED==2 && FULL) (negedge SRC -*> (DST +: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + + // DD=2 + + if (EN && DD==2 && SD==0 && ED==0 && !FULL) ( SRC => (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==2 && SD==0 && ED==0 && FULL) ( SRC *> (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==2 && SD==0 && ED==1 && !FULL) (posedge SRC => (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==2 && SD==0 && ED==1 && FULL) (posedge SRC *> (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==2 && SD==0 && ED==2 && !FULL) (negedge SRC => (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==2 && SD==0 && ED==2 && FULL) (negedge SRC *> (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + + if (EN && DD==2 && SD==1 && ED==0 && !FULL) ( SRC +=> (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==2 && SD==1 && ED==0 && FULL) ( SRC +*> (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==2 && SD==1 && ED==1 && !FULL) (posedge SRC +=> (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==2 && SD==1 && ED==1 && FULL) (posedge SRC +*> (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==2 && SD==1 && ED==2 && !FULL) (negedge SRC +=> (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==2 && SD==1 && ED==2 && FULL) (negedge SRC +*> (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + + if (EN && DD==2 && SD==2 && ED==0 && !FULL) ( SRC -=> (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==2 && SD==2 && ED==0 && FULL) ( SRC -*> (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==2 && SD==2 && ED==1 && !FULL) (posedge SRC -=> (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==2 && SD==2 && ED==1 && FULL) (posedge SRC -*> (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==2 && SD==2 && ED==2 && !FULL) (negedge SRC -=> (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); + if (EN && DD==2 && SD==2 && ED==2 && FULL) (negedge SRC -*> (DST -: DAT)) = (T_RISE_MIN:T_RISE_TYP:T_RISE_MAX, T_FALL_MIN:T_FALL_TYP:T_FALL_MAX); +endspecify +`endif + +endmodule + +// -------------------------------------------------------- + +module \$specrule (EN_SRC, EN_DST, SRC, DST); + +parameter TYPE = ""; +parameter T_LIMIT = 0; +parameter T_LIMIT2 = 0; + +parameter SRC_WIDTH = 1; +parameter DST_WIDTH = 1; + +parameter SRC_PEN = 0; +parameter SRC_POL = 0; + +parameter DST_PEN = 0; +parameter DST_POL = 0; + +input EN_SRC, EN_DST; +input [SRC_WIDTH-1:0] SRC; +input [DST_WIDTH-1:0] DST; + +`ifdef SIMLIB_SPECIFY +specify + // TBD +endspecify +`endif + +endmodule + +// -------------------------------------------------------- + module \$assert (A, EN); input A, EN; @@ -1863,4 +2038,5 @@ end endmodule `endif + // -------------------------------------------------------- diff --git a/tests/various/specify.v b/tests/various/specify.v new file mode 100644 index 000000000..afc421da8 --- /dev/null +++ b/tests/various/specify.v @@ -0,0 +1,30 @@ +module test ( + input EN, CLK, + input [3:0] D, + output reg [3:0] Q +); + always @(posedge CLK) + if (EN) Q <= D; + + specify + if (EN) (CLK *> (Q : D)) = (1, 2:3:4); + $setup(D, posedge CLK &&& EN, 5); + $hold(posedge CLK, D &&& EN, 6); + endspecify +endmodule + +module test2 ( + input A, B, + output Q +); + xor (Q, A, B); + specify + //specparam T_rise = 1; + //specparam T_fall = 2; + `define T_rise 1 + `define T_fall 2 + (A => Q) = (`T_rise,`T_fall); + //(B => Q) = (`T_rise+`T_fall)/2.0; + (B => Q) = 1.5; + endspecify +endmodule diff --git a/tests/various/specify.ys b/tests/various/specify.ys new file mode 100644 index 000000000..a5ca07219 --- /dev/null +++ b/tests/various/specify.ys @@ -0,0 +1,56 @@ +read_verilog -specify specify.v +prep +cd test +select t:$specify2 -assert-count 0 +select t:$specify3 -assert-count 1 +select t:$specrule -assert-count 2 +cd test2 +select t:$specify2 -assert-count 2 +select t:$specify3 -assert-count 0 +select t:$specrule -assert-count 0 +cd +write_verilog specify.out +design -stash gold + +read_verilog -specify specify.out +prep +cd test +select t:$specify2 -assert-count 0 +select t:$specify3 -assert-count 1 +select t:$specrule -assert-count 2 +cd test2 +select t:$specify2 -assert-count 2 +select t:$specify3 -assert-count 0 +select t:$specrule -assert-count 0 +cd +design -stash gate + +design -copy-from gold -as gold test +design -copy-from gate -as gate test +rename -hide +rename -enumerate -pattern A_% t:$specify3 +rename -enumerate -pattern B_% t:$specrule r:TYPE=$setup %i +rename -enumerate -pattern C_% t:$specrule r:TYPE=$hold %i +select n:A_* -assert-count 2 +select n:B_* -assert-count 2 +select n:C_* -assert-count 2 +equiv_make gold gate equiv +hierarchy -top equiv +equiv_struct +equiv_induct -seq 5 +equiv_status -assert +design -reset + +design -copy-from gold -as gold test2 +design -copy-from gate -as gate test2 +rename -hide +rename -enumerate -pattern A_% t:$specify2 r:T_RISE_TYP=1 %i +rename -enumerate -pattern B_% t:$specify2 n:A_* %d +select n:A_* -assert-count 2 +select n:B_* -assert-count 2 +equiv_make gold gate equiv +hierarchy -top equiv +equiv_struct +equiv_induct -seq 5 +equiv_status -assert +design -reset