mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-03 21:09:12 +00:00
Code Activity

Add "read_verilog -noassert -noassume -assert-assumes"

Browse source 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-09-24 20:51:16 +02:00
parent eb452ffb28
commit 8fde05dfa5
3 changed files with 49 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

23
frontends/verilog/verilog_frontend.cc
View file

@ -66,12 +66,21 @@ struct VerilogFrontend : public Frontend {
log(" enable support for SystemVerilog assertions and some Yosys extensions\n");
log(" replace the implicit -D SYNTHESIS with -D FORMAL\n");
log("\n");
log(" -noassert\n");
log(" ignore assert() statements\n");
log("\n");
log(" -noassume\n");
log(" ignore assume() statements\n");
log("\n");
log(" -norestrict\n");
log(" ignore restrict() assertions\n");
log(" ignore restrict() statements\n");
log("\n");
log(" -assume-asserts\n");
log(" treat all assert() statements like assume() statements\n");
log("\n");
log(" -assert-assumes\n");
log(" treat all assume() statements like assert() statements\n");
log("\n");
log(" -dump_ast1\n");
log(" dump abstract syntax tree (before simplification)\n");
log("\n");
@ -229,6 +238,14 @@ struct VerilogFrontend : public Frontend {
formal_mode = true;
continue;
}
if (arg == "-noassert") {
noassert_mode = true;
continue;
}
if (arg == "-noassume") {
noassume_mode = true;
continue;
}
if (arg == "-norestrict") {
norestrict_mode = true;
continue;
@ -237,6 +254,10 @@ struct VerilogFrontend : public Frontend {
assume_asserts_mode = true;
continue;
}
if (arg == "-assert-assumes") {
assert_assumes_mode = true;
continue;
}
if (arg == "-dump_ast1") {
flag_dump_ast1 = true;
continue;

9
frontends/verilog/verilog_frontend.h
View file

@ -54,12 +54,21 @@ namespace VERILOG_FRONTEND
// running in -formal mode
extern bool formal_mode;
// running in -noassert mode
extern bool noassert_mode;
// running in -noassume mode
extern bool noassume_mode;
// running in -norestrict mode
extern bool norestrict_mode;
// running in -assume-asserts mode
extern bool assume_asserts_mode;
// running in -assert-assumes mode
extern bool assert_assumes_mode;
// running in -lib mode
extern bool lib_mode;

23
frontends/verilog/verilog_parser.y
View file

@ -58,7 +58,8 @@ namespace VERILOG_FRONTEND {
bool do_not_require_port_stubs;
bool default_nettype_wire;
bool sv_mode, formal_mode, lib_mode;
bool norestrict_mode, assume_asserts_mode;
bool noassert_mode, noassume_mode, norestrict_mode;
bool assume_asserts_mode, assert_assumes_mode;
bool current_wire_rand, current_wire_const;
std::istream *lexin;
}
@ -1281,16 +1282,28 @@ opt_stmt_label:
assert:
opt_stmt_label TOK_ASSERT opt_property '(' expr ')' ';' {
ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5));
if (noassert_mode)
delete $5;
else
ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5));
} |
opt_stmt_label TOK_ASSUME opt_property '(' expr ')' ';' {
ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $5));
if (noassume_mode)
delete $5;
else
ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_ASSERT : AST_ASSUME, $5));
} |
opt_stmt_label TOK_ASSERT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6));
if (noassert_mode)
delete $6;
else
ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6));
} |
opt_stmt_label TOK_ASSUME opt_property '(' TOK_EVENTUALLY expr ')' ';' {
ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $6));
if (noassume_mode)
delete $6;
else
ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_LIVE : AST_FAIR, $6));
} |
opt_stmt_label TOK_COVER opt_property '(' expr ')' ';' {
ast_stack.back()->children.push_back(new AstNode(AST_COVER, $5));