Merge dcf72ff8e2 into 262b00d5e5

backends/functional/smtlib_rosette.cc

@@ -188,12 +188,14 @@ struct SmtrModule {
 	Functional::IR ir;
 	SmtrScope scope;
 	std::string name;
-	
+	std::optional<std::string> input_helper_name;
+	std::optional<std::string> output_helper_name;
+
 	SmtrStruct input_struct;
 	SmtrStruct output_struct;
 	SmtrStruct state_struct;
 
-	SmtrModule(Module *module)
+	SmtrModule(Module *module, bool assoc_list_helpers)
 		: ir(Functional::IR::from_module(module))
 		, scope()
 		, name(scope.unique_name(module->name))
@@ -202,6 +204,12 @@ struct SmtrModule {
 		, state_struct(scope.unique_name(module->name.str() + "_State"), scope)
 	{
 		scope.reserve(name + "_initial");
+		if (assoc_list_helpers) {
+			input_helper_name = scope.unique_name(module->name.str() + "_inputs_helper");
+			scope.reserve(*input_helper_name);
+			output_helper_name = scope.unique_name(module->name.str() + "_outputs_helper");
+			scope.reserve(*output_helper_name);
+		}
 		for (auto input : ir.inputs())
 			input_struct.insert(input->name, input->sort);
 		for (auto output : ir.outputs())
@@ -257,6 +265,43 @@ struct SmtrModule {
 		w.pop();
 	}
 
+	void write_assoc_list_helpers(SExprWriter &w)
+	{
+		// Input struct keyword-based constructor.
+		w.push();
+		w.open(list("define"));
+		const auto inputs_name = "inputs";
+		w.open(list(*input_helper_name, inputs_name));
+		w.close();
+		w.open(list(input_struct.name));
+		for (auto input : ir.inputs()) {
+			w.push();
+			w.open(list("let"));
+			w.push();
+			w.open(list());
+			w.open(list("assoc-result"));
+			w << list("assoc", "\"" + RTLIL::unescape_id(input->name) + "\"", inputs_name);
+			w.pop();
+			w.open(list("if", "assoc-result"));
+			w << list("cdr", "assoc-result");
+			w.open(list("begin"));
+			w << list("fprintf", list("current-error-port"), "\"%s not found in inputs\"");
+			w << "'not-found";
+			w.pop();
+		}
+		w.pop();
+		// Output struct keyword-based destructor.
+		w.push();
+		w.open(list("define"));
+		const auto outputs_name = "outputs";
+		w << list(*output_helper_name, outputs_name);
+		w.open(list("list"));
+		for (auto output : ir.outputs()) {
+			w << list("cons", "\"" + RTLIL::unescape_id(output->name) + "\"", output_struct.access("outputs", output->name));
+		}
+		w.pop();
+	}
+
 	void write(std::ostream &out)
 	{    
 		SExprWriter w(out);
@@ -265,6 +310,12 @@ struct SmtrModule {
 		output_struct.write_definition(w);
 		state_struct.write_definition(w);
 
+		if (input_helper_name) {
+			if (!output_helper_name)
+				log_error("if keyword helpers are enabled, both input and output helper names are expected");
+			write_assoc_list_helpers(w);
+		}
+
 		write_eval(w);
 		write_initial(w);
 	}
@@ -282,12 +333,16 @@ struct FunctionalSmtrBackend : public Backend {
 		log("\n");
 		log("    -provides\n");
 		log("        include 'provide' statement(s) for loading output as a module\n");
+		log("    -assoc-list-helpers\n");
+		log("        provide helper functions which convert inputs/outputs from/to association lists\n");
+		log("        \n");
 		log("\n");
 	}
 
 	void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
 	{
 		auto provides = false;
+		auto assoc_list_helpers = false;
 
 		log_header(design, "Executing Functional Rosette Backend.\n");
 
@@ -296,6 +351,8 @@ struct FunctionalSmtrBackend : public Backend {
 		{
 			if (args[argidx] == "-provides")
 				provides = true;
+			else if (args[argidx] == "-assoc-list-helpers")
+				assoc_list_helpers = true;
 			else
 				break;
 		}
@@ -308,7 +365,7 @@ struct FunctionalSmtrBackend : public Backend {
 
 		for (auto module : design->selected_modules()) {
 			log("Processing module `%s`.\n", module->name.c_str());
-			SmtrModule smtr(module);
+			SmtrModule smtr(module, assoc_list_helpers);
 			smtr.write(*f);
 		}
 	}

docs/source/yosys_internals/extending_yosys/test_suites.rst

@@ -14,6 +14,24 @@ compiler versions.  For up to date information, including OS versions, refer to
 .. _Yosys Git repo: https://github.com/YosysHQ/yosys
 .. _the git actions page: https://github.com/YosysHQ/yosys/actions
 
+Functional backend testing
+--------------------------
+
+Testing of the functional backend is controlled by the
+``ENABLE_FUNCTIONAL_TESTS`` make variable.  Setting it to a value of ``1``,
+either when calling ``make test`` or in your ``Makefile.conf`` file, will enable
+these additional tests.
+
+.. note::
+
+   The functional backend tests requires additional prerequisites to be
+   installed:
+
+   - racket and z3, available via ``apt-get`` or similar.
+   - pytest and pytest-xdist, available via ``pip``; pytest-xdist-gnumake is
+     also recommended.
+   - rosette, available via ``raco`` (after installing racket).
+
 .. todo:: are unit tests currently working
 
 ..

tests/functional/conftest.py

@@ -31,4 +31,4 @@ def pytest_generate_tests(metafunc):
         seed1 = metafunc.config.getoption("seed")
         rnd = lambda seed2: random.Random('{}-{}'.format(seed1, seed2))
         names, cases = generate_test_cases(per_cell, rnd)
-        metafunc.parametrize("cell,parameters", cases, ids=names)
+        metafunc.parametrize("name,cell,parameters", cases, ids=names)

tests/functional/rkt_vcd.py

@@ -43,21 +43,37 @@ def write_vcd(filename: Path, signals: SignalStepMap, timescale='1 ns', date='to
                         if change_time == time:
                             f.write(f"{value} {signal_name}\n")
 
-def simulate_rosette(rkt_file_path: Path, vcd_path: Path, num_steps: int, rnd: Random):
+
+def simulate_rosette(
+    rkt_file_path: Path,
+    vcd_path: Path,
+    num_steps: int,
+    rnd: Random,
+    use_assoc_list_helpers: bool = False,
+):
+    """
+    Args:
+      - use_assoc_list_helpers: If True, will use the association list helpers
+        in the Racket file. The file should have been generated with the
+        -assoc-list-helpers flag in the yosys command.
+    """
     signals: dict[str, list[str]] = {}
     inputs: SignalWidthMap = {}
     outputs: SignalWidthMap = {}
 
     current_struct_name: str = ""
-    with open(rkt_file_path, 'r') as rkt_file:
+    with open(rkt_file_path, "r") as rkt_file:
         for line in rkt_file:
-            m = re.search(r'gold_(Inputs|Outputs|State)', line)
+            m = re.search(r"gold_(Inputs|Outputs|State)", line)
             if m:
                 current_struct_name = m.group(1)
-                if current_struct_name == "State": break
+                if current_struct_name == "State":
-            elif not current_struct_name: continue # skip lines before structs
+                    break
-            m = re.search(r'; (.+?)\b \(bitvector (\d+)\)', line)
+            elif not current_struct_name:
-            if not m: continue # skip non matching lines (probably closing the struct)
+                continue  # skip lines before structs
+            m = re.search(r"; (.+?)\b \(bitvector (\d+)\)", line)
+            if not m:
+                continue  # skip non matching lines (probably closing the struct)
             signal = m.group(1)
             width = int(m.group(2))
             if current_struct_name == "Inputs":
@@ -69,43 +85,86 @@ def simulate_rosette(rkt_file_path: Path, vcd_path: Path, num_steps: int, rnd: R
         step_list: list[int] = []
         for step in range(num_steps):
             value = rnd.getrandbits(width)
-            binary_string = format(value, '0{}b'.format(width))
+            binary_string = format(value, "0{}b".format(width))
             step_list.append(binary_string)
         signals[signal] = step_list
 
-    test_rkt_file_path = rkt_file_path.with_suffix('.tst.rkt')
+    test_rkt_file_path = rkt_file_path.with_suffix(".tst.rkt")
-    with open(test_rkt_file_path, 'w') as test_rkt_file:
+    with open(test_rkt_file_path, "w") as test_rkt_file:
-        test_rkt_file.writelines([
+        test_rkt_file.writelines(
-            '#lang rosette\n',
+            [
-            f'(require "{rkt_file_path.name}")\n',
+                "#lang rosette\n",
-        ])
+                f'(require "{rkt_file_path.name}")\n',
+            ]
+        )
 
         for step in range(num_steps):
             this_step = f"step_{step}"
             value_list: list[str] = []
-            for signal, width in inputs.items():
+            if use_assoc_list_helpers:
-                value = signals[signal][step]
+                # Generate inputs as a list of cons pairs making up the
-                value_list.append(f"(bv #b{value} {width})")
+                # association list.
-            gold_Inputs = f"(gold_Inputs {' '.join(value_list)})"
+                for signal, width in inputs.items():
+                    value = signals[signal][step]
+                    value_list.append(f'(cons "{signal}" (bv #b{value} {width}))')
+            else:
+                # Otherwise, we generate the inputs as a list of bitvectors.
+                for signal, width in inputs.items():
+                    value = signals[signal][step]
+                    value_list.append(f"(bv #b{value} {width})")
+            gold_Inputs = (
+                f"(gold_inputs_helper (list {' '.join(value_list)}))"
+                if use_assoc_list_helpers
+                else f"(gold_Inputs {' '.join(value_list)})"
+            )
             gold_State = f"(cdr step_{step-1})" if step else "gold_initial"
-            test_rkt_file.write(f"(define {this_step} (gold {gold_Inputs} {gold_State})) (car {this_step})\n")
+            get_value_expr = (
+                f"(gold_outputs_helper (car {this_step}))"
+                if use_assoc_list_helpers
+                else f"(car {this_step})"
+            )
+            test_rkt_file.write(
+                f"(define {this_step} (gold {gold_Inputs} {gold_State})) {get_value_expr}\n"
+            )
+
 
     cmd = ["racket", test_rkt_file_path]
-    status = subprocess.run(cmd, capture_output=True)
+    try:
-    assert status.returncode == 0, f"{cmd[0]} failed"
+        status = subprocess.run(cmd, capture_output=True, check=True)
+    except subprocess.CalledProcessError as e:
+        raise RuntimeError(
+            f"Racket simulation failed with command: {cmd}\n"
+            f"Error: {e.stderr.decode()}"
+        ) from e
 
     for signal in outputs.keys():
         signals[signal] = []
 
     for line in status.stdout.decode().splitlines():
-        m = re.match(r'\(gold_Outputs( \(bv \S+ \d+\))+\)', line)
+        m = (
+            re.match(r"\(list( \(cons \"\S+\" \(bv \S+ \d+\)\))+\)", line)
+            if use_assoc_list_helpers
+            else re.match(r"\(gold_Outputs( \(bv \S+ \d+\))+\)", line)
+        )
         assert m, f"Incomplete output definition {line!r}"
-        for output, (value, width) in zip(outputs.keys(), re.findall(r'\(bv (\S+) (\d+)\)', line)):
+        outputs_values_and_widths = (
+            {
+                output: re.findall(
+                    r"\(cons \"" + output + r"\" \(bv (\S+) (\d+)\)\)", line
+                )[0]
+                for output in outputs.keys()
+            }.items()
+            if use_assoc_list_helpers
+            else zip(outputs.keys(), re.findall(r"\(bv (\S+) (\d+)\)", line))
+        )
+        for output, (value, width) in outputs_values_and_widths:
             assert isinstance(value, str), f"Bad value {value!r}"
-            assert value.startswith(('#b', '#x')), f"Non-binary value {value!r}"
+            assert value.startswith(("#b", "#x")), f"Non-binary value {value!r}"
-            assert int(width) == outputs[output], f"Width mismatch for output {output!r} (got {width}, expected {outputs[output]})"
+            assert (
-            int_value = int(value[2:], 16 if value.startswith('#x') else 2)
+                int(width) == outputs[output]
-            binary_string = format(int_value, '0{}b'.format(width))
+            ), f"Width mismatch for output {output!r} (got {width}, expected {outputs[output]})"
+            int_value = int(value[2:], 16 if value.startswith("#x") else 2)
+            binary_string = format(int_value, "0{}b".format(width))
             signals[output].append(binary_string)
 
     vcd_signals: SignalStepMap = {}

tests/functional/rtlil_cells.py

@@ -374,8 +374,9 @@ def generate_test_cases(per_cell, rnd):
         for (name, parameters) in cell.generate_tests(rnd):
             if not name in seen_names:
                 seen_names.add(name)
-                tests.append((cell, parameters))
+                full_name = f'{cell.name}-{name}' if name != '' else cell.name
-                names.append(f'{cell.name}-{name}' if name != '' else cell.name)
+                tests.append((full_name, cell, parameters))
+                names.append(full_name)
                 if per_cell is not None and len(seen_names) >= per_cell:
                     break
     return (names, tests)

tests/functional/run-test.sh

@@ -1,2 +1,2 @@
 #!/usr/bin/env bash
-pytest -v -m "not smt and not rkt" "$@"
+pytest -v -n auto "$@" --steps 100

tests/functional/simulate_rosette.py

@@ -0,0 +1 @@
+"""Python utilities for simulating Rosette code."""

tests/functional/test_functional.py

@@ -40,12 +40,12 @@ def yosys_sim(rtlil_file, vcd_reference_file, vcd_out_file, preprocessing = ""):
             capture_output=True, check=False)
         raise
 
-def test_cxx(cell, parameters, tmp_path, num_steps, rnd):
+def test_cxx(name, cell, parameters, tmp_path, num_steps, rnd):
     rtlil_file = tmp_path / 'rtlil.il'
     vcdharness_cc_file = base_path / 'tests/functional/vcd_harness.cc'
     cc_file = tmp_path / 'my_module_functional_cxx.cc'
     vcdharness_exe_file = tmp_path / 'a.out'
-    vcd_functional_file = tmp_path / 'functional.vcd'
+    vcd_functional_file = tmp_path / f'{name}.vcd'
     vcd_yosys_sim_file = tmp_path / 'yosys.vcd'
 
     cell.write_rtlil_file(rtlil_file, parameters)
@@ -56,12 +56,12 @@ def test_cxx(cell, parameters, tmp_path, num_steps, rnd):
     yosys_sim(rtlil_file, vcd_functional_file, vcd_yosys_sim_file, getattr(cell, 'sim_preprocessing', ''))
 
 @pytest.mark.smt
-def test_smt(cell, parameters, tmp_path, num_steps, rnd):
+def test_smt(name, cell, parameters, tmp_path, num_steps, rnd):
     import smt_vcd
 
     rtlil_file = tmp_path / 'rtlil.il'
     smt_file = tmp_path / 'smtlib.smt'
-    vcd_functional_file = tmp_path / 'functional.vcd'
+    vcd_functional_file = tmp_path / f'{name}.vcd'
     vcd_yosys_sim_file = tmp_path / 'yosys.vcd'
 
     if hasattr(cell, 'smt_max_steps'):
@@ -74,17 +74,19 @@ def test_smt(cell, parameters, tmp_path, num_steps, rnd):
     yosys_sim(rtlil_file, vcd_functional_file, vcd_yosys_sim_file, getattr(cell, 'sim_preprocessing', ''))
 
 @pytest.mark.rkt
-def test_rkt(cell, parameters, tmp_path, num_steps, rnd):
+@pytest.mark.parametrize("use_assoc_list_helpers", [True, False])
+def test_rkt(name, cell, parameters, tmp_path, num_steps, rnd, use_assoc_list_helpers):
     import rkt_vcd
 
     rtlil_file = tmp_path / 'rtlil.il'
     rkt_file = tmp_path / 'smtlib.rkt'
-    vcd_functional_file = tmp_path / 'functional.vcd'
+    vcd_functional_file = tmp_path / f'{name}.vcd'
     vcd_yosys_sim_file = tmp_path / 'yosys.vcd'
 
     cell.write_rtlil_file(rtlil_file, parameters)
-    yosys(f"read_rtlil {quote(rtlil_file)} ; clk2fflogic ; write_functional_rosette -provides {quote(rkt_file)}")
+    use_assoc_helpers_flag = '-assoc-list-helpers' if use_assoc_list_helpers else ''
-    rkt_vcd.simulate_rosette(rkt_file, vcd_functional_file, num_steps, rnd(cell.name + "-rkt"))
+    yosys(f"read_rtlil {quote(rtlil_file)} ; clk2fflogic ; write_functional_rosette -provides {use_assoc_helpers_flag} {quote(rkt_file)}")
+    rkt_vcd.simulate_rosette(rkt_file, vcd_functional_file, num_steps, rnd(cell.name + "-rkt"), use_assoc_list_helpers=use_assoc_list_helpers)
     yosys_sim(rtlil_file, vcd_functional_file, vcd_yosys_sim_file, getattr(cell, 'sim_preprocessing', ''))
 
 def test_print_graph(tmp_path):