mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-06-12 00:53:26 +00:00
Code Activity

Add output helper as well

Browse source
This commit is contained in:
Gus Smith 2025-05-17 15:19:09 -07:00
parent 1fdfba2a1a
commit c1111f125c
1 changed files with 20 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

22
backends/functional/smtlib_rosette.cc
View file

@ -205,6 +205,7 @@ struct SmtrModule {
SmtrScope scope;
std::string name;
std::optional<std::string> input_kw_name;
std::optional<std::string> output_kw_name;
SmtrStruct input_struct;
SmtrStruct output_struct;
@ -222,6 +223,8 @@ struct SmtrModule {
if (keyword_helpers) {
input_kw_name = scope.unique_name(module->name.str() + "_inputs_kw");
scope.reserve(*input_kw_name);
output_kw_name = scope.unique_name(module->name.str() + "_outputs_kw");
scope.reserve(*output_kw_name);
}
for (auto input : ir.inputs())
input_struct.insert(input->name, input->sort);
@ -278,8 +281,9 @@ struct SmtrModule {
w.pop();
}
void write_input_kw(SExprWriter &w)
void write_keyword_helpers(SExprWriter &w)
{
// Input struct keyword-based constructor.
w.push();
w.open(list("define"));
w.open(list(name + "_inputs_kw"));
@ -292,6 +296,18 @@ struct SmtrModule {
w << name;
}
w.pop();
// Output struct keyword-based destructor.
w.push();
w.open(list("define"));
w.open(list(name + "_outputs_kw"));
const auto outputs_name = "outputs";
w << outputs_name;
w.close();
w.open(list("list"));
for (auto name : output_struct.get_field_names()) {
w << list("cons", "\"" + name + "\"", output_struct.access_by_base_name(outputs_name, name));
}
w.pop();
}
void write(std::ostream &out)
@ -303,7 +319,9 @@ struct SmtrModule {
state_struct.write_definition(w);
if (input_kw_name) {
write_input_kw(w);
if (!output_kw_name)
log_error("if keyword helpers are enabled, both input and output helper names are expected");
write_keyword_helpers(w);
}
write_eval(w);