Skip to content

Commit

Permalink
Merge branch 'functional' into krys/functional_rosette
Browse files Browse the repository at this point in the history
  • Loading branch information
@KrystalDelusion
KrystalDelusion committed Aug 13, 2024
2 parents 357d3b9 + 9fbb3c8 commit 97d6be0
Show file tree
Hide file tree
Showing 11 changed files with 3,396 additions and 139 deletions.
39 changes: 20 additions & 19 deletions backends/functional/cxx.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2024 Emily Schmidt <[email protected]>
* 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
Expand Down Expand Up @@ -150,8 +151,8 @@ template<class NodePrinter> struct CxxPrintVisitor : public Functional::Abstract
void arithmetic_shift_right(Node, Node a, Node b) override { print("{}.arithmetic_shift_right({})", a, b); }
void mux(Node, Node a, Node b, Node s) override { print("{2}.any() ? {1} : {0}", a, b, s); }
void constant(Node, RTLIL::Const const & value) override { print("{}", cxx_const(value)); }
void input(Node, IdString name) override { print("input.{}", input_struct[name]); }
void state(Node, IdString name) override { print("current_state.{}", state_struct[name]); }
void input(Node, IdString name, IdString type) override { log_assert(type == ID($input)); print("input.{}", input_struct[name]); }
void state(Node, IdString name, IdString type) override { log_assert(type == ID($state)); print("current_state.{}", state_struct[name]); }
void memory_read(Node, Node mem, Node addr) override { print("{}.read({})", mem, addr); }
void memory_write(Node, Node mem, Node addr, Node data) override { print("{}.write({}, {})", mem, addr, data); }
};
Expand All @@ -175,12 +176,12 @@ struct CxxModule {
output_struct("Outputs"),
state_struct("State")
{
for (auto [name, sort] : ir.inputs())
input_struct.insert(name, sort);
for (auto [name, sort] : ir.outputs())
output_struct.insert(name, sort);
for (auto [name, sort] : ir.state())
state_struct.insert(name, sort);
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);
module_name = CxxScope<int>().unique_name(module->name);
}
void write_header(CxxWriter &f) {
Expand All @@ -197,19 +198,19 @@ struct CxxModule {
}
void write_initial_def(CxxWriter &f) {
f.print("void {0}::initialize({0}::State &state)\n{{\n", module_name);
for (auto [name, sort] : ir.state()) {
if (sort.is_signal())
f.print("\tstate.{} = {};\n", state_struct[name], cxx_const(ir.get_initial_state_signal(name)));
else if (sort.is_memory()) {
for (auto state : ir.states()) {
if (state->sort.is_signal())
f.print("\tstate.{} = {};\n", state_struct[state->name], cxx_const(state->initial_value_signal()));
else if (state->sort.is_memory()) {
f.print("\t{{\n");
f.print("\t\tstd::array<Signal<{}>, {}> mem;\n", sort.data_width(), 1<<sort.addr_width());
const auto &contents = ir.get_initial_state_memory(name);
f.print("\t\tstd::array<Signal<{}>, {}> mem;\n", state->sort.data_width(), 1<<state->sort.addr_width());
const auto &contents = state->initial_value_memory();
f.print("\t\tmem.fill({});\n", cxx_const(contents.default_value()));
for(auto range : contents)
for(auto addr = range.base(); addr < range.limit(); addr++)
if(!equal_def(range[addr], contents.default_value()))
f.print("\t\tmem[{}] = {};\n", addr, cxx_const(range[addr]));
f.print("\t\tstate.{} = mem;\n", state_struct[name]);
f.print("\t\tstate.{} = mem;\n", state_struct[state->name]);
f.print("\t}}\n");
}
}
Expand All @@ -229,10 +230,10 @@ struct CxxModule {
node.visit(printVisitor);
f.print(";\n");
}
for (auto [name, sort] : ir.state())
f.print("\tnext_state.{} = {};\n", state_struct[name], node_name(ir.get_state_next_node(name)));
for (auto [name, sort] : ir.outputs())
f.print("\toutput.{} = {};\n", output_struct[name], node_name(ir.get_output_node(name)));
for (auto state : ir.states())
f.print("\tnext_state.{} = {};\n", state_struct[state->name], node_name(state->next_value()));
for (auto output : ir.outputs())
f.print("\toutput.{} = {};\n", output_struct[output->name], node_name(output->value()));
f.print("}}\n\n");
}
};
Expand Down
1 change: 1 addition & 0 deletions backends/functional/cxx_runtime/sim.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2024 Emily Schmidt <[email protected]>
* 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
Expand Down
37 changes: 19 additions & 18 deletions backends/functional/smtlib.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2024 Emily Schmidt <[email protected]>
* 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
Expand Down Expand Up @@ -178,8 +179,8 @@ struct SmtPrintVisitor : public Functional::AbstractVisitor<SExpr> {
SExpr memory_read(Node, Node mem, Node addr) override { return list("select", n(mem), n(addr)); }
SExpr memory_write(Node, Node mem, Node addr, Node data) override { return list("store", n(mem), n(addr), n(data)); }

SExpr input(Node, IdString name) override { return input_struct.access("inputs", name); }
SExpr state(Node, IdString name) override { return state_struct.access("state", name); }
SExpr input(Node, IdString name, IdString type) override { log_assert(type == ID($input)); return input_struct.access("inputs", name); }
SExpr state(Node, IdString name, IdString type) override { log_assert(type == ID($state)); return state_struct.access("state", name); }
};

struct SmtModule {
Expand All @@ -200,12 +201,12 @@ struct SmtModule {
, state_struct(scope.unique_name(module->name.str() + "_State"), scope)
{
scope.reserve(name + "-initial");
for (const auto &input : ir.inputs())
input_struct.insert(input.first, input.second);
for (const auto &output : ir.outputs())
output_struct.insert(output.first, output.second);
for (const auto &state : ir.state())
state_struct.insert(state.first, state.second);
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_eval(SExprWriter &w)
Expand All @@ -232,23 +233,23 @@ struct SmtModule {
w.comment(SmtSort(n.sort()).to_sexpr().to_string(), true);
}
w.open(list("pair"));
output_struct.write_value(w, [&](IdString name) { return node_to_sexpr(ir.get_output_node(name)); });
state_struct.write_value(w, [&](IdString name) { return node_to_sexpr(ir.get_state_next_node(name)); });
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();
}

void write_initial(SExprWriter &w)
{
std::string initial = name + "-initial";
w << list("declare-const", initial, state_struct.name);
for (const auto &[name, sort] : ir.state()) {
if(sort.is_signal())
w << list("assert", list("=", state_struct.access(initial, name), smt_const(ir.get_initial_state_signal(name))));
else if(sort.is_memory()) {
auto contents = ir.get_initial_state_memory(name);
for(int i = 0; i < 1<<sort.addr_width(); i++) {
auto addr = smt_const(RTLIL::Const(i, sort.addr_width()));
w << list("assert", list("=", list("select", state_struct.access(initial, name), addr), smt_const(contents[i])));
for (auto state : ir.states()) {
if(state->sort.is_signal())
w << list("assert", list("=", state_struct.access(initial, state->name), smt_const(state->initial_value_signal())));
else if(state->sort.is_memory()) {
const auto &contents = state->initial_value_memory();
for(int i = 0; i < 1<<state->sort.addr_width(); i++) {
auto addr = smt_const(RTLIL::Const(i, state->sort.addr_width()));
w << list("assert", list("=", list("select", state_struct.access(initial, state->name), addr), smt_const(contents[i])));
}
}
}
Expand Down
35 changes: 18 additions & 17 deletions backends/functional/smtlib_rosette.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2024 Emily Schmidt <[email protected]>
* 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
Expand Down Expand Up @@ -174,8 +175,8 @@ struct SmtrPrintVisitor : public Functional::AbstractVisitor<SExpr> {
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) override { return input_struct.access("inputs", name); }
SExpr state(Node, IdString name) override { return state_struct.access("state", name); }
SExpr input(Node, IdString name, IdString type) override { log_assert(type == ID($input)); return input_struct.access("inputs", name); }
SExpr state(Node, IdString name, IdString type) override { log_assert(type == ID($state)); return state_struct.access("state", name); }
};

struct SmtrModule {
Expand All @@ -196,12 +197,12 @@ struct SmtrModule {
, state_struct(scope.unique_name(module->name.str() + "_State"), scope)
{
scope.reserve(name + "_initial");
for (const auto &input : ir.inputs())
input_struct.insert(input.first, input.second);
for (const auto &output : ir.outputs())
output_struct.insert(output.first, output.second);
for (const auto &state : ir.state())
state_struct.insert(state.first, state.second);
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)
Expand Down Expand Up @@ -231,22 +232,22 @@ struct SmtrModule {
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.get_output_node(name)); });
state_struct.write_value(w, [&](IdString name) { return node_to_sexpr(ir.get_state_next_node(name)); });
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 (const auto &[name, sort] : ir.state()) {
if (sort.is_signal())
w << list("bv", smt_const(ir.get_initial_state_signal(name)), sort.width());
else if (sort.is_memory()) {
auto contents = ir.get_initial_state_memory(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]), sort.data_width());
for(int i = 0; i < 1<<state->sort.addr_width(); i++) {
w << list("bv", smt_const(contents[i]), state->sort.data_width());
}
w.close();
}
Expand Down
9 changes: 5 additions & 4 deletions backends/functional/test_generic.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2024 Emily Schmidt <[email protected]>
* 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
Expand Down Expand Up @@ -142,10 +143,10 @@ struct FunctionalTestGeneric : public Pass
auto fir = Functional::IR::from_module(module);
for(auto node : fir)
std::cout << RTLIL::unescape_id(node.name()) << " = " << node.to_string([](auto n) { return RTLIL::unescape_id(n.name()); }) << "\n";
for(auto [name, sort] : fir.outputs())
std::cout << "output " << RTLIL::unescape_id(name) << " = " << RTLIL::unescape_id(fir.get_output_node(name).name()) << "\n";
for(auto [name, sort] : fir.state())
std::cout << "state " << RTLIL::unescape_id(name) << " = " << RTLIL::unescape_id(fir.get_state_next_node(name).name()) << "\n";
for(auto output : fir.all_outputs())
std::cout << RTLIL::unescape_id(output->type) << " " << RTLIL::unescape_id(output->name) << " = " << RTLIL::unescape_id(output->value().name()) << "\n";
for(auto state : fir.all_states())
std::cout << RTLIL::unescape_id(state->type) << " " << RTLIL::unescape_id(state->name) << " = " << RTLIL::unescape_id(state->next_value().name()) << "\n";
}
}
} FunctionalCxxBackend;
Expand Down
Loading

0 comments on commit 97d6be0

Please sign in to comment.