Merge remote-tracking branch 'upstream/master'

.gitignore

@@ -34,3 +34,4 @@
 /libyosys.so
 /tests/unit/bintest/
 /tests/unit/objtest/
+/tests/ystests

.travis/setup.sh

@@ -64,7 +64,7 @@ if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then
 		brew tap Homebrew/bundle
 		brew bundle
 		brew install ccache
-		brew install gcc
+		brew install gcc@7
 		echo
 		echo -en 'travis_fold:end:before_install.brew\\r'
 		echo

CodingReadme

@@ -373,6 +373,7 @@ Finally run all tests with "make config-{clang,gcc,gcc-4.8}":
 	cd ~yosys
 	make clean
 	make test
+	make ystests
 	make vloghtb
 	make install
 

Makefile

@@ -585,6 +585,14 @@ vloghtb: $(TARGETS) $(EXTRA_TARGETS)
 	@echo "  Passed \"make vloghtb\"."
 	@echo ""
 
+ystests: $(TARGETS) $(EXTRA_TARGETS)
+	rm -rf tests/ystests
+	git clone https://github.com/YosysHQ/yosys-tests.git tests/ystests
+	+PATH="$$PWD:$$PATH" cd tests/ystests && $(MAKE)
+	@echo ""
+	@echo "  Finished \"make ystests\"."
+	@echo ""
+
 # Unit test
 unit-test: libyosys.so
 	@$(MAKE) -C $(UNITESTPATH) CXX="$(CXX)" CPPFLAGS="$(CPPFLAGS)" \

backends/verilog/verilog_backend.cc

@@ -779,6 +779,19 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		return true;
 	}
 
