riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

docs/rosette: Regen rosette.diff 

This time from the actual source, which apparently means changing all of the spaces for tabs.
This commit is contained in:
Krystine Sherwin 2025-02-07 14:13:34 +13:00
parent fa2d45a922
commit dc5a5b7bd1
No known key found for this signature in database
1 changed files with 320 additions and 334 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

654
docs/source/code_examples/functional/rosette.diff
View File

@ -1,385 +1,371 @@
diff --git a/smtlib.cc b/smtlib_rosette.cc diff --git a/backends/functional/smtlib.cc b/backends/functional/smtlib_rosette.cc
index 3eacf407c..a93bd04b0 100644 index 3eacf407c..c9e737d19 100644
--- a/smtlib.cc --- a/backends/functional/smtlib.cc
+++ b/smtlib_rosette.cc +++ b/backends/functional/smtlib_rosette.cc
@@ -29,80 +29,86 @@ PRIVATE_NAMESPACE_BEGIN @@ -29,80 +29,86 @@ PRIVATE_NAMESPACE_BEGIN
using SExprUtil::list; using SExprUtil::list;
const char *reserved_keywords[] = { const char *reserved_keywords[] = {
- // reserved keywords from the smtlib spec - // reserved keywords from the smtlib spec
- "BINARY", "DECIMAL", "HEXADECIMAL", "NUMERAL", "STRING", "_", "!", "as", "let", "exists", "forall", "match", "par", - "BINARY", "DECIMAL", "HEXADECIMAL", "NUMERAL", "STRING", "_", "!", "as", "let", "exists", "forall", "match", "par",
- "assert", "check-sat", "check-sat-assuming", "declare-const", "declare-datatype", "declare-datatypes", - "assert", "check-sat", "check-sat-assuming", "declare-const", "declare-datatype", "declare-datatypes",
- "declare-fun", "declare-sort", "define-fun", "define-fun-rec", "define-funs-rec", "define-sort", - "declare-fun", "declare-sort", "define-fun", "define-fun-rec", "define-funs-rec", "define-sort",
- "exit", "get-assertions", "symbol", "sort", "get-assignment", "get-info", "get-model", - "exit", "get-assertions", "symbol", "sort", "get-assignment", "get-info", "get-model",
- "get-option", "get-proof", "get-unsat-assumptions", "get-unsat-core", "get-value", - "get-option", "get-proof", "get-unsat-assumptions", "get-unsat-core", "get-value",
- "pop", "push", "reset", "reset-assertions", "set-info", "set-logic", "set-option", - "pop", "push", "reset", "reset-assertions", "set-info", "set-logic", "set-option",
+ // reserved keywords from the racket spec + // reserved keywords from the racket spec
+ "struct", "lambda", "values", "extract", "concat", "bv", "let", "define", "cons", "list", "read", "write", + "struct", "lambda", "values", "extract", "concat", "bv", "let", "define", "cons", "list", "read", "write",
+ "stream", "error", "raise", "exit", "for", "begin", "when", "unless", "module", "require", "provide", "apply", + "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", + "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", + "future", "touch", "subprocess", "make-custodian", "custodian-shutdown-all", "current-custodian", "make", "tcp",
+ "connect", "prepare", "malloc", "free", "_fun", "_cprocedure", "build", "path", "file", "peek", "bytes", + "connect", "prepare", "malloc", "free", "_fun", "_cprocedure", "build", "path", "file", "peek", "bytes",
+ "flush", "with", "lexer", "parser", "syntax", "interface", "send", "make-object", "new", "instantiate", + "flush", "with", "lexer", "parser", "syntax", "interface", "send", "make-object", "new", "instantiate",
+ "define-generics", "set", + "define-generics", "set",
// reserved for our own purposes // reserved for our own purposes
- "pair", "Pair", "first", "second", - "pair", "Pair", "first", "second",
- "inputs", "state", - "inputs", "state",
+ "inputs", "state", "name", + "inputs", "state", "name",
nullptr nullptr
}; };
-struct SmtScope : public Functional::Scope<int> { -struct SmtScope : public Functional::Scope<int> {
- SmtScope() { - SmtScope() {
+struct SmtrScope : public Functional::Scope<int> { +struct SmtrScope : public Functional::Scope<int> {
+ SmtrScope() { + SmtrScope() {
for(const char **p = reserved_keywords; *p != nullptr; p++) for(const char **p = reserved_keywords; *p != nullptr; p++)
reserve(*p); reserve(*p);
} }
bool is_character_legal(char c, int index) override { bool is_character_legal(char c, int index) override {
- return isascii(c) && (isalpha(c) || (isdigit(c) && index > 0) || strchr("~!@$%^&*_-+=<>.?/", c)); - return isascii(c) && (isalpha(c) || (isdigit(c) && index > 0) || strchr("~!@$%^&*_-+=<>.?/", c));
+ return isascii(c) && (isalpha(c) || (isdigit(c) && index > 0) || strchr("@$%^&_+=.", c)); + return isascii(c) && (isalpha(c) || (isdigit(c) && index > 0) || strchr("@$%^&_+=.", c));
} }
}; };
-struct SmtSort { -struct SmtSort {
+struct SmtrSort { +struct SmtrSort {
Functional::Sort sort; Functional::Sort sort;
- SmtSort(Functional::Sort sort) : sort(sort) {} - SmtSort(Functional::Sort sort) : sort(sort) {}
+ SmtrSort(Functional::Sort sort) : sort(sort) {} + SmtrSort(Functional::Sort sort) : sort(sort) {}
SExpr to_sexpr() const { SExpr to_sexpr() const {
if(sort.is_memory()) { if(sort.is_memory()) {
- return list("Array", list("_", "BitVec", sort.addr_width()), list("_", "BitVec", sort.data_width())); - return list("Array", list("_", "BitVec", sort.addr_width()), list("_", "BitVec", sort.data_width()));
+ return list("list", list("bitvector", sort.addr_width()), list("bitvector", sort.data_width())); + return list("list", list("bitvector", sort.addr_width()), list("bitvector", sort.data_width()));
} else if(sort.is_signal()) { } else if(sort.is_signal()) {
- return list("_", "BitVec", sort.width()); - return list("_", "BitVec", sort.width());
+ return list("bitvector", sort.width()); + return list("bitvector", sort.width());
} else { } else {
log_error("unknown sort"); log_error("unknown sort");
} }
} }
}; };
-class SmtStruct { -class SmtStruct {
+class SmtrStruct { +class SmtrStruct {
struct Field { struct Field {
- SmtSort sort; - SmtSort sort;
+ SmtrSort sort; + SmtrSort sort;
std::string accessor; std::string accessor;
+ std::string name; + std::string name;
}; };
idict<IdString> field_names; idict<IdString> field_names;
vector<Field> fields; vector<Field> fields;
- SmtScope &scope; - SmtScope &scope;
+ SmtrScope &global_scope; + SmtrScope &global_scope;
+ SmtrScope local_scope; + SmtrScope local_scope;
public: public:
std::string name; std::string name;
- SmtStruct(std::string name, SmtScope &scope) : scope(scope), name(name) {} - SmtStruct(std::string name, SmtScope &scope) : scope(scope), name(name) {}
- void insert(IdString field_name, SmtSort sort) { - void insert(IdString field_name, SmtSort sort) {
+ SmtrStruct(std::string name, SmtrScope &scope) : global_scope(scope), local_scope(), name(name) {} + SmtrStruct(std::string name, SmtrScope &scope) : global_scope(scope), local_scope(), name(name) {}
+ void insert(IdString field_name, SmtrSort sort) { + void insert(IdString field_name, SmtrSort sort) {
field_names(field_name); field_names(field_name);
- auto accessor = scope.unique_name("\\" + name + "_" + RTLIL::unescape_id(field_name)); - auto accessor = scope.unique_name("\\" + name + "_" + RTLIL::unescape_id(field_name));
- fields.emplace_back(Field{sort, accessor}); - fields.emplace_back(Field{sort, accessor});
+ auto base_name = local_scope.unique_name(field_name); + auto base_name = local_scope.unique_name(field_name);
+ auto accessor = name + "-" + base_name; + auto accessor = name + "-" + base_name;
+ global_scope.reserve(accessor); + global_scope.reserve(accessor);
+ fields.emplace_back(Field{sort, accessor, base_name}); + fields.emplace_back(Field{sort, accessor, base_name});
} }
void write_definition(SExprWriter &w) { void write_definition(SExprWriter &w) {
- w.open(list("declare-datatype", name)); - w.open(list("declare-datatype", name));
- w.open(list()); - w.open(list());
- w.open(list(name)); - w.open(list(name));
- for(const auto &field : fields) - for(const auto &field : fields)
- w << list(field.accessor, field.sort.to_sexpr()); - w << list(field.accessor, field.sort.to_sexpr());
- w.close(3); - w.close(3);
+ vector<SExpr> field_list; + vector<SExpr> field_list;
+ for(const auto &field : fields) { + for(const auto &field : fields) {
+ field_list.emplace_back(field.name); + field_list.emplace_back(field.name);
+ } + }
+ w.push(); + w.push();
+ w.open(list("struct", name, field_list, "#:transparent")); + w.open(list("struct", name, field_list, "#:transparent"));
+ if (field_names.size()) { + if (field_names.size()) {
+ for (const auto &field : fields) { + for (const auto &field : fields) {
+ auto bv_type = field.sort.to_sexpr(); + auto bv_type = field.sort.to_sexpr();
+ w.comment(field.name + " " + bv_type.to_string()); + w.comment(field.name + " " + bv_type.to_string());
+ } + }
+ } + }
+ w.pop(); + w.pop();
} }
template<typename Fn> void write_value(SExprWriter &w, Fn fn) { template<typename Fn> void write_value(SExprWriter &w, Fn fn) {
- if(field_names.empty()) { - if(field_names.empty()) {
- // Zero-argument constructors in SMTLIB must not be called as functions. - // Zero-argument constructors in SMTLIB must not be called as functions.
- w << name; - w << name;
- } else { - } else {
- w.open(list(name)); - w.open(list(name));
- for(auto field_name : field_names) { - for(auto field_name : field_names) {
- w << fn(field_name); - w << fn(field_name);
- w.comment(RTLIL::unescape_id(field_name), true); - w.comment(RTLIL::unescape_id(field_name), true);
- } - }
- w.close(); - w.close();
+ w.open(list(name)); + w.open(list(name));
+ for(auto field_name : field_names) { + for(auto field_name : field_names) {
+ w << fn(field_name); + w << fn(field_name);
+ w.comment(RTLIL::unescape_id(field_name), true); + w.comment(RTLIL::unescape_id(field_name), true);
} }
+ w.close(); + w.close();
} }
SExpr access(SExpr record, IdString name) { SExpr access(SExpr record, IdString name) {
size_t i = field_names.at(name); size_t i = field_names.at(name);
@@ -117,28 +123,28 @@ std::string smt_const(RTLIL::Const const &c) { @@ -117,28 +123,28 @@ std::string smt_const(RTLIL::Const const &c) {
return s; return s;
} }
-struct SmtPrintVisitor : public Functional::AbstractVisitor<SExpr> { -struct SmtPrintVisitor : public Functional::AbstractVisitor<SExpr> {
+struct SmtrPrintVisitor : public Functional::AbstractVisitor<SExpr> { +struct SmtrPrintVisitor : public Functional::AbstractVisitor<SExpr> {
using Node = Functional::Node; using Node = Functional::Node;
std::function<SExpr(Node)> n; std::function<SExpr(Node)> n;
- SmtStruct &input_struct; - SmtStruct &input_struct;
- SmtStruct &state_struct; - SmtStruct &state_struct;
+ SmtrStruct &input_struct; + SmtrStruct &input_struct;
+ SmtrStruct &state_struct; + SmtrStruct &state_struct;
- SmtPrintVisitor(SmtStruct &input_struct, SmtStruct &state_struct) : input_struct(input_struct), state_struct(state_struct) {} - SmtPrintVisitor(SmtStruct &input_struct, SmtStruct &state_struct) : input_struct(input_struct), state_struct(state_struct) {}
+ SmtrPrintVisitor(SmtrStruct &input_struct, SmtrStruct &state_struct) : input_struct(input_struct), state_struct(state_struct) {} + SmtrPrintVisitor(SmtrStruct &input_struct, SmtrStruct &state_struct) : input_struct(input_struct), state_struct(state_struct) {}
SExpr from_bool(SExpr &&arg) { SExpr from_bool(SExpr &&arg) {
- return list("ite", std::move(arg), "#b1", "#b0"); - return list("ite", std::move(arg), "#b1", "#b0");
+ return list("bool->bitvector", std::move(arg)); + return list("bool->bitvector", std::move(arg));
} }
SExpr to_bool(SExpr &&arg) { SExpr to_bool(SExpr &&arg) {
- return list("=", std::move(arg), "#b1"); - return list("=", std::move(arg), "#b1");
+ return list("bitvector->bool", std::move(arg)); + return list("bitvector->bool", std::move(arg));
} }
- SExpr extract(SExpr &&arg, int offset, int out_width = 1) { - SExpr extract(SExpr &&arg, int offset, int out_width = 1) {
- return list(list("_", "extract", offset + out_width - 1, offset), std::move(arg)); - return list(list("_", "extract", offset + out_width - 1, offset), std::move(arg));
+ SExpr to_list(SExpr &&arg) { + SExpr to_list(SExpr &&arg) {
+ return list("bitvector->bits", std::move(arg)); + return list("bitvector->bits", std::move(arg));
} }
SExpr buf(Node, Node a) override { return n(a); } SExpr buf(Node, Node a) override { return n(a); }
- SExpr slice(Node, Node a, int offset, int out_width) override { return extract(n(a), offset, out_width); } - SExpr slice(Node, Node a, int offset, int out_width) override { return extract(n(a), offset, out_width); }
- SExpr zero_extend(Node, Node a, int out_width) override { return list(list("_", "zero_extend", out_width - a.width()), n(a)); } - SExpr zero_extend(Node, Node a, int out_width) override { return list(list("_", "zero_extend", out_width - a.width()), n(a)); }
- SExpr sign_extend(Node, Node a, int out_width) override { return list(list("_", "sign_extend", out_width - a.width()), n(a)); } - SExpr sign_extend(Node, Node a, int out_width) override { return list(list("_", "sign_extend", out_width - a.width()), n(a)); }
+ SExpr slice(Node, Node a, int offset, int out_width) override { return list("extract", offset + out_width - 1, offset, 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 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 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 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 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 sub(Node, Node a, Node b) override { return list("bvsub", n(a), n(b)); }
@@ -150,16 +156,11 @@ struct SmtPrintVisitor : public Functional::AbstractVisitor<SExpr> { @@ -150,16 +156,11 @@ struct SmtPrintVisitor : public Functional::AbstractVisitor<SExpr> {
SExpr bitwise_xor(Node, Node a, Node b) override { return list("bvxor", 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 bitwise_not(Node, Node a) override { return list("bvnot", n(a)); }
SExpr unary_minus(Node, Node a) override { return list("bvneg", 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), smt_const(RTLIL::Const(State::S1, 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_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 { - SExpr reduce_xor(Node, Node a) override {
- vector<SExpr> s { "bvxor" }; - vector<SExpr> s { "bvxor" };
- for(int i = 0; i < a.width(); i++) - for(int i = 0; i < a.width(); i++)
- s.push_back(extract(n(a), i)); - s.push_back(extract(n(a), i));
- return s; - return s;
- } - }
- SExpr equal(Node, Node a, Node b) override { return from_bool(list("=", n(a), n(b))); } - SExpr equal(Node, Node a, Node b) override { return from_bool(list("=", n(a), n(b))); }
- SExpr not_equal(Node, Node a, Node b) override { return from_bool(list("distinct", n(a), n(b))); } - SExpr not_equal(Node, Node a, Node b) override { return from_bool(list("distinct", n(a), n(b))); }
+ SExpr reduce_and(Node, Node a) override { return list("apply", "bvand", to_list(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_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 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 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 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_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 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_than(Node, Node a, Node b) override { return from_bool(list("bvugt", n(a), n(b))); }
@@ -167,32 +168,32 @@ struct SmtPrintVisitor : public Functional::AbstractVisitor<SExpr> { @@ -167,32 +168,32 @@ struct SmtPrintVisitor : public Functional::AbstractVisitor<SExpr> {
SExpr extend(SExpr &&a, int in_width, int out_width) { SExpr extend(SExpr &&a, int in_width, int out_width) {
if(in_width < out_width) if(in_width < out_width)
- return list(list("_", "zero_extend", out_width - in_width), std::move(a)); - return list(list("_", "zero_extend", out_width - in_width), std::move(a));
+ return list("zero-extend", std::move(a), list("bitvector", out_width)); + return list("zero-extend", std::move(a), list("bitvector", out_width));
else else
return std::move(a); 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_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 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 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 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 const &value) override { return smt_const(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_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 memory_write(Node, Node mem, Node addr, Node data) override { return list("store", n(mem), n(addr), n(data)); }
+ SExpr mux(Node, Node a, Node b, Node s) override { return list("if", to_bool(n(s)), n(b), n(a)); } + 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 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_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 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 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); } SExpr state(Node, IdString name, IdString kind) override { log_assert(kind == ID($state)); return state_struct.access("state", name); }
}; };
-struct SmtModule { -struct SmtModule {
+struct SmtrModule { +struct SmtrModule {
Functional::IR ir; Functional::IR ir;
- SmtScope scope; - SmtScope scope;
+ SmtrScope scope; + SmtrScope scope;
std::string name; std::string name;
- SmtStruct input_struct; - SmtStruct input_struct;
- SmtStruct output_struct; - SmtStruct output_struct;
- SmtStruct state_struct; - SmtStruct state_struct;
+ SmtrStruct input_struct; + SmtrStruct input_struct;
+ SmtrStruct output_struct; + SmtrStruct output_struct;
+ SmtrStruct state_struct; + SmtrStruct state_struct;
- SmtModule(Module *module) - SmtModule(Module *module)
+ SmtrModule(Module *module) + SmtrModule(Module *module)
: ir(Functional::IR::from_module(module)) : ir(Functional::IR::from_module(module))
, scope() , scope()
, name(scope.unique_name(module->name)) , name(scope.unique_name(module->name))
@@ -200,7 +201,7 @@ struct SmtModule { @@ -200,7 +201,7 @@ struct SmtModule {
, output_struct(scope.unique_name(module->name.str() + "_Outputs"), scope) , output_struct(scope.unique_name(module->name.str() + "_Outputs"), scope)
, state_struct(scope.unique_name(module->name.str() + "_State"), scope) , state_struct(scope.unique_name(module->name.str() + "_State"), scope)
{ {
- scope.reserve(name + "-initial"); - scope.reserve(name + "-initial");
+ scope.reserve(name + "_initial"); + scope.reserve(name + "_initial");
for (auto input : ir.inputs()) for (auto input : ir.inputs())
input_struct.insert(input->name, input->sort); input_struct.insert(input->name, input->sort);
for (auto output : ir.outputs()) for (auto output : ir.outputs())
@@ -209,17 +210,20 @@ struct SmtModule { @@ -212,14 +213,11 @@ struct SmtModule {
state_struct.insert(state->name, state->sort); void write_eval(SExprWriter &w)
} {
w.push();
- w.open(list("define-fun", name,
- list(list("inputs", input_struct.name),
- list("state", state_struct.name)),
- list("Pair", output_struct.name, state_struct.name)));
+ w.open(list("define", list(name, "inputs", "state")));
auto inlined = [&](Functional::Node n) {
return n.fn() == Functional::Fn::constant;
};
- SmtPrintVisitor visitor(input_struct, state_struct);
+ SmtrPrintVisitor visitor(input_struct, state_struct);
auto node_to_sexpr = [&](Functional::Node n) -> SExpr {
if(inlined(n))
return n.visit(visitor);
@@ -230,9 +228,9 @@ struct SmtModule {
for(auto n : ir)
if(!inlined(n)) {
w.open(list("let", list(list(node_to_sexpr(n), n.visit(visitor)))), false);
- w.comment(SmtSort(n.sort()).to_sexpr().to_string(), true);
+ w.comment(SmtrSort(n.sort()).to_sexpr().to_string(), true);
}
- w.open(list("pair"));
+ 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();
@@ -240,19 +238,23 @@ struct SmtModule {
- void write_eval(SExprWriter &w) void write_initial(SExprWriter &w)
- { {
+ void write(std::ostream &out) - std::string initial = name + "-initial";
+ { - w << list("declare-const", initial, state_struct.name);
+ SExprWriter w(out); + w.push();
+ + auto initial = name + "_initial";
+ input_struct.write_definition(w); + w.open(list("define", initial));
+ output_struct.write_definition(w); + w.open(list(state_struct.name));
+ state_struct.write_definition(w); for (auto state : ir.states()) {
+ - if(state->sort.is_signal())
w.push(); - w << list("assert", list("=", state_struct.access(initial, state->name), smt_const(state->initial_value_signal())));
- w.open(list("define-fun", name, - else if(state->sort.is_memory()) {
- list(list("inputs", input_struct.name), + if (state->sort.is_signal())
- list("state", state_struct.name)), + w << list("bv", smt_const(state->initial_value_signal()), state->sort.width());
- list("Pair", output_struct.name, state_struct.name))); + else if (state->sort.is_memory()) {
+ w.open(list("define", list(name, "inputs", "state"))); const auto &contents = state->initial_value_memory();
auto inlined = [&](Functional::Node n) { + w.open(list("list"));
return n.fn() == Functional::Fn::constant; for(int i = 0; i < 1<<state->sort.addr_width(); i++) {
}; - auto addr = smt_const(RTLIL::Const(i, state->sort.addr_width()));
- SmtPrintVisitor visitor(input_struct, state_struct); - w << list("assert", list("=", list("select", state_struct.access(initial, state->name), addr), smt_const(contents[i])));
+ SmtrPrintVisitor visitor(input_struct, state_struct); + w << list("bv", smt_const(contents[i]), state->sort.data_width());
auto node_to_sexpr = [&](Functional::Node n) -> SExpr { }
if(inlined(n)) + w.close();
return n.visit(visitor); }
@@ -230,66 +234,75 @@ struct SmtModule { }
for(auto n : ir) + w.pop();
if(!inlined(n)) { }
w.open(list("let", list(list(node_to_sexpr(n), n.visit(visitor)))), false);
- w.comment(SmtSort(n.sort()).to_sexpr().to_string(), true);
+ w.comment(SmtrSort(n.sort()).to_sexpr().to_string(), true);
}
- w.open(list("pair"));
+ 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();
- }
- void write_initial(SExprWriter &w) void write(std::ostream &out)
- { @@ -263,33 +265,53 @@ struct SmtModule {
- std::string initial = name + "-initial"; output_struct.write_definition(w);
- w << list("declare-const", initial, state_struct.name); state_struct.write_definition(w);
+ w.push();
+ auto initial = name + "_initial"; - w << list("declare-datatypes",
+ w.open(list("define", initial)); - list(list("Pair", 2)),
+ w.open(list(state_struct.name)); - list(list("par", list("X", "Y"), list(list("pair", list("first", "X"), list("second", "Y"))))));
for (auto state : ir.states()) { -
- if(state->sort.is_signal()) write_eval(w);
- w << list("assert", list("=", state_struct.access(initial, state->name), smt_const(state->initial_value_signal()))); write_initial(w);
- else if(state->sort.is_memory()) { }
+ 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<<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])));
+ w << list("bv", smt_const(contents[i]), state->sort.data_width());
}
+ w.close();
}
}
- }
-
- 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);
+ w.pop();
}
}; };
-struct FunctionalSmtBackend : public Backend { -struct FunctionalSmtBackend : public Backend {
- FunctionalSmtBackend() : Backend("functional_smt2", "Generate SMT-LIB from Functional IR") {} - FunctionalSmtBackend() : Backend("functional_smt2", "Generate SMT-LIB from Functional IR") {}
+struct FunctionalSmtrBackend : public Backend { +struct FunctionalSmtrBackend : public Backend {
+ FunctionalSmtrBackend() : Backend("functional_rosette", "Generate Rosette compatible Racket from Functional IR") {} + FunctionalSmtrBackend() : Backend("functional_rosette", "Generate Rosette compatible Racket from Functional IR") {}
- void help() override { log("\nFunctional SMT Backend.\n\n"); } - void help() override { log("\nFunctional SMT Backend.\n\n"); }
+ void help() override { + void help() override {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n"); + log("\n");
+ log(" write_functional_rosette [options] [filename]\n"); + log(" write_functional_rosette [options] [filename]\n");
+ log("\n"); + log("\n");
+ log("Functional Rosette Backend.\n"); + log("Functional Rosette Backend.\n");
+ log("\n"); + log("\n");
+ log(" -provides\n"); + log(" -provides\n");
+ log(" include 'provide' statement(s) for loading output as a module\n"); + log(" include 'provide' statement(s) for loading output as a module\n");
+ log("\n"); + log("\n");
+ } + }
void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
{ {
- log_header(design, "Executing Functional SMT Backend.\n"); - log_header(design, "Executing Functional SMT Backend.\n");
+ auto provides = false; + auto provides = false;
+ +
+ log_header(design, "Executing Functional Rosette Backend.\n"); + log_header(design, "Executing Functional Rosette Backend.\n");
- size_t argidx = 1; - size_t argidx = 1;
- extra_args(f, filename, args, argidx, design); - extra_args(f, filename, args, argidx, design);
+ size_t argidx; + size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++) + for (argidx = 1; argidx < args.size(); argidx++)
+ { + {
+ if (args[argidx] == "-provides") + if (args[argidx] == "-provides")
+ provides = true; + provides = true;
+ else + else
+ break; + break;
+ } + }
+ extra_args(f, filename, args, argidx); + extra_args(f, filename, args, argidx);
+ +
+ *f << "#lang rosette/safe\n"; + *f << "#lang rosette/safe\n";
+ if (provides) { + if (provides) {
+ *f << "(provide (all-defined-out))\n"; + *f << "(provide (all-defined-out))\n";
+ } + }
for (auto module : design->selected_modules()) { for (auto module : design->selected_modules()) {
log("Processing module `%s`.\n", module->name.c_str()); log("Processing module `%s`.\n", module->name.c_str());
- SmtModule smt(module); - SmtModule smt(module);
- smt.write(*f); - smt.write(*f);
+ SmtrModule smtr(module); + SmtrModule smtr(module);
+ smtr.write(*f); + smtr.write(*f);
} }
} }
-} FunctionalSmtBackend; -} FunctionalSmtBackend;
+} FunctionalSmtrBackend; +} FunctionalSmtrBackend;