Added non-std verilog assume() statement

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)

frontends/ast/ast.h

@@ -64,6 +64,7 @@ namespace AST
 		AST_IDENTIFIER,
 		AST_PREFIX,
 		AST_ASSERT,
+		AST_ASSUME,
 
 		AST_FCALL,
 		AST_TO_BITS,

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) {

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;
 	}

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;

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;
 }

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); }
+"assert"   { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); }
-"property" { SV_KEYWORD(TOK_PROPERTY); }
+"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); }
 

frontends/verilog/verilog_parser.y

@@ -57,7 +57,7 @@ namespace VERILOG_FRONTEND {
 	std::vector<char> 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<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_PROPERTY
+%token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME TOK_PROPERTY
 
 %type <ast> range range_or_multirange  non_opt_range non_opt_multirange range_or_signed_int
 %type <ast> 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:

passes/opt/opt_clean.cc

@@ -47,7 +47,7 @@ void rmunused_module_cells(Module *module, bool verbose)
 					if (bit.wire != nullptr)
 						wire2driver[bit].insert(cell);
 		}
-		if (cell->type.in("$memwr", "$meminit", "$assert") || cell->has_keep_attr())
+		if (cell->type.in("$memwr", "$meminit", "$assert", "$assume") || cell->has_keep_attr())
 			queue.insert(cell);
 		else
 			unused.insert(cell);

passes/sat/sat.cc

@@ -51,7 +51,7 @@ struct SatHelper
 	std::vector<std::pair<std::string, std::string>> sets, prove, prove_x, sets_init;
 	std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
 	std::map<int, std::vector<std::string>> unsets_at;
-	bool prove_asserts;
+	bool prove_asserts, set_assumes;
 
 	// undef constraints
 	bool enable_undef, set_init_def, set_init_undef, set_init_zero, ignore_unknown_cells;
@@ -319,20 +319,28 @@ struct SatHelper
 		}
 
 		int import_cell_counter = 0;
-		for (auto &c : module->cells_)
+		for (auto cell : module->cells())
-			if (design->selected(module, c.second)) {
+			if (design->selected(module, cell)) {
-				// log("Import cell: %s\n", RTLIL::id2cstr(c.first));
+				// log("Import cell: %s\n", RTLIL::id2cstr(cell->name));
-				if (satgen.importCell(c.second, timestep)) {
+				if (satgen.importCell(cell, timestep)) {
-					for (auto &p : c.second->connections())
+					for (auto &p : cell->connections())
-						if (ct.cell_output(c.second->type, p.first))
+						if (ct.cell_output(cell->type, p.first))
-							show_drivers.insert(sigmap(p.second), c.second);
+							show_drivers.insert(sigmap(p.second), cell);
 					import_cell_counter++;
 				} else if (ignore_unknown_cells)
-					log_warning("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
+					log_warning("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type));
 				else
-					log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
+					log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type));
 		}
 		log("Imported %d cells to SAT database.\n", import_cell_counter);
+
+		if (set_assumes) {
+			RTLIL::SigSpec assumes_a, assumes_en;
+			satgen.getAssumes(assumes_a, assumes_en, timestep);
+			for (int i = 0; i < GetSize(assumes_a); i++)
+				log("Import constraint from assume cell: %s when %s.\n", log_signal(assumes_a[i]), log_signal(assumes_en[i]));
+			ez->assume(satgen.importAssumes(timestep));
+		}
 	}
 
 	int setup_proof(int timestep = -1)
@@ -948,6 +956,9 @@ struct SatPass : public Pass {
 		log("        set or unset the specified signal to the specified value in the\n");
 		log("        given timestep. this has priority over a -set for the same signal.\n");
 		log("\n");
+		log("    -set-assumes\n");
+		log("        set all assumptions provided via $assume cells\n");
+		log("\n");
 		log("    -set-def-at <N> <signal>\n");
 		log("    -set-any-undef-at <N> <signal>\n");
 		log("    -set-all-undef-at <N> <signal>\n");
@@ -1054,7 +1065,7 @@ struct SatPass : public Pass {
 		bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false;
 		bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
 		bool ignore_unknown_cells = false, falsify = false, tempinduct_def = false, set_init_def = false;
-		bool tempinduct_baseonly = false, tempinduct_inductonly = false;
+		bool tempinduct_baseonly = false, tempinduct_inductonly = false, set_assumes = false;
 		int tempinduct_skip = 0, stepsize = 1;
 		std::string vcd_file_name, json_file_name, cnf_file_name;
 
@@ -1143,6 +1154,10 @@ struct SatPass : public Pass {
 				enable_undef = true;
 				continue;
 			}
+			if (args[argidx] == "-set-assumes") {
+				set_assumes = true;
+				continue;
+			}
 			if (args[argidx] == "-tempinduct") {
 				tempinduct = true;
 				continue;
@@ -1328,6 +1343,7 @@ struct SatPass : public Pass {
 			bool basecase_setup_init = true;
 
 			basecase.sets = sets;
+			basecase.set_assumes = set_assumes;
 			basecase.prove = prove;
 			basecase.prove_x = prove_x;
 			basecase.prove_asserts = prove_asserts;
@@ -1353,6 +1369,7 @@ struct SatPass : public Pass {
 					basecase.setup(timestep);
 
 			inductstep.sets = sets;
+			inductstep.set_assumes = set_assumes;
 			inductstep.prove = prove;
 			inductstep.prove_x = prove_x;
 			inductstep.prove_asserts = prove_asserts;
@@ -1517,6 +1534,7 @@ struct SatPass : public Pass {
 			SatHelper sathelper(design, module, enable_undef);
 
 			sathelper.sets = sets;
+			sathelper.set_assumes = set_assumes;
 			sathelper.prove = prove;
 			sathelper.prove_x = prove_x;
 			sathelper.prove_asserts = prove_asserts;