From 1f1deda888ea32ade2478fca9fcb510ada477606 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 26 Feb 2015 18:47:39 +0100 Subject: Added non-std verilog assume() statement --- frontends/ast/ast.cc | 1 + frontends/ast/ast.h | 1 + frontends/ast/genrtlil.cc | 11 +++++++---- frontends/ast/simplify.cc | 7 +++---- frontends/verilog/verilog_frontend.cc | 12 +++++++++++- frontends/verilog/verilog_frontend.h | 3 +++ frontends/verilog/verilog_lexer.l | 5 +++-- frontends/verilog/verilog_parser.y | 10 ++++++++-- 8 files changed, 37 insertions(+), 13 deletions(-) (limited to 'frontends') diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc index 0de24013..0b63248d 100644 --- a/frontends/ast/ast.cc +++ b/frontends/ast/ast.cc @@ -90,6 +90,7 @@ std::string AST::type2str(AstNodeType type) X(AST_IDENTIFIER) X(AST_PREFIX) X(AST_ASSERT) + X(AST_ASSUME) X(AST_FCALL) X(AST_TO_BITS) X(AST_TO_SIGNED) diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h index 0c113562..d57e91e5 100644 --- a/frontends/ast/ast.h +++ b/frontends/ast/ast.h @@ -64,6 +64,7 @@ namespace AST AST_IDENTIFIER, AST_PREFIX, AST_ASSERT, + AST_ASSUME, AST_FCALL, AST_TO_BITS, diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index 4a84e0a9..c421364a 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -1265,19 +1265,22 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint) // generate $assert cells case AST_ASSERT: + case AST_ASSUME: { log_assert(children.size() == 2); RTLIL::SigSpec check = children[0]->genRTLIL(); - log_assert(check.size() == 1); + if (GetSize(check) != 1) + check = current_module->ReduceBool(NEW_ID, check); RTLIL::SigSpec en = children[1]->genRTLIL(); - log_assert(en.size() == 1); + if (GetSize(en) != 1) + en = current_module->ReduceBool(NEW_ID, en); std::stringstream sstr; - sstr << "$assert$" << filename << ":" << linenum << "$" << (autoidx++); + sstr << (type == AST_ASSERT ? "$assert$" : "$assume$") << filename << ":" << linenum << "$" << (autoidx++); - RTLIL::Cell *cell = current_module->addCell(sstr.str(), "$assert"); + RTLIL::Cell *cell = current_module->addCell(sstr.str(), type == AST_ASSERT ? "$assert" : "$assume"); cell->attributes["\\src"] = stringf("%s:%d", filename.c_str(), linenum); for (auto &attr : attributes) { diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index 404dab4e..a65d2dbb 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -1211,7 +1211,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, } skip_dynamic_range_lvalue_expansion:; - if (stage > 1 && type == AST_ASSERT && current_block != NULL) + if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME) && current_block != NULL) { std::stringstream sstr; sstr << "$assert$" << filename << ":" << linenum << "$" << (autoidx++); @@ -1255,7 +1255,7 @@ skip_dynamic_range_lvalue_expansion:; newNode->children.push_back(assign_check); newNode->children.push_back(assign_en); - AstNode *assertnode = new AstNode(AST_ASSERT); + AstNode *assertnode = new AstNode(type); assertnode->children.push_back(new AstNode(AST_IDENTIFIER)); assertnode->children.push_back(new AstNode(AST_IDENTIFIER)); assertnode->children[0]->str = id_check; @@ -1266,9 +1266,8 @@ skip_dynamic_range_lvalue_expansion:; goto apply_newNode; } - if (stage > 1 && type == AST_ASSERT && children.size() == 1) + if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME) && children.size() == 1) { - children[0] = new AstNode(AST_REDUCE_BOOL, children[0]->clone()); children.push_back(mkconst_int(1, false, 1)); did_something = true; } diff --git a/frontends/verilog/verilog_frontend.cc b/frontends/verilog/verilog_frontend.cc index 41561e80..635c9ce4 100644 --- a/frontends/verilog/verilog_frontend.cc +++ b/frontends/verilog/verilog_frontend.cc @@ -54,6 +54,10 @@ struct VerilogFrontend : public Frontend { log(" enable support for SystemVerilog features. (only a small subset\n"); log(" of SystemVerilog is supported)\n"); log("\n"); + log(" -formal\n"); + log(" enable support for assert() and assume() statements\n"); + log(" (assert support is also enabled with -sv)\n"); + log("\n"); log(" -dump_ast1\n"); log(" dump abstract syntax tree (before simplification)\n"); log("\n"); @@ -164,6 +168,7 @@ struct VerilogFrontend : public Frontend { frontend_verilog_yydebug = false; sv_mode = false; + formal_mode = false; log_header("Executing Verilog-2005 frontend.\n"); @@ -176,6 +181,10 @@ struct VerilogFrontend : public Frontend { sv_mode = true; continue; } + if (arg == "-formal") { + formal_mode = true; + continue; + } if (arg == "-dump_ast1") { flag_dump_ast1 = true; continue; @@ -271,7 +280,8 @@ struct VerilogFrontend : public Frontend { } extra_args(f, filename, args, argidx); - log("Parsing %s input from `%s' to AST representation.\n", sv_mode ? "SystemVerilog" : "Verilog", filename.c_str()); + log("Parsing %s%s input from `%s' to AST representation.\n", + formal_mode ? "formal " : "", sv_mode ? "SystemVerilog" : "Verilog", filename.c_str()); AST::current_filename = filename; AST::set_line_num = &frontend_verilog_yyset_lineno; diff --git a/frontends/verilog/verilog_frontend.h b/frontends/verilog/verilog_frontend.h index e277f3e3..5561f54c 100644 --- a/frontends/verilog/verilog_frontend.h +++ b/frontends/verilog/verilog_frontend.h @@ -51,6 +51,9 @@ namespace VERILOG_FRONTEND // running in SystemVerilog mode extern bool sv_mode; + // running in -formal mode + extern bool formal_mode; + // lexer input stream extern std::istream *lexin; } diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l index 13b3e2bf..3a57514a 100644 --- a/frontends/verilog/verilog_lexer.l +++ b/frontends/verilog/verilog_lexer.l @@ -166,8 +166,9 @@ YOSYS_NAMESPACE_END "always_ff" { SV_KEYWORD(TOK_ALWAYS); } "always_latch" { SV_KEYWORD(TOK_ALWAYS); } -"assert" { SV_KEYWORD(TOK_ASSERT); } -"property" { SV_KEYWORD(TOK_PROPERTY); } +"assert" { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); } +"assume" { if (formal_mode) return TOK_ASSUME; return TOK_ID; } +"property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); } "logic" { SV_KEYWORD(TOK_REG); } "bit" { SV_KEYWORD(TOK_REG); } diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y index fee438a9..d935cab3 100644 --- a/frontends/verilog/verilog_parser.y +++ b/frontends/verilog/verilog_parser.y @@ -57,7 +57,7 @@ namespace VERILOG_FRONTEND { std::vector case_type_stack; bool do_not_require_port_stubs; bool default_nettype_wire; - bool sv_mode; + bool sv_mode, formal_mode; std::istream *lexin; } YOSYS_NAMESPACE_END @@ -111,7 +111,7 @@ static void free_attr(std::map *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_PROPERTY +%token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME TOK_PROPERTY %type range range_or_multirange non_opt_range non_opt_multirange range_or_signed_int %type wire_type expr basic_expr concat_list rvalue lvalue lvalue_concat_list @@ -934,11 +934,17 @@ opt_label: assert: TOK_ASSERT '(' expr ')' ';' { ast_stack.back()->children.push_back(new AstNode(AST_ASSERT, $3)); + } | + TOK_ASSUME '(' expr ')' ';' { + ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $3)); }; assert_property: TOK_ASSERT TOK_PROPERTY '(' expr ')' ';' { ast_stack.back()->children.push_back(new AstNode(AST_ASSERT, $4)); + } | + TOK_ASSUME TOK_PROPERTY '(' expr ')' ';' { + ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $4)); }; simple_behavioral_stmt: -- cgit v1.2.3