Writing a new backend using FunctionalIR¶
What is FunctionalIR¶
To simplify the writing of backends for functional languages or similar targets, Yosys provides an alternative intermediate representation called FunctionalIR which maps more directly on those targets.
FunctionalIR represents the design as a function (inputs, current_state) ->
(outputs, next_state). This function is broken down into a series of
assignments to variables. Each assignment is a simple operation, such as an
addition. Complex operations are broken up into multiple steps. For example, an
RTLIL addition will be translated into a sign/zero extension of the inputs,
followed by an addition.
Like SSA form, each variable is assigned to exactly once. We can thus treat variables and assignments as equivalent and, since this is a graph-like representation, those variables are also called “nodes”. Unlike RTLIL’s cells and wires representation, this representation is strictly ordered (topologically sorted) with definitions preceding their use.
Every node has a “sort” (the FunctionalIR term for what might otherwise be called a “type”). The sorts available are
bit[n]for ann-bit bitvector, andmemory[n,m]for an immutable array of2**nvalues of sortbit[m].
In terms of actual code, Yosys provides a class Functional::IR that
represents a design in FunctionalIR. Functional::IR::from_module generates
an instance from an RTLIL module. The entire design is stored as a whole in an
internal data structure. To access the design, the Functional::Node class
provides a reference to a particular node in the design. The Functional::IR
class supports the syntax for(auto node : ir) to iterate over every node.
Functional::IR also keeps track of inputs, outputs and states. By a “state”
we mean a pair of a “current state” input and a “next state” output. One such
pair is created for every register and for every memory. Every input, output and
state has a name (equal to their name in RTLIL), a sort and a kind. The kind
field usually remains as the default value $input, $output or
$state, however some RTLIL cells such as $assert or $anyseq generate
auxiliary inputs/outputs/states that are given a different kind to distinguish
them from ordinary RTLIL inputs/outputs/states.
To access an individual input/output/state, use
ir.input(name, kind),ir.output(name, kind)orir.state(name, kind).kinddefaults to the default kind.To iterate over all inputs/outputs/states of a certain kind, methods
ir.inputs,ir.outputs,ir.statesare provided. Their argument defaults to the default kinds mentioned.To iterate over inputs/outputs/states of any kind, use
ir.all_inputs,ir.all_outputsandir.all_states.Outputs have a node that indicate the value of the output, this can be retrieved via
output.value().States have a node that indicate the next value of the state, this can be retrieved via
state.next_value(). They also have an initial value that is accessed as eitherstate.initial_value_signal()orstate.initial_value_memory(), depending on their sort.
Each node has a “function”, which defines its operation (for a complete list of
functions and a specification of their operation, see functional.h).
Functions are represented as an enum Functional::Fn and the function field
can be accessed as node.fn(). Since the most common operation is a switch
over the function that also accesses the arguments, the Node class provides
a method visit that implements the visitor pattern. For example, for an
addition node node with arguments n1 and n2, node.visit(visitor)
would call visitor.add(node, n1, n2). Thus typically one would implement a
class with a method for every function. Visitors should inherit from either
Functional::AbstractVisitor<ReturnType> or
Functional::DefaultVisitor<ReturnType>. The former will produce a compiler
error if a case is unhandled, the latter will call default_handler(node)
instead. Visitor methods should be marked as override to provide compiler
errors if the arguments are wrong.
Utility classes¶
functional.h also provides utility classes that are independent of the main
FunctionalIR representation but are likely to be useful for backends.
Functional::Writer provides a simple formatting class that wraps a
std::ostream and provides the following methods:
writer << valuewrapsos << value.writer.print(fmt, value0, value1, value2, ...)replaces{0},{1},{2}, etc in the stringfmtwithvalue0,value1,value2, resp. Each value is formatted usingos << value. It is also possible to write{}to refer to one past the last index, i.e.{1} {} {} {7} {}is equivalent to{1} {2} {3} {7} {8}.writer.print_with(fn, fmt, value0, value1, value2, ...)functions much the same asprintbut it usesos << fn(value)to print each value and falls back toos << valueiffn(value)is not legal.
Functional::Scope keeps track of variable names in a target language. It is
used to translate between different sets of legal characters and to avoid
accidentally re-defining identifiers. Users should derive a class from Scope
and supply the following:
Scope<Id>takes a template argument that specifies a type that’s used to uniquely distinguish variables. Typically this would beint(if variables are used forFunctional::IRnodes) orIdString.The derived class should provide a constructor that calls
reservefor every reserved word in the target language.A method
bool is_character_legal(char c, int index)has to be provided that returnstrueiffcis legal in an identifier at positionindex.
Given an instance scope of the derived class, the following methods are then
available:
scope.reserve(std::string name)marks the given name as being in-usescope.unique_name(IdString suggestion)generates a previously unused name and attempts to make it similar tosuggestion.scope(Id id, IdString suggestion)functions similar tounique_name, except that multiple calls with the sameidare guaranteed to retrieve the same name (independent ofsuggestion).
sexpr.h provides classes that represent and pretty-print s-expressions.
S-expressions can be constructed with SExpr::list, for example SExpr expr
= SExpr::list("add", "x", SExpr::list("mul", "y", "z")) represents (add x
(mul y z)) (by adding using SExprUtil::list to the top of the file,
list can be used as shorthand for SExpr::list). For prettyprinting,
SExprWriter wraps an std::ostream and provides the following methods:
writer << sexprwrites the provided expression to the output, breaking long lines and adding appropriate indentation.writer.open(sexpr)is similar towriter << sexprbut will omit the last closing parenthesis. Further arguments can then be added separately with<<oropen. This allows for printing large s-expressions without needing to construct the whole expression in memory first.writer.open(sexpr, false)is similar towriter.open(sexpr)but further arguments will not be indented. This is used to avoid unlimited indentation on structures with unlimited nesting.writer.close(n = 1)closes the lastnopen s-expressions.writer.push()andwriter.pop()are used to automatically close s-expressions.writer.pop()closes all s-expressions opened since the last call towriter.push().writer.comment(string)writes a comment on a separate-line.writer.comment(string, true)appends a comment to the last printed s-expression.writer.flush()flushes any buffering and should be called before any direct access to the underlyingstd::ostream. It does not close unclosed parentheses.The destructor calls
flushbut also closes all unclosed parentheses.
Example: A minimal functional backend¶
At its most basic, there are three steps we need to accomplish for a minimal
functional backend. First, we need to convert our design into FunctionalIR.
This is most easily done by calling the Functional::IR::from_module() static
method with our top-level module, or iterating over and converting each of the
modules in our design. Second, we need to handle each of the
Functional::Nodes in our design. Iterating over the Functional::IR
includes reading the module inputs and current state, but not writing the
results. So our final step is to handle the outputs and next state.
In order to add an output command to Yosys, we implement the Yosys::Backend
class and provide an instance of it:
#include "kernel/functional.h"
#include "kernel/yosys.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
struct FunctionalDummyBackend : public Backend {
FunctionalDummyBackend() : Backend("functional_dummy", "dump generated Functional IR") {}
void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
{
// backend pass boiler plate
log_header(design, "Executing dummy functional backend.\n");
size_t argidx = 1;
extra_args(f, filename, args, argidx, design);
for (auto module : design->selected_modules())
{
log("Processing module `%s`.\n", module->name.c_str());
// convert module to FunctionalIR
auto ir = Functional::IR::from_module(module);
*f << "module " << module->name.c_str() << "\n";
// write node functions
for (auto node : ir)
*f << " assign " << id2cstr(node.name())
<< " = " << node.to_string() << "\n";
*f << "\n";
// write outputs and next state
for (auto output : ir.outputs())
*f << " " << id2cstr(output->kind)
<< " " << id2cstr(output->name)
<< " = " << id2cstr(output->value().name()) << "\n";
for (auto state : ir.states())
*f << " " << id2cstr(state->kind)
<< " " << id2cstr(state->name)
<< " = " << id2cstr(state->next_value().name()) << "\n";
}
}
} FunctionalDummyBackend;
PRIVATE_NAMESPACE_END
Because we are using the Backend class, our "functional_dummy" is
registered as the write_functional_dummy command. The execute method is
the part that runs when the user calls the command, handling any options,
preparing the output file for writing, and iterating over selected modules in
the design. Since we don’t have any options here, we set argidx = 1 and
call the extra_args() method. This method will read the command arguments,
raising an error if there are any unexpected ones. It will also assign the
pointer f to the output file, or stdout if none is given.
Note
For more on adding new commands to Yosys and how they work, refer to Writing extensions.
For this minimal example all we are doing is printing out each node. The
node.name() method returns an RTLIL::IdString, which we convert for
printing with id2cstr(). Then, to print the function of the node, we use
node.to_string() which gives us a string of the form function(args). The
function part is the result of Functional::IR::fn_to_string(node.fn());
while args is the zero or more arguments passed to the function, most
commonly the name of another node. Behind the scenes, the node.to_string()
method actually wraps node.visit(visitor) with a private visitor whose
return type is std::string.
Finally we iterate over the module’s outputs and states, using
Functional::IROutput::value() and Functional::IRState::next_value()
respectively in order to get the results of the transfer function.
Example: Adapting SMT-LIB backend for Rosette¶
This section will introduce the SMT-LIB functional backend
(write_functional_smt2) and what changes are needed to work with another
s-expression target, Rosette (write_functional_rosette).
Overview¶
Rosette, being backed by SMT solvers and written with s-expressions, uses code
very similar to the write_functional_smt2 output. As a result, the SMT-LIB
functional backend can be used as a starting point for implementing a Rosette
backend.
Full code listings for the initial SMT-LIB backend and the converted Rosette
backend are included in the Yosys source repository under
backends/functional as smtlib.cc and smtlib_rosette.cc
respectively. Note that the Rosette language is an extension of the Racket
language; this guide tends to refer to Racket when talking about the underlying
semantics/syntax of the language.
The major changes from the SMT-LIB backend are as follows:
all of the
Smtprefixes in names are replaced withSmtrto meansmtlib_rosette;syntax is adjusted for Racket;
data structures for input/output/state are changed from using
declare-datatypewith statically typed fields, to usingstructwith no static typing;the transfer function also loses its static typing;
sign/zero extension in Rosette use the output width instead of the number of extra bits, gaining static typing;
the single scope is traded for a global scope with local scope for each struct;
initial state is provided as a constant value instead of a set of assertions;
and the
-providesoption is introduced to more easily use generated code within Rosette based applications.
Scope¶
Our first addition to the minimal backend above is that for both SMT-LIB and
Rosette backends, we are now targetting real languages which bring with them
their own sets of constraints with what we can use as identifiers. This is
where the Functional::Scope class described above comes in; by using this
class we can safely rename our identifiers in the generated output without
worrying about collisions or illegal names/characters.
In the SMT-LIB version, the SmtScope class implements Scope<int>;
provides a constructor that iterates over a list of reserved keywords, calling
reserve on each; and defines the is_character_legal method to reject any
characters which are not allowed in SMT-LIB variable names to then be replaced
with underscores in the output. To use this scope we create an instance of it,
and call the Scope::unique_name() method to generate a unique and legal name
for each of our identifiers.
In the Rosette version we update the list of legal ascii characters in the
is_character_legal method to only those allowed in Racket variable names.
-struct SmtScope : public Functional::Scope<int> {
- SmtScope() {
+struct SmtrScope : public Functional::Scope<int> {
+ SmtrScope() {
for(const char **p = reserved_keywords; *p != nullptr; p++)
reserve(*p);
}
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));
}
};
For the reserved keywords we trade the SMT-LIB specification for Racket to
prevent parts of our design from accidentally being treated as Racket code. We
also no longer need to reserve pair, first, and second. In
write_functional_smt2 these are used for combining the (inputs,
current_state) and (outputs, next_state) into a single variable. Racket
provides this functionality natively with cons, which we will see later.
const char *reserved_keywords[] = {
- // reserved keywords from the smtlib spec
- ...
+ // reserved keywords from the racket spec
+ ...
// reserved for our own purposes
- "pair", "Pair", "first", "second",
- "inputs", "state",
+ "inputs", "state", "name",
nullptr
};
Note
We skip over the actual list of reserved keywords from both the smtlib and racket specifications to save on space in this document.
Sort¶
Next up in write_functional_smt2 we see the Sort class. This is a wrapper
for the Functional::Sort class, providing the additional functionality of
mapping variable declarations to s-expressions with the to_sexpr() method.
The main change from SmtSort to SmtrSort is a syntactical one with
signals represented as bitvectors, and memories as lists of signals.
SExpr to_sexpr() const {
if(sort.is_memory()) {
- 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()));
} else if(sort.is_signal()) {
- return list("_", "BitVec", sort.width());
+ return list("bitvector", sort.width());
} else {
log_error("unknown sort");
}
}
Struct¶
As we saw in the minimal backend above, the Functional::IR class tracks
the set of inputs, the set of outputs, and the set of “state” variables. The
SMT-LIB backend maps each of these sets into its own SmtStruct, with each
variable getting a corresponding field in the struct and a specified Sort.
write_functional_smt2 then defines each of these structs as a new
datatype, with each element being strongly-typed.
In Rosette, rather than defining new datatypes for our structs, we use the
native struct. We also only declare each field by name because Racket
provides less static typing. For ease of use, we provide the expected type for
each field as comments.
void write_definition(SExprWriter &w) {
- w.open(list("declare-datatype", name));
- w.open(list());
- w.open(list(name));
- for(const auto &field : fields)
- w << list(field.accessor, field.sort.to_sexpr());
- w.close(3);
+ vector<SExpr> field_list;
+ for(const auto &field : fields) {
+ field_list.emplace_back(field.name);
+ }
+ w.push();
+ w.open(list("struct", name, field_list, "#:transparent"));
+ if (field_names.size()) {
+ for (const auto &field : fields) {
+ auto bv_type = field.sort.to_sexpr();
+ w.comment(field.name + " " + bv_type.to_string());
+ }
+ }
+ w.pop();
}
Each field is added to the SmtStruct with the insert method, which also
reserves a unique name (or accessor) within the Scope. These accessors
combine the struct name and field name and are globally unique, being used in
the access method for reading values from the input/current state.
SExpr access(SExpr record, IdString name) {
size_t i = field_names.at(name);
return list(fields[i].accessor, std::move(record));
}
In Rosette, struct fields are accessed as <struct_name>-<field_name> so
including the struct name in the field name would be redundant. For
write_functional_rosette we instead choose to make field names unique only
within the struct, while accessors are unique across the whole module. We thus
modify the class constructor and insert method to support this; providing
one scope that is local to the struct (local_scope) and one which is shared
across the whole module (global_scope), leaving the access method
unchanged.
- SmtStruct(std::string name, SmtScope &scope) : scope(scope), name(name) {}
- void insert(IdString field_name, SmtSort sort) {
+ SmtrStruct(std::string name, SmtrScope &scope) : global_scope(scope), local_scope(), name(name) {}
+ void insert(IdString field_name, SmtrSort sort) {
field_names(field_name);
- auto accessor = scope.unique_name("\\" + name + "_" + RTLIL::unescape_id(field_name));
- fields.emplace_back(Field{sort, accessor});
+ auto base_name = local_scope.unique_name(field_name);
+ auto accessor = name + "-" + base_name;
+ global_scope.reserve(accessor);
+ fields.emplace_back(Field{sort, accessor, base_name});
}
Finally, SmtStruct also provides a write_value template method which
calls a provided function on each element in the struct. This is used later for
assigning values to the output/next state pair. The only change here is to
remove the check for zero-argument constructors since this is not necessary with
Rosette structs.
template<typename Fn> void write_value(SExprWriter &w, Fn fn) {
- if(field_names.empty()) {
- // Zero-argument constructors in SMTLIB must not be called as functions.
- w << name;
- } else {
- w.open(list(name));
- for(auto field_name : field_names) {
- w << fn(field_name);
- w.comment(RTLIL::unescape_id(field_name), true);
- }
- w.close();
+ w.open(list(name));
+ for(auto field_name : field_names) {
+ w << fn(field_name);
+ w.comment(RTLIL::unescape_id(field_name), true);
}
+ w.close();
}
PrintVisitor¶
Remember in the minimal backend we converted nodes into strings for writing
using the node.to_string() method, which wrapped node.visit() with a
private visitor. We now want a custom visitor which can convert nodes into
s-expressions. This is where the PrintVisitor comes in, implementing the
abstract Functional::AbstractVisitor class with a return type of SExpr.
For most functions, the Rosette output is very similar to the corresponding
SMT-LIB function with minor adjustments for syntax.
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 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 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)); }
+ 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 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)); }
However there are some differences in the two formats with regards to how booleans are handled, with Rosette providing built-in functions for conversion.
SExpr from_bool(SExpr &&arg) {
- return list("ite", std::move(arg), "#b1", "#b0");
+ return list("bool->bitvector", std::move(arg));
}
SExpr to_bool(SExpr &&arg) {
- return list("=", std::move(arg), "#b1");
+ return list("bitvector->bool", std::move(arg));
}
Of note here is the rare instance of the Rosette implementation gaining static
typing rather than losing it. Where SMT_LIB calls zero/sign extension with the
number of extra bits needed (given by out_width - a.width()), Rosette
instead specifies the type of the output (given by list("bitvector",
out_width)).
- 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 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)); }
Note
Be sure to check the source code for the full list of differences here.
Module¶
With most of the supporting classes out of the way, we now reach our three main
steps from the minimal backend. These are all handled by the SmtModule
class, with the mapping from RTLIL module to FunctionalIR happening in the
constructor. Each of the three SmtStructs; inputs, outputs, and state;
are also created in the constructor, with each value in the corresponding lists
in the IR being inserted.
SmtModule(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)
{
scope.reserve(name + "-initial");
for (auto input : ir.inputs())
input_struct.insert(input->name, input->sort);
for (auto output : ir.outputs())
output_struct.insert(output->name, output->sort);
for (auto state : ir.states())
state_struct.insert(state->name, state->sort);
}
Since Racket uses the - to access struct fields, the SmtrModule instead
uses an underscore for the name of the initial state.
- scope.reserve(name + "-initial");
+ scope.reserve(name + "_initial");
The write method is then responsible for writing the FunctionalIR to the
output file, formatted for the corresponding backend. SmtModule::write()
breaks the output file down into four parts: defining the three structs,
declaring the pair datatype, defining the transfer function (inputs,
current_state) -> (outputs, next_state) with write_eval, and declaring the
initial state with write_initial. The only change for the SmtrModule is
that the pair declaration isn’t needed.
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);
}
The write_eval method is where the FunctionalIR nodes, outputs, and next
state are handled. Just as with the minimal backend, we iterate over the
nodes with for(auto n : ir), and then use the Struct::write_value()
method for the output_struct and state_struct to iterate over the
outputs and next state respectively.
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);
}
The main differences between our two backends here are syntactical. First we
change the define-fun for the Racket style define which drops the
explicitly typed inputs/outputs. And then we change the final result from a
pair to the native cons which acts in much the same way, returning both
the outputs and the next_state in a single variable.
- 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")));
- 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();
For the write_initial method, the SMT-LIB backend uses declare-const and
asserts which must always hold true. For Rosette we instead define the
initial state as any other variable that can be used by external code. This
variable, [name]_initial, can then be used in the [name] function call;
allowing the Rosette code to be used in the generation of the next_state,
whereas the SMT-LIB code can only verify that a given next_state is correct.
void write_initial(SExprWriter &w)
{
- std::string initial = name + "-initial";
- w << list("declare-const", initial, state_struct.name);
+ w.push();
+ auto initial = name + "_initial";
+ w.open(list("define", initial));
+ w.open(list(state_struct.name));
for (auto state : ir.states()) {
- if(state->sort.is_signal())
- w << list("assert", list("=", state_struct.access(initial, state->name), smt_const(state->initial_value_signal())));
- 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();
}
}
+ w.pop();
}
Backend¶
The final part is the Backend itself, with much of the same boiler plate as
the minimal backend. The main difference is that we use the Module to
perform the actual processing.
struct FunctionalSmtBackend : public Backend {
FunctionalSmtBackend() : Backend("functional_smt2", "Generate SMT-LIB from Functional IR") {}
void help() override { log("\nFunctional SMT Backend.\n\n"); }
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");
size_t argidx = 1;
extra_args(f, filename, args, argidx, design);
for (auto module : design->selected_modules()) {
log("Processing module `%s`.\n", module->name.c_str());
SmtModule smt(module);
smt.write(*f);
}
}
} FunctionalSmtBackend;
There are two additions here for Rosette. The first is that the output file
needs to start with the #lang definition which tells the
compiler/interpreter that we want to use the Rosette language module. The
second is that the write_functional_rosette command takes an optional
argument, -provides. If this argument is given, then the output file gets
an additional line declaring that everything in the file should be exported for
use; allowing the file to be treated as a Racket package with structs and
mapping function available for use externally.
+ *f << "#lang rosette/safe\n";
+ if (provides) {
+ *f << "(provide (all-defined-out))\n";
+ }