+	if (cell->type == "$lut")
+	{
+		f << stringf("%s" "assign ", indent.c_str());
+		dump_sigspec(f, cell->getPort("\\Y"));
+		f << stringf(" = ");
+		dump_const(f, cell->parameters.at("\\LUT"));
+		f << stringf(" >> ");
+		dump_attributes(f, "", cell->attributes, ' ');
+		dump_sigspec(f, cell->getPort("\\A"));
+		f << stringf(";\n");
+		return true;
+	}
+
 	if (cell->type == "$dffsr")
 	{
 		SigSpec sig_clk = cell->getPort("\\CLK");

frontends/verific/verific.cc

@@ -64,6 +64,7 @@ YOSYS_NAMESPACE_BEGIN
 int verific_verbose;
 bool verific_import_pending;
 string verific_error_msg;
+int verific_sva_fsm_limit;
 
 vector<string> verific_incdirs, verific_libdirs;
 
@@ -1618,6 +1619,8 @@ struct VerificExtNets
 
 void verific_import(Design *design, std::string top)
 {
+	verific_sva_fsm_limit = 16;
+
 	std::set<Netlist*> nl_todo, nl_done;
 
 	{
@@ -1789,6 +1792,9 @@ struct VerificPass : public Pass {
 		log("  -nosva\n");
 		log("    Ignore SVA properties, do not infer checker logic.\n");
 		log("\n");
+		log("  -L <int>\n");
+		log("    Maximum number of ctrl bits for SVA checker FSMs (default=16).\n");
+		log("\n");
 		log("  -n\n");
 		log("    Keep all Verific names on instances and nets. By default only\n");
 		log("    user-declared names are preserved.\n");
@@ -1830,6 +1836,7 @@ struct VerificPass : public Pass {
 		}
 
 		verific_verbose = 0;
+		verific_sva_fsm_limit = 16;
 
 		const char *release_str = Message::ReleaseString();
 		time_t release_time = Message::ReleaseDate();
@@ -2036,6 +2043,10 @@ struct VerificPass : public Pass {
 					mode_nosva = true;
 					continue;
 				}
+				if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
+					verific_sva_fsm_limit = atoi(args[++argidx].c_str());
+					continue;
+				}
 				if (args[argidx] == "-n") {
 					mode_names = true;
 					continue;

frontends/verific/verific.h

@@ -101,6 +101,8 @@ void verific_import_sva_cover(VerificImporter *importer, Verific::Instance *inst
 void verific_import_sva_trigger(VerificImporter *importer, Verific::Instance *inst);
 bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net);
 
+extern int verific_sva_fsm_limit;
+
 YOSYS_NAMESPACE_END
 
 #endif

frontends/verific/verificsva.cc

@@ -466,13 +466,14 @@ struct SvaFsm
 
 		dnode.ctrl.sort_and_unify();
 
-		if (GetSize(dnode.ctrl) > 16) {
+		if (GetSize(dnode.ctrl) > verific_sva_fsm_limit) {
 			if (verific_verbose >= 2) {
 				log("    detected state explosion in DFSM generation:\n");
 				dump();
 				log("      ctrl signal: %s\n", log_signal(dnode.ctrl));
 			}
-			log_error("SVA DFSM state ctrl signal has %d (>16) bits. Stopping to prevent exponential design size explosion.\n", GetSize(dnode.ctrl));
+			log_error("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n",
+					GetSize(dnode.ctrl), verific_sva_fsm_limit);
 		}
 
 		for (int i = 0; i < (1 << GetSize(dnode.ctrl)); i++)

passes/cmds/setundef.cc

@@ -162,7 +162,6 @@ struct SetundefPass : public Pass {
 				continue;
 			}
 			if (args[argidx] == "-expose") {
-				got_value = true;
 				expose_mode = true;
 				continue;
 			}
@@ -212,6 +211,13 @@ struct SetundefPass : public Pass {
 		}
 		extra_args(args, argidx, design);
 
+		if (!got_value && expose_mode) {
+			log("Using default as -undef with -expose.\n");
+			got_value = true;
+			worker.next_bit_mode = MODE_UNDEF;
+			worker.next_bit_state = 0;
+		}
+
 		if (expose_mode && !undriven_mode)
 			log_cmd_error("Option -expose must be used with option -undriven.\n");
 		if (!got_value)

passes/sat/sim.cc

@@ -778,7 +778,7 @@ struct SimPass : public Pass {
 		log("        number of cycles to simulate (default: 20)\n");
 		log("\n");
 		log("    -a\n");
-		log("        include all nets in VCD output, nut just those with public names\n");
+		log("        include all nets in VCD output, not just those with public names\n");
 		log("\n");
 		log("    -w\n");
 		log("        writeback mode: use final simulation state as new init state\n");

techlibs/ice40/cells_sim.v

@@ -920,19 +920,40 @@ parameter A_SIGNED = 1'b0;
 parameter B_SIGNED = 1'b0;
 endmodule
 
-(* blackbox *)
-module SB_SPRAM256KA(
+module SB_SPRAM256KA (
 	input [13:0] ADDRESS,
 	input [15:0] DATAIN,
 	input [3:0] MASKWREN,
-	input WREN,
-	input CHIPSELECT,
-	input CLOCK,
-	input STANDBY,
-	input SLEEP,
-	input POWEROFF,
-	output [15:0] DATAOUT
+	input WREN, CHIPSELECT, CLOCK, STANDBY, SLEEP, POWEROFF,
+	output reg [15:0] DATAOUT
 );
+`ifndef BLACKBOX
+	reg [15:0] mem [0:16383];
+	wire off = SLEEP || !POWEROFF;
+	integer i;
+
+	always @(negedge POWEROFF) begin
+		for (i = 0; i <= 16383; i = i+1)
+			mem[i] = 'bx;
+	end
+
+	always @(posedge CLOCK, posedge off) begin
+		if (off) begin
+			DATAOUT <= 0;
+		end else
+		if (CHIPSELECT && !STANDBY && !WREN) begin
+			DATAOUT <= mem[ADDRESS];
+		end else begin
+			if (CHIPSELECT && !STANDBY && WREN) begin
+				if (MASKWREN[0]) mem[ADDRESS][ 3: 0] = DATAIN[ 3: 0];
+				if (MASKWREN[1]) mem[ADDRESS][ 7: 4] = DATAIN[ 7: 4];
+				if (MASKWREN[2]) mem[ADDRESS][11: 8] = DATAIN[11: 8];
+				if (MASKWREN[3]) mem[ADDRESS][15:12] = DATAIN[15:12];
+			end
+			DATAOUT <= 'bx;
+		end
+	end
+`endif
 endmodule
 
 (* blackbox *)