Merge remote-tracking branch 'origin/master' into xc7dsp

CHANGELOG

@@ -39,6 +39,7 @@ Yosys 0.9 .. Yosys 0.9-dev
     - Added "xilinx_srl" for Xilinx shift register extraction
     - Removed "shregmap -tech xilinx" (superseded by "xilinx_srl")
     - Added "_TECHMAP_WIREINIT_*_" attribute and "_TECHMAP_REMOVEINIT_*_" wire for "techmap" pass
+    - Added "-match-init" option to "dff2dffs" pass
     - Added +/mul2dsp.v for decomposing wide multipliers to custom-sized ones
     - Added "xilinx_dsp" for Xilinx DSP packing
     - "synth_xilinx" to now infer DSP blocks (-nodsp to disable)

backends/smt2/Makefile.inc

@@ -16,7 +16,7 @@ yosys-smtbmc-script.py: backends/smt2/smtbmc.py
 		-e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@
 
 yosys-smtbmc.exe: misc/launcher.c yosys-smtbmc-script.py
-	$(P) gcc -DGUI=0 -O -s -o $@ $<
+	$(P) $(CXX) -DGUI=0 -O -s -o $@ $<
 # Other targets
 else
 TARGETS += yosys-smtbmc

misc/launcher.c

@@ -65,7 +65,7 @@ SOFTWARE. */
 
 int child_pid=0;
 
-int fail(char *format, char *data) {
+int fail(const char *format, const char *data) {
     /* Print error message to stderr and return 2 */
     fprintf(stderr, format, data);
     return 2;
@@ -76,7 +76,7 @@ char *quoted(char *data) {
 
     /* We allocate twice as much space as needed to deal with worse-case
        of having to escape everything. */
-    char *result = calloc(ln*2+3, sizeof(char));
+    char *result = (char *)calloc(ln*2+3, sizeof(char));
     char *presult = result;
 
     *presult++ = '"';
@@ -120,7 +120,7 @@ char *loadable_exe(char *exename) {
     if (!hPython) return NULL; */
 
     /* Return the absolute filename for spawnv */
-    result = calloc(MAX_PATH, sizeof(char));
+    result = (char *)calloc(MAX_PATH, sizeof(char));
     strncpy(result, exename, MAX_PATH);
     /*if (result) GetModuleFileNameA(hPython, result, MAX_PATH);
 
@@ -158,7 +158,7 @@ char **parse_argv(char *cmdline, int *argc)
 {
     /* Parse a command line in-place using MS C rules */
 
-    char **result = calloc(strlen(cmdline), sizeof(char *));
+    char **result = (char **)calloc(strlen(cmdline), sizeof(char *));
     char *output = cmdline;
     char c;
     int nb = 0;

passes/equiv/equiv_opt.cc

@@ -46,6 +46,9 @@ struct EquivOptPass:public ScriptPass
 		log("    -assert\n");
 		log("        produce an error if the circuits are not equivalent.\n");
 		log("\n");
+		log("    -multiclock\n");
+		log("        run clk2fflogic before equivalence checking.\n");
+		log("\n");
 		log("    -undef\n");
 		log("        enable modelling of undef states during equiv_induct.\n");
 		log("\n");
@@ -55,7 +58,7 @@ struct EquivOptPass:public ScriptPass
 	}
 
 	std::string command, techmap_opts;
-	bool assert, undef;
+	bool assert, undef, multiclock;
 
 	void clear_flags() YS_OVERRIDE
 	{
@@ -63,6 +66,7 @@ struct EquivOptPass:public ScriptPass
 		techmap_opts = "";
 		assert = false;
 		undef = false;
+		multiclock = false;
 	}
 
 	void execute(std::vector < std::string > args, RTLIL::Design * design) YS_OVERRIDE
@@ -92,6 +96,10 @@ struct EquivOptPass:public ScriptPass
 				undef = true;
 				continue;
 			}
+			if (args[argidx] == "-multiclock") {
+				multiclock = true;
+				continue;
+			}
 			break;
 		}
 
@@ -146,6 +154,8 @@ struct EquivOptPass:public ScriptPass
 		}
 
 		if (check_label("prove")) {
+			if (multiclock || help_mode)
+				run("clk2fflogic", "(only with -multiclock)");
 			run("equiv_make gold gate equiv");
 			if (help_mode)
 				run("equiv_induct [-undef] equiv");

passes/opt/opt_share.cc

@@ -108,12 +108,13 @@ bool cell_supported(RTLIL::Cell *cell)
 	return false;
 }
 
