mirror of https://github.com/YosysHQ/yosys.git
Merge pull request #858 from YosysHQ/clifford/svalabels
Add support for using SVA labels in yosys-smtbmc console output
This commit is contained in:
commit
cebd21aa96
|
@ -887,8 +887,8 @@ struct Smt2Worker
|
|||
|
||||
string name_a = get_bool(cell->getPort("\\A"));
|
||||
string name_en = get_bool(cell->getPort("\\EN"));
|
||||
decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id,
|
||||
cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
|
||||
string infostr = (cell->name[0] == '$' && cell->attributes.count("\\src")) ? cell->attributes.at("\\src").decode_string() : get_id(cell);
|
||||
decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str()));
|
||||
|
||||
if (cell->type == "$cover")
|
||||
decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
|
||||
|
|
|
@ -1413,10 +1413,16 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
|
|||
if (GetSize(en) != 1)
|
||||
en = current_module->ReduceBool(NEW_ID, en);
|
||||
|
||||
std::stringstream sstr;
|
||||
sstr << celltype << "$" << filename << ":" << linenum << "$" << (autoidx++);
|
||||
IdString cellname;
|
||||
if (str.empty()) {
|
||||
std::stringstream sstr;
|
||||
sstr << celltype << "$" << filename << ":" << linenum << "$" << (autoidx++);
|
||||
cellname = sstr.str();
|
||||
} else {
|
||||
cellname = str;
|
||||
}
|
||||
|
||||
RTLIL::Cell *cell = current_module->addCell(sstr.str(), celltype);
|
||||
RTLIL::Cell *cell = current_module->addCell(cellname, celltype);
|
||||
cell->attributes["\\src"] = stringf("%s:%d", filename.c_str(), linenum);
|
||||
|
||||
for (auto &attr : attributes) {
|
||||
|
|
|
@ -1511,6 +1511,7 @@ skip_dynamic_range_lvalue_expansion:;
|
|||
newNode->children.push_back(assign_en);
|
||||
|
||||
AstNode *assertnode = new AstNode(type);
|
||||
assertnode->str = str;
|
||||
assertnode->children.push_back(new AstNode(AST_IDENTIFIER));
|
||||
assertnode->children.push_back(new AstNode(AST_IDENTIFIER));
|
||||
assertnode->children[0]->str = id_check;
|
||||
|
|
|
@ -1666,7 +1666,20 @@ struct VerificSvaImporter
|
|||
log(" importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(),
|
||||
LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile()));
|
||||
|
||||
RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
|
||||
bool is_user_declared = root->IsUserDeclared();
|
||||
|
||||
// FIXME
|
||||
if (!is_user_declared) {
|
||||
const char *name = root->Name();
|
||||
for (int i = 0; name[i]; i++) {
|
||||
if (i ? (name[i] < '0' || name[i] > '9') : (name[i] != 'i')) {
|
||||
is_user_declared = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
RTLIL::IdString root_name = module->uniquify(importer->mode_names || is_user_declared ? RTLIL::escape_id(root->Name()) : NEW_ID);
|
||||
|
||||
// parse SVA sequence into trigger signal
|
||||
|
||||
|
|
|
@ -189,10 +189,57 @@ YOSYS_NAMESPACE_END
|
|||
"always_ff" { SV_KEYWORD(TOK_ALWAYS); }
|
||||
"always_latch" { SV_KEYWORD(TOK_ALWAYS); }
|
||||
|
||||
"assert" { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); }
|
||||
"assume" { if (formal_mode) return TOK_ASSUME; SV_KEYWORD(TOK_ASSUME); }
|
||||
"cover" { if (formal_mode) return TOK_COVER; SV_KEYWORD(TOK_COVER); }
|
||||
"restrict" { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); }
|
||||
/* parse labels on assert, assume, cover, and restrict right here because it's insanley complex
|
||||
to do it in the parser (because we force the parser too early to reduce when parsing cells..) */
|
||||
([a-zA-Z_$][a-zA-Z0-9_$]*[ \t\r\n]*:[ \t\r\n]*)?(assert|assume|cover|restrict)/[^a-zA-Z0-9_$\.] {
|
||||
frontend_verilog_yylval.string = new std::string(yytext);
|
||||
auto &str = *frontend_verilog_yylval.string;
|
||||
std::string keyword;
|
||||
int cursor = 0;
|
||||
|
||||
while (1) {
|
||||
if (cursor == GetSize(str)) {
|
||||
keyword = str;
|
||||
delete frontend_verilog_yylval.string;
|
||||
frontend_verilog_yylval.string = nullptr;
|
||||
goto sva_without_label;
|
||||
}
|
||||
char c = str[cursor];
|
||||
if (c != ' ' && c != '\t' && c != '\r' && c != '\n' && c != ':') {
|
||||
cursor++;
|
||||
continue;
|
||||
}
|
||||
|
||||
keyword = str.substr(cursor);
|
||||
str = "\\" + str.substr(0, cursor);
|
||||
break;
|
||||
}
|
||||
|
||||
cursor = 0;
|
||||
while (1) {
|
||||
log_assert(cursor < GetSize(keyword));
|
||||
char c = keyword[cursor];
|
||||
if (c != ' ' && c != '\t' && c != '\r' && c != '\n' && c != ':') {
|
||||
keyword = keyword.substr(cursor);
|
||||
break;
|
||||
}
|
||||
cursor++;
|
||||
}
|
||||
|
||||
if (keyword == "assert") { return TOK_ASSERT; }
|
||||
else if (keyword == "assume") { return TOK_ASSUME; }
|
||||
else if (keyword == "cover") { return TOK_COVER; }
|
||||
else if (keyword == "restrict") { return TOK_RESTRICT; }
|
||||
else log_abort();
|
||||
|
||||
sva_without_label:
|
||||
if (keyword == "assert") { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); }
|
||||
else if (keyword == "assume") { if (formal_mode) return TOK_ASSUME; SV_KEYWORD(TOK_ASSUME); }
|
||||
else if (keyword == "cover") { if (formal_mode) return TOK_COVER; SV_KEYWORD(TOK_COVER); }
|
||||
else if (keyword == "restrict") { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); }
|
||||
else log_abort();
|
||||
}
|
||||
|
||||
"property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); }
|
||||
"rand" { if (formal_mode) return TOK_RAND; SV_KEYWORD(TOK_RAND); }
|
||||
"const" { if (formal_mode) return TOK_CONST; SV_KEYWORD(TOK_CONST); }
|
||||
|
@ -303,7 +350,7 @@ supply1 { return TOK_SUPPLY1; }
|
|||
|
||||
[a-zA-Z_$][a-zA-Z0-9_$\.]* {
|
||||
frontend_verilog_yylval.string = new std::string(std::string("\\") + yytext);
|
||||
return TOK_ID;
|
||||
return TOK_ID;
|
||||
}
|
||||
|
||||
"/*"[ \t]*(synopsys|synthesis)[ \t]*translate_off[ \t]*"*/" {
|
||||
|
|
|
@ -106,6 +106,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
|
|||
}
|
||||
|
||||
%token <string> TOK_STRING TOK_ID TOK_CONSTVAL TOK_REALVAL TOK_PRIMITIVE
|
||||
%token <string> TOK_ASSERT TOK_ASSUME TOK_RESTRICT TOK_COVER
|
||||
%token ATTR_BEGIN ATTR_END DEFATTR_BEGIN DEFATTR_END
|
||||
%token TOK_MODULE TOK_ENDMODULE TOK_PARAMETER TOK_LOCALPARAM TOK_DEFPARAM
|
||||
%token TOK_PACKAGE TOK_ENDPACKAGE TOK_PACKAGESEP
|
||||
|
@ -119,8 +120,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
|
|||
%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
|
||||
%token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME
|
||||
%token TOK_RESTRICT TOK_COVER TOK_PROPERTY TOK_ENUM TOK_TYPEDEF
|
||||
%token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_PROPERTY TOK_ENUM TOK_TYPEDEF
|
||||
%token TOK_RAND TOK_CONST TOK_CHECKER TOK_ENDCHECKER TOK_EVENTUALLY
|
||||
%token TOK_INCREMENT TOK_DECREMENT TOK_UNIQUE TOK_PRIORITY
|
||||
|
||||
|
@ -1337,9 +1337,6 @@ opt_property:
|
|||
$$ = false;
|
||||
};
|
||||
|
||||
opt_stmt_label:
|
||||
TOK_ID ':' | /* empty */;
|
||||
|
||||
modport_stmt:
|
||||
TOK_MODPORT TOK_ID {
|
||||
AstNode *modport = new AstNode(AST_MODPORT);
|
||||
|
@ -1376,83 +1373,164 @@ modport_type_token:
|
|||
TOK_INPUT {current_modport_input = 1; current_modport_output = 0;} | TOK_OUTPUT {current_modport_input = 0; current_modport_output = 1;}
|
||||
|
||||
assert:
|
||||
opt_stmt_label TOK_ASSERT opt_property '(' expr ')' ';' {
|
||||
if (noassert_mode)
|
||||
TOK_ASSERT opt_property '(' expr ')' ';' {
|
||||
if (noassert_mode) {
|
||||
delete $4;
|
||||
} else {
|
||||
AstNode *node = new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $4);
|
||||
if ($1 != nullptr)
|
||||
node->str = *$1;
|
||||
ast_stack.back()->children.push_back(node);
|
||||
}
|
||||
if ($1 != nullptr)
|
||||
delete $1;
|
||||
} |
|
||||
TOK_ASSUME opt_property '(' expr ')' ';' {
|
||||
if (noassume_mode) {
|
||||
delete $4;
|
||||
} else {
|
||||
AstNode *node = new AstNode(assert_assumes_mode ? AST_ASSERT : AST_ASSUME, $4);
|
||||
if ($1 != nullptr)
|
||||
node->str = *$1;
|
||||
ast_stack.back()->children.push_back(node);
|
||||
}
|
||||
if ($1 != nullptr)
|
||||
delete $1;
|
||||
} |
|
||||
TOK_ASSERT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
|
||||
if (noassert_mode) {
|
||||
delete $5;
|
||||
else
|
||||
ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5));
|
||||
} else {
|
||||
AstNode *node = new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $5);
|
||||
if ($1 != nullptr)
|
||||
node->str = *$1;
|
||||
ast_stack.back()->children.push_back(node);
|
||||
}
|
||||
if ($1 != nullptr)
|
||||
delete $1;
|
||||
} |
|
||||
opt_stmt_label TOK_ASSUME opt_property '(' expr ')' ';' {
|
||||
if (noassume_mode)
|
||||
TOK_ASSUME opt_property '(' TOK_EVENTUALLY expr ')' ';' {
|
||||
if (noassume_mode) {
|
||||
delete $5;
|
||||
else
|
||||
ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_ASSERT : AST_ASSUME, $5));
|
||||
} else {
|
||||
AstNode *node = new AstNode(assert_assumes_mode ? AST_LIVE : AST_FAIR, $5);
|
||||
if ($1 != nullptr)
|
||||
node->str = *$1;
|
||||
ast_stack.back()->children.push_back(node);
|
||||
}
|
||||
if ($1 != nullptr)
|
||||
delete $1;
|
||||
} |
|
||||
opt_stmt_label TOK_ASSERT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
|
||||
if (noassert_mode)
|
||||
delete $6;
|
||||
else
|
||||
ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6));
|
||||
TOK_COVER opt_property '(' expr ')' ';' {
|
||||
AstNode *node = new AstNode(AST_COVER, $4);
|
||||
if ($1 != nullptr) {
|
||||
node->str = *$1;
|
||||
delete $1;
|
||||
}
|
||||
ast_stack.back()->children.push_back(node);
|
||||
} |
|
||||
opt_stmt_label TOK_ASSUME opt_property '(' TOK_EVENTUALLY expr ')' ';' {
|
||||
if (noassume_mode)
|
||||
delete $6;
|
||||
else
|
||||
ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_LIVE : AST_FAIR, $6));
|
||||
TOK_COVER opt_property '(' ')' ';' {
|
||||
AstNode *node = new AstNode(AST_COVER, AstNode::mkconst_int(1, false));
|
||||
if ($1 != nullptr) {
|
||||
node->str = *$1;
|
||||
delete $1;
|
||||
}
|
||||
ast_stack.back()->children.push_back(node);
|
||||
} |
|
||||
opt_stmt_label TOK_COVER opt_property '(' expr ')' ';' {
|
||||
ast_stack.back()->children.push_back(new AstNode(AST_COVER, $5));
|
||||
TOK_COVER ';' {
|
||||
AstNode *node = new AstNode(AST_COVER, AstNode::mkconst_int(1, false));
|
||||
if ($1 != nullptr) {
|
||||
node->str = *$1;
|
||||
delete $1;
|
||||
}
|
||||
ast_stack.back()->children.push_back(node);
|
||||
} |
|
||||
opt_stmt_label TOK_COVER opt_property '(' ')' ';' {
|
||||
ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false)));
|
||||
} |
|
||||
opt_stmt_label TOK_COVER ';' {
|
||||
ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false)));
|
||||
} |
|
||||
opt_stmt_label TOK_RESTRICT opt_property '(' expr ')' ';' {
|
||||
if (norestrict_mode)
|
||||
delete $5;
|
||||
else
|
||||
ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $5));
|
||||
if (!$3)
|
||||
TOK_RESTRICT opt_property '(' expr ')' ';' {
|
||||
if (norestrict_mode) {
|
||||
delete $4;
|
||||
} else {
|
||||
AstNode *node = new AstNode(AST_ASSUME, $4);
|
||||
if ($1 != nullptr)
|
||||
node->str = *$1;
|
||||
ast_stack.back()->children.push_back(node);
|
||||
}
|
||||
if (!$2)
|
||||
log_file_warning(current_filename, get_line_num(), "SystemVerilog does not allow \"restrict\" without \"property\".\n");
|
||||
if ($1 != nullptr)
|
||||
delete $1;
|
||||
} |
|
||||
opt_stmt_label TOK_RESTRICT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
|
||||
if (norestrict_mode)
|
||||
delete $6;
|
||||
else
|
||||
ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $6));
|
||||
if (!$3)
|
||||
TOK_RESTRICT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
|
||||
if (norestrict_mode) {
|
||||
delete $5;
|
||||
} else {
|
||||
AstNode *node = new AstNode(AST_FAIR, $5);
|
||||
if ($1 != nullptr)
|
||||
node->str = *$1;
|
||||
ast_stack.back()->children.push_back(node);
|
||||
}
|
||||
if (!$2)
|
||||
log_file_warning(current_filename, get_line_num(), "SystemVerilog does not allow \"restrict\" without \"property\".\n");
|
||||
if ($1 != nullptr)
|
||||
delete $1;
|
||||
};
|
||||
|
||||
assert_property:
|
||||
TOK_ASSERT TOK_PROPERTY '(' expr ')' ';' {
|
||||
ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $4));
|
||||
if ($1 != nullptr) {
|
||||
ast_stack.back()->children.back()->str = *$1;
|
||||
delete $1;
|
||||
}
|
||||
} |
|
||||
TOK_ASSUME TOK_PROPERTY '(' expr ')' ';' {
|
||||
ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $4));
|
||||
if ($1 != nullptr) {
|
||||
ast_stack.back()->children.back()->str = *$1;
|
||||
delete $1;
|
||||
}
|
||||
} |
|
||||
TOK_ASSERT TOK_PROPERTY '(' TOK_EVENTUALLY expr ')' ';' {
|
||||
ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $5));
|
||||
if ($1 != nullptr) {
|
||||
ast_stack.back()->children.back()->str = *$1;
|
||||
delete $1;
|
||||
}
|
||||
} |
|
||||
TOK_ASSUME TOK_PROPERTY '(' TOK_EVENTUALLY expr ')' ';' {
|
||||
ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $5));
|
||||
if ($1 != nullptr) {
|
||||
ast_stack.back()->children.back()->str = *$1;
|
||||
delete $1;
|
||||
}
|
||||
} |
|
||||
TOK_COVER TOK_PROPERTY '(' expr ')' ';' {
|
||||
ast_stack.back()->children.push_back(new AstNode(AST_COVER, $4));
|
||||
if ($1 != nullptr) {
|
||||
ast_stack.back()->children.back()->str = *$1;
|
||||
delete $1;
|
||||
}
|
||||
} |
|
||||
TOK_RESTRICT TOK_PROPERTY '(' expr ')' ';' {
|
||||
if (norestrict_mode)
|
||||
if (norestrict_mode) {
|
||||
delete $4;
|
||||
else
|
||||
} else {
|
||||
ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $4));
|
||||
if ($1 != nullptr) {
|
||||
ast_stack.back()->children.back()->str = *$1;
|
||||
delete $1;
|
||||
}
|
||||
}
|
||||
} |
|
||||
TOK_RESTRICT TOK_PROPERTY '(' TOK_EVENTUALLY expr ')' ';' {
|
||||
if (norestrict_mode)
|
||||
if (norestrict_mode) {
|
||||
delete $5;
|
||||
else
|
||||
} else {
|
||||
ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $5));
|
||||
if ($1 != nullptr) {
|
||||
ast_stack.back()->children.back()->str = *$1;
|
||||
delete $1;
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
simple_behavioral_stmt:
|
||||
|
|
Loading…
Reference in New Issue