mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-07-23 23:52:32 +00:00
Code Activity

functinoal: twines

Browse source
This commit is contained in:
Emil J. Tywoniak 2026-06-24 11:53:14 +02:00
parent 5b5e7ce771
commit d8e09f4e0c
4 changed files with 56 additions and 47 deletions
Download patch file Download diff file Expand all files Collapse all files

37
backends/functional/smtlib_rosette.cc
View file

@ -44,7 +44,8 @@ const char *reserved_keywords[] = {
};
struct SmtrScope : public Functional::Scope<int> {
SmtrScope() {
SmtrScope(Design *design = nullptr) {
this->design = design;
for(const char **p = reserved_keywords; *p != nullptr; p++)
reserve(*p);
}
@ -73,14 +74,15 @@ class SmtrStruct {
std::string accessor;
std::string name;
};
idict<IdString> field_names;
idict<TwineRef> field_names;
vector<Field> fields;
SmtrScope &global_scope;
SmtrScope local_scope;
Design *design;
public:
std::string name;
SmtrStruct(std::string name, SmtrScope &scope) : global_scope(scope), local_scope(), name(name) {}
void insert(IdString field_name, SmtrSort sort) {
SmtrStruct(std::string name, SmtrScope &scope, Design *design) : global_scope(scope), local_scope(design), design(design), name(name) {}
void insert(TwineRef field_name, SmtrSort sort) {
field_names(field_name);
auto base_name = local_scope.unique_name(field_name);
auto accessor = name + "-" + base_name;
@ -106,11 +108,11 @@ public:
w.open(list(name));
for(auto field_name : field_names) {
w << fn(field_name);
w.comment(field_name.unescape(), true);
w.comment(design->twines.unescaped_str(field_name), true);
}
w.close();
}
SExpr access(SExpr record, IdString name) {
SExpr access(SExpr record, TwineRef name) {
size_t i = field_names.at(name);
return list(fields[i].accessor, std::move(record));
}
@ -180,12 +182,13 @@ 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, IdString kind) override { log_assert(kind == TW($input)); return input_struct.access("inputs", name); }
SExpr state(Node, IdString name, IdString kind) override { log_assert(kind == TW($state)); return state_struct.access("state", name); }
SExpr input(Node, TwineRef name, TwineRef kind) override { log_assert(kind == TW($input)); return input_struct.access("inputs", name); }
SExpr state(Node, TwineRef name, TwineRef kind) override { log_assert(kind == TW($state)); return state_struct.access("state", name); }
};
struct SmtrModule {
Functional::IR ir;
Design *design;
SmtrScope scope;
std::string name;
bool use_assoc_list_helpers;
@ -197,16 +200,16 @@ struct SmtrModule {
SmtrStruct state_struct;
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)
: ir(Functional::IR::from_module(module)), design(module->design), scope(module->design), name(scope.unique_name(module->name.ref())), use_assoc_list_helpers(assoc_list_helpers),
input_struct(scope.unique_name(module->design->twines.add(module->name.str() + "_Inputs")), scope, module->design),
output_struct(scope.unique_name(module->design->twines.add(module->name.str() + "_Outputs")), scope, module->design),
state_struct(scope.unique_name(module->design->twines.add(module->name.str() + "_State")), scope, module->design)
{
scope.reserve(name + "_initial");
if (assoc_list_helpers) {
input_helper_name = scope.unique_name(module->name.str() + "_inputs_helper");
input_helper_name = scope.unique_name(module->design->twines.add(module->name.str() + "_inputs_helper"));
scope.reserve(*input_helper_name);
output_helper_name = scope.unique_name(module->name.str() + "_outputs_helper");
output_helper_name = scope.unique_name(module->design->twines.add(module->name.str() + "_outputs_helper"));
scope.reserve(*output_helper_name);
}
for (auto input : ir.inputs())
@ -238,8 +241,8 @@ 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.output(name).value()); });
state_struct.write_value(w, [&](IdString name) { return node_to_sexpr(ir.state(name).next_value()); });
output_struct.write_value(w, [&](TwineRef name) { return node_to_sexpr(ir.output(name).value()); });
state_struct.write_value(w, [&](TwineRef name) { return node_to_sexpr(ir.state(name).next_value()); });
w.pop();
}
@ -363,7 +366,7 @@ struct FunctionalSmtrBackend : public Backend {
}
for (auto module : design->selected_modules()) {
log("Processing module `%s`.\n", module->name.c_str());
log("Processing module `%s`.\n", module->name.str().c_str());
SmtrModule smtr(module, assoc_list_helpers);
smtr.write(*f);
}