-std::map<IdString, IdString> mergeable_type_map{
-  {ID($sub), ID($add)},
-};
+std::map<IdString, IdString> mergeable_type_map;
 
 bool mergeable(RTLIL::Cell *a, RTLIL::Cell *b)
 {
+	if (mergeable_type_map.empty()) {
+		mergeable_type_map.insert({ID($sub), ID($add)});
+	}
 	auto a_type = a->type;
 	if (mergeable_type_map.count(a_type))
 		a_type = mergeable_type_map.at(a_type);

passes/techmap/dff2dffs.cc

@@ -34,11 +34,16 @@ struct Dff2dffsPass : public Pass {
 		log("Merge synchronous set/reset $_MUX_ cells to create $__DFFS_[NP][NP][01], to be run before\n");
 		log("dff2dffe for SR over CE priority.\n");
 		log("\n");
+		log("    -match-init\n");
+		log("        Disallow merging synchronous set/reset that has polarity opposite of the\n");
+		log("        output wire's init attribute (if any).\n");
+		log("\n");
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 	{
 		log_header(design, "Executing dff2dffs pass (merge synchronous set/reset into FF cells).\n");
 
+		bool match_init = false;
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++)
 		{
@@ -46,6 +51,10 @@ struct Dff2dffsPass : public Pass {
 			// 	singleton_mode = true;
 			// 	continue;
 			// }
+			if (args[argidx] == "-match-init") {
+				match_init = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -96,9 +105,6 @@ struct Dff2dffsPass : public Pass {
 				SigBit bit_b = sigmap(mux_cell->getPort(ID::B));
 				SigBit bit_s = sigmap(mux_cell->getPort(ID(S)));
 
-				log("  Merging %s (A=%s, B=%s, S=%s) into %s (%s).\n", log_id(mux_cell),
-						log_signal(bit_a), log_signal(bit_b), log_signal(bit_s), log_id(cell), log_id(cell->type));
-
 				SigBit sr_val, sr_sig;
 				bool invert_sr;
 				sr_sig = bit_s;
@@ -113,6 +119,23 @@ struct Dff2dffsPass : public Pass {
 					invert_sr = false;
 				}
 
+				if (match_init) {
+					SigBit bit_q = cell->getPort(ID(Q));
+					if (bit_q.wire) {
+						auto it = bit_q.wire->attributes.find(ID(init));
+						if (it != bit_q.wire->attributes.end()) {
+							auto init_val = it->second[bit_q.offset];
+							if (init_val == State::S1 && sr_val != State::S1)
+								continue;
+							if (init_val == State::S0 && sr_val != State::S0)
+								continue;
+						}
+					}
+				}
+
+				log("  Merging %s (A=%s, B=%s, S=%s) into %s (%s).\n", log_id(mux_cell),
+						log_signal(bit_a), log_signal(bit_b), log_signal(bit_s), log_id(cell), log_id(cell->type));
+
 				if (sr_val == State::S1) {
 					if (cell->type == ID($_DFF_N_)) {
 						if (invert_sr) cell->type = ID($__DFFS_NN1_);

tests/ice40/div_mod.ys

@@ -4,6 +4,6 @@ flatten
 equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
-select -assert-count 62 t:SB_LUT4
+select -assert-count 59 t:SB_LUT4
 select -assert-count 41 t:SB_CARRY
 select -assert-none t:SB_LUT4 t:SB_CARRY %% t:* %D

tests/techmap/dff2dffs.ys

@@ -0,0 +1,50 @@
+read_verilog << EOT
+module top(...);
+input clk;
+input d;
+input sr;
+output reg q0, q1, q2, q3, q4, q5;
+
+initial q0 = 1'b0;
+initial q1 = 1'b0;
+initial q2 = 1'b1;
+initial q3 = 1'b1;
+initial q4 = 1'bx;
+initial q5 = 1'bx;
+
+always @(posedge clk) begin
+	q0 <= sr ? 1'b0 : d;
+	q1 <= sr ? 1'b1 : d;
+	q2 <= sr ? 1'b0 : d;
+	q3 <= sr ? 1'b1 : d;
+	q4 <= sr ? 1'b0 : d;
+	q5 <= sr ? 1'b1 : d;
+end
+
+endmodule
+EOT
+
+proc
+simplemap
+design -save ref
+
+dff2dffs
+clean
+
+select -assert-count 1 w:q0 %x t:$__DFFS_PP0_ %i
+select -assert-count 1 w:q1 %x t:$__DFFS_PP1_ %i
+select -assert-count 1 w:q2 %x t:$__DFFS_PP0_ %i
+select -assert-count 1 w:q3 %x t:$__DFFS_PP1_ %i
+select -assert-count 1 w:q4 %x t:$__DFFS_PP0_ %i
+select -assert-count 1 w:q5 %x t:$__DFFS_PP1_ %i
+
+design -load ref
+dff2dffs -match-init
+clean
+
+select -assert-count 1 w:q0 %x t:$__DFFS_PP0_ %i
+select -assert-count 0 w:q1 %x t:$__DFFS_PP1_ %i
+select -assert-count 0 w:q2 %x t:$__DFFS_PP0_ %i
+select -assert-count 1 w:q3 %x t:$__DFFS_PP1_ %i
+select -assert-count 1 w:q4 %x t:$__DFFS_PP0_ %i
+select -assert-count 1 w:q5 %x t:$__DFFS_PP1_ %i

tests/various/equiv_opt_multiclock.ys

@@ -0,0 +1,12 @@
+read_verilog <<EOT
+module top(input clk, pre, d, output reg q);
+	always @(posedge clk, posedge pre)
+		if (pre)
+			q <= 1'b1;
+		else
+			q <= d;
+endmodule
+EOT
+
+prep
+equiv_opt -assert -multiclock -map +/simcells.v synth