mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-07-29 23:43:16 +00:00
Code Activity

add support for initializing registers and memories to the functional backend

Browse source
This commit is contained in:
Emily Schmidt 2024-07-24 17:37:17 +01:00
parent bdb59ffc8e
commit 99effb6789
10 changed files with 418 additions and 282 deletions
Download patch file Download diff file Expand all files Collapse all files

68
backends/functional/smtlib.cc
View file

@ -109,6 +109,13 @@ public:
}
};
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 SmtPrintVisitor : public FunctionalIR::AbstractVisitor<SExpr> {
using Node = FunctionalIR::Node;
std::function<SExpr(Node)> n;
@ -117,13 +124,6 @@ struct SmtPrintVisitor : public FunctionalIR::AbstractVisitor<SExpr> {
SmtPrintVisitor(SmtStruct &input_struct, SmtStruct &state_struct) : input_struct(input_struct), state_struct(state_struct) {}
std::string literal(RTLIL::Const c) {
std::string s = "#b";
for(int i = c.size(); i-- > 0; )
s += c[i] == State::S1 ? '1' : '0';
return s;
}
SExpr from_bool(SExpr &&arg) {
return list("ite", std::move(arg), "#b1", "#b0");
}
@ -149,8 +149,8 @@ struct SmtPrintVisitor : public FunctionalIR::AbstractVisitor<SExpr> {
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 from_bool(list("=", n(a), literal(RTLIL::Const(State::S1, a.width())))); }
SExpr reduce_or(Node, Node a) override { return from_bool(list("distinct", n(a), literal(RTLIL::Const(State::S0, a.width())))); }
SExpr reduce_and(Node, Node a) override { return from_bool(list("=", n(a), smt_const(RTLIL::Const(State::S1, a.width())))); }
SExpr reduce_or(Node, Node a) override { return from_bool(list("distinct", n(a), smt_const(RTLIL::Const(State::S0, a.width())))); }
SExpr reduce_xor(Node, Node a) override {
vector<SExpr> s { "bvxor" };
for(int i = 0; i < a.width(); i++)
@ -174,7 +174,7 @@ struct SmtPrintVisitor : public FunctionalIR::AbstractVisitor<SExpr> {
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("ite", to_bool(n(s)), n(b), n(a)); }
SExpr constant(Node, RTLIL::Const value) override { return literal(value); }
SExpr constant(Node, RTLIL::Const const &value) override { return smt_const(value); }
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)); }
@ -199,6 +199,7 @@ struct SmtModule {
, 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 (const auto &input : ir.inputs())
input_struct.insert(input.first, input.second);
for (const auto &output : ir.outputs())
@ -207,18 +208,8 @@ struct SmtModule {
state_struct.insert(state.first, state.second);
}
void write(std::ostream &out)
{
SExprWriter w(out);
input_struct.write_definition(w);
output_struct.write_definition(w);
state_struct.write_definition(w);
w << list("declare-datatypes",
list(list("Pair", 2)),
list(list("par", list("X", "Y"), list(list("pair", list("first", "X"), list("second", "Y"))))));
void write_eval(SExprWriter &w)
{
w.push();
w.open(list("define-fun", name,
list(list("inputs", input_struct.name),
@ -245,6 +236,39 @@ struct SmtModule {
state_struct.write_value(w, [&](IdString name) { return node_to_sexpr(ir.get_state_next_node(name)); });
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])));
}
}
}
}
void write(std::ostream &out)
{
SExprWriter w(out);
input_struct.write_definition(w);
output_struct.write_definition(w);
state_struct.write_definition(w);
w << list("declare-datatypes",
list(list("Pair", 2)),
list(list("par", list("X", "Y"), list(list("pair", list("first", "X"), list("second", "Y"))))));
write_eval(w);
write_initial(w);
}
};
struct FunctionalSmtBackend : public Backend {