Merge remote-tracking branch 'upstream' into merge3

backends/aiger/xaiger.cc

@@ -95,7 +95,7 @@ struct XAigerWriter
 		}
 
 		bit2aig_stack.push_back(bit);
-		
+
 		// NB: Cannot use iterator returned from aig_map.insert()
 		//     since this function is called recursively
 

backends/btor/test_cells.sh

@@ -27,4 +27,3 @@ for fn in test_*.il; do
 done
 
 echo "OK."
-

backends/cxxrtl/runtime/README.txt

@@ -15,4 +15,4 @@ file of the simulation toplevel).
 The interfaces declared in `cxxrtl*.h` (without `capi`) are unstable and may change without notice.
 
 For clarity, all of the files in this directory and its subdirectories have unique names regardless
-of the directory where they are placed.
+of the directory where they are placed.

backends/edif/runtest.py

@@ -118,4 +118,3 @@ os.system("set -x; ./test_gold > test_gold.out")
 os.system("set -x; ./test_gate > test_gate.out")
 
 os.system("set -x; md5sum test_gold.out test_gate.out")
-

backends/functional/smtlib.cc

@@ -187,7 +187,7 @@ struct SmtModule {
 	Functional::IR ir;
 	SmtScope scope;
 	std::string name;
-	
+
 	SmtStruct input_struct;
 	SmtStruct output_struct;
 	SmtStruct state_struct;
@@ -256,7 +256,7 @@ struct SmtModule {
 	}
 
 	void write(std::ostream &out)
-	{    
+	{
 		SExprWriter w(out);
 
 		input_struct.write_definition(w);
@@ -266,7 +266,7 @@ struct SmtModule {
 		w << list("declare-datatypes",
 			list(list("Pair", 2)),
 			list(list("par", list("X", "Y"), list(list("pair", list("first", "X"), list("second", "Y"))))));
-		
+
 		write_eval(w);
 		write_initial(w);
 	}

backends/functional/smtlib_rosette.cc

@@ -304,7 +304,7 @@ struct SmtrModule {
 	}
 
 	void write(std::ostream &out)
-	{    
+	{
 		SExprWriter w(out);
 
 		input_struct.write_definition(w);

backends/functional/test_generic.cc

@@ -46,7 +46,7 @@ struct MemContentsTest {
 		error:
 		printf("FAIL\n");
 		int digits = (data_width + 3) / 4;
-		
+
 		for(auto addr = 0; addr < (1<<addr_width); addr++) {
 			if(addr % 8 == 0) printf("%.8x   ", addr);
 			auto it = reference.find(addr);

backends/simplec/test00_uut.v

@@ -11,4 +11,3 @@ endmodule
 module unit_y(input [31:0] a, b, c, output [31:0] y);
   assign y = a & (b | c);
 endmodule
-

backends/smt2/smt2.cc

@@ -788,7 +788,7 @@ struct Smt2Worker
 			if (has_async_wr && has_sync_wr)
 				log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", cell, module);
 
-			decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", mem->memid.unescape(), abits, mem->width, GetSize(mem->rd_ports), GetSize(mem->wr_ports), has_async_wr ? "async" : "sync"));
+			decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(mem->memid), abits, mem->width, GetSize(mem->rd_ports), GetSize(mem->wr_ports), has_async_wr ? "async" : "sync"));
 			decls.push_back(witness_memory(get_id(mem->memid), cell, mem));
 
 			string memstate;

backends/smt2/smtio.py

@@ -226,7 +226,7 @@ class SmtIo:
                 print('timeout option is not supported for mathsat.')
                 sys.exit(1)
 
-        if self.solver in ["boolector", "bitwuzla"]:
+        if self.solver == "boolector":
             if self.noincr:
                 self.popen_vargs = [self.solver, '--smt2'] + self.solver_opts
             else:
@@ -236,6 +236,29 @@ class SmtIo:
                 print('timeout option is not supported for %s.' % self.solver)
                 sys.exit(1)
 
+        if self.solver == "bitwuzla":
+            try:
+                help_text = subprocess.check_output([self.solver, "--help"], text=True)
+            except FileNotFoundError:
+                print("%s SMT Solver '%s' not found in path." % (self.timestamp(), self.solver), flush=True)
+                sys.exit(1)
+            if "--lang" in help_text:
+                self.popen_vargs = [self.solver, '--lang', 'smt2'] + self.solver_opts
+                self.unroll = True
+                if self.timeout != 0:
+                    self.popen_vargs.append('--time-limit')
+                    self.popen_vargs.append('%d000' % self.timeout)
+            else:
+                # Versions before 0.3
+                if self.noincr:
+                    self.popen_vargs = [self.solver, '--smt2'] + self.solver_opts
+                else:
+                    self.popen_vargs = [self.solver, '--smt2', '-i'] + self.solver_opts
+                self.unroll = True
+                if self.timeout != 0:
+                    print('timeout option is not supported for %s.' % self.solver)
+                    sys.exit(1)
+
         if self.solver == "abc":
             if len(self.solver_opts) > 0:
                 self.popen_vargs = ['yosys-abc', '-S', '; '.join(self.solver_opts)]

backends/smt2/test_cells.sh

@@ -52,4 +52,3 @@ echo ""
 echo "  All tests passed."
 echo ""
 exit 0
-

backends/smt2/ywio.py

@@ -398,13 +398,13 @@ class ReadWitness:
 
     def init_step(self):
         return self.step(0)
-    
+
     def non_init_bits(self):
         if len(self) > 1:
             return len(self.bits[1])
         else:
             return sum([sig.width for sig in self.signals if not sig.init_only])
-    
+
     def first_step(self):
         values = WitnessValues()
         # may have issues when non_init_bits is 0

backends/smv/test_cells.sh

@@ -30,4 +30,3 @@ for fn in test_*.il; do
 done
 
 grep '^-- invariant .* is false' *.out || echo 'All OK.'
-

backends/verilog/verilog_backend.cc

@@ -197,14 +197,22 @@ bool is_reg_wire(RTLIL::SigSpec sig, std::string &reg_name)
 
 	reg_name = id(chunk.wire->name);
 	if (sig.size() != chunk.wire->width) {
-		if (sig.size() == 1)
-			reg_name += stringf("[%d]", chunk.wire->start_offset +  chunk.offset);
-		else if (chunk.wire->upto)
-			reg_name += stringf("[%d:%d]", (chunk.wire->width - (chunk.offset + chunk.width - 1) - 1) + chunk.wire->start_offset,
-					(chunk.wire->width - chunk.offset - 1) + chunk.wire->start_offset);
+		int idx;
+		if (chunk.wire->upto)
+			idx = (chunk.wire->width - chunk.offset - 1) + chunk.wire->start_offset;
 		else
-			reg_name += stringf("[%d:%d]", chunk.wire->start_offset +  chunk.offset + chunk.width - 1,
-					chunk.wire->start_offset +  chunk.offset);
+			idx = chunk.wire->start_offset + chunk.offset;
+
+		if (sig.size() == 1)
+			reg_name += stringf("[%d]", idx);
+		else {
+			int left_idx;
+			if (chunk.wire->upto)
+				left_idx = (chunk.wire->width - (chunk.offset + chunk.width - 1) - 1) + chunk.wire->start_offset;
+			else
+				left_idx = chunk.wire->start_offset +  chunk.offset + chunk.width - 1;
+			reg_name += stringf("[%d:%d]", left_idx, idx);
+		}
 	}
 
 	return true;
@@ -474,21 +482,22 @@ void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire)
 		if (wire->attributes.count(ID::single_bit_vector))
 			range = stringf(" [%d:%d]", wire->start_offset, wire->start_offset);
 	}
+	std::string sign = wire->is_signed ? " signed" : "";
 	if (wire->port_input && !wire->port_output)
-		f << stringf("%s" "input%s %s;\n", indent, range, id(wire->name));
+		f << stringf("%s" "input%s%s %s;\n", indent, sign, range, id(wire->name));
 	if (!wire->port_input && wire->port_output)
-		f << stringf("%s" "output%s %s;\n", indent, range, id(wire->name));
+		f << stringf("%s" "output%s%s %s;\n", indent, sign, range, id(wire->name));
 	if (wire->port_input && wire->port_output)
-		f << stringf("%s" "inout%s %s;\n", indent, range, id(wire->name));
+		f << stringf("%s" "inout%s%s %s;\n", indent, sign, range, id(wire->name));
 	if (reg_wires.count(wire->name)) {
-		f << stringf("%s" "reg%s %s", indent, range, id(wire->name));
+		f << stringf("%s" "reg%s%s %s", indent, sign, range, id(wire->name));
 		if (wire->attributes.count(ID::init)) {
 			f << stringf(" = ");
 			dump_const(f, wire->attributes.at(ID::init));
 		}
 		f << stringf(";\n");
 	} else
-		f << stringf("%s" "wire%s %s;\n", indent, range, id(wire->name));
+		f << stringf("%s" "wire%s%s %s;\n", indent, sign, range, id(wire->name));
 #endif
 }