mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-02-18 06:34:23 +00:00
Code Activity

Merge pull request #5128 from gussmith23/gussmith23-rosette-backend-updates

Browse source 
Add association-list-based helper functions into Rosette backend
This commit is contained in:
Gus Smith 2025-12-02 16:27:05 -08:00 • committed by GitHub
commit 07a690570e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 130 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

76
backends/functional/smtlib_rosette.cc
View file

@ -188,20 +188,27 @@ struct SmtrModule {
Functional::IR ir;
SmtrScope scope;
std::string name;
bool use_assoc_list_helpers;
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)
: 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<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 +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);
}
}

63
tests/functional/rkt_vcd.py
View file

@ -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]})"

5
tests/functional/run-test.sh
View file

@ -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" "$@"

8
tests/functional/test_functional.py
View file

@ -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):