From: Ahmed Irfan <irfan@ubuntu.(none)>
Date: Mon, 20 Jan 2014 09:45:02 +0000 (+0100)
Subject: assert feature
X-Git-Tag: yosys-0.2.0~146^2~7^2~3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c347f2825f150451e6fb82d3c1d65015cd5405d8;p=yosys.git

assert feature
---

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 866bfe52a..8377b2591 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -96,13 +96,16 @@ struct BtorDumper
 		}
 		curr_cell.clear();
 		cell_type_translation = { 
+					//assert
+					{"$assert","root"},					
 					//unary
 					{"$not","not"},{"$neg","neg"},{"$reduce_and","redand"},
 					{"$reduce_or","redor"},{"$reduce_xor","redxor"},{"$reduce_bool","redor"},
 					//binary
 					{"$and","and"},{"$or","or"},{"$xor","xor"},{"$xnor","xnor"},
 					{"$shr","srl"},{"$shl","sll"},{"$sshr","sra"},{"$sshl","sll"},
-					{"$lt","ult"},{"$le","ulte"},{"$eq","eq"},{"$ne","ne"},{"$gt","ugt"},{"$ge","ugte"},
+					{"$lt","ult"},{"$le","ulte"},{"$gt","ugt"},{"$ge","ugte"},
+					{"$eq","eq"},{"$eqx","eq"},{"$ne","ne"},{"$nex","ne"},
 					{"$add","add"},{"$sub","sub"},{"$mul","mul"},{"$mod","urem"},{"$div","udiv"},
 					//mux
 					{"$mux","cond"},
@@ -365,6 +368,31 @@ struct BtorDumper
 		if(it==std::end(line_ref))
 		{
 			curr_cell = cell->name;
+			//assert cell
+			if(cell->type == "$assert")
+			{
+				log("writing assert cell - %s\n", cstr(cell->type));
+				const RTLIL::SigSpec* expr = &cell->connections.at(RTLIL::IdString("\\A"));
+				const RTLIL::SigSpec* en = &cell->connections.at(RTLIL::IdString("\\EN"));
+				assert(expr->width == 1);
+				assert(en->width == 1);
+				int expr_line = dump_sigspec(expr, 1);
+				int en_line = dump_sigspec(en, 1);
+				int one_line = ++line_num;
+				str = stringf("%d one 1", line_num);
+				fprintf(f, "%s\n", str.c_str());
+				++line_num;
+				str = stringf("%d %s %d %d %d", line_num, cell_type_translation.at("$eq").c_str(), 1, en_line, one_line);
+				fprintf(f, "%s\n", str.c_str());
+				++line_num;
+				str = stringf("%d %s %d %d %d %d", line_num, cell_type_translation.at("$mux").c_str(), 1, line_num-1,
+					expr_line, one_line);
+				fprintf(f, "%s\n", str.c_str());
+				int cell_line = ++line_num;
+				str = stringf("%d %s %d %d", line_num, cell_type_translation.at("$assert").c_str(), 1, line_num-1);
+				fprintf(f, "%s\n", str.c_str());
+				line_ref[cell->name]=cell_line;
+			}
 			//unary cells
 			if(cell->type == "$not" || cell->type == "$neg" || cell->type == "$pos" || cell->type == "$reduce_and" ||
 				cell->type == "$reduce_or" || cell->type == "$reduce_xor" || cell->type == "$reduce_bool")
@@ -417,12 +445,13 @@ struct BtorDumper
 			}
 			//binary cells
 			else if(cell->type == "$and" || cell->type == "$or" || cell->type == "$xor" || cell->type == "$xnor" ||
-				 cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || 
-				 cell->type == "$ne" || cell->type == "$ge" || cell->type == "$gt" )
+				 cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" || 
+				 cell->type == "$eqx" || cell->type == "$nex" || cell->type == "$ge" || cell->type == "$gt" )
 			{
 				log("writing binary cell - %s\n", cstr(cell->type));
 				int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
-				assert(!(cell->type == "$eq" || cell->type == "$ne" || cell->type == "$ge" || cell->type == "$gt") || output_width == 1);
+				assert(!(cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex" ||
+					cell->type == "$ge" || cell->type == "$gt") || output_width == 1);
 				bool l1_signed = cell->parameters.at(RTLIL::IdString("\\A_SIGNED")).as_bool();
 				bool l2_signed = cell->parameters.at(RTLIL::IdString("\\B_SIGNED")).as_bool();
 				int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
@@ -439,7 +468,8 @@ struct BtorDumper
 				++line_num;
 				std::string op = cell_type_translation.at(cell->type);
 				if(cell->type == "$lt" || cell->type == "$le" ||
-				 cell->type == "$eq" || cell->type == "$ne" || cell->type == "$ge" || cell->type == "$gt")
+				 cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex" ||
+				 cell->type == "$ge" || cell->type == "$gt")
 				{
 					if(l1_signed)
 						op = s_cell_type_translation.at(cell->type);
@@ -717,7 +747,7 @@ struct BtorDumper
 		{
 			output_sig = &cell->connections.at(RTLIL::IdString("\\DATA"));
 		}
-		else if(cell->type == "$memwr")
+		else if(cell->type == "$memwr" || cell->type == "$assert")
 		{
 			//no output
 		}
@@ -884,9 +914,10 @@ struct BtorBackend : public Backend {
 					top_module_name = mod_it.first;
 
 		fprintf(f, "; Generated by %s\n", yosys_version_str);
-		fprintf(f, "; BTOR Backend developed by Ahmed Irfan <irfan@fbk.eu>\n");
-		fprintf(f, ";  at Fondazione Bruno Kessler, Trento, Italy\n");
-
+		fprintf(f, ";  %s developed and maintained by Clifford Wolf <clifford@clifford.at>\n", yosys_version_str);
+		fprintf(f, "; BTOR Backend developed by Ahmed Irfan <irfan@fbk.eu> - Fondazione Bruno Kessler, Trento, Italy\n");
+		fprintf(f, ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\n");
+		
 		std::vector<RTLIL::Module*> mod_list;
 
 		for (auto module_it : design->modules)