diff --git a/backends/functional/smtlib_rosette.cc b/backends/functional/smtlib_rosette.cc index 8abfe3e4105..73e1b48c670 100644 --- a/backends/functional/smtlib_rosette.cc +++ b/backends/functional/smtlib_rosette.cc @@ -188,20 +188,27 @@ struct SmtrModule { Functional::IR ir; SmtrScope scope; std::string name; - + bool use_assoc_list_helpers; + std::optional input_helper_name; + std::optional output_helper_name; + SmtrStruct input_struct; SmtrStruct output_struct; SmtrStruct state_struct; - SmtrModule(Module *module) - : ir(Functional::IR::from_module(module)) - , scope() - , name(scope.unique_name(module->name)) - , input_struct(scope.unique_name(module->name.str() + "_Inputs"), scope) - , output_struct(scope.unique_name(module->name.str() + "_Outputs"), scope) - , state_struct(scope.unique_name(module->name.str() + "_State"), scope) + SmtrModule(Module *module, bool assoc_list_helpers) + : ir(Functional::IR::from_module(module)), scope(), name(scope.unique_name(module->name)), use_assoc_list_helpers(assoc_list_helpers), + input_struct(scope.unique_name(module->name.str() + "_Inputs"), scope), + output_struct(scope.unique_name(module->name.str() + "_Outputs"), scope), + 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 +264,45 @@ struct SmtrModule { w.pop(); } + void write_assoc_list_helpers(SExprWriter &w) + { + log_assert(output_helper_name && input_helper_name); + + // 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 destructuring + 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 +311,10 @@ struct SmtrModule { output_struct.write_definition(w); state_struct.write_definition(w); + if (use_assoc_list_helpers) { + write_assoc_list_helpers(w); + } + write_eval(w); write_initial(w); } @@ -282,12 +332,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 +350,8 @@ struct FunctionalSmtrBackend : public Backend { { if (args[argidx] == "-provides") provides = true; + else if (args[argidx] == "-assoc-list-helpers") + assoc_list_helpers = true; else break; } @@ -307,8 +363,8 @@ struct FunctionalSmtrBackend : public Backend { } for (auto module : design->selected_modules()) { - log("Processing module `%s`.\n", module->name); - SmtrModule smtr(module); + log("Processing module `%s`.\n", module->name.c_str()); + SmtrModule smtr(module, assoc_list_helpers); smtr.write(*f); } } diff --git a/tests/functional/rkt_vcd.py b/tests/functional/rkt_vcd.py index 1b2cf31e384..548a4ba744e 100644 --- a/tests/functional/rkt_vcd.py +++ b/tests/functional/rkt_vcd.py @@ -43,7 +43,20 @@ 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 = {} @@ -83,12 +96,32 @@ def simulate_rosette(rkt_file_path: Path, vcd_path: Path, num_steps: int, rnd: R 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) @@ -98,9 +131,23 @@ def simulate_rosette(rkt_file_path: Path, vcd_path: Path, num_steps: int, rnd: R 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]})" diff --git a/tests/functional/run-test.sh b/tests/functional/run-test.sh index 9f70462eed9..e0bedf8d415 100755 --- a/tests/functional/run-test.sh +++ b/tests/functional/run-test.sh @@ -1,2 +1,5 @@ #!/usr/bin/env bash -pytest -v -m "not smt and not rkt" "$@" + +SCRIPT_DIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd ) + +pytest -v -m "not smt and not rkt" "$SCRIPT_DIR" "$@" diff --git a/tests/functional/test_functional.py b/tests/functional/test_functional.py index e4c78a1fb1b..aa7500f8bd7 100644 --- a/tests/functional/test_functional.py +++ b/tests/functional/test_functional.py @@ -74,7 +74,8 @@ 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(cell, parameters, tmp_path, num_steps, rnd, use_assoc_list_helpers): import rkt_vcd rtlil_file = tmp_path / 'rtlil.il' @@ -83,8 +84,9 @@ def test_rkt(cell, parameters, tmp_path, num_steps, rnd): 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):