mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-13 12:28:44 +00:00
Code Activity

Merge pull request #946 from YosysHQ/clifford/specify

Browse source 
Add specify parser
This commit is contained in:
Clifford Wolf 2019-05-06 20:57:15 +02:00 committed by GitHub
parent 1706798f4e 8c6e94d57c
commit 752553d8e9
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
19 changed files with 811 additions and 52 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
README.md
View file

@ -259,11 +259,7 @@ for them:
- The ``tri``, ``triand``, ``trior``, ``wand`` and ``wor`` net types - The ``tri``, ``triand``, ``trior``, ``wand`` and ``wor`` net types
- The ``config`` keyword and library map files - The ``config`` and ``disable`` keywords and library map files
- The ``disable``, ``primitive`` and ``specify`` statements
- Latched logic (is synthesized as logic with feedback loops)
Verilog Attributes and non-standard features 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 in an unconditional context (only if/case statements on parameters
and constant values). The intended use for this is synthesis-time DRC. 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 Non-standard or SystemVerilog features for formal verification
============================================================== ==============================================================

5
backends/ilang/ilang_backend.cc
View file

@ -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()); f << stringf("%s" "cell %s %s\n", indent.c_str(), cell->type.c_str(), cell->name.c_str());
for (auto &it : cell->parameters) { 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); dump_const(f, it.second);
f << stringf("\n"); f << stringf("\n");
} }

129
backends/verilog/verilog_backend.cc
View file

@ -183,8 +183,9 @@ bool is_reg_wire(RTLIL::SigSpec sig, std::string &reg_name)
return true; 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) if (width < 0)
width = data.bits.size() - offset; width = data.bits.size() - offset;
if (width == 0) { if (width == 0) {
@ -275,7 +276,8 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
} }
} }
} else { } else {
f << stringf("\""); if ((data.flags & RTLIL::CONST_FLAG_REAL) == 0)
f << stringf("\"");
std::string str = data.decode_string(); std::string str = data.decode_string();
for (size_t i = 0; i < str.size(); i++) { for (size_t i = 0; i < str.size(); i++) {
if (str[i] == '\n') if (str[i] == '\n')
@ -293,7 +295,8 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
else else
f << str[i]; 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, dict<RTLIL::IdString,
else if (modattr && (it->second == Const(1, 1) || it->second == Const(1))) else if (modattr && (it->second == Const(1, 1) || it->second == Const(1)))
f << stringf(" 1 "); f << stringf(" 1 ");
else 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); 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; 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_[PN][PN]_, $_DLATCH_[PN]_, $_DLATCHSR_[PN][PN][PN]_
// FIXME: $sr, $dlatch, $memrd, $memwr, $fsm // 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()) if (it != cell->parameters.begin())
f << stringf(","); f << stringf(",");
f << stringf("\n%s .%s(", indent.c_str(), id(it->first).c_str()); 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);
dump_const(f, it->second, -1, 0, false, is_signed);
f << stringf(")"); f << stringf(")");
} }
f << stringf("\n%s" ")", indent.c_str()); 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) { if (defparam && cell->parameters.size() > 0) {
for (auto it = cell->parameters.begin(); it != cell->parameters.end(); ++it) { 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()); 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);
dump_const(f, it->second, -1, 0, false, is_signed);
f << stringf(";\n"); f << stringf(";\n");
} }
} }

6
frontends/ast/ast.cc
View file

@ -951,6 +951,9 @@ static AstModule* process_module(AstNode *ast, bool defer, AstNode *original_ast
continue; continue;
if (child->type == AST_PARAMETER || child->type == AST_LOCALPARAM) if (child->type == AST_PARAMETER || child->type == AST_LOCALPARAM)
continue; 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; blackbox_module = false;
break; break;
} }
@ -1035,6 +1038,9 @@ static AstModule* process_module(AstNode *ast, bool defer, AstNode *original_ast
child->delete_children(); child->delete_children();
child->children.push_back(AstNode::mkconst_int(0, false, 0)); child->children.push_back(AstNode::mkconst_int(0, false, 0));
new_children.push_back(child); 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 { } else {
delete child; delete child;
} }

25
frontends/ast/genrtlil.cc
View file

