mirror of https://github.com/YosysHQ/yosys.git
Merge pull request #1703 from YosysHQ/eddie/specify_improve
Improve specify parser
This commit is contained in:
commit
760096e8d2
|
@ -1417,11 +1417,19 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
|
||||||
decimal = 1;
|
decimal = 1;
|
||||||
|
|
||||||
f << ", ";
|
f << ", ";
|
||||||
dump_const(f, cell->getParam("\\T_LIMIT"));
|
dump_const(f, cell->getParam("\\T_LIMIT_MIN"));
|
||||||
|
f << ": ";
|
||||||
|
dump_const(f, cell->getParam("\\T_LIMIT_TYP"));
|
||||||
|
f << ": ";
|
||||||
|
dump_const(f, cell->getParam("\\T_LIMIT_MAX"));
|
||||||
|
|
||||||
if (spec_type == "$setuphold" || spec_type == "$recrem" || spec_type == "$fullskew") {
|
if (spec_type == "$setuphold" || spec_type == "$recrem" || spec_type == "$fullskew") {
|
||||||
f << ", ";
|
f << ", ";
|
||||||
dump_const(f, cell->getParam("\\T_LIMIT2"));
|
dump_const(f, cell->getParam("\\T_LIMIT2_MIN"));
|
||||||
|
f << ": ";
|
||||||
|
dump_const(f, cell->getParam("\\T_LIMIT2_TYP"));
|
||||||
|
f << ": ";
|
||||||
|
dump_const(f, cell->getParam("\\T_LIMIT2_MAX"));
|
||||||
}
|
}
|
||||||
|
|
||||||
f << ");\n";
|
f << ");\n";
|
||||||
|
|
|
@ -1563,21 +1563,25 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
|
||||||
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")) {
|
if (cell->type == "$specify2") {
|
||||||
int src_width = GetSize(cell->getPort("\\SRC"));
|
int src_width = GetSize(cell->getPort("\\SRC"));
|
||||||
int dst_width = GetSize(cell->getPort("\\DST"));
|
int dst_width = GetSize(cell->getPort("\\DST"));
|
||||||
bool full = cell->getParam("\\FULL").as_bool();
|
bool full = cell->getParam("\\FULL").as_bool();
|
||||||
if (!full && src_width != dst_width)
|
if (!full && src_width != dst_width)
|
||||||
log_file_error(filename, linenum, "Parallel specify SRC width does not match DST width.\n");
|
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("\\SRC_WIDTH", Const(src_width));
|
||||||
cell->setParam("\\DST_WIDTH", Const(dst_width));
|
cell->setParam("\\DST_WIDTH", Const(dst_width));
|
||||||
}
|
}
|
||||||
if (cell->type == "$specrule") {
|
else if (cell->type == "$specify3") {
|
||||||
|
int dat_width = GetSize(cell->getPort("\\DAT"));
|
||||||
|
int dst_width = GetSize(cell->getPort("\\DST"));
|
||||||
|
if (dat_width != dst_width)
|
||||||
|
log_file_error(filename, linenum, "Specify DAT width does not match DST width.\n");
|
||||||
|
int src_width = GetSize(cell->getPort("\\SRC"));
|
||||||
|
cell->setParam("\\SRC_WIDTH", Const(src_width));
|
||||||
|
cell->setParam("\\DST_WIDTH", Const(dst_width));
|
||||||
|
}
|
||||||
|
else if (cell->type == "$specrule") {
|
||||||
int src_width = GetSize(cell->getPort("\\SRC"));
|
int src_width = GetSize(cell->getPort("\\SRC"));
|
||||||
int dst_width = GetSize(cell->getPort("\\DST"));
|
int dst_width = GetSize(cell->getPort("\\DST"));
|
||||||
cell->setParam("\\SRC_WIDTH", Const(src_width));
|
cell->setParam("\\SRC_WIDTH", Const(src_width));
|
||||||
|
|
|
@ -440,7 +440,7 @@ import[ \t\r\n]+\"(DPI|DPI-C)\"[ \t\r\n]+function[ \t\r\n]+ {
|
||||||
}
|
}
|
||||||
|
|
||||||
"&&&" {
|
"&&&" {
|
||||||
if (!specify_mode) REJECT;
|
if (!specify_mode) return TOK_IGNORED_SPECIFY_AND;
|
||||||
return TOK_SPECIFY_AND;
|
return TOK_SPECIFY_AND;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -160,7 +160,7 @@ static void addRange(AstNode *parent, int msb = 31, int lsb = 0, bool isSigned =
|
||||||
%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
|
%token TOK_FUNCTION TOK_ENDFUNCTION TOK_TASK TOK_ENDTASK TOK_SPECIFY
|
||||||
%token TOK_IGNORED_SPECIFY TOK_ENDSPECIFY TOK_SPECPARAM TOK_SPECIFY_AND
|
%token TOK_IGNORED_SPECIFY TOK_ENDSPECIFY TOK_SPECPARAM TOK_SPECIFY_AND TOK_IGNORED_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
|
||||||
|
@ -176,9 +176,9 @@ static void addRange(AstNode *parent, int msb = 31, int lsb = 0, bool isSigned =
|
||||||
%type <al> attr case_attr
|
%type <al> attr case_attr
|
||||||
|
|
||||||
%type <specify_target_ptr> specify_target
|
%type <specify_target_ptr> specify_target
|
||||||
%type <specify_triple_ptr> specify_triple
|
%type <specify_triple_ptr> specify_triple specify_opt_triple
|
||||||
%type <specify_rise_fall_ptr> specify_rise_fall
|
%type <specify_rise_fall_ptr> specify_rise_fall
|
||||||
%type <ast> specify_if specify_condition specify_opt_arg
|
%type <ast> specify_if specify_condition
|
||||||
%type <ch> specify_edge
|
%type <ch> specify_edge
|
||||||
|
|
||||||
// operator precedence from low to high
|
// operator precedence from low to high
|
||||||
|
@ -873,7 +873,7 @@ specify_item:
|
||||||
delete target;
|
delete target;
|
||||||
delete timing;
|
delete timing;
|
||||||
} |
|
} |
|
||||||
TOK_ID '(' specify_edge expr specify_condition ',' specify_edge expr specify_condition ',' expr specify_opt_arg ')' ';' {
|
TOK_ID '(' specify_edge expr specify_condition ',' specify_edge expr specify_condition ',' specify_triple specify_opt_triple ')' ';' {
|
||||||
if (*$1 != "$setup" && *$1 != "$hold" && *$1 != "$setuphold" && *$1 != "$removal" && *$1 != "$recovery" &&
|
if (*$1 != "$setup" && *$1 != "$hold" && *$1 != "$setuphold" && *$1 != "$removal" && *$1 != "$recovery" &&
|
||||||
*$1 != "$recrem" && *$1 != "$skew" && *$1 != "$timeskew" && *$1 != "$fullskew" && *$1 != "$nochange")
|
*$1 != "$recrem" && *$1 != "$skew" && *$1 != "$timeskew" && *$1 != "$fullskew" && *$1 != "$nochange")
|
||||||
frontend_verilog_yyerror("Unsupported specify rule type: %s\n", $1->c_str());
|
frontend_verilog_yyerror("Unsupported specify rule type: %s\n", $1->c_str());
|
||||||
|
@ -886,8 +886,8 @@ specify_item:
|
||||||
AstNode *dst_pol = AstNode::mkconst_int($7 == 'p', 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 *dst_expr = $8, *dst_en = $9 ? $9 : AstNode::mkconst_int(1, false, 1);
|
||||||
|
|
||||||
AstNode *limit = $11;
|
specify_triple *limit = $11;
|
||||||
AstNode *limit2 = $12;
|
specify_triple *limit2 = $12;
|
||||||
|
|
||||||
AstNode *cell = new AstNode(AST_CELL);
|
AstNode *cell = new AstNode(AST_CELL);
|
||||||
ast_stack.back()->children.push_back(cell);
|
ast_stack.back()->children.push_back(cell);
|
||||||
|
@ -898,11 +898,23 @@ specify_item:
|
||||||
cell->children.push_back(new AstNode(AST_PARASET, AstNode::mkconst_str(*$1)));
|
cell->children.push_back(new AstNode(AST_PARASET, AstNode::mkconst_str(*$1)));
|
||||||
cell->children.back()->str = "\\TYPE";
|
cell->children.back()->str = "\\TYPE";
|
||||||
|
|
||||||
cell->children.push_back(new AstNode(AST_PARASET, limit));
|
cell->children.push_back(new AstNode(AST_PARASET, limit->t_min));
|
||||||
cell->children.back()->str = "\\T_LIMIT";
|
cell->children.back()->str = "\\T_LIMIT_MIN";
|
||||||
|
|
||||||
cell->children.push_back(new AstNode(AST_PARASET, limit2 ? limit2 : AstNode::mkconst_int(0, true)));
|
cell->children.push_back(new AstNode(AST_PARASET, limit->t_avg));
|
||||||
cell->children.back()->str = "\\T_LIMIT2";
|
cell->children.back()->str = "\\T_LIMIT_TYP";
|
||||||
|
|
||||||
|
cell->children.push_back(new AstNode(AST_PARASET, limit->t_max));
|
||||||
|
cell->children.back()->str = "\\T_LIMIT_MAX";
|
||||||
|
|
||||||
|
cell->children.push_back(new AstNode(AST_PARASET, limit2 ? limit2->t_min : AstNode::mkconst_int(0, true)));
|
||||||
|
cell->children.back()->str = "\\T_LIMIT2_MIN";
|
||||||
|
|
||||||
|
cell->children.push_back(new AstNode(AST_PARASET, limit2 ? limit2->t_avg : AstNode::mkconst_int(0, true)));
|
||||||
|
cell->children.back()->str = "\\T_LIMIT2_TYP";
|
||||||
|
|
||||||
|
cell->children.push_back(new AstNode(AST_PARASET, limit2 ? limit2->t_max : AstNode::mkconst_int(0, true)));
|
||||||
|
cell->children.back()->str = "\\T_LIMIT2_MAX";
|
||||||
|
|
||||||
cell->children.push_back(new AstNode(AST_PARASET, src_pen));
|
cell->children.push_back(new AstNode(AST_PARASET, src_pen));
|
||||||
cell->children.back()->str = "\\SRC_PEN";
|
cell->children.back()->str = "\\SRC_PEN";
|
||||||
|
@ -931,8 +943,8 @@ specify_item:
|
||||||
delete $1;
|
delete $1;
|
||||||
};
|
};
|
||||||
|
|
||||||
specify_opt_arg:
|
specify_opt_triple:
|
||||||
',' expr {
|
',' specify_triple {
|
||||||
$$ = $2;
|
$$ = $2;
|
||||||
} |
|
} |
|
||||||
/* empty */ {
|
/* empty */ {
|
||||||
|
@ -1001,7 +1013,46 @@ specify_rise_fall:
|
||||||
$$->fall = *$4;
|
$$->fall = *$4;
|
||||||
delete $2;
|
delete $2;
|
||||||
delete $4;
|
delete $4;
|
||||||
};
|
} |
|
||||||
|
'(' specify_triple ',' specify_triple ',' specify_triple ')' {
|
||||||
|
$$ = new specify_rise_fall;
|
||||||
|
$$->rise = *$2;
|
||||||
|
$$->fall = *$4;
|
||||||
|
delete $2;
|
||||||
|
delete $4;
|
||||||
|
delete $6;
|
||||||
|
log_file_warning(current_filename, get_line_num(), "Path delay expressions beyond rise/fall not currently supported. Ignoring.\n");
|
||||||
|
} |
|
||||||
|
'(' specify_triple ',' specify_triple ',' specify_triple ',' specify_triple ',' specify_triple ',' specify_triple ')' {
|
||||||
|
$$ = new specify_rise_fall;
|
||||||
|
$$->rise = *$2;
|
||||||
|
$$->fall = *$4;
|
||||||
|
delete $2;
|
||||||
|
delete $4;
|
||||||
|
delete $6;
|
||||||
|
delete $8;
|
||||||
|
delete $10;
|
||||||
|
delete $12;
|
||||||
|
log_file_warning(current_filename, get_line_num(), "Path delay expressions beyond rise/fall not currently supported. Ignoring.\n");
|
||||||
|
} |
|
||||||
|
'(' specify_triple ',' specify_triple ',' specify_triple ',' specify_triple ',' specify_triple ',' specify_triple ',' specify_triple ',' specify_triple ',' specify_triple ',' specify_triple ',' specify_triple ',' specify_triple ')' {
|
||||||
|
$$ = new specify_rise_fall;
|
||||||
|
$$->rise = *$2;
|
||||||
|
$$->fall = *$4;
|
||||||
|
delete $2;
|
||||||
|
delete $4;
|
||||||
|
delete $6;
|
||||||
|
delete $8;
|
||||||
|
delete $10;
|
||||||
|
delete $12;
|
||||||
|
delete $14;
|
||||||
|
delete $16;
|
||||||
|
delete $18;
|
||||||
|
delete $20;
|
||||||
|
delete $22;
|
||||||
|
delete $24;
|
||||||
|
log_file_warning(current_filename, get_line_num(), "Path delay expressions beyond rise/fall not currently supported. Ignoring.\n");
|
||||||
|
}
|
||||||
|
|
||||||
specify_triple:
|
specify_triple:
|
||||||
expr {
|
expr {
|
||||||
|
@ -1049,7 +1100,7 @@ list_of_specparam_assignments:
|
||||||
specparam_assignment | list_of_specparam_assignments ',' specparam_assignment;
|
specparam_assignment | list_of_specparam_assignments ',' specparam_assignment;
|
||||||
|
|
||||||
specparam_assignment:
|
specparam_assignment:
|
||||||
ignspec_id '=' constant_mintypmax_expression ;
|
ignspec_id '=' ignspec_expr ;
|
||||||
|
|
||||||
ignspec_opt_cond:
|
ignspec_opt_cond:
|
||||||
TOK_IF '(' ignspec_expr ')' | /* empty */;
|
TOK_IF '(' ignspec_expr ')' | /* empty */;
|
||||||
|
@ -1066,13 +1117,15 @@ simple_path_declaration :
|
||||||
;
|
;
|
||||||
|
|
||||||
path_delay_value :
|
path_delay_value :
|
||||||
'(' path_delay_expression list_of_path_delay_extra_expressions ')'
|
'(' ignspec_expr list_of_path_delay_extra_expressions ')'
|
||||||
| path_delay_expression
|
| ignspec_expr
|
||||||
| path_delay_expression list_of_path_delay_extra_expressions
|
| ignspec_expr list_of_path_delay_extra_expressions
|
||||||
;
|
;
|
||||||
|
|
||||||
list_of_path_delay_extra_expressions :
|
list_of_path_delay_extra_expressions :
|
||||||
',' path_delay_expression | ',' path_delay_expression list_of_path_delay_extra_expressions;
|
',' ignspec_expr
|
||||||
|
| ',' ignspec_expr list_of_path_delay_extra_expressions
|
||||||
|
;
|
||||||
|
|
||||||
specify_edge_identifier :
|
specify_edge_identifier :
|
||||||
TOK_POSEDGE | TOK_NEGEDGE ;
|
TOK_POSEDGE | TOK_NEGEDGE ;
|
||||||
|
@ -1123,16 +1176,9 @@ system_timing_arg :
|
||||||
|
|
||||||
system_timing_args :
|
system_timing_args :
|
||||||
system_timing_arg |
|
system_timing_arg |
|
||||||
|
system_timing_args TOK_IGNORED_SPECIFY_AND system_timing_arg |
|
||||||
system_timing_args ',' system_timing_arg ;
|
system_timing_args ',' system_timing_arg ;
|
||||||
|
|
||||||
path_delay_expression :
|
|
||||||
ignspec_constant_expression;
|
|
||||||
|
|
||||||
constant_mintypmax_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.
|
// 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'
|
||||||
|
@ -1141,10 +1187,16 @@ ignspec_constant_expression:
|
||||||
expr { delete $1; };
|
expr { delete $1; };
|
||||||
|
|
||||||
ignspec_expr:
|
ignspec_expr:
|
||||||
expr { delete $1; };
|
expr { delete $1; } |
|
||||||
|
expr ':' expr ':' expr {
|
||||||
|
delete $1;
|
||||||
|
delete $3;
|
||||||
|
delete $5;
|
||||||
|
};
|
||||||
|
|
||||||
ignspec_id:
|
ignspec_id:
|
||||||
TOK_ID { delete $1; };
|
TOK_ID { delete $1; }
|
||||||
|
range_or_multirange { delete $3; };
|
||||||
|
|
||||||
/**********************************************************************/
|
/**********************************************************************/
|
||||||
|
|
||||||
|
|
|
@ -1258,8 +1258,12 @@ namespace {
|
||||||
param_bool(ID(SRC_POL));
|
param_bool(ID(SRC_POL));
|
||||||
param_bool(ID(DST_PEN));
|
param_bool(ID(DST_PEN));
|
||||||
param_bool(ID(DST_POL));
|
param_bool(ID(DST_POL));
|
||||||
param(ID(T_LIMIT));
|
param(ID(T_LIMIT_MIN));
|
||||||
param(ID(T_LIMIT2));
|
param(ID(T_LIMIT_TYP));
|
||||||
|
param(ID(T_LIMIT_MAX));
|
||||||
|
param(ID(T_LIMIT2_MIN));
|
||||||
|
param(ID(T_LIMIT2_TYP));
|
||||||
|
param(ID(T_LIMIT2_MAX));
|
||||||
port(ID(SRC_EN), 1);
|
port(ID(SRC_EN), 1);
|
||||||
port(ID(DST_EN), 1);
|
port(ID(DST_EN), 1);
|
||||||
port(ID(SRC), param(ID(SRC_WIDTH)));
|
port(ID(SRC), param(ID(SRC_WIDTH)));
|
||||||
|
|
|
@ -51,20 +51,26 @@ struct keep_cache_t
|
||||||
if (cache.count(module))
|
if (cache.count(module))
|
||||||
return cache.at(module);
|
return cache.at(module);
|
||||||
|
|
||||||
cache[module] = true;
|
bool found_keep = false;
|
||||||
if (!module->get_bool_attribute(ID::keep)) {
|
if (module->get_bool_attribute(ID::keep))
|
||||||
bool found_keep = false;
|
found_keep = true;
|
||||||
|
else
|
||||||
for (auto cell : module->cells())
|
for (auto cell : module->cells())
|
||||||
if (query(cell)) found_keep = true;
|
if (query(cell, true /* ignore_specify */)) {
|
||||||
cache[module] = found_keep;
|
found_keep = true;
|
||||||
}
|
break;
|
||||||
|
}
|
||||||
|
cache[module] = found_keep;
|
||||||
|
|
||||||
return cache[module];
|
return found_keep;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool query(Cell *cell)
|
bool query(Cell *cell, bool ignore_specify = false)
|
||||||
{
|
{
|
||||||
if (cell->type.in(ID($memwr), ID($meminit), ID($assert), ID($assume), ID($live), ID($fair), ID($cover), ID($specify2), ID($specify3), ID($specrule)))
|
if (cell->type.in(ID($memwr), ID($meminit), ID($assert), ID($assume), ID($live), ID($fair), ID($cover)))
|
||||||
|
return true;
|
||||||
|
|
||||||
|
if (!ignore_specify && cell->type.in(ID($specify2), ID($specify3), ID($specrule)))
|
||||||
return true;
|
return true;
|
||||||
|
|
||||||
if (cell->has_keep_attr())
|
if (cell->has_keep_attr())
|
||||||
|
|
|
@ -7,11 +7,9 @@ module test (
|
||||||
if (EN) Q <= D;
|
if (EN) Q <= D;
|
||||||
|
|
||||||
specify
|
specify
|
||||||
`ifndef SKIP_UNSUPPORTED_IGN_PARSER_CONSTRUCTS
|
|
||||||
if (EN) (posedge CLK *> (Q : D)) = (1, 2:3:4);
|
if (EN) (posedge CLK *> (Q : D)) = (1, 2:3:4);
|
||||||
$setup(D, posedge CLK &&& EN, 5);
|
$setup(D, posedge CLK &&& EN, 5);
|
||||||
$hold(posedge CLK, D &&& EN, 6);
|
$hold(posedge CLK, D &&& EN, 6);
|
||||||
`endif
|
|
||||||
endspecify
|
endspecify
|
||||||
endmodule
|
endmodule
|
||||||
|
|
||||||
|
@ -37,3 +35,30 @@ specify
|
||||||
(posedge clk *> (q +: d)) = (3,1);
|
(posedge clk *> (q +: d)) = (3,1);
|
||||||
endspecify
|
endspecify
|
||||||
endmodule
|
endmodule
|
||||||
|
|
||||||
|
module test3(input clk, input [1:0] d, output [1:0] q);
|
||||||
|
specify
|
||||||
|
(posedge clk => (q +: d)) = (3,1);
|
||||||
|
(posedge clk *> (q +: d)) = (3,1);
|
||||||
|
endspecify
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
module test4(input clk, d, output q);
|
||||||
|
specify
|
||||||
|
$setup(d, posedge clk, 1:2:3);
|
||||||
|
$setuphold(d, posedge clk, 1:2:3, 4:5:6);
|
||||||
|
endspecify
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
module test5(input clk, d, e, output q);
|
||||||
|
specify
|
||||||
|
$setup(d, posedge clk &&& e, 1:2:3);
|
||||||
|
endspecify
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
module test6(input clk, d, e, output q);
|
||||||
|
specify
|
||||||
|
(d[0] *> q[0]) = (3,1);
|
||||||
|
(posedge clk[0] => (q[0] +: d[0])) = (3,1);
|
||||||
|
endspecify
|
||||||
|
endmodule
|
||||||
|
|
|
@ -55,4 +55,23 @@ equiv_induct -seq 5
|
||||||
equiv_status -assert
|
equiv_status -assert
|
||||||
design -reset
|
design -reset
|
||||||
|
|
||||||
read_verilog -DSKIP_UNSUPPORTED_IGN_PARSER_CONSTRUCTS specify.v
|
read_verilog -specify <<EOT
|
||||||
|
(* blackbox *)
|
||||||
|
module test7_sub(input i, output o);
|
||||||
|
specify
|
||||||
|
(i => o) = 1;
|
||||||
|
endspecify
|
||||||
|
assign o = ~i;
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
module test7(input i, output o);
|
||||||
|
wire w;
|
||||||
|
test7_sub unused(i, w);
|
||||||
|
test7_sub used(i, o);
|
||||||
|
endmodule
|
||||||
|
EOT
|
||||||
|
hierarchy
|
||||||
|
cd test7
|
||||||
|
clean
|
||||||
|
select -assert-count 1 c:used
|
||||||
|
select -assert-none c:* c:used %d
|
||||||
|
|
Loading…
Reference in New Issue