Merge of function black boxing

backends/rtlil/rtlil_backend.cc

@@ -303,6 +303,8 @@ void RTLIL_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Modu
 	bool print_header = flag_m || design->selected_whole_module(module->name);
 	bool print_body = !flag_n || !design->selected_whole_module(module->name);
 
+    log("Dumping module %s %d %d\n", module->name.c_str(), print_header, print_body);
+
 	if (print_header)
 	{
 		for (auto it = module->attributes.begin(); it != module->attributes.end(); ++it) {
@@ -331,36 +333,45 @@ void RTLIL_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Modu
 
 	if (print_body)
 	{
-		for (auto it : module->wires())
+		for (auto it : module->wires()) {
+			log("    testing wire\n");
 			if (!only_selected || design->selected(module, it)) {
+				log("    dumping wire\n");
 				if (only_selected)
 					f << stringf("\n");
 				dump_wire(f, indent + "  ", it);
 			}
+		}
 
 		for (auto it : module->memories)
 			if (!only_selected || design->selected(module, it.second)) {
+				log("    dumping memory\n");
 				if (only_selected)
 					f << stringf("\n");
 				dump_memory(f, indent + "  ", it.second);
 			}
 
-		for (auto it : module->cells())
+		for (auto it : module->cells()) {
+			log("    testing cell\n");
 			if (!only_selected || design->selected(module, it)) {
+				log("    dumping cell\n");
 				if (only_selected)
 					f << stringf("\n");
 				dump_cell(f, indent + "  ", it);
 			}
+		}
 
 		for (auto it : module->processes)
 			if (!only_selected || design->selected(module, it.second)) {
+				log("    dumping processes\n");
 				if (only_selected)
 					f << stringf("\n");
 				dump_proc(f, indent + "  ", it.second);
 			}
 
 		bool first_conn_line = true;
 		for (auto it = module->connections().begin(); it != module->connections().end(); ++it) {
+			log("    dumping connection\n");
 			bool show_conn = !only_selected || design->selected_whole_module(module->name);
 			if (!show_conn) {
 				RTLIL::SigSpec sigs = it->first;

backends/smt2/smt2.cc

@@ -48,7 +48,7 @@
 
 	pool<SigBit> clock_posedge, clock_negedge;
 	vector<string> ex_state_eq, ex_input_eq;
-
+    std::map<IdString, std::string> blackbox_funs;
 	std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
 	std::map<Mem*, int> memarrays;
 	std::map<int, int> bvsizes;
@@ -456,6 +456,7 @@
 
 	void export_bvop(RTLIL::Cell *cell, std::string expr, char type = 0)
 	{
+		log("export_bvop %s\n", expr.c_str());
 		RTLIL::SigSpec sig_a, sig_b;
 		RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y));
 		bool is_signed = type == 'U' ? false : cell->getParam(ID::A_SIGNED).as_bool();
@@ -537,7 +538,7 @@
 
 	void export_cell(RTLIL::Cell *cell)
 	{
-		if (verbose)
+		//if (verbose)
 			log("%*s=> export_cell %s (%s) [%s]\n", 2+2*GetSize(recursive_cells), "",
 					log_id(cell), log_id(cell->type), exported_cells.count(cell) ? "old" : "new");
 
@@ -694,6 +695,73 @@
 					return export_bvop(cell, "(bvurem A B)", 'd');
 				}
 			}
+			if (cell->type == ID($fun)) {
+				int count = cell->getParam(ID(ARG_COUNT)).as_int();
+				int width = cell->getParam(ID::Y_WIDTH).as_int();
+				bool have = false;
+				for (auto e : blackbox_funs) {
+					if (e.first==cell->getParam(ID(CALLING)).decode_string()) {
+                        have = true;
+					}
+				}
+				if (!have) {
+					std::string str = stringf("(declare-fun %s (", cell->getParam(ID(CALLING)).decode_string().c_str()+1);
+					for (int i = 0; i < count; ++i) {
+    					char s[20];
+    					snprintf(s, sizeof(s), "\\A%d_WIDTH", i);
+	    				IdString id_width = IdString(s);
+    		            int width = cell->parameters[id_width].as_int();
+                        str += stringf(" (_ BitVec %d)", width);
+					}
+					str += stringf(") (_ BitVec %d))\n", width);
+					blackbox_funs[cell->getParam(ID(CALLING)).decode_string().c_str()] = str;
+					decls.push_back(str);
+				}
+				std::string str = stringf("(%s", cell->getParam(ID(CALLING)).decode_string().c_str()+1);
+				for (int i = 0; i < count; ++i) {
+					char s[20];
+					snprintf(s, sizeof(s), "\\A%d", i);
+                    IdString id = IdString(s);
+					snprintf(s, sizeof(s), "\\A%d_SIGNED", i);
+					IdString id_signed = IdString(s);
+					snprintf(s, sizeof(s), "\\A%d_WIDTH", i);
+					IdString id_width = IdString(s);
+		            int width = cell->parameters[id_width].as_int();
+               		bool is_signed = cell->parameters[id_signed].as_bool();
+            		RTLIL::SigSpec sig;
+        			sig = cell->getPort(id);
+		        	sig.extend_u0(width, is_signed);
+					str += " ";
+                    str += get_bv(sig);
+				}
+				str += ")";
+				log("Here 0\n");
+         		RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y));
+
+				log("Here 1\n");
+    	    	if (width != GetSize(sig_y)) // } && type != 'b')
+	    	    	str = stringf("((_ extract %d 0) %s)", GetSize(sig_y)-1, str.c_str());
+
+				log("Here 2\n");
+		        if (verbose)
+			        log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
+
+         		//if (type == 'b') {
+		        //	decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
+				//    	get_id(module), idcounter, get_id(module), str.c_str(), log_signal(sig_y)));
+        		//	register_boolvec(sig_y, idcounter++);
+		        //} else {
+    				log("Here 3\n");
+			        decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+					    get_id(module), idcounter, get_id(module), GetSize(sig_y), str.c_str(), log_signal(sig_y)));
+    				log("Here 4\n");
+			        register_bv(sig_y, idcounter++);
+		        //}
+				log("Here 5\n");
+    			recursive_cells.erase(cell);
+				return;
+			}
+
 			// "div" = flooring division
 			if (cell->type == ID($divfloor)) {
 				if (cell->getParam(ID::A_SIGNED).as_bool()) {

examples/funabs/multiplier/multiplier.v

@@ -0,0 +1,146 @@
+`timescale 1ns / 1ps
+// fpga4student.com FPGA projects, Verilog projects, VHDL projects
+// multiplier 4x4 using Shift/Add Algorithm and 2-phase clocking system
+// Verilog project: Verilog code for multiplier
+
+function [8:0] concat54;
+    input [4:0] a;
+    input [3:0] b;
+    begin
+        concat54 = {a,b};
+    end
+endfunction
+
+function [4:0] concat14;
+    input [0:0] a;
+    input [3:0] b;
+    begin
+        concat14 = {a,b};
+    end
+endfunction
+
+function [3:0] high54;
+    input [8:0] a;
+    begin
+        high54 = a[7:4];
+    end
+endfunction
+
+function [3:0] low54;
+    input [8:0] a;
+    begin
+        low54 = a[3:0];
+    end
+endfunction
+
+function lowbit;
+    input [8:0] a;
+    begin
+        lowbit = a[0];
+    end
+endfunction
+
+function high9;
+    input [8:0] a;
+    begin
+        high9 = a[8:8];
+    end
+endfunction
+
+function [7:0] low18;
+    input [8:0] a;
+    begin
+        low18 = a[7:0];
+    end
+endfunction
+
+function [4:0] add54;
+    input [4:0] a;
+    input [3:0] b;
+    begin
+        add54 = a+b;
+    end
+endfunction
+
+function [8:0] shiftright9;
+    input [8:0] a;
+    begin
+        shiftright9 = {1'b0,a[8:1]};
+    end
+endfunction
+
+function [8:0] accumulate;
+   input [8:0] acc;
+   input [3:0] b;
+   begin
+      accumulate = {1'b0,acc[7:4],acc[3:0]} + b;
+   end
+endfunction
+
+module mult_4x4(
+         input clk,reset,start, 
+         input[3:0] A,B, 
+         output [7:0] O, output Finish
+             );
+reg [7:0] O;
+wire Finish;  
+wire Phi0,Phi1;// 2 phase clocking
+wire m1,m2,m3,m4;
+
+// state machine
+reg[3:0] State;
+
+// Accumulator
+reg [8:0] ACC; // Accumulator
+
+reg [3:0] Asave;
+reg [3:0] Bsave;
+
+// logic to create 2 phase clocking when starting
+//nand u0(m1,start,m2);
+//buf #20 u1(m2,m1);
+//buf #10 u2(Phi0,m1);// First phase clocking
+//not #2 u5(m4,Phi0);
+//assign m3=~m1; 
+//and #2 u4(Phi1,m3,m4);// Second phase clocking
+
+assign Finish = (State==9)? 1'b1:1'b0; // Finish Flag
+assign O = low18(ACC); 
+
+initial assume (State==12);
+
+// FSM
+always @(posedge clk) begin
+    if(reset) begin
+        State <= 0;
+        ACC <= 0;
+    end else begin
+        //if((Phi0==1'b1) || (Phi1==1'b1)) begin // 2 phase clocking
+        if (State==0) begin
+            ACC <= concat54(5'b00000,A); // begin cycle
+            Asave <= A;
+            Bsave <= B;
+            State <= 1;
+        end else if(State==1 || State == 3 || State ==5 || State ==7) begin
+            if (ACC[0] == 1'b1) begin // add multiplicand
+                ACC <= concat54(add54(concat14(1'b0,high54(ACC)),Bsave),low54(ACC));
+                State <= State + 1;
+            end else begin
+                ACC <= shiftright9(ACC);// shift right
+                State <= State + 2;
+            end
+        end else if(State==2 || State == 4 || State ==6 || State ==8) begin
+                // shift State
+            ACC <= shiftright9(ACC);// shift right
+            State <= State + 1;
+        end else if(State == 9) begin
+            State <= 0;
+        end else begin
+            State <= 10;
+        end
+    end
+    mult_correct: assert (~Finish || (O==Asave*Bsave));
+end
+
+endmodule
+

examples/funabs/multiplier/multiplier_orig.v

@@ -0,0 +1,74 @@
+`timescale 1ns / 1ps
+// fpga4student.com FPGA projects, Verilog projects, VHDL projects
+// multiplier 4x4 using Shift/Add Algorithm and 2-phase clocking system
+// Verilog project: Verilog code for multiplier
+
+module mult_4x4(
+         input clk,reset,start, 
+         input[3:0] A,B, 
+         output [7:0] O, output Finish
+             );
+reg [7:0] O;
+wire Finish;  
+wire Phi0,Phi1;// 2 phase clocking
+wire m1,m2,m3,m4;
+
+// state machine
+reg[3:0] State;
+
+// Accumulator
+reg [8:0] ACC; // Accumulator
+
+reg [3:0] Asave;
+reg [3:0] Bsave;
+
+// logic to create 2 phase clocking when starting
+//nand u0(m1,start,m2);
+//buf #20 u1(m2,m1);
+//buf #10 u2(Phi0,m1);// First phase clocking
+//not #2 u5(m4,Phi0);
+//assign m3=~m1; 
+//and #2 u4(Phi1,m3,m4);// Second phase clocking
+
+assign Finish = (State==9)? 1'b1:1'b0; // Finish Flag
+assign O = ACC[7:0];
+
+initial assume (State==12);
+
+// FSM
+always @(posedge clk) begin
+    if(reset) begin
+        State <= 0; 
+        ACC <= 0; 
+    end else begin 
+        //if((Phi0==1'b1) || (Phi1==1'b1)) begin // 2 phase clocking
+        if (State==0) begin
+            ACC[8:4] <= 5'b00000; // begin cycle
+            ACC[3:0] <= A; // Load A
+            Asave <= A;
+            Bsave <= B;
+            State <= 1;
+        end else if(State==1 || State == 3 || State ==5 || State ==7) begin
+                // add/shift State
+            if (ACC[0] == 1'b1) begin // add multiplicand
+                ACC[8:4] <= {1'b0,ACC[7:4]} + Bsave; 
+                State <= State + 1;
+            end else begin
+                ACC <= {1'b0,ACC[8:1]};// shift right
+                State <= State + 2;
+            end
+        end else if(State==2 || State == 4 || State ==6 || State ==8) begin 
+                // shift State
+            ACC <= {1'b0,ACC[8:1]}; // shift right
+            State <= State + 1;
+        end else if(State == 9) begin
+            State <= 0;
+        end else begin
+            State <= 10;
+        end
+    end
+    mult_correct: assert (~Finish || (O==Asave*Bsave));
+end 
+
+endmodule
+

examples/funabs/multiplier/run.sby

@@ -0,0 +1,13 @@
+[options]
+mode bmc
+depth 100
+
+[engines]
+smtbmc
+
+[script]
+read -formal multiplier.v
+prep -top mult_4x4
+
+[files]
+multiplier.v