diff --git a/backends/functional/Makefile.inc b/backends/functional/Makefile.inc index 13c962c99ff..16d1c054273 100644 --- a/backends/functional/Makefile.inc +++ b/backends/functional/Makefile.inc @@ -1,3 +1,4 @@ OBJS += backends/functional/cxx.o OBJS += backends/functional/smtlib.o +OBJS += backends/functional/smtlib_rosette.o OBJS += backends/functional/test_generic.o diff --git a/backends/functional/smtlib_rosette.cc b/backends/functional/smtlib_rosette.cc new file mode 100644 index 00000000000..ea14da85428 --- /dev/null +++ b/backends/functional/smtlib_rosette.cc @@ -0,0 +1,308 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2024 Emily Schmidt + * Copyright (C) 2024 National Technology and Engineering Solutions of Sandia, LLC + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "kernel/functional.h" +#include "kernel/yosys.h" +#include "kernel/sexpr.h" +#include + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +using SExprUtil::list; + +const char *reserved_keywords[] = { + // reserved keywords from the racket spec + "struct", "lambda", "values", "extract", "concat", "bv", "let", "define", "cons", "list", "read", "write", + "stream", "error", "raise", "exit", "for", "begin", "when", "unless", "module", "require", "provide", "apply", + "if", "cond", "even", "odd", "any", "and", "or", "match", "command-line", "ffi-lib", "thread", "kill", "sync", + "future", "touch", "subprocess", "make-custodian", "custodian-shutdown-all", "current-custodian", "make", "tcp", + "connect", "prepare", "malloc", "free", "_fun", "_cprocedure", "build", "path", "file", "peek", "bytes", + "flush", "with", "lexer", "parser", "syntax", "interface", "send", "make-object", "new", "instantiate", + "define-generics", "set", + + // reserved for our own purposes + "inputs", "state", "name", + nullptr +}; + +struct SmtrScope : public Functional::Scope { + SmtrScope() { + for(const char **p = reserved_keywords; *p != nullptr; p++) + reserve(*p); + } + bool is_character_legal(char c, int index) override { + return isascii(c) && (isalpha(c) || (isdigit(c) && index > 0) || strchr("@$%^&_+=.", c)); + } +}; + +struct SmtrSort { + Functional::Sort sort; + SmtrSort(Functional::Sort sort) : sort(sort) {} + SExpr to_sexpr() const { + if(sort.is_memory()) { + return list("list", list("bitvector", sort.addr_width()), list("bitvector", sort.data_width())); + } else if(sort.is_signal()) { + return list("bitvector", sort.width()); + } else { + log_error("unknown sort"); + } + } +}; + +class SmtrStruct { + struct Field { + SmtrSort sort; + std::string accessor; + std::string name; + }; + idict field_names; + vector fields; + SmtrScope &global_scope; + SmtrScope local_scope; +public: + std::string name; + SmtrStruct(std::string name, SmtrScope &scope) : global_scope(scope), local_scope(), name(name) {} + void insert(IdString field_name, SmtrSort sort) { + field_names(field_name); + auto base_name = local_scope.unique_name(field_name); + auto accessor = name + "-" + base_name; + global_scope.reserve(accessor); + fields.emplace_back(Field{sort, accessor, base_name}); + } + void write_definition(SExprWriter &w) { + vector field_list; + for(const auto &field : fields) { + field_list.emplace_back(field.name); + } + w.push(); + w.open(list("struct", name, field_list, "#:transparent")); + if (field_names.size()) { + for (const auto &field : fields) { + auto bv_type = field.sort.to_sexpr(); + w.comment(field.name + " " + bv_type.to_string()); + } + } + w.pop(); + } + template void write_value(SExprWriter &w, Fn fn) { + w.open(list(name)); + for(auto field_name : field_names) { + w << fn(field_name); + w.comment(RTLIL::unescape_id(field_name), true); + } + w.close(); + } + SExpr access(SExpr record, IdString name) { + size_t i = field_names.at(name); + return list(fields[i].accessor, std::move(record)); + } +}; + +std::string smt_const(RTLIL::Const const &c) { + std::string s = "#b"; + for(int i = c.size(); i-- > 0; ) + s += c[i] == State::S1 ? '1' : '0'; + return s; +} + +struct SmtrPrintVisitor : public Functional::AbstractVisitor { + using Node = Functional::Node; + std::function n; + SmtrStruct &input_struct; + SmtrStruct &state_struct; + + SmtrPrintVisitor(SmtrStruct &input_struct, SmtrStruct &state_struct) : input_struct(input_struct), state_struct(state_struct) {} + + SExpr from_bool(SExpr &&arg) { + return list("bool->bitvector", std::move(arg)); + } + SExpr to_bool(SExpr &&arg) { + return list("bitvector->bool", std::move(arg)); + } + SExpr to_list(SExpr &&arg) { + return list("bitvector->bits", std::move(arg)); + } + + SExpr buf(Node, Node a) override { return n(a); } + SExpr slice(Node, Node a, int offset, int out_width) override { return list("extract", offset + out_width - 1, offset, n(a)); } + SExpr zero_extend(Node, Node a, int out_width) override { return list("zero-extend", n(a), list("bitvector", out_width)); } + SExpr sign_extend(Node, Node a, int out_width) override { return list("sign-extend", n(a), list("bitvector", out_width)); } + SExpr concat(Node, Node a, Node b) override { return list("concat", n(b), n(a)); } + SExpr add(Node, Node a, Node b) override { return list("bvadd", n(a), n(b)); } + SExpr sub(Node, Node a, Node b) override { return list("bvsub", n(a), n(b)); } + SExpr mul(Node, Node a, Node b) override { return list("bvmul", n(a), n(b)); } + SExpr unsigned_div(Node, Node a, Node b) override { return list("bvudiv", n(a), n(b)); } + SExpr unsigned_mod(Node, Node a, Node b) override { return list("bvurem", n(a), n(b)); } + SExpr bitwise_and(Node, Node a, Node b) override { return list("bvand", n(a), n(b)); } + SExpr bitwise_or(Node, Node a, Node b) override { return list("bvor", n(a), n(b)); } + SExpr bitwise_xor(Node, Node a, Node b) override { return list("bvxor", n(a), n(b)); } + SExpr bitwise_not(Node, Node a) override { return list("bvnot", n(a)); } + SExpr unary_minus(Node, Node a) override { return list("bvneg", n(a)); } + SExpr reduce_and(Node, Node a) override { return list("apply", "bvand", to_list(n(a))); } + SExpr reduce_or(Node, Node a) override { return list("apply", "bvor", to_list(n(a))); } + SExpr reduce_xor(Node, Node a) override { return list("apply", "bvxor", to_list(n(a))); } + SExpr equal(Node, Node a, Node b) override { return from_bool(list("bveq", n(a), n(b))); } + SExpr not_equal(Node, Node a, Node b) override { return from_bool(list("not", list("bveq", n(a), n(b)))); } + SExpr signed_greater_than(Node, Node a, Node b) override { return from_bool(list("bvsgt", n(a), n(b))); } + SExpr signed_greater_equal(Node, Node a, Node b) override { return from_bool(list("bvsge", n(a), n(b))); } + SExpr unsigned_greater_than(Node, Node a, Node b) override { return from_bool(list("bvugt", n(a), n(b))); } + SExpr unsigned_greater_equal(Node, Node a, Node b) override { return from_bool(list("bvuge", n(a), n(b))); } + + SExpr extend(SExpr &&a, int in_width, int out_width) { + if(in_width < out_width) + return list("zero-extend", std::move(a), list("bitvector", out_width)); + else + return std::move(a); + } + SExpr logical_shift_left(Node, Node a, Node b) override { return list("bvshl", n(a), extend(n(b), b.width(), a.width())); } + SExpr logical_shift_right(Node, Node a, Node b) override { return list("bvlshr", n(a), extend(n(b), b.width(), a.width())); } + SExpr arithmetic_shift_right(Node, Node a, Node b) override { return list("bvashr", n(a), extend(n(b), b.width(), a.width())); } + SExpr mux(Node, Node a, Node b, Node s) override { return list("if", to_bool(n(s)), n(b), n(a)); } + SExpr constant(Node, RTLIL::Const const& value) override { return list("bv", smt_const(value), value.size()); } + SExpr memory_read(Node, Node mem, Node addr) override { return list("list-ref-bv", n(mem), n(addr)); } + SExpr memory_write(Node, Node mem, Node addr, Node data) override { return list("list-set-bv", n(mem), n(addr), n(data)); } + + SExpr input(Node, IdString name, IdString kind) override { log_assert(kind == ID($input)); return input_struct.access("inputs", name); } + SExpr state(Node, IdString name, IdString kind) override { log_assert(kind == ID($state)); return state_struct.access("state", name); } +}; + +struct SmtrModule { + Functional::IR ir; + SmtrScope scope; + std::string 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) + { + scope.reserve(name + "_initial"); + for (auto input : ir.inputs()) + input_struct.insert(input->name, input->sort); + for (auto output : ir.outputs()) + output_struct.insert(output->name, output->sort); + for (auto state : ir.states()) + state_struct.insert(state->name, state->sort); + } + + void write(std::ostream &out) + { + SExprWriter w(out); + + input_struct.write_definition(w); + output_struct.write_definition(w); + state_struct.write_definition(w); + + w.push(); + w.open(list("define", list(name, "inputs", "state"))); + auto inlined = [&](Functional::Node n) { + return n.fn() == Functional::Fn::constant; + }; + SmtrPrintVisitor visitor(input_struct, state_struct); + auto node_to_sexpr = [&](Functional::Node n) -> SExpr { + if(inlined(n)) + return n.visit(visitor); + else + return scope(n.id(), n.name()); + }; + visitor.n = node_to_sexpr; + for(auto n : ir) + if(!inlined(n)) { + w.open(list("let", list(list(node_to_sexpr(n), n.visit(visitor)))), false); + w.comment(SmtrSort(n.sort()).to_sexpr().to_string(), true); + } + w.open(list("cons")); + output_struct.write_value(w, [&](IdString name) { return node_to_sexpr(ir.output(name).value()); }); + state_struct.write_value(w, [&](IdString name) { return node_to_sexpr(ir.state(name).next_value()); }); + w.pop(); + + w.push(); + auto initial = name + "_initial"; + w.open(list("define", initial)); + w.open(list(state_struct.name)); + for (auto state : ir.states()) { + if (state->sort.is_signal()) + w << list("bv", smt_const(state->initial_value_signal()), state->sort.width()); + else if (state->sort.is_memory()) { + const auto &contents = state->initial_value_memory(); + w.open(list("list")); + for(int i = 0; i < 1<sort.addr_width(); i++) { + w << list("bv", smt_const(contents[i]), state->sort.data_width()); + } + w.close(); + } + } + w.pop(); + } +}; + +struct FunctionalSmtrBackend : public Backend { + FunctionalSmtrBackend() : Backend("functional_rosette", "Generate Rosette compatible Racket from Functional IR") {} + + void help() override { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" write_functional_rosette [options] [selection] [filename]\n"); + log("\n"); + log("Functional Rosette Backend.\n"); + log("\n"); + log(" -provides\n"); + log(" include 'provide' statement(s) for loading output as a module\n"); + log("\n"); + } + + void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) override + { + auto provides = false; + + log_header(design, "Executing Functional Rosette Backend.\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) + { + if (args[argidx] == "-provides") + provides = true; + else + break; + } + extra_args(f, filename, args, argidx); + + *f << "#lang rosette/safe\n"; + if (provides) { + *f << "(provide (all-defined-out))\n"; + } + + for (auto module : design->selected_modules()) { + log("Processing module `%s`.\n", module->name.c_str()); + SmtrModule smtr(module); + smtr.write(*f); + } + } +} FunctionalSmtrBackend; + +PRIVATE_NAMESPACE_END diff --git a/tests/functional/.gitignore b/tests/functional/.gitignore index 1ffe9926ef6..f0c4cf14e45 100644 --- a/tests/functional/.gitignore +++ b/tests/functional/.gitignore @@ -3,3 +3,4 @@ my_module_functional_cxx.cc vcd_harness *.vcd *.smt2 +*.rkt diff --git a/tests/functional/rkt_vcd.py b/tests/functional/rkt_vcd.py new file mode 100644 index 00000000000..1b2cf31e384 --- /dev/null +++ b/tests/functional/rkt_vcd.py @@ -0,0 +1,115 @@ +from __future__ import annotations +from pathlib import Path +import re +import subprocess +from typing import Dict, List, Tuple +from random import Random + +vcd_version = "Yosys/tests/functional/rkt_vcd.py" +StepList = List[Tuple[int, str]] +SignalStepMap = Dict[str, StepList] +SignalWidthMap = Dict[str, int] + +def write_vcd(filename: Path, signals: SignalStepMap, timescale='1 ns', date='today'): + with open(filename, 'w') as f: + # Write the header + f.write(f"$date\n {date}\n$end\n") + f.write(f"$timescale {timescale} $end\n") + + # Declare signals + f.write("$scope module gold $end\n") + for signal_name, changes in signals.items(): + signal_size = len(changes[0][1]) + f.write(f"$var wire {signal_size - 1} {signal_name} {signal_name} $end\n") + f.write("$upscope $end\n") + f.write("$enddefinitions $end\n") + + # Collect all unique timestamps + timestamps = sorted(set(time for changes in signals.values() for time, _ in changes)) + + # Write initial values + f.write("#0\n") + for signal_name, changes in signals.items(): + for time, value in changes: + if time == 0: + f.write(f"{value} {signal_name}\n") + + # Write value changes + for time in timestamps: + if time != 0: + f.write(f"#{time}\n") + for signal_name, changes in signals.items(): + for change_time, value in changes: + 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): + signals: dict[str, list[str]] = {} + inputs: SignalWidthMap = {} + outputs: SignalWidthMap = {} + + current_struct_name: str = "" + with open(rkt_file_path, 'r') as rkt_file: + for line in rkt_file: + 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) + signal = m.group(1) + width = int(m.group(2)) + if current_struct_name == "Inputs": + inputs[signal] = width + elif current_struct_name == "Outputs": + outputs[signal] = width + + for signal, width in inputs.items(): + step_list: list[int] = [] + for step in range(num_steps): + value = rnd.getrandbits(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', + ]) + + 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)})" + 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") + + cmd = ["racket", test_rkt_file_path] + status = subprocess.run(cmd, capture_output=True) + assert status.returncode == 0, f"{cmd[0]} failed" + + for signal in outputs.keys(): + signals[signal] = [] + + for line in status.stdout.decode().splitlines(): + m = 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)): + 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)) + signals[output].append(binary_string) + + vcd_signals: SignalStepMap = {} + for signal, steps in signals.items(): + vcd_signals[signal] = [(time, f"b{value}") for time, value in enumerate(steps)] + + write_vcd(vcd_path, vcd_signals) diff --git a/tests/functional/test_functional.py b/tests/functional/test_functional.py index 55e4acc3340..3b006676a14 100644 --- a/tests/functional/test_functional.py +++ b/tests/functional/test_functional.py @@ -72,6 +72,19 @@ def test_smt(cell, parameters, tmp_path, num_steps, rnd): smt_vcd.simulate_smt(smt_file, vcd_functional_file, num_steps, rnd(cell.name + "-smt")) yosys_sim(rtlil_file, vcd_functional_file, vcd_yosys_sim_file, getattr(cell, 'sim_preprocessing', '')) +def test_rkt(cell, parameters, tmp_path, num_steps, rnd): + import rkt_vcd + + rtlil_file = tmp_path / 'rtlil.il' + rkt_file = tmp_path / 'smtlib.rkt' + vcd_functional_file = tmp_path / 'functional.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")) + yosys_sim(rtlil_file, vcd_functional_file, vcd_yosys_sim_file, getattr(cell, 'sim_preprocessing', '')) + def test_print_graph(tmp_path): tb_file = base_path / 'tests/functional/picorv32_tb.v' cpu_file = base_path / 'tests/functional/picorv32.v'