@ -1492,10 +1492,12 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
continue; continue;
} }
if (child->type == AST_PARASET) { if (child->type == AST_PARASET) {
int extra_const_flags = 0;
IdString paraname = child->str.empty() ? stringf("$%d", ++para_counter) : child->str; IdString paraname = child->str.empty() ? stringf("$%d", ++para_counter) : child->str;
if (child->children[0]->type == AST_REALVALUE) { if (child->children[0]->type == AST_REALVALUE) {
log_file_warning(filename, linenum, "Replacing floating point parameter %s.%s = %f with string.\n", 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); 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)); auto strnode = AstNode::mkconst_str(stringf("%f", child->children[0]->realvalue));
strnode->cloneInto(child->children[0]); strnode->cloneInto(child->children[0]);
delete strnode; 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_file_error(filename, linenum, "Parameter %s.%s with non-constant value!\n",
log_id(cell), log_id(paraname)); log_id(cell), log_id(paraname));
cell->parameters[paraname] = child->children[0]->asParaConst(); cell->parameters[paraname] = child->children[0]->asParaConst();
cell->parameters[paraname].flags |= extra_const_flags;
continue; continue;
} }
if (child->type == AST_ARGUMENT) { if (child->type == AST_ARGUMENT) {
@ -1523,9 +1526,29 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
} }
for (auto &attr : attributes) { for (auto &attr : attributes) {
if (attr.second->type != AST_CONSTANT) 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(); 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; break;

1
frontends/ilang/ilang_lexer.l
View file

@ -53,6 +53,7 @@ USING_YOSYS_NAMESPACE
"attribute" { return TOK_ATTRIBUTE; } "attribute" { return TOK_ATTRIBUTE; }
"parameter" { return TOK_PARAMETER; } "parameter" { return TOK_PARAMETER; }
"signed" { return TOK_SIGNED; } "signed" { return TOK_SIGNED; }
"real" { return TOK_REAL; }
"wire" { return TOK_WIRE; } "wire" { return TOK_WIRE; }
"memory" { return TOK_MEMORY; } "memory" { return TOK_MEMORY; }
"width" { return TOK_WIDTH; } "width" { return TOK_WIDTH; }

8
frontends/ilang/ilang_parser.y
View file

@ -61,7 +61,7 @@ USING_YOSYS_NAMESPACE
%token TOK_CELL TOK_CONNECT TOK_SWITCH TOK_CASE TOK_ASSIGN TOK_SYNC %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_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_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 <rsigspec> sigspec_list_reversed %type <rsigspec> sigspec_list_reversed
%type <sigspec> sigspec sigspec_list %type <sigspec> sigspec sigspec_list
@ -241,6 +241,12 @@ cell_body:
free($4); free($4);
delete $5; 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 { cell_body TOK_CONNECT TOK_ID sigspec EOL {
if (current_cell->hasPort($3)) if (current_cell->hasPort($3))
rtlil_frontend_ilang_yyerror(stringf("ilang error: redefinition of cell port %s.", $3).c_str()); rtlil_frontend_ilang_yyerror(stringf("ilang error: redefinition of cell port %s.", $3).c_str());

18
frontends/verilog/verilog_frontend.cc
View file

@ -158,6 +158,9 @@ struct VerilogFrontend : public Frontend {
log(" delete (* whitebox *) and (* lib_whitebox *) attributes from\n"); log(" delete (* whitebox *) and (* lib_whitebox *) attributes from\n");
log(" all modules.\n"); log(" all modules.\n");
log("\n"); log("\n");
log(" -specify\n");
log(" parse and import specify blocks\n");
log("\n");
log(" -noopt\n"); log(" -noopt\n");
log(" don't perform basic optimizations (such as const folding) in the\n"); log(" don't perform basic optimizations (such as const folding) in the\n");
log(" high-level front-end.\n"); log(" high-level front-end.\n");
@ -228,6 +231,8 @@ struct VerilogFrontend : public Frontend {
bool flag_nooverwrite = false; bool flag_nooverwrite = false;
bool flag_overwrite = false; bool flag_overwrite = false;
bool flag_defer = false; bool flag_defer = false;
bool flag_noblackbox = false;
bool flag_nowb = false;
std::map<std::string, std::string> defines_map; std::map<std::string, std::string> defines_map;
std::list<std::string> include_dirs; std::list<std::string> include_dirs;
std::list<std::string> attributes; std::list<std::string> attributes;
@ -237,9 +242,8 @@ struct VerilogFrontend : public Frontend {
formal_mode = false; formal_mode = false;
norestrict_mode = false; norestrict_mode = false;
assume_asserts_mode = false; assume_asserts_mode = false;
noblackbox_mode = false;
lib_mode = false; lib_mode = false;
nowb_mode = false; specify_mode = false;
default_nettype_wire = true; default_nettype_wire = true;
args.insert(args.begin()+1, verilog_defaults.begin(), verilog_defaults.end()); args.insert(args.begin()+1, verilog_defaults.begin(), verilog_defaults.end());
@ -340,7 +344,7 @@ struct VerilogFrontend : public Frontend {
continue; continue;
} }
if (arg == "-noblackbox") { if (arg == "-noblackbox") {
noblackbox_mode = true; flag_noblackbox = true;
continue; continue;
} }
if (arg == "-lib") { if (arg == "-lib") {
@ -349,7 +353,11 @@ struct VerilogFrontend : public Frontend {
continue; continue;
} }
if (arg == "-nowb") { if (arg == "-nowb") {
nowb_mode = true; flag_nowb = true;
continue;
}
if (arg == "-specify") {
specify_mode = true;
continue; continue;
} }
if (arg == "-noopt") { if (arg == "-noopt") {
@ -450,7 +458,7 @@ struct VerilogFrontend : public Frontend {
error_on_dpi_function(current_ast); 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, 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) if (!flag_nopp)
delete lexin; delete lexin;

7
frontends/verilog/verilog_frontend.h
View file

@ -69,14 +69,11 @@ namespace VERILOG_FRONTEND
// running in -assert-assumes mode // running in -assert-assumes mode
extern bool assert_assumes_mode; extern bool assert_assumes_mode;
// running in -noblackbox mode
extern bool noblackbox_mode;
// running in -lib mode // running in -lib mode
extern bool lib_mode; extern bool lib_mode;
// running in -nowb mode // running in -specify mode
extern bool nowb_mode; extern bool specify_mode;
// lexer input stream // lexer input stream
extern std::istream *lexin; extern std::istream *lexin;

19
frontends/verilog/verilog_lexer.l
View file

@ -148,7 +148,7 @@ YOSYS_NAMESPACE_END
"endfunction" { return TOK_ENDFUNCTION; } "endfunction" { return TOK_ENDFUNCTION; }
"task" { return TOK_TASK; } "task" { return TOK_TASK; }
"endtask" { return TOK_ENDTASK; } "endtask" { return TOK_ENDTASK; }
"specify" { return TOK_SPECIFY; } "specify" { return specify_mode ? TOK_SPECIFY : TOK_IGNORED_SPECIFY; }
"endspecify" { return TOK_ENDSPECIFY; } "endspecify" { return TOK_ENDSPECIFY; }
"specparam" { return TOK_SPECPARAM; } "specparam" { return TOK_SPECPARAM; }
"package" { SV_KEYWORD(TOK_PACKAGE); } "package" { SV_KEYWORD(TOK_PACKAGE); }
@ -303,6 +303,12 @@ supply1 { return TOK_SUPPLY1; }
return TOK_ID; 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; } "$signed" { return TOK_TO_SIGNED; }
"$unsigned" { return TOK_TO_UNSIGNED; } "$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_POS_INDEXED; }
"-:" { return TOK_NEG_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); } "/*" { BEGIN(COMMENT); }
<COMMENT>. /* ignore comment body */ <COMMENT>. /* ignore comment body */
<COMMENT>\n /* ignore comment body */ <COMMENT>\n /* ignore comment body */

319
frontends/verilog/verilog_parser.y
View file

@ -59,7 +59,7 @@ namespace VERILOG_FRONTEND {
std::vector<char> case_type_stack; std::vector<char> case_type_stack;
bool do_not_require_port_stubs; bool do_not_require_port_stubs;
bool default_nettype_wire; 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 noassert_mode, noassume_mode, norestrict_mode;
bool assume_asserts_mode, assert_assumes_mode; bool assume_asserts_mode, assert_assumes_mode;
bool current_wire_rand, current_wire_const; bool current_wire_rand, current_wire_const;
@ -94,6 +94,20 @@ static void free_attr(std::map<std::string, AstNode*> *al)
delete 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} %define api.prefix {frontend_verilog_yy}
@ -102,10 +116,15 @@ static void free_attr(std::map<std::string, AstNode*> *al)
std::string *string; std::string *string;
struct YOSYS_NAMESPACE_PREFIX AST::AstNode *ast; struct YOSYS_NAMESPACE_PREFIX AST::AstNode *ast;
std::map<std::string, YOSYS_NAMESPACE_PREFIX AST::AstNode*> *al; std::map<std::string, YOSYS_NAMESPACE_PREFIX AST::AstNode*> *al;
struct specify_target *specify_target_ptr;
struct specify_triple *specify_triple_ptr;
struct specify_rise_fall *specify_rise_fall_ptr;
bool boolean; bool boolean;
char ch;
} }
%token <string> TOK_STRING TOK_ID TOK_CONSTVAL TOK_REALVAL TOK_PRIMITIVE TOK_SVA_LABEL %token <string> TOK_STRING TOK_ID TOK_CONSTVAL TOK_REALVAL TOK_PRIMITIVE
%token <string> TOK_SVA_LABEL TOK_SPECIFY_OPER
%token TOK_ASSERT TOK_ASSUME TOK_RESTRICT TOK_COVER TOK_FINAL %token TOK_ASSERT TOK_ASSUME TOK_RESTRICT TOK_COVER TOK_FINAL
%token ATTR_BEGIN ATTR_END DEFATTR_BEGIN DEFATTR_END %token ATTR_BEGIN ATTR_END DEFATTR_BEGIN DEFATTR_END
%token TOK_MODULE TOK_ENDMODULE TOK_PARAMETER TOK_LOCALPARAM TOK_DEFPARAM %token TOK_MODULE TOK_ENDMODULE TOK_PARAMETER TOK_LOCALPARAM TOK_DEFPARAM
@ -116,7 +135,8 @@ static void free_attr(std::map<std::string, AstNode*> *al)
%token TOK_BEGIN TOK_END TOK_IF TOK_ELSE TOK_FOR TOK_WHILE TOK_REPEAT %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_DPI_FUNCTION TOK_POSEDGE TOK_NEGEDGE TOK_OR TOK_AUTOMATIC
%token TOK_CASE TOK_CASEX TOK_CASEZ TOK_ENDCASE TOK_DEFAULT %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_GENERATE TOK_ENDGENERATE TOK_GENVAR TOK_REAL
%token TOK_SYNOPSYS_FULL_CASE TOK_SYNOPSYS_PARALLEL_CASE %token TOK_SYNOPSYS_FULL_CASE TOK_SYNOPSYS_PARALLEL_CASE
%token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED %token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED
@ -130,6 +150,12 @@ static void free_attr(std::map<std::string, AstNode*> *al)
%type <boolean> opt_signed opt_property unique_case_attr %type <boolean> opt_signed opt_property unique_case_attr
%type <al> attr case_attr %type <al> attr case_attr
%type <specify_target_ptr> specify_target
%type <specify_triple_ptr> specify_triple
%type <specify_rise_fall_ptr> specify_rise_fall
%type <ast> specify_if specify_condition specify_opt_arg
%type <ch> specify_edge
// operator precedence from low to high // operator precedence from low to high
%left OP_LOR %left OP_LOR
%left OP_LAND %left OP_LAND
@ -542,7 +568,7 @@ module_body:
module_body_stmt: module_body_stmt:
task_func_decl | specify_block |param_decl | localparam_decl | defparam_decl | specparam_declaration | wire_decl | assign_stmt | cell_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: checker_decl:
TOK_CHECKER TOK_ID ';' { TOK_CHECKER TOK_ID ';' {
@ -700,15 +726,254 @@ task_func_body:
task_func_body behavioral_stmt | task_func_body behavioral_stmt |
/* empty */; /* empty */;
specify_block: /*************************** specify parser ***************************/
TOK_SPECIFY specify_item_opt TOK_ENDSPECIFY |
TOK_SPECIFY TOK_ENDSPECIFY ;
specify_item_opt: specify_block:
specify_item_opt specify_item | TOK_SPECIFY specify_item_list TOK_ENDSPECIFY;
specify_item ;
specify_item_list:
specify_item specify_item_list |
/* empty */;
specify_item: 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 specparam_declaration
// | pulsestyle_declaration // | pulsestyle_declaration
// | showcancelled_declaration // | showcancelled_declaration
@ -724,13 +989,13 @@ specparam_declaration:
// and the 'non_opt_range' rule allows index ranges not allowed by 1364-2005 // and the 'non_opt_range' rule allows index ranges not allowed by 1364-2005
// exxxxtending this for SV specparam would change this anyhow // exxxxtending this for SV specparam would change this anyhow
specparam_range: specparam_range:
'[' constant_expression ':' constant_expression ']' ; '[' ignspec_constant_expression ':' ignspec_constant_expression ']' ;
list_of_specparam_assignments: list_of_specparam_assignments:
specparam_assignment | list_of_specparam_assignments ',' specparam_assignment; specparam_assignment | list_of_specparam_assignments ',' specparam_assignment;
specparam_assignment: specparam_assignment:
TOK_ID '=' constant_mintypmax_expression ; ignspec_id '=' constant_mintypmax_expression ;
/* /*
pulsestyle_declaration : pulsestyle_declaration :
@ -805,19 +1070,19 @@ opt_polarity_operator :
// Good enough for the time being // Good enough for the time being
specify_input_terminal_descriptor : specify_input_terminal_descriptor :
TOK_ID ; ignspec_id ;
// Good enough for the time being // Good enough for the time being
specify_output_terminal_descriptor : specify_output_terminal_descriptor :
TOK_ID ; ignspec_id ;
system_timing_declaration : system_timing_declaration :
TOK_ID '(' system_timing_args ')' ';' ; ignspec_id '(' system_timing_args ')' ';' ;
system_timing_arg : system_timing_arg :
TOK_POSEDGE TOK_ID | TOK_POSEDGE ignspec_id |
TOK_NEGEDGE TOK_ID | TOK_NEGEDGE ignspec_id |
expr ; ignspec_expr ;
system_timing_args : system_timing_args :
system_timing_arg | system_timing_arg |
@ -874,19 +1139,27 @@ tzx_path_delay_expression :
*/ */
path_delay_expression : path_delay_expression :
constant_expression; ignspec_constant_expression;
constant_mintypmax_expression : constant_mintypmax_expression :
constant_expression ignspec_constant_expression
| constant_expression ':' constant_expression ':' 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. // 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) // 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' // 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 // (such as param assignment), so we may leave this as-is, perhaps adding runtime checks for constant-ness
constant_expression: ignspec_constant_expression:
expr ; expr { delete $1; };
ignspec_expr:
expr { delete $1; };
ignspec_id:
TOK_ID { delete $1; };
/**********************************************************************/
param_signed: param_signed:
TOK_SIGNED { TOK_SIGNED {

5
kernel/celltypes.h
View file

@ -85,6 +85,8 @@ struct CellTypes
setup_internals_eval(); setup_internals_eval();
IdString A = "\\A", B = "\\B", EN = "\\EN", Y = "\\Y"; 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); setup_type("$tribuf", {A, EN}, {Y}, true);
@ -99,6 +101,9 @@ struct CellTypes
setup_type("$allconst", pool<RTLIL::IdString>(), {Y}, true); setup_type("$allconst", pool<RTLIL::IdString>(), {Y}, true);
setup_type("$allseq", pool<RTLIL::IdString>(), {Y}, true); setup_type("$allseq", pool<RTLIL::IdString>(), {Y}, true);
setup_type("$equiv", {A, B}, {Y}, true); setup_type("$equiv", {A, B}, {Y}, true);
setup_type("$specify2", {EN, SRC, DST}, pool<RTLIL::IdString>(), true);
setup_type("$specify3", {EN, SRC, DST, DAT}, pool<RTLIL::IdString>(), true);
setup_type("$specrule", {EN_SRC, EN_DST, SRC, DST}, pool<RTLIL::IdString>(), true);
} }
void setup_internals_eval() void setup_internals_eval()

40
kernel/rtlil.cc
View file

@ -1194,6 +1194,46 @@ namespace {
return; 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 == "$_BUF_") { check_gate("AY"); return; }
if (cell->type == "$_NOT_") { check_gate("AY"); return; } if (cell->type == "$_NOT_") { check_gate("AY"); return; }
if (cell->type == "$_AND_") { check_gate("ABY"); return; } if (cell->type == "$_AND_") { check_gate("ABY"); return; }

2
kernel/rtlil.h
View file

@ -50,7 +50,7 @@ namespace RTLIL
CONST_FLAG_NONE = 0, CONST_FLAG_NONE = 0,
CONST_FLAG_STRING = 1, CONST_FLAG_STRING = 1,
CONST_FLAG_SIGNED = 2, // only used for parameters 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; struct Const;

4
manual/CHAPTER_CellLib.tex
View file

@ -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. {\tt \$initstate}, {\tt \$anyconst}, {\tt \$anyseq}, {\tt \$allconst}, {\tt \$allseq} cells.
\end{fixme} \end{fixme}
\begin{fixme}
Add information about {\tt \$specify2}, {\tt \$specify3}, and {\tt \$specrule} cells.
\end{fixme}
\begin{fixme} \begin{fixme}
Add information about {\tt \$slice} and {\tt \$concat} cells. Add information about {\tt \$slice} and {\tt \$concat} cells.
\end{fixme} \end{fixme}

2
passes/opt/opt_clean.cc
View file

@ -64,7 +64,7 @@ struct keep_cache_t
bool query(Cell *cell) 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; return true;
if (cell->has_keep_attr()) if (cell->has_keep_attr())

176
techlibs/common/simlib.v
View file

@ -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); module \$assert (A, EN);
input A, EN; input A, EN;
@ -1863,4 +2038,5 @@ end
endmodule endmodule
`endif `endif
// -------------------------------------------------------- // --------------------------------------------------------

30
tests/various/specify.v Normal file
View file

@ -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

56
tests/various/specify.ys Normal file
View file

@ -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