mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-07-19 13:45:48 +00:00
Code Activity

Merge branch 'YosysHQ:main' into main

Browse source
This commit is contained in:
Akash Levy 2025-12-03 13:28:56 -05:00 • committed by GitHub
commit 5dfadb968f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
7 changed files with 145 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

76
backends/functional/smtlib_rosette.cc
View file

@ -188,20 +188,27 @@ struct SmtrModule {
Functional::IR ir;
SmtrScope scope;
std::string name;
bool use_assoc_list_helpers;
std::optional<std::string> input_helper_name;
std::optional<std::string> output_helper_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)
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)
{
scope.reserve(name + "_initial");
if (assoc_list_helpers) {
input_helper_name = scope.unique_name(module->name.str() + "_inputs_helper");
scope.reserve(*input_helper_name);
output_helper_name = scope.unique_name(module->name.str() + "_outputs_helper");
scope.reserve(*output_helper_name);
}
for (auto input : ir.inputs())
input_struct.insert(input->name, input->sort);
for (auto output : ir.outputs())
@ -257,6 +264,45 @@ struct SmtrModule {
w.pop();
}
void write_assoc_list_helpers(SExprWriter &w)
{
log_assert(output_helper_name && input_helper_name);
// Input struct keyword-based constructor.
w.push();
w.open(list("define"));
const auto inputs_name = "inputs";
w.open(list(*input_helper_name, inputs_name));
w.close();
w.open(list(input_struct.name));
for (auto input : ir.inputs()) {
w.push();
w.open(list("let"));
w.push();
w.open(list());
w.open(list("assoc-result"));
w << list("assoc", "\"" + RTLIL::unescape_id(input->name) + "\"", inputs_name);
w.pop();
w.open(list("if", "assoc-result"));
w << list("cdr", "assoc-result");
w.open(list("begin"));
w << list("fprintf", list("current-error-port"), "\"%s not found in inputs\"");
w << "'not-found";
w.pop();
}
w.pop();
// Output struct keyword-based destructuring
w.push();
w.open(list("define"));
const auto outputs_name = "outputs";
w << list(*output_helper_name, outputs_name);
w.open(list("list"));
for (auto output : ir.outputs()) {
w << list("cons", "\"" + RTLIL::unescape_id(output->name) + "\"", output_struct.access("outputs", output->name));
}
w.pop();
}
void write(std::ostream &out)
{
SExprWriter w(out);
@ -265,6 +311,10 @@ struct SmtrModule {
output_struct.write_definition(w);
state_struct.write_definition(w);
if (use_assoc_list_helpers) {
write_assoc_list_helpers(w);
}
write_eval(w);
write_initial(w);
}
@ -282,12 +332,16 @@ struct FunctionalSmtrBackend : public Backend {
log("\n");
log(" -provides\n");
log(" include 'provide' statement(s) for loading output as a module\n");
log(" -assoc-list-helpers\n");
log(" provide helper functions which convert inputs/outputs from/to association lists\n");
log(" \n");
log("\n");
}
void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
{
auto provides = false;
auto assoc_list_helpers = false;
log_header(design, "Executing Functional Rosette Backend.\n");
@ -296,6 +350,8 @@ struct FunctionalSmtrBackend : public Backend {
{
if (args[argidx] == "-provides")
provides = true;
else if (args[argidx] == "-assoc-list-helpers")
assoc_list_helpers = true;
else
break;
}
@ -307,8 +363,8 @@ struct FunctionalSmtrBackend : public Backend {
}
for (auto module : design->selected_modules()) {
log("Processing module `%s`.\n", module->name);
SmtrModule smtr(module);
log("Processing module `%s`.\n", module->name.c_str());
SmtrModule smtr(module, assoc_list_helpers);
smtr.write(*f);
}
}