diff --git a/backends/functional/smtlib_rosette.cc b/backends/functional/smtlib_rosette.cc index c9e737d19..639efb46e 100644 --- a/backends/functional/smtlib_rosette.cc +++ b/backends/functional/smtlib_rosette.cc @@ -188,12 +188,14 @@ struct SmtrModule { Functional::IR ir; SmtrScope scope; std::string name; - + std::optional input_helper_name; + std::optional 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 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); } } diff --git a/docs/source/yosys_internals/extending_yosys/test_suites.rst b/docs/source/yosys_internals/extending_yosys/test_suites.rst index 3e5f45b94..6627fdbdd 100644 --- a/docs/source/yosys_internals/extending_yosys/test_suites.rst +++ b/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 .. diff --git a/tests/functional/conftest.py b/tests/functional/conftest.py index a9fbb3c59..fb00d4f22 100644 --- a/tests/functional/conftest.py +++ b/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) diff --git a/tests/functional/rkt_vcd.py b/tests/functional/rkt_vcd.py index 1b2cf31e3..f06c2dc27 100644 --- a/tests/functional/rkt_vcd.py +++ b/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 - elif not current_struct_name: 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) + if current_struct_name == "State": + break + elif not current_struct_name: + 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') - with open(test_rkt_file_path, 'w') as test_rkt_file: - test_rkt_file.writelines([ - '#lang rosette\n', - f'(require "{rkt_file_path.name}")\n', - ]) + test_rkt_file_path = rkt_file_path.with_suffix(".tst.rkt") + with open(test_rkt_file_path, "w") as test_rkt_file: + test_rkt_file.writelines( + [ + "#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(): - value = signals[signal][step] - value_list.append(f"(bv #b{value} {width})") - gold_Inputs = f"(gold_Inputs {' '.join(value_list)})" + if use_assoc_list_helpers: + # Generate inputs as a list of cons pairs making up the + # association 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) - assert status.returncode == 0, f"{cmd[0]} failed" + try: + 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 int(width) == outputs[output], 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)) + 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]})" + 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 = {} diff --git a/tests/functional/rtlil_cells.py b/tests/functional/rtlil_cells.py index 964d81ddf..ab7cd4e0c 100644 --- a/tests/functional/rtlil_cells.py +++ b/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)) - names.append(f'{cell.name}-{name}' if name != '' else cell.name) + full_name = 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) \ No newline at end of file diff --git a/tests/functional/run-test.sh b/tests/functional/run-test.sh index 9f70462ee..03e3b60f8 100755 --- a/tests/functional/run-test.sh +++ b/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 diff --git a/tests/functional/simulate_rosette.py b/tests/functional/simulate_rosette.py new file mode 100644 index 000000000..9400a575a --- /dev/null +++ b/tests/functional/simulate_rosette.py @@ -0,0 +1 @@ +"""Python utilities for simulating Rosette code.""" \ No newline at end of file diff --git a/tests/functional/test_functional.py b/tests/functional/test_functional.py index 7a09966d8..0553d6ecc 100644 --- a/tests/functional/test_functional.py +++ b/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)}") - rkt_vcd.simulate_rosette(rkt_file, vcd_functional_file, num_steps, rnd(cell.name + "-rkt")) + use_assoc_helpers_flag = '-assoc-list-helpers' if use_assoc_list_helpers else '' + 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):