add picorv test to functional backend

kernel/functional.cc

@@ -530,6 +530,7 @@ public:
 				memories[mem.cell] = &mem;
 		}
 	}
+private:
 	Node concatenate_read_results(Mem *mem, vector<Node> results)
 	{
 		// sanity check: all read ports concatenated should equal to the RD_DATA port
@@ -632,6 +633,17 @@ public:
 			}
 		}
 	}
+	void undriven(const char *name) {
+		log_error("The design contains an undriven signal %s. This is not supported by the functional backend. "
+			"Call setundef with appropriate options to avoid this error.\n", name);
+	}
+	// we perform this check separately to give better error messages that include the wire or port name
+	void check_undriven(DriveSpec const& spec, std::string const& name) {
+		for(auto const &chunk : spec.chunks())
+			if(chunk.is_none())
+				undriven(name.c_str());
+	}
+public:
 	void process_queue()
 	{
 		for (; !queue.empty(); queue.pop_front()) {
@@ -660,6 +672,7 @@ public:
 							factory.update_pending(pending, node);
 						} else {
 							DriveSpec driver = driver_map(DriveSpec(wire_chunk));
+							check_undriven(driver, RTLIL::unescape_id(wire_chunk.wire->name));
 							Node node = enqueue(driver);
 							factory.suggest_name(node, wire_chunk.wire->name);
 							factory.update_pending(pending, node);
@@ -677,6 +690,7 @@ public:
 							factory.update_pending(pending, node);
 						} else {
 							DriveSpec driver = driver_map(DriveSpec(port_chunk));
+							check_undriven(driver, RTLIL::unescape_id(port_chunk.cell->name) + " port " + RTLIL::unescape_id(port_chunk.port));
 							factory.update_pending(pending, enqueue(driver));
 						}
 					} else {
@@ -692,8 +706,7 @@ public:
 					log_error("Signal %s has multiple drivers. This is not supported by the functional backend. "
 						"If tristate drivers are used, call tristate -formal to avoid this error.\n", log_signal(chunk));
 				} else if (chunk.is_none()) {
-					log_error("The design contains an undriven signal %s. This is not supported by the functional backend. "
+					undriven(log_signal(chunk));
-						"Call setundef with appropriate options to avoid this error.\n", log_signal(chunk));
 				} else {
 					log_error("unhandled drivespec: %s\n", log_signal(chunk));
 					log_abort();

tests/functional/picorv32_tb.v

@@ -0,0 +1,62 @@
+module gold(
+	input wire clk,
+	output reg resetn,
+	output wire trap,
+	output wire mem_valid,
+	output wire mem_instr,
+	output wire mem_ready,
+	output wire [31:0] mem_addr,
+	output wire [31:0] mem_wdata,
+	output wire [31:0] mem_wstrb,
+	output wire [31:0] mem_rdata,
+);
+
+	initial resetn = 1'b0;
+	always @(posedge clk) resetn <= 1'b1;
+
+	reg [31:0] rom[0:15];
+
+	initial begin
+		rom[0]  = 32'h00200093;
+		rom[1]  = 32'h00200113;
+		rom[2]  = 32'h00111863;
+		rom[3]  = 32'h00102023;
+		rom[4]  = 32'h00108093;
+		rom[5]  = 32'hfe0008e3;
+		rom[6]  = 32'h00008193;
+		rom[7]  = 32'h402181b3;
+		rom[8]  = 32'hfe304ee3;
+		rom[9]  = 32'hfe0186e3;
+		rom[10] = 32'h00110113;
+		rom[11] = 32'hfc000ee3;
+	end
+
+	assign mem_ready = 1'b1;
+	assign mem_rdata = rom[mem_addr[5:2]];
+
+	wire pcpi_wr = 1'b0;
+	wire [31:0] pcpi_rd = 32'b0;
+	wire pcpi_wait = 1'b0;
+	wire pcpi_ready = 1'b0;
+
+	wire [31:0] irq = 32'b0;
+
+	picorv32 picorv32_i(
+		.clk(clk),
+		.resetn(resetn),
+		.trap(trap),
+		.mem_valid(mem_valid),
+		.mem_instr(mem_instr),
+		.mem_ready(mem_ready),
+		.mem_addr(mem_addr),
+		.mem_wdata(mem_wdata),
+		.mem_wstrb(mem_wstrb),
+		.mem_rdata(mem_rdata),
+		.pcpi_wr(pcpi_wr),
+		.pcpi_rd(pcpi_rd),
+		.pcpi_wait(pcpi_wait),
+		.pcpi_ready(pcpi_ready),
+		.irq(irq)
+	);
+
+endmodule

tests/functional/rtlil_cells.py

@@ -233,6 +233,16 @@ module gold(
 endmodule""".format(parameters['DATA_WIDTH'] - 1, parameters['ADDR_WIDTH'] - 1, 2**parameters['ADDR_WIDTH'] - 1))
         yosys_synth(verilog_file, path)
 
+class PicorvCell(BaseCell):
+    def __init__(self):
+        super().__init__("picorv", [], {}, {}, [()])
+        self.smt_max_steps = 50 # z3 is too slow for more steps
+    def write_rtlil_file(self, path, parameters):
+        from test_functional import yosys, base_path, quote
+        tb_file = base_path / 'tests/functional/picorv32_tb.v'
+        cpu_file = base_path / 'tests/functional/picorv32.v'
+        yosys(f"read_verilog {quote(tb_file)} {quote(cpu_file)}; prep -top gold; flatten; write_rtlil {quote(path)}")
+
 binary_widths = [
     # try to cover extending A operand, extending B operand, extending/truncating result
     (16, 32, 48, True, True),
@@ -353,6 +363,7 @@ rtlil_cells = [
 #    ("original_tag", ["A", "Y"]),
 #    ("future_ff", ["A", "Y"]),
 #    ("scopeinfo", []),
+    PicorvCell()
 ]
 
 def generate_test_cases(per_cell, rnd):

tests/functional/test_functional.py

@@ -63,6 +63,9 @@ def test_smt(cell, parameters, tmp_path, num_steps, rnd):
     vcd_functional_file = tmp_path / 'functional.vcd'
     vcd_yosys_sim_file = tmp_path / 'yosys.vcd'
 
+    if hasattr(cell, 'smt_max_steps'):
+        num_steps = min(num_steps, cell.smt_max_steps)
+
     cell.write_rtlil_file(rtlil_file, parameters)
     yosys(f"read_rtlil {quote(rtlil_file)} ; clk2fflogic ; write_functional_smt2 {quote(smt_file)}")
     run(['z3', smt_file]) # check if output is valid smtlib before continuing