From ef7734d610305c8a396ec43717d98de7472d8143 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 6 Jan 2025 12:01:21 +1300 Subject: [PATCH 01/19] functional_ir.rst: Formatting Line breaks. Put intro under sub-heading. --- .../extending_yosys/functional_ir.rst | 181 +++++++++++------- 1 file changed, 116 insertions(+), 65 deletions(-) diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst index a763e0508..11f5c579f 100644 --- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst +++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst @@ -1,94 +1,145 @@ Writing a new backend using 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. +What is FunctionalIR +-------------------- -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. +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. -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. +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. -Every node has a "sort" (the FunctionalIR term for what might otherwise be called a "type"). The sorts available are +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 an ``n``-bit bitvector, and - ``memory[n,m]`` for an immutable array of ``2**n`` values of sort ``bit[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. +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. +``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)`` or ``ir.state(name, kind)``. ``kind`` defaults to the default kind. -- To iterate over all inputs/outputs/states of a certain kind, methods ``ir.inputs``, ``ir.outputs``, ``ir.states`` are provided. Their argument defaults to the default kinds mentioned. -- To iterate over inputs/outputs/states of any kind, use ``ir.all_inputs``, ``ir.all_outputs`` and ``ir.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 either ``state.initial_value_signal()`` or ``state.initial_value_memory()``, depending on their sort. +- To access an individual input/output/state, use ``ir.input(name, kind)``, + ``ir.output(name, kind)`` or ``ir.state(name, kind)``. ``kind`` defaults to + the default kind. +- To iterate over all inputs/outputs/states of a certain kind, methods + ``ir.inputs``, ``ir.outputs``, ``ir.states`` are provided. Their argument + defaults to the default kinds mentioned. +- To iterate over inputs/outputs/states of any kind, use ``ir.all_inputs``, + ``ir.all_outputs`` and ``ir.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 either ``state.initial_value_signal()`` or + ``state.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`` or ``Functional::DefaultVisitor``. -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. +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`` or +``Functional::DefaultVisitor``. 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.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: +``Functional::Writer`` provides a simple formatting class that wraps a +``std::ostream`` and provides the following methods: - ``writer << value`` wraps ``os << value``. -- ``writer.print(fmt, value0, value1, value2, ...)`` replaces ``{0}``, ``{1}``, ``{2}``, etc in the string ``fmt`` with ``value0``, ``value1``, ``value2``, resp. - Each value is formatted using ``os << 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 as ``print`` but it uses ``os << fn(value)`` to print each value and falls back to ``os << value`` if ``fn(value)`` is not legal. +- ``writer.print(fmt, value0, value1, value2, ...)`` replaces ``{0}``, ``{1}``, + ``{2}``, etc in the string ``fmt`` with ``value0``, ``value1``, ``value2``, + resp. Each value is formatted using ``os << 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 as ``print`` but it uses ``os << fn(value)`` to print each value and + falls back to ``os << value`` if ``fn(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: +``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`` takes a template argument that specifies a type that's used to uniquely distinguish variables. - Typically this would be ``int`` (if variables are used for ``Functional::IR`` nodes) or ``IdString``. -- The derived class should provide a constructor that calls ``reserve`` for every reserved word in the target language. -- A method ``bool is_legal_character(char c, int index)`` has to be provided that returns ``true`` iff ``c`` is legal in an identifier at position ``index``. +- ``Scope`` takes a template argument that specifies a type that's used to + uniquely distinguish variables. Typically this would be ``int`` (if variables + are used for ``Functional::IR`` nodes) or ``IdString``. +- The derived class should provide a constructor that calls ``reserve`` for + every reserved word in the target language. +- A method ``bool is_legal_character(char c, int index)`` has to be provided + that returns ``true`` iff ``c`` is legal in an identifier at position + ``index``. -Given an instance ``scope`` of the derived class, the following methods are then available: +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-use -- ``scope.unique_name(IdString suggestion)`` generates a previously unused name and attempts to make it similar to ``suggestion``. -- ``scope(Id id, IdString suggestion)`` functions similar to ``unique_name``, except that multiple calls with the same ``id`` are guaranteed to retrieve the same name (independent of ``suggestion``). +- ``scope.unique_name(IdString suggestion)`` generates a previously unused name + and attempts to make it similar to ``suggestion``. +- ``scope(Id id, IdString suggestion)`` functions similar to ``unique_name``, + except that multiple calls with the same ``id`` are guaranteed to retrieve the + same name (independent of ``suggestion``). ``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: +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 << sexpr`` writes the provided expression to the output, breaking long lines and adding appropriate indentation. -- ``writer.open(sexpr)`` is similar to ``writer << sexpr`` but will omit the last closing parenthesis. - Further arguments can then be added separately with ``<<`` or ``open``. - This allows for printing large s-expressions without needing to construct the whole expression in memory first. -- ``writer.open(sexpr, false)`` is similar to ``writer.open(sexpr)`` but further arguments will not be indented. - This is used to avoid unlimited indentation on structures with unlimited nesting. +- ``writer << sexpr`` writes the provided expression to the output, breaking + long lines and adding appropriate indentation. +- ``writer.open(sexpr)`` is similar to ``writer << sexpr`` but will omit the + last closing parenthesis. Further arguments can then be added separately with + ``<<`` or ``open``. This allows for printing large s-expressions without + needing to construct the whole expression in memory first. +- ``writer.open(sexpr, false)`` is similar to ``writer.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 last ``n`` open s-expressions. -- ``writer.push()`` and ``writer.pop()`` are used to automatically close s-expressions. - ``writer.pop()`` closes all s-expressions opened since the last call to ``writer.push()``. +- ``writer.push()`` and ``writer.pop()`` are used to automatically close + s-expressions. ``writer.pop()`` closes all s-expressions opened since the last + call to ``writer.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 underlying ``std::ostream``. It does not close unclosed parentheses. + ``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 underlying ``std::ostream``. It does not close unclosed + parentheses. - The destructor calls ``flush`` but also closes all unclosed parentheses. From 23fa9b201421dc95642ba96f0cbda45bcf32e75d Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 6 Jan 2025 14:30:29 +1300 Subject: [PATCH 02/19] functional_ir.rst: Initial skeleton for Rosette --- .../extending_yosys/functional_ir.rst | 70 +++++++++++++++++++ 1 file changed, 70 insertions(+) diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst index 11f5c579f..30fc63899 100644 --- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst +++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst @@ -143,3 +143,73 @@ S-expressions can be constructed with ``SExpr::list``, for example ``SExpr expr direct access to the underlying ``std::ostream``. It does not close unclosed parentheses. - The destructor calls ``flush`` but also closes all unclosed parentheses. + +Example: Adapting SMT-LIB backend for Rosette +--------------------------------------------- + +Overview +~~~~~~~~ + +- What is Rosette + - Racket package + - solver-aided programming language + - uses symbolic expressions + - able to perform functional verification + +- link to file (both smtlib and rosette) + +Scope +~~~~~ + +- as above, prevents namespace collision +- reserved keywords + - language (Racket) keywords + - output keywords + +- ``is_character_legal`` + +Sort +~~~~ + +- map variable declarations to s-expressions +- handles signals (bitvectors) and memories (arrays of bitvectors) + +Struct +~~~~~~ + +- helpers for defining inputs/outputs/state + - each is a single (transparent) struct with zero or more fields + - each field has a name, with the type (sort) as a comment + - struct fields in Rosette are accessed as ``-`` + - field names only need to be unique within the struct, while accessors + are unique within the module + +- writing outputs/next state + +PrintVisitor +~~~~~~~~~~~~ + +- map FunctionalIR operations to Rosette + - most functions are the same or very similar to their corresponding smtlib + function + +- reading inputs/current state + +Module +~~~~~~ + +- map RTLIL module to FunctionalIR +- iterate over FunctionalIR and map to Rosette + - defines the mapping function, ``(inputs, current_state) -> (outputs, + next_state)`` + +Backend +~~~~~~~ + +- registers the `write_functional_rosette` command +- options (``-provides``) + - allows file to be treated as a Racket package with structs and mapping + function available for use externally + +- opens and prepares file for writing +- iterates over modules in design From f4c7377ac1637b6159ac7f7eb1b40fcb1048a4ab Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 6 Jan 2025 14:30:55 +1300 Subject: [PATCH 03/19] functional_ir.rst: Fix typo --- docs/source/yosys_internals/extending_yosys/functional_ir.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst index 30fc63899..7a3799ac1 100644 --- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst +++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst @@ -102,7 +102,7 @@ and supply the following: are used for ``Functional::IR`` nodes) or ``IdString``. - The derived class should provide a constructor that calls ``reserve`` for every reserved word in the target language. -- A method ``bool is_legal_character(char c, int index)`` has to be provided +- A method ``bool is_character_legal(char c, int index)`` has to be provided that returns ``true`` iff ``c`` is legal in an identifier at position ``index``. From 7698dfba5e14dc766c387b5fca2e4e3554ad2b20 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 6 Jan 2025 14:31:50 +1300 Subject: [PATCH 04/19] smtr: Fix help text Can't take both [selection] and [filename] optional arguments. --- backends/functional/smtlib_rosette.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/functional/smtlib_rosette.cc b/backends/functional/smtlib_rosette.cc index ea14da854..a93bd04b0 100644 --- a/backends/functional/smtlib_rosette.cc +++ b/backends/functional/smtlib_rosette.cc @@ -267,7 +267,7 @@ struct FunctionalSmtrBackend : public Backend { void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); - log(" write_functional_rosette [options] [selection] [filename]\n"); + log(" write_functional_rosette [options] [filename]\n"); log("\n"); log("Functional Rosette Backend.\n"); log("\n"); From 242c03715810319928b5917ccade7a1df3314397 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 24 Jan 2025 13:10:34 +1300 Subject: [PATCH 05/19] docs/rosette: Add overview --- .../extending_yosys/functional_ir.rst | 25 ++++++++++++++----- 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst index 7a3799ac1..662f3df8b 100644 --- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst +++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst @@ -147,16 +147,29 @@ S-expressions can be constructed with ``SExpr::list``, for example ``SExpr expr Example: Adapting SMT-LIB backend for Rosette --------------------------------------------- +This section will walk through the process of adapting the SMT-LIB functional +backend (`write_functional_smt2`) to work with another s-expression target, +`Rosette`_. + +.. _Rosette: http://emina.github.io/rosette/ + Overview ~~~~~~~~ -- What is Rosette - - Racket package - - solver-aided programming language - - uses symbolic expressions - - able to perform functional verification + Rosette is a solver-aided programming language that extends `Racket`_ with + language constructs for program synthesis, verification, and more. To verify + or synthesize code, Rosette compiles it to logical constraints solved with + off-the-shelf `SMT`_ solvers. -- link to file (both smtlib and rosette) + -- https://emina.github.io/rosette/ + +.. _Racket: http://racket-lang.org/ +.. _SMT: http://smtlib.cs.uiowa.edu/ + +Full code listings for the initial SMT-LIB backend and the converted Rosette +backend are included in the Yosys source repository under +:file:`backends/functional` as ``smtlib.cc`` and ``smtlib_rosette.cc`` +respectively. Scope ~~~~~ From 1b6b6a77ba9ec4fb5ed40346371cc3df78f20168 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 25 Jan 2025 09:51:20 +1300 Subject: [PATCH 06/19] docs/rosette: Add details for Scope Add a diff file and use it for showing changes from smtlib to rosette. Also add relevant sections of diff to Sort and Struct sections. --- .../code_examples/functional/rosette.diff | 386 ++++++++++++++++++ .../extending_yosys/functional_ir.rst | 82 +++- 2 files changed, 456 insertions(+), 12 deletions(-) create mode 100644 docs/source/code_examples/functional/rosette.diff diff --git a/docs/source/code_examples/functional/rosette.diff b/docs/source/code_examples/functional/rosette.diff new file mode 100644 index 000000000..60fb60c1b --- /dev/null +++ b/docs/source/code_examples/functional/rosette.diff @@ -0,0 +1,386 @@ +diff --git a/smtlib.cc b/smtlib_rosette.cc +index 3eacf407c..a93bd04b0 100644 +--- a/smtlib.cc ++++ b/smtlib_rosette.cc +@@ -29,80 +29,86 @@ PRIVATE_NAMESPACE_BEGIN + using SExprUtil::list; + + const char *reserved_keywords[] = { +- // reserved keywords from the smtlib spec +- "BINARY", "DECIMAL", "HEXADECIMAL", "NUMERAL", "STRING", "_", "!", "as", "let", "exists", "forall", "match", "par", +- "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", +- "exit", "get-assertions", "symbol", "sort", "get-assignment", "get-info", "get-model", +- "get-option", "get-proof", "get-unsat-assumptions", "get-unsat-core", "get-value", +- "pop", "push", "reset", "reset-assertions", "set-info", "set-logic", "set-option", ++ // reserved keywords from the racket spec ++ "struct", "lambda", "values", "extract", "concat", "bv", "let", "define", "cons", "list", "read", "write", ++ "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", ++ "future", "touch", "subprocess", "make-custodian", "custodian-shutdown-all", "current-custodian", "make", "tcp", ++ "connect", "prepare", "malloc", "free", "_fun", "_cprocedure", "build", "path", "file", "peek", "bytes", ++ "flush", "with", "lexer", "parser", "syntax", "interface", "send", "make-object", "new", "instantiate", ++ "define-generics", "set", + + // reserved for our own purposes +- "pair", "Pair", "first", "second", +- "inputs", "state", ++ "inputs", "state", "name", + nullptr + }; + +-struct SmtScope : public Functional::Scope { +- SmtScope() { ++struct SmtrScope : public Functional::Scope { ++ 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)); + } + }; + +-struct SmtSort { ++struct SmtrSort { + Functional::Sort sort; +- SmtSort(Functional::Sort sort) : sort(sort) {} ++ SmtrSort(Functional::Sort sort) : sort(sort) {} + 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"); + } + } + }; + +-class SmtStruct { ++class SmtrStruct { + struct Field { +- SmtSort sort; ++ SmtrSort sort; + std::string accessor; ++ std::string name; + }; + idict field_names; + vector fields; +- SmtScope &scope; ++ SmtrScope &global_scope; ++ SmtrScope local_scope; + public: + std::string name; +- 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}); + } + 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 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(); + } + template 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(); + } + SExpr access(SExpr record, IdString name) { + size_t i = field_names.at(name); +@@ -117,28 +123,28 @@ std::string smt_const(RTLIL::Const const &c) { + return s; + } + +-struct SmtPrintVisitor : public Functional::AbstractVisitor { ++struct SmtrPrintVisitor : public Functional::AbstractVisitor { + using Node = Functional::Node; + std::function n; +- SmtStruct &input_struct; +- SmtStruct &state_struct; ++ SmtrStruct &input_struct; ++ SmtrStruct &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) {} + + 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)); + } +- SExpr extract(SExpr &&arg, int offset, int out_width = 1) { +- return list(list("_", "extract", offset + out_width - 1, offset), std::move(arg)); ++ SExpr to_list(SExpr &&arg) { ++ return list("bitvector->bits", std::move(arg)); + } + + 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 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 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 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 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)); } +@@ -150,16 +156,11 @@ struct SmtPrintVisitor : public Functional::AbstractVisitor { + 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 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_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 { +- vector s { "bvxor" }; +- for(int i = 0; i < a.width(); i++) +- s.push_back(extract(n(a), i)); +- return s; +- } +- 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 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_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 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_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))); } +@@ -167,32 +168,32 @@ struct SmtPrintVisitor : public Functional::AbstractVisitor { + + SExpr extend(SExpr &&a, int in_width, int out_width) { + if(in_width < out_width) +- return list(list("_", "zero_extend", out_width - in_width), std::move(a)); ++ return list("zero-extend", std::move(a), list("bitvector", out_width)); + else + 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_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)); } + + 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); } + }; + +-struct SmtModule { ++struct SmtrModule { + Functional::IR ir; +- SmtScope scope; ++ SmtrScope scope; + std::string name; + +- SmtStruct input_struct; +- SmtStruct output_struct; +- SmtStruct state_struct; ++ SmtrStruct input_struct; ++ SmtrStruct output_struct; ++ SmtrStruct state_struct; + +- SmtModule(Module *module) ++ SmtrModule(Module *module) + : ir(Functional::IR::from_module(module)) + , scope() + , name(scope.unique_name(module->name)) +@@ -200,7 +201,7 @@ struct SmtModule { + , output_struct(scope.unique_name(module->name.str() + "_Outputs"), scope) + , state_struct(scope.unique_name(module->name.str() + "_State"), scope) + { +- scope.reserve(name + "-initial"); ++ scope.reserve(name + "_initial"); + for (auto input : ir.inputs()) + input_struct.insert(input->name, input->sort); + for (auto output : ir.outputs()) +@@ -209,17 +210,20 @@ struct SmtModule { + state_struct.insert(state->name, state->sort); + } + +- void write_eval(SExprWriter &w) +- { ++ void write(std::ostream &out) ++ { ++ SExprWriter w(out); ++ ++ input_struct.write_definition(w); ++ output_struct.write_definition(w); ++ state_struct.write_definition(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,66 +234,75 @@ 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(); +- } + +- 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<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 { +- FunctionalSmtBackend() : Backend("functional_smt2", "Generate SMT-LIB from Functional IR") {} ++struct FunctionalSmtrBackend : public Backend { ++ FunctionalSmtrBackend() : Backend("functional_rosette", "Generate Rosette compatible Racket from Functional IR") {} + +- void help() override { log("\nFunctional SMT Backend.\n\n"); } ++ void help() override { ++ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| ++ log("\n"); ++ log(" write_functional_rosette [options] [filename]\n"); ++ log("\n"); ++ log("Functional Rosette Backend.\n"); ++ log("\n"); ++ log(" -provides\n"); ++ log(" include 'provide' statement(s) for loading output as a module\n"); ++ log("\n"); ++ } + + void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) override + { +- log_header(design, "Executing Functional SMT Backend.\n"); ++ auto provides = false; ++ ++ log_header(design, "Executing Functional Rosette Backend.\n"); + +- size_t argidx = 1; +- extra_args(f, filename, args, argidx, design); ++ size_t argidx; ++ for (argidx = 1; argidx < args.size(); argidx++) ++ { ++ if (args[argidx] == "-provides") ++ provides = true; ++ else ++ break; ++ } ++ extra_args(f, filename, args, argidx); ++ ++ *f << "#lang rosette/safe\n"; ++ if (provides) { ++ *f << "(provide (all-defined-out))\n"; ++ } + + for (auto module : design->selected_modules()) { + log("Processing module `%s`.\n", module->name.c_str()); +- SmtModule smt(module); +- smt.write(*f); ++ SmtrModule smtr(module); ++ smtr.write(*f); + } + } +-} FunctionalSmtBackend; ++} FunctionalSmtrBackend; + + PRIVATE_NAMESPACE_END diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst index 662f3df8b..0eb9451be 100644 --- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst +++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst @@ -169,17 +169,50 @@ Overview Full code listings for the initial SMT-LIB backend and the converted Rosette backend are included in the Yosys source repository under :file:`backends/functional` as ``smtlib.cc`` and ``smtlib_rosette.cc`` -respectively. +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. Scope ~~~~~ -- as above, prevents namespace collision -- reserved keywords - - language (Racket) keywords - - output keywords +As described above, the ``Functional::Scope`` class is derived in order to avoid +collisions between identifiers in the generated output. We switch out ``Smt`` +in the class name for ``Smtr`` for ``smtlib_rosette``; which will happen through +the rest of the code too. We also update the ``is_character_legal`` method to +reject ascii characters which are not allowed in Racket variable names. -- ``is_character_legal`` +.. literalinclude:: /code_examples/functional/rosette.diff + :language: diff + :caption: diff of ``Scope`` close + :start-at: -struct SmtScope : public Functional::Scope { + :end-at: }; + +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. + +.. code-block:: diff + :caption: diff of ``reserved_keywords`` list + + 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 that we skip over the actual list of reserved keywords from both the smtlib +and racket specifications to save on space in this document. Sort ~~~~ @@ -187,18 +220,43 @@ Sort - map variable declarations to s-expressions - handles signals (bitvectors) and memories (arrays of bitvectors) +.. literalinclude:: /code_examples/functional/rosette.diff + :language: diff + :caption: diff of ``Sort`` wrapper + :start-at: -struct SmtSort { + :end-at: }; + Struct ~~~~~~ - helpers for defining inputs/outputs/state - - each is a single (transparent) struct with zero or more fields - - each field has a name, with the type (sort) as a comment - - struct fields in Rosette are accessed as ``-`` - - field names only need to be unique within the struct, while accessors - are unique within the module - +- struct fields in Rosette are accessed as ``-`` + - field names only need to be unique within the struct, while accessors + are unique within the module + +.. literalinclude:: /code_examples/functional/rosette.diff + :language: diff + :caption: diff of struct constructor + :start-at: - SmtStruct(std::string name, SmtScope &scope) + :end-before: void write_definition + +- each is a single (transparent) struct with zero or more fields +- each field has a name, with the type (sort) as a comment + +.. literalinclude:: /code_examples/functional/rosette.diff + :language: diff + :caption: diff of ``write_definition`` method + :start-at: void write_definition + :end-before: template void write_value + - writing outputs/next state +.. literalinclude:: /code_examples/functional/rosette.diff + :language: diff + :caption: diff of ``write_value`` method + :start-at: template void write_value + :end-before: SExpr access + PrintVisitor ~~~~~~~~~~~~ From d73c58fad1578ab6753b92ec55921ffd3335d1bc Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Tue, 4 Feb 2025 12:24:34 +1300 Subject: [PATCH 07/19] docs/rosette: Sort, Struct, and PrintVisitor sections --- .../extending_yosys/functional_ir.rst | 69 +++++++++++++------ 1 file changed, 47 insertions(+), 22 deletions(-) diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst index 0eb9451be..f44693c16 100644 --- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst +++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst @@ -217,31 +217,27 @@ and racket specifications to save on space in this document. Sort ~~~~ -- map variable declarations to s-expressions -- handles signals (bitvectors) and memories (arrays of bitvectors) +The ``Sort`` class 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 ``bitvector``\ +s, and memories as ``list``\ s of signals. .. literalinclude:: /code_examples/functional/rosette.diff :language: diff :caption: diff of ``Sort`` wrapper - :start-at: -struct SmtSort { - :end-at: }; + :start-at: SExpr to_sexpr() const { + :end-before: }; Struct ~~~~~~ -- helpers for defining inputs/outputs/state -- struct fields in Rosette are accessed as ``-`` - - field names only need to be unique within the struct, while accessors - are unique within the module - -.. literalinclude:: /code_examples/functional/rosette.diff - :language: diff - :caption: diff of struct constructor - :start-at: - SmtStruct(std::string name, SmtScope &scope) - :end-before: void write_definition - -- each is a single (transparent) struct with zero or more fields -- each field has a name, with the type (sort) as a comment +The SMT-LIB backend uses a class, ``SmtStruct``, to help with describing the +input, output, and state data structs. Where each struct in the SMT-LIB output +is a new ``datatype`` with each element having its type declared using the +`Sort`_ above, in Rosette we use the native ``struct`` with each field only +being referred to by name. For ease of use, we include comments for each field +to indicate the expected type. .. literalinclude:: /code_examples/functional/rosette.diff :language: diff @@ -249,7 +245,22 @@ Struct :start-at: void write_definition :end-before: template void write_value -- writing outputs/next state +Struct fields in Rosette are accessed as ``-``, where +field names only need to be unique within the struct, while accessors are unique +within the 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``). + +.. literalinclude:: /code_examples/functional/rosette.diff + :language: diff + :caption: diff of struct constructor + :start-at: - SmtStruct(std::string name, SmtScope &scope) + :end-before: void write_definition + +For writing outputs/next state (the ``write_value`` method), the only change is +to remove the check for zero-argument constructors since this is not necessary +with Rosette ``struct``\ s. .. literalinclude:: /code_examples/functional/rosette.diff :language: diff @@ -260,11 +271,25 @@ Struct PrintVisitor ~~~~~~~~~~~~ -- map FunctionalIR operations to Rosette - - most functions are the same or very similar to their corresponding smtlib - function +The ``PrintVisitor`` implements the abstract ``Functional::AbstractVisitor`` +class for converting FunctionalIR functions into s-expressions, including +reading inputs/current state. For most functions, the Rosette output is very +similar to the corresponding SMT-LIB function with minor adjustments for syntax. -- reading inputs/current state +.. literalinclude:: /code_examples/functional/rosette.diff + :language: diff + :caption: portion of ``Functional::AbstractVisitor`` implementation diff showing similarities + :start-at: SExpr zero_extend + :end-at: SExpr sub + +However there are some differences in the two formats with regards to how +booleans are handled, with Rosette providing built-in functions for conversion. + +.. literalinclude:: /code_examples/functional/rosette.diff + :language: diff + :caption: portion of ``Functional::AbstractVisitor`` implementation diff showing differences + :start-at: SExpr from_bool + :end-before: SExpr extract Module ~~~~~~ From fa2d45a9220c5d650a4b14d3dc183324325f0e5c Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 7 Feb 2025 13:58:09 +1300 Subject: [PATCH 08/19] smtr: Refactor write back into _eval and _initial Easier for comparisons, and the structure still works. (I don't remember why I moved away from it in the first place.) --- backends/functional/smtlib_rosette.cc | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/backends/functional/smtlib_rosette.cc b/backends/functional/smtlib_rosette.cc index a93bd04b0..c9e737d19 100644 --- a/backends/functional/smtlib_rosette.cc +++ b/backends/functional/smtlib_rosette.cc @@ -210,14 +210,8 @@ struct SmtrModule { state_struct.insert(state->name, state->sort); } - void write(std::ostream &out) - { - SExprWriter w(out); - - input_struct.write_definition(w); - output_struct.write_definition(w); - state_struct.write_definition(w); - + void write_eval(SExprWriter &w) + { w.push(); w.open(list("define", list(name, "inputs", "state"))); auto inlined = [&](Functional::Node n) { @@ -240,7 +234,10 @@ struct SmtrModule { 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) + { w.push(); auto initial = name + "_initial"; w.open(list("define", initial)); @@ -259,6 +256,18 @@ struct SmtrModule { } w.pop(); } + + void write(std::ostream &out) + { + SExprWriter w(out); + + input_struct.write_definition(w); + output_struct.write_definition(w); + state_struct.write_definition(w); + + write_eval(w); + write_initial(w); + } }; struct FunctionalSmtrBackend : public Backend { From dc5a5b7bd1518341fc983061c818f40190e9f8c4 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 7 Feb 2025 14:13:34 +1300 Subject: [PATCH 09/19] docs/rosette: Regen rosette.diff This time from the actual source, which apparently means changing all of the spaces for tabs. --- .../code_examples/functional/rosette.diff | 654 +++++++++--------- 1 file changed, 320 insertions(+), 334 deletions(-) diff --git a/docs/source/code_examples/functional/rosette.diff b/docs/source/code_examples/functional/rosette.diff index 60fb60c1b..35c7936d1 100644 --- a/docs/source/code_examples/functional/rosette.diff +++ b/docs/source/code_examples/functional/rosette.diff @@ -1,385 +1,371 @@ -diff --git a/smtlib.cc b/smtlib_rosette.cc -index 3eacf407c..a93bd04b0 100644 ---- a/smtlib.cc -+++ b/smtlib_rosette.cc +diff --git a/backends/functional/smtlib.cc b/backends/functional/smtlib_rosette.cc +index 3eacf407c..c9e737d19 100644 +--- a/backends/functional/smtlib.cc ++++ b/backends/functional/smtlib_rosette.cc @@ -29,80 +29,86 @@ PRIVATE_NAMESPACE_BEGIN using SExprUtil::list; const char *reserved_keywords[] = { -- // reserved keywords from the smtlib spec -- "BINARY", "DECIMAL", "HEXADECIMAL", "NUMERAL", "STRING", "_", "!", "as", "let", "exists", "forall", "match", "par", -- "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", -- "exit", "get-assertions", "symbol", "sort", "get-assignment", "get-info", "get-model", -- "get-option", "get-proof", "get-unsat-assumptions", "get-unsat-core", "get-value", -- "pop", "push", "reset", "reset-assertions", "set-info", "set-logic", "set-option", -+ // reserved keywords from the racket spec -+ "struct", "lambda", "values", "extract", "concat", "bv", "let", "define", "cons", "list", "read", "write", -+ "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", -+ "future", "touch", "subprocess", "make-custodian", "custodian-shutdown-all", "current-custodian", "make", "tcp", -+ "connect", "prepare", "malloc", "free", "_fun", "_cprocedure", "build", "path", "file", "peek", "bytes", -+ "flush", "with", "lexer", "parser", "syntax", "interface", "send", "make-object", "new", "instantiate", -+ "define-generics", "set", +- // reserved keywords from the smtlib spec +- "BINARY", "DECIMAL", "HEXADECIMAL", "NUMERAL", "STRING", "_", "!", "as", "let", "exists", "forall", "match", "par", +- "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", +- "exit", "get-assertions", "symbol", "sort", "get-assignment", "get-info", "get-model", +- "get-option", "get-proof", "get-unsat-assumptions", "get-unsat-core", "get-value", +- "pop", "push", "reset", "reset-assertions", "set-info", "set-logic", "set-option", ++ // reserved keywords from the racket spec ++ "struct", "lambda", "values", "extract", "concat", "bv", "let", "define", "cons", "list", "read", "write", ++ "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", ++ "future", "touch", "subprocess", "make-custodian", "custodian-shutdown-all", "current-custodian", "make", "tcp", ++ "connect", "prepare", "malloc", "free", "_fun", "_cprocedure", "build", "path", "file", "peek", "bytes", ++ "flush", "with", "lexer", "parser", "syntax", "interface", "send", "make-object", "new", "instantiate", ++ "define-generics", "set", - // reserved for our own purposes -- "pair", "Pair", "first", "second", -- "inputs", "state", -+ "inputs", "state", "name", - nullptr + // reserved for our own purposes +- "pair", "Pair", "first", "second", +- "inputs", "state", ++ "inputs", "state", "name", + nullptr }; -struct SmtScope : public Functional::Scope { -- SmtScope() { +- SmtScope() { +struct SmtrScope : public Functional::Scope { -+ 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)); - } ++ 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)); + } }; -struct SmtSort { +struct SmtrSort { - Functional::Sort sort; -- SmtSort(Functional::Sort sort) : sort(sort) {} -+ SmtrSort(Functional::Sort sort) : sort(sort) {} - 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"); - } - } + Functional::Sort sort; +- SmtSort(Functional::Sort sort) : sort(sort) {} ++ SmtrSort(Functional::Sort sort) : sort(sort) {} + 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"); + } + } }; -class SmtStruct { +class SmtrStruct { - struct Field { -- SmtSort sort; -+ SmtrSort sort; - std::string accessor; -+ std::string name; - }; - idict field_names; - vector fields; -- SmtScope &scope; -+ SmtrScope &global_scope; -+ SmtrScope local_scope; + struct Field { +- SmtSort sort; ++ SmtrSort sort; + std::string accessor; ++ std::string name; + }; + idict field_names; + vector fields; +- SmtScope &scope; ++ SmtrScope &global_scope; ++ SmtrScope local_scope; public: - std::string name; -- 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}); - } - 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 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(); - } - template 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(); - } - SExpr access(SExpr record, IdString name) { - size_t i = field_names.at(name); + std::string name; +- 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}); + } + 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 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(); + } + template 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(); + } + SExpr access(SExpr record, IdString name) { + size_t i = field_names.at(name); @@ -117,28 +123,28 @@ std::string smt_const(RTLIL::Const const &c) { - return s; + return s; } -struct SmtPrintVisitor : public Functional::AbstractVisitor { +struct SmtrPrintVisitor : public Functional::AbstractVisitor { - using Node = Functional::Node; - std::function n; -- SmtStruct &input_struct; -- SmtStruct &state_struct; -+ SmtrStruct &input_struct; -+ SmtrStruct &state_struct; + using Node = Functional::Node; + std::function n; +- SmtStruct &input_struct; +- SmtStruct &state_struct; ++ SmtrStruct &input_struct; ++ SmtrStruct &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) {} +- 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) {} - 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)); - } -- SExpr extract(SExpr &&arg, int offset, int out_width = 1) { -- return list(list("_", "extract", offset + out_width - 1, offset), std::move(arg)); -+ SExpr to_list(SExpr &&arg) { -+ return list("bitvector->bits", std::move(arg)); - } + 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)); + } +- SExpr extract(SExpr &&arg, int offset, int out_width = 1) { +- return list(list("_", "extract", offset + out_width - 1, offset), std::move(arg)); ++ SExpr to_list(SExpr &&arg) { ++ return list("bitvector->bits", std::move(arg)); + } - 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 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 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 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 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 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 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 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 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 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)); } @@ -150,16 +156,11 @@ struct SmtPrintVisitor : public Functional::AbstractVisitor { - 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 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_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 { -- vector s { "bvxor" }; -- for(int i = 0; i < a.width(); i++) -- s.push_back(extract(n(a), i)); -- return s; -- } -- 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 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_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 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_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 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 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_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 { +- vector s { "bvxor" }; +- for(int i = 0; i < a.width(); i++) +- s.push_back(extract(n(a), i)); +- return s; +- } +- 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 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_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 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_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))); } @@ -167,32 +168,32 @@ struct SmtPrintVisitor : public Functional::AbstractVisitor { - SExpr extend(SExpr &&a, int in_width, int out_width) { - if(in_width < out_width) -- return list(list("_", "zero_extend", out_width - in_width), std::move(a)); -+ return list("zero-extend", std::move(a), list("bitvector", out_width)); - else - 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_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)); } + SExpr extend(SExpr &&a, int in_width, int out_width) { + if(in_width < out_width) +- return list(list("_", "zero_extend", out_width - in_width), std::move(a)); ++ return list("zero-extend", std::move(a), list("bitvector", out_width)); + else + 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_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)); } - 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 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); } }; -struct SmtModule { +struct SmtrModule { - Functional::IR ir; -- SmtScope scope; -+ SmtrScope scope; - std::string name; - -- SmtStruct input_struct; -- SmtStruct output_struct; -- SmtStruct state_struct; -+ SmtrStruct input_struct; -+ SmtrStruct output_struct; -+ SmtrStruct state_struct; + Functional::IR ir; +- SmtScope scope; ++ SmtrScope scope; + std::string name; + +- SmtStruct input_struct; +- SmtStruct output_struct; +- SmtStruct state_struct; ++ SmtrStruct input_struct; ++ SmtrStruct output_struct; ++ SmtrStruct state_struct; -- SmtModule(Module *module) -+ SmtrModule(Module *module) - : ir(Functional::IR::from_module(module)) - , scope() - , name(scope.unique_name(module->name)) +- SmtModule(Module *module) ++ SmtrModule(Module *module) + : ir(Functional::IR::from_module(module)) + , scope() + , name(scope.unique_name(module->name)) @@ -200,7 +201,7 @@ struct SmtModule { - , output_struct(scope.unique_name(module->name.str() + "_Outputs"), scope) - , state_struct(scope.unique_name(module->name.str() + "_State"), scope) - { -- scope.reserve(name + "-initial"); -+ scope.reserve(name + "_initial"); - for (auto input : ir.inputs()) - input_struct.insert(input->name, input->sort); - for (auto output : ir.outputs()) -@@ -209,17 +210,20 @@ struct SmtModule { - state_struct.insert(state->name, state->sort); - } + , output_struct(scope.unique_name(module->name.str() + "_Outputs"), scope) + , state_struct(scope.unique_name(module->name.str() + "_State"), scope) + { +- scope.reserve(name + "-initial"); ++ scope.reserve(name + "_initial"); + for (auto input : ir.inputs()) + input_struct.insert(input->name, input->sort); + for (auto output : ir.outputs()) +@@ -212,14 +213,11 @@ struct SmtModule { + 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(std::ostream &out) -+ { -+ SExprWriter w(out); -+ -+ input_struct.write_definition(w); -+ output_struct.write_definition(w); -+ state_struct.write_definition(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,66 +234,75 @@ 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(); -- } + 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<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(); + } -- 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<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(); - } + void write(std::ostream &out) +@@ -263,33 +265,53 @@ struct SmtModule { + 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); + } }; -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 { -+ 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 { -+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| -+ log("\n"); -+ log(" write_functional_rosette [options] [filename]\n"); -+ log("\n"); -+ log("Functional Rosette Backend.\n"); -+ log("\n"); -+ log(" -provides\n"); -+ log(" include 'provide' statement(s) for loading output as a module\n"); -+ log("\n"); -+ } +- void help() override { log("\nFunctional SMT Backend.\n\n"); } ++ void help() override { ++ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| ++ log("\n"); ++ log(" write_functional_rosette [options] [filename]\n"); ++ log("\n"); ++ log("Functional Rosette Backend.\n"); ++ log("\n"); ++ log(" -provides\n"); ++ log(" include 'provide' statement(s) for loading output as a module\n"); ++ log("\n"); ++ } - void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) override - { -- log_header(design, "Executing Functional SMT Backend.\n"); -+ auto provides = false; + void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) override + { +- log_header(design, "Executing Functional SMT Backend.\n"); ++ auto provides = false; + -+ log_header(design, "Executing Functional Rosette Backend.\n"); ++ log_header(design, "Executing Functional Rosette Backend.\n"); -- size_t argidx = 1; -- extra_args(f, filename, args, argidx, design); -+ size_t argidx; -+ for (argidx = 1; argidx < args.size(); argidx++) -+ { -+ if (args[argidx] == "-provides") -+ provides = true; -+ else -+ break; -+ } -+ extra_args(f, filename, args, argidx); +- size_t argidx = 1; +- extra_args(f, filename, args, argidx, design); ++ size_t argidx; ++ for (argidx = 1; argidx < args.size(); argidx++) ++ { ++ if (args[argidx] == "-provides") ++ provides = true; ++ else ++ break; ++ } ++ extra_args(f, filename, args, argidx); + -+ *f << "#lang rosette/safe\n"; -+ if (provides) { -+ *f << "(provide (all-defined-out))\n"; -+ } ++ *f << "#lang rosette/safe\n"; ++ if (provides) { ++ *f << "(provide (all-defined-out))\n"; ++ } - for (auto module : design->selected_modules()) { - log("Processing module `%s`.\n", module->name.c_str()); -- SmtModule smt(module); -- smt.write(*f); -+ SmtrModule smtr(module); -+ smtr.write(*f); - } - } + for (auto module : design->selected_modules()) { + log("Processing module `%s`.\n", module->name.c_str()); +- SmtModule smt(module); +- smt.write(*f); ++ SmtrModule smtr(module); ++ smtr.write(*f); + } + } -} FunctionalSmtBackend; +} FunctionalSmtrBackend; From 34c424be68dab9c9160e8e2b7acf2f5c1cdf6463 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 7 Feb 2025 15:08:24 +1300 Subject: [PATCH 10/19] docs/rosette: Minor updates - Fixing typo - Reference `write_functional_rosette` - Adjusting/fixing diff sections - Comment on why the `code-block:: diff` isn't a `literalinclude` --- .../yosys_internals/extending_yosys/functional_ir.rst | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst index f44693c16..30d2b3b45 100644 --- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst +++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst @@ -149,7 +149,7 @@ Example: Adapting SMT-LIB backend for Rosette This section will walk through the process of adapting the SMT-LIB functional backend (`write_functional_smt2`) to work with another s-expression target, -`Rosette`_. +`Rosette`_ (`write_functional_rosette`). .. _Rosette: http://emina.github.io/rosette/ @@ -184,7 +184,7 @@ reject ascii characters which are not allowed in Racket variable names. .. literalinclude:: /code_examples/functional/rosette.diff :language: diff - :caption: diff of ``Scope`` close + :caption: diff of ``Scope`` class :start-at: -struct SmtScope : public Functional::Scope { :end-at: }; @@ -195,6 +195,7 @@ also no longer need to reserve ``pair``, ``first``, and ``second``. In current_state)`` and ``(outputs, next_state)`` into a single variable. Racket provides this functionality natively with ``cons``, which we will see later. +.. inlined diff for skipping the actual lists .. code-block:: diff :caption: diff of ``reserved_keywords`` list @@ -255,7 +256,7 @@ to support this; providing one scope that is local to the struct .. literalinclude:: /code_examples/functional/rosette.diff :language: diff :caption: diff of struct constructor - :start-at: - SmtStruct(std::string name, SmtScope &scope) + :start-at: SmtStruct(std::string name, SmtScope &scope) :end-before: void write_definition For writing outputs/next state (the ``write_value`` method), the only change is @@ -279,8 +280,8 @@ similar to the corresponding SMT-LIB function with minor adjustments for syntax. .. literalinclude:: /code_examples/functional/rosette.diff :language: diff :caption: portion of ``Functional::AbstractVisitor`` implementation diff showing similarities - :start-at: SExpr zero_extend - :end-at: SExpr sub + :start-at: SExpr logical_shift_left + :end-before: SExpr input However there are some differences in the two formats with regards to how booleans are handled, with Rosette providing built-in functions for conversion. From b02d2c633e9ba617a8b69ac86a26fac2ffc6690e Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 7 Feb 2025 15:08:49 +1300 Subject: [PATCH 11/19] docs/rosette: Module section body --- .../extending_yosys/functional_ir.rst | 85 ++++++++++++++++++- 1 file changed, 81 insertions(+), 4 deletions(-) diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst index 30d2b3b45..73589dfe4 100644 --- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst +++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst @@ -295,10 +295,87 @@ booleans are handled, with Rosette providing built-in functions for conversion. Module ~~~~~~ -- map RTLIL module to FunctionalIR -- iterate over FunctionalIR and map to Rosette - - defines the mapping function, ``(inputs, current_state) -> (outputs, - next_state)`` +The ``Functional::IR`` is wrapped in the ``Module`` class, with the mapping from +RTLIL module to FunctionalIR happening in the constructor. Each of the three +structs; inputs, outputs, and state; are then created from the corresponding +lists in the IR. The only change here is rename the initial state to use ``_`` +instead of ``-``, since the ``-`` in Rosette can be used to access struct +fields. + +.. literalinclude:: /code_examples/functional/rosette.diff + :language: diff + :caption: diff of ``Module`` constructor + :start-at: scope.reserve(name + :end-before: for (auto input + +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 mapping 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. + +.. inlined diff to show the complete function +.. code-block:: diff + :caption: diff of ``Module::write()`` method + + 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); + } + +For the ``write_eval`` method, the main differences are syntactical. First we +change the function declaration line for the Rosette style which drops the +explicit output typing and uses the ``define`` keyword instead of +``define-fun``. 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. Iteration over all of the +``Functional::Node``\ s in the IR is the same in both. + +.. inlined diff for showing the whole function while skipping the middle part +.. code-block:: diff + :caption: diff of ``Module::write_eval()`` method + + 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"))); + ... + - 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 +`assert`\ s 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. + +.. literalinclude:: /code_examples/functional/rosette.diff + :language: diff + :caption: diff of ``Module::write_initial()`` method + :start-at: void write_initial + :end-before: void write Backend ~~~~~~~ From 819c3260ec28797d12d5afe6ff356c10b7c786ee Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 7 Feb 2025 15:33:40 +1300 Subject: [PATCH 12/19] docs/rosette: Backend section body --- .../extending_yosys/functional_ir.rst | 26 ++++++++++++++----- 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst index 73589dfe4..81d987f0e 100644 --- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst +++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst @@ -380,10 +380,24 @@ whereas the SMT-LIB code can only verify that a given ``next_state`` is correct. Backend ~~~~~~~ -- registers the `write_functional_rosette` command -- options (``-provides``) - - allows file to be treated as a Racket package with structs and mapping - function available for use externally +The final part is the ``Backend`` itself, which registers the command in Yosys. +The ``execute`` method is the part that runs when the user calls +`write_functional_rosette`, handling any options, preparing the output file for +writing, and iterating over selected modules in the design. For more on adding +new commands to Yosys and how they work, refer to +:doc:`/yosys_internals/extending_yosys/extensions`. -- opens and prepares file for writing -- iterates over modules in design +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. + +.. literalinclude:: /code_examples/functional/rosette.diff + :language: diff + :caption: relevant portion of diff of ``Backend::execute()`` method + :start-at: lang rosette/safe + :end-before: for (auto module From c429aef60f60cf405cf9e35e019446b37c430617 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 22 Feb 2025 17:14:13 +1300 Subject: [PATCH 13/19] docs/rosette: More intro of SMT-LIB backend As the intro paragraph (now) says: > This section will introduce the SMT-LIB functional backend and what changes are needed... The example is intended to be read without prior knowledge of the SMT-LIB backend, but the previous version glossed over a lot and instead focused on *just* what was changed. This version should now be easier to follow without prior knowledge, while still being able to learn enough about the `Smt` version to adapt it to a different s-expression target that isn't Rosette. Also adds a few `literalinclude`s of smtlib.cc, which is now copied to `docs/source/generated` along with producing the rosette diff on the fly (which now also has up to 20 lines of context, enabling the full `Module::write()` diff to be literal included). --- Makefile | 14 +- .../code_examples/functional/rosette.diff | 372 ------------------ .../extending_yosys/functional_ir.rst | 149 ++++--- 3 files changed, 98 insertions(+), 437 deletions(-) delete mode 100644 docs/source/code_examples/functional/rosette.diff diff --git a/Makefile b/Makefile index 6f5fec6a2..73dd2e335 100644 --- a/Makefile +++ b/Makefile @@ -996,6 +996,18 @@ docs/source/cell/word_add.rst: $(TARGETS) $(EXTRA_TARGETS) docs/source/generated/cells.json: docs/source/generated $(TARGETS) $(EXTRA_TARGETS) $(Q) ./$(PROGRAM_PREFIX)yosys -p 'help -dump-cells-json $@' +docs/source/generated/%.cc: backends/%.cc + $(Q) mkdir -p $(@D) + $(Q) cp $< $@ + +# diff returns exit code 1 if the files are different, but it's not an error +docs/source/generated/functional/rosette.diff: backends/functional/smtlib.cc backends/functional/smtlib_rosette.cc + $(Q) mkdir -p $(@D) + $(Q) diff -U 20 $^ > $@ || exit 0 + +PHONY: docs/gen/functional_ir +docs/gen/functional_ir: docs/source/generated/functional/smtlib.cc docs/source/generated/functional/rosette.diff + PHONY: docs/gen docs/usage docs/reqs docs/gen: $(TARGETS) $(Q) $(MAKE) -C docs gen @@ -1031,7 +1043,7 @@ docs/reqs: $(Q) $(MAKE) -C docs reqs .PHONY: docs/prep -docs/prep: docs/source/cmd/abc.rst docs/source/generated/cells.json docs/gen docs/usage +docs/prep: docs/source/cmd/abc.rst docs/source/generated/cells.json docs/gen docs/usage docs/gen/functional_ir DOC_TARGET ?= html docs: docs/prep diff --git a/docs/source/code_examples/functional/rosette.diff b/docs/source/code_examples/functional/rosette.diff deleted file mode 100644 index 35c7936d1..000000000 --- a/docs/source/code_examples/functional/rosette.diff +++ /dev/null @@ -1,372 +0,0 @@ -diff --git a/backends/functional/smtlib.cc b/backends/functional/smtlib_rosette.cc -index 3eacf407c..c9e737d19 100644 ---- a/backends/functional/smtlib.cc -+++ b/backends/functional/smtlib_rosette.cc -@@ -29,80 +29,86 @@ PRIVATE_NAMESPACE_BEGIN - using SExprUtil::list; - - const char *reserved_keywords[] = { -- // reserved keywords from the smtlib spec -- "BINARY", "DECIMAL", "HEXADECIMAL", "NUMERAL", "STRING", "_", "!", "as", "let", "exists", "forall", "match", "par", -- "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", -- "exit", "get-assertions", "symbol", "sort", "get-assignment", "get-info", "get-model", -- "get-option", "get-proof", "get-unsat-assumptions", "get-unsat-core", "get-value", -- "pop", "push", "reset", "reset-assertions", "set-info", "set-logic", "set-option", -+ // reserved keywords from the racket spec -+ "struct", "lambda", "values", "extract", "concat", "bv", "let", "define", "cons", "list", "read", "write", -+ "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", -+ "future", "touch", "subprocess", "make-custodian", "custodian-shutdown-all", "current-custodian", "make", "tcp", -+ "connect", "prepare", "malloc", "free", "_fun", "_cprocedure", "build", "path", "file", "peek", "bytes", -+ "flush", "with", "lexer", "parser", "syntax", "interface", "send", "make-object", "new", "instantiate", -+ "define-generics", "set", - - // reserved for our own purposes -- "pair", "Pair", "first", "second", -- "inputs", "state", -+ "inputs", "state", "name", - nullptr - }; - --struct SmtScope : public Functional::Scope { -- SmtScope() { -+struct SmtrScope : public Functional::Scope { -+ 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)); - } - }; - --struct SmtSort { -+struct SmtrSort { - Functional::Sort sort; -- SmtSort(Functional::Sort sort) : sort(sort) {} -+ SmtrSort(Functional::Sort sort) : sort(sort) {} - 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"); - } - } - }; - --class SmtStruct { -+class SmtrStruct { - struct Field { -- SmtSort sort; -+ SmtrSort sort; - std::string accessor; -+ std::string name; - }; - idict field_names; - vector fields; -- SmtScope &scope; -+ SmtrScope &global_scope; -+ SmtrScope local_scope; - public: - std::string name; -- 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}); - } - 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 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(); - } - template 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(); - } - SExpr access(SExpr record, IdString name) { - size_t i = field_names.at(name); -@@ -117,28 +123,28 @@ std::string smt_const(RTLIL::Const const &c) { - return s; - } - --struct SmtPrintVisitor : public Functional::AbstractVisitor { -+struct SmtrPrintVisitor : public Functional::AbstractVisitor { - using Node = Functional::Node; - std::function n; -- SmtStruct &input_struct; -- SmtStruct &state_struct; -+ SmtrStruct &input_struct; -+ SmtrStruct &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) {} - - 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)); - } -- SExpr extract(SExpr &&arg, int offset, int out_width = 1) { -- return list(list("_", "extract", offset + out_width - 1, offset), std::move(arg)); -+ SExpr to_list(SExpr &&arg) { -+ return list("bitvector->bits", std::move(arg)); - } - - 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 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 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 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 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)); } -@@ -150,16 +156,11 @@ struct SmtPrintVisitor : public Functional::AbstractVisitor { - 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 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_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 { -- vector s { "bvxor" }; -- for(int i = 0; i < a.width(); i++) -- s.push_back(extract(n(a), i)); -- return s; -- } -- 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 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_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 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_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))); } -@@ -167,32 +168,32 @@ struct SmtPrintVisitor : public Functional::AbstractVisitor { - - SExpr extend(SExpr &&a, int in_width, int out_width) { - if(in_width < out_width) -- return list(list("_", "zero_extend", out_width - in_width), std::move(a)); -+ return list("zero-extend", std::move(a), list("bitvector", out_width)); - else - 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_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)); } - - 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); } - }; - --struct SmtModule { -+struct SmtrModule { - Functional::IR ir; -- SmtScope scope; -+ SmtrScope scope; - std::string name; - -- SmtStruct input_struct; -- SmtStruct output_struct; -- SmtStruct state_struct; -+ SmtrStruct input_struct; -+ SmtrStruct output_struct; -+ SmtrStruct state_struct; - -- SmtModule(Module *module) -+ SmtrModule(Module *module) - : ir(Functional::IR::from_module(module)) - , scope() - , name(scope.unique_name(module->name)) -@@ -200,7 +201,7 @@ struct SmtModule { - , output_struct(scope.unique_name(module->name.str() + "_Outputs"), scope) - , state_struct(scope.unique_name(module->name.str() + "_State"), scope) - { -- scope.reserve(name + "-initial"); -+ scope.reserve(name + "_initial"); - for (auto input : ir.inputs()) - input_struct.insert(input->name, input->sort); - for (auto output : ir.outputs()) -@@ -212,14 +213,11 @@ struct SmtModule { - 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_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<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(); - } - - void write(std::ostream &out) -@@ -263,33 +265,53 @@ struct SmtModule { - 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); - } - }; - --struct FunctionalSmtBackend : public Backend { -- FunctionalSmtBackend() : Backend("functional_smt2", "Generate SMT-LIB from Functional IR") {} -+struct FunctionalSmtrBackend : public Backend { -+ FunctionalSmtrBackend() : Backend("functional_rosette", "Generate Rosette compatible Racket from Functional IR") {} - -- void help() override { log("\nFunctional SMT Backend.\n\n"); } -+ void help() override { -+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| -+ log("\n"); -+ log(" write_functional_rosette [options] [filename]\n"); -+ log("\n"); -+ log("Functional Rosette Backend.\n"); -+ log("\n"); -+ log(" -provides\n"); -+ log(" include 'provide' statement(s) for loading output as a module\n"); -+ log("\n"); -+ } - - void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) override - { -- log_header(design, "Executing Functional SMT Backend.\n"); -+ auto provides = false; -+ -+ log_header(design, "Executing Functional Rosette Backend.\n"); - -- size_t argidx = 1; -- extra_args(f, filename, args, argidx, design); -+ size_t argidx; -+ for (argidx = 1; argidx < args.size(); argidx++) -+ { -+ if (args[argidx] == "-provides") -+ provides = true; -+ else -+ break; -+ } -+ extra_args(f, filename, args, argidx); -+ -+ *f << "#lang rosette/safe\n"; -+ if (provides) { -+ *f << "(provide (all-defined-out))\n"; -+ } - - for (auto module : design->selected_modules()) { - log("Processing module `%s`.\n", module->name.c_str()); -- SmtModule smt(module); -- smt.write(*f); -+ SmtrModule smtr(module); -+ smtr.write(*f); - } - } --} FunctionalSmtBackend; -+} FunctionalSmtrBackend; - - PRIVATE_NAMESPACE_END diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst index 81d987f0e..42eabc0b1 100644 --- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst +++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst @@ -147,9 +147,9 @@ S-expressions can be constructed with ``SExpr::list``, for example ``SExpr expr Example: Adapting SMT-LIB backend for Rosette --------------------------------------------- -This section will walk through the process of adapting the SMT-LIB functional -backend (`write_functional_smt2`) to work with another s-expression target, -`Rosette`_ (`write_functional_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`). .. _Rosette: http://emina.github.io/rosette/ @@ -177,12 +177,19 @@ Scope ~~~~~ As described above, the ``Functional::Scope`` class is derived in order to avoid -collisions between identifiers in the generated output. We switch out ``Smt`` -in the class name for ``Smtr`` for ``smtlib_rosette``; which will happen through -the rest of the code too. We also update the ``is_character_legal`` method to -reject ascii characters which are not allowed in Racket variable names. +collisions between identifiers in the generated output. In the SMT-LIB version +the ``SmtScope`` class implements ``Scope``; 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. -.. literalinclude:: /code_examples/functional/rosette.diff +In the Rosette version we switch out ``Smt`` in the class name for ``Smtr`` to +mean ``smtlib_rosette``; this will happen through the rest of the code too. We +also update list of legal ascii characters in the ``is_character_legal`` method +to only those allowed in Racket variable names. + +.. literalinclude:: /generated/functional/rosette.diff :language: diff :caption: diff of ``Scope`` class :start-at: -struct SmtScope : public Functional::Scope { @@ -218,13 +225,13 @@ and racket specifications to save on space in this document. Sort ~~~~ -The ``Sort`` class 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 ``bitvector``\ -s, and memories as ``list``\ s of signals. +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 ``bitvector``\ s, and memories as ``list``\ s of signals. -.. literalinclude:: /code_examples/functional/rosette.diff +.. literalinclude:: /generated/functional/rosette.diff :language: diff :caption: diff of ``Sort`` wrapper :start-at: SExpr to_sexpr() const { @@ -233,37 +240,56 @@ s, and memories as ``list``\ s of signals. Struct ~~~~~~ -The SMT-LIB backend uses a class, ``SmtStruct``, to help with describing the -input, output, and state data structs. Where each struct in the SMT-LIB output -is a new ``datatype`` with each element having its type declared using the -`Sort`_ above, in Rosette we use the native ``struct`` with each field only -being referred to by name. For ease of use, we include comments for each field -to indicate the expected type. +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. -.. literalinclude:: /code_examples/functional/rosette.diff +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 is +not as strongly-typed. For ease of use, we provide the expected type for each +field as comments. + +.. literalinclude:: /generated/functional/rosette.diff :language: diff :caption: diff of ``write_definition`` method :start-at: void write_definition :end-before: template void write_value -Struct fields in Rosette are accessed as ``-``, where -field names only need to be unique within the struct, while accessors are unique -within the 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``). +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. -.. literalinclude:: /code_examples/functional/rosette.diff +.. literalinclude:: /generated/functional/smtlib.cc + :language: c++ + :caption: ``Struct::access()`` method + :start-at: SExpr access( + :end-before: }; + +In Rosette, struct fields are accessed as ``-`` 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. + +.. literalinclude:: /generated/functional/rosette.diff :language: diff :caption: diff of struct constructor :start-at: SmtStruct(std::string name, SmtScope &scope) :end-before: void write_definition -For writing outputs/next state (the ``write_value`` method), the only change is -to remove the check for zero-argument constructors since this is not necessary -with Rosette ``struct``\ s. +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 ``struct``\ s. -.. literalinclude:: /code_examples/functional/rosette.diff +.. literalinclude:: /generated/functional/rosette.diff :language: diff :caption: diff of ``write_value`` method :start-at: template void write_value @@ -273,11 +299,13 @@ PrintVisitor ~~~~~~~~~~~~ The ``PrintVisitor`` implements the abstract ``Functional::AbstractVisitor`` -class for converting FunctionalIR functions into s-expressions, including -reading inputs/current state. For most functions, the Rosette output is very -similar to the corresponding SMT-LIB function with minor adjustments for syntax. +class, described above in `What is FunctionalIR`_, with a return type of +``SExpr``. This class converts FunctionalIR functions into s-expressions, +including reading inputs/current state with the ``access`` method from the +`Struct`_. For most functions, the Rosette output is very similar to the +corresponding SMT-LIB function with minor adjustments for syntax. -.. literalinclude:: /code_examples/functional/rosette.diff +.. literalinclude:: /generated/functional/rosette.diff :language: diff :caption: portion of ``Functional::AbstractVisitor`` implementation diff showing similarities :start-at: SExpr logical_shift_left @@ -286,7 +314,7 @@ similar to the corresponding SMT-LIB function with minor adjustments for syntax. However there are some differences in the two formats with regards to how booleans are handled, with Rosette providing built-in functions for conversion. -.. literalinclude:: /code_examples/functional/rosette.diff +.. literalinclude:: /generated/functional/rosette.diff :language: diff :caption: portion of ``Functional::AbstractVisitor`` implementation diff showing differences :start-at: SExpr from_bool @@ -295,14 +323,21 @@ booleans are handled, with Rosette providing built-in functions for conversion. Module ~~~~~~ -The ``Functional::IR`` is wrapped in the ``Module`` class, with the mapping from -RTLIL module to FunctionalIR happening in the constructor. Each of the three -structs; inputs, outputs, and state; are then created from the corresponding -lists in the IR. The only change here is rename the initial state to use ``_`` -instead of ``-``, since the ``-`` in Rosette can be used to access struct -fields. +The ``Functional::IR`` is wrapped in the ``SmtModule`` class, with the mapping +from RTLIL module to FunctionalIR happening in the constructor. Each of the +three ``SmtStruct``\ s; inputs, outputs, and state; are created, with each value +in the corresponding lists in the IR being ``insert``\ ed. -.. literalinclude:: /code_examples/functional/rosette.diff +.. literalinclude:: /generated/functional/smtlib.cc + :language: c++ + :caption: ``SmtModule`` constructor + :start-at: SmtModule(Module + :end-at: } + +Since Racket uses the ``-`` to access struct fields, the ``SmtrModule`` instead +uses an underscore for the name of the initial state. + +.. literalinclude:: /generated/functional/rosette.diff :language: diff :caption: diff of ``Module`` constructor :start-at: scope.reserve(name @@ -316,25 +351,11 @@ 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. -.. inlined diff to show the complete function -.. code-block:: diff +.. literalinclude:: /generated/functional/rosette.diff + :language: diff :caption: diff of ``Module::write()`` method - - 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); - } + :start-at: void write(std::ostream &out) + :end-at: } For the ``write_eval`` method, the main differences are syntactical. First we change the function declaration line for the Rosette style which drops the @@ -371,7 +392,7 @@ 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. -.. literalinclude:: /code_examples/functional/rosette.diff +.. literalinclude:: /generated/functional/rosette.diff :language: diff :caption: diff of ``Module::write_initial()`` method :start-at: void write_initial @@ -396,7 +417,7 @@ 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. -.. literalinclude:: /code_examples/functional/rosette.diff +.. literalinclude:: /generated/functional/rosette.diff :language: diff :caption: relevant portion of diff of ``Backend::execute()`` method :start-at: lang rosette/safe From db823a6acb772de4b06c4cf4b136f0b8dff5a86a Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Thu, 27 Feb 2025 16:11:44 +1300 Subject: [PATCH 14/19] docs/rosette: Fix inline code --- docs/source/yosys_internals/extending_yosys/functional_ir.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst index 42eabc0b1..c82a2828a 100644 --- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst +++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst @@ -386,7 +386,7 @@ and the ``next_state`` in a single variable. Iteration over all of the } For the ``write_initial`` method, the SMT-LIB backend uses ``declare-const`` and -`assert`\ s which must always hold true. For Rosette we instead define the +``assert``\ s 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``, From 560b5fe6bd53dd174d16698b4639a8b168d20f79 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Thu, 27 Feb 2025 16:14:59 +1300 Subject: [PATCH 15/19] docs/functional: Add dummy toy example Add `dummy.cc`, loosely based on `backends/functional/test_generic.cc` but as an actualy backend and without the memory testing. Skeleton section for minimal functional backend, describing the aforementioned `dummy.cc`. --- docs/source/code_examples/functional/dummy.cc | 44 +++++++++++++++++++ .../extending_yosys/functional_ir.rst | 35 +++++++++++++++ 2 files changed, 79 insertions(+) create mode 100644 docs/source/code_examples/functional/dummy.cc diff --git a/docs/source/code_examples/functional/dummy.cc b/docs/source/code_examples/functional/dummy.cc new file mode 100644 index 000000000..3d84b84ba --- /dev/null +++ b/docs/source/code_examples/functional/dummy.cc @@ -0,0 +1,44 @@ +#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 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 diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst index c82a2828a..80eeeebf2 100644 --- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst +++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst @@ -144,6 +144,41 @@ S-expressions can be constructed with ``SExpr::list``, for example ``SExpr expr parentheses. - The destructor calls ``flush`` but also closes all unclosed parentheses. +Example: A minimal functional backend +------------------------------------- + +.. literalinclude:: /code_examples/functional/dummy.cc + :language: c++ + :caption: Example source code for a minimal functional backend + +- three main steps needed + + + convert to FunctionalIR + + handle nodes + + handle outputs and next state + +- backend pass boiler plate gives us ``write_functional_dummy`` command +- pointer ``f`` is a ``std::ostream`` we can write to, being either a file or + stdout +- FunctionalIR conversion done by ``Functional::IR::from_module()`` +- each node performs some function or operation (including reading input/current + state) + + + each variable is assigned exactly once before being used + + ``node.name()`` returns a ``RTLIL::IdString``, which we convert for + printing with ``id2cstr()`` + + ``node.to_string()`` converts the node into a string of the form + ``function(args)`` + + * ``function`` is the result of ``Functional::IR::fn_to_string(node.fn())`` + * ``args`` are the zero or more arguments passed to the function, most + commonly the name of another node + * wraps ``node.visit()`` with a private visitor with return type + ``std::string`` + +- ``Functional::IROutput::value()`` and ``Functional::IRState::next_value()`` + represent the outputs of our function + Example: Adapting SMT-LIB backend for Rosette --------------------------------------------- From e01a4137222d6c2f76da1c017aaa70cd91a290da Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 28 Feb 2025 14:49:05 +1300 Subject: [PATCH 16/19] docs/rosette: List major changes in overview Also a little paragraph on why SMT-LIB is used as the base. --- .../extending_yosys/functional_ir.rst | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst index 80eeeebf2..8395e6504 100644 --- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst +++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst @@ -201,6 +201,11 @@ Overview .. _Racket: http://racket-lang.org/ .. _SMT: http://smtlib.cs.uiowa.edu/ +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 :file:`backends/functional` as ``smtlib.cc`` and ``smtlib_rosette.cc`` @@ -208,6 +213,23 @@ 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 ``Smt`` prefixes in names are replace with ``Smtr`` to mean + ``smtlib_rosette``; +- syntax is adjusted for Racket; +- data structures for input/output/state are changed from using + ``declare-datatype`` with statically typed fields, to using ``struct`` with no + static typing; +- the transfer function also loses its static typing; +- sign/zero extension in Rosette uses 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 ``-provides`` option is introduced to more easily use generated code + within Rosette based applications. + Scope ~~~~~ From 3c493d2bef628fb92f5d5bb375a38b97197762e5 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 28 Feb 2025 16:33:57 +1300 Subject: [PATCH 17/19] docs/rosette: Reword Acknowledge the minimal functional backend, highlighting what's new/different for our SExpr targets. Add and use the reference `minimal backend`. Use `note` directives to point out missing code sections (highlighting that the included diffs are not complete). Racket *is* still strongly-typed, it's just dynamic instead of static. Adjust phrasing to reflect that. Adjust some of the literal includes, adding a new section from the `Functional::AbstractVisitor`, splitting the `Module::write_eval()` in twain and adding a `smtlib.cc` literal include for the node iteration, as well as for the `FunctionalSmtBackend` to compare against the minimal backend. Move `Backend` description up to minimal functional backend section. --- .../extending_yosys/functional_ir.rst | 166 +++++++++++------- 1 file changed, 102 insertions(+), 64 deletions(-) diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst index 8395e6504..689d45d32 100644 --- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst +++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst @@ -144,6 +144,8 @@ S-expressions can be constructed with ``SExpr::list``, for example ``SExpr expr parentheses. - The destructor calls ``flush`` but also closes all unclosed parentheses. +.. _minimal backend: + Example: A minimal functional backend ------------------------------------- @@ -158,6 +160,13 @@ Example: A minimal functional backend + handle outputs and next state - backend pass boiler plate gives us ``write_functional_dummy`` command + +The final part is the ``Backend`` itself, which registers the command in Yosys. +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. For more on adding new commands to Yosys and +how they work, refer to :doc:`/yosys_internals/extending_yosys/extensions`. + - pointer ``f`` is a ``std::ostream`` we can write to, being either a file or stdout - FunctionalIR conversion done by ``Functional::IR::from_module()`` @@ -233,18 +242,23 @@ The major changes from the SMT-LIB backend are as follows: Scope ~~~~~ -As described above, the ``Functional::Scope`` class is derived in order to avoid -collisions between identifiers in the generated output. In the SMT-LIB version -the ``SmtScope`` class implements ``Scope``; 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. +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 Rosette version we switch out ``Smt`` in the class name for ``Smtr`` to -mean ``smtlib_rosette``; this will happen through the rest of the code too. We -also update list of legal ascii characters in the ``is_character_legal`` method -to only those allowed in Racket variable names. +In the SMT-LIB version, the ``SmtScope`` class implements ``Scope``; +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. .. literalinclude:: /generated/functional/rosette.diff :language: diff @@ -276,8 +290,8 @@ provides this functionality natively with ``cons``, which we will see later. nullptr }; -Note that we skip over the actual list of reserved keywords from both the smtlib -and racket specifications to save on space in this document. +.. 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 ~~~~ @@ -297,16 +311,17 @@ signals represented as ``bitvector``\ s, and memories as ``list``\ s of signals. Struct ~~~~~~ -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. +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 is -not as strongly-typed. For ease of use, we provide the expected type for each -field as comments. +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. .. literalinclude:: /generated/functional/rosette.diff :language: diff @@ -355,18 +370,19 @@ Rosette ``struct``\ s. PrintVisitor ~~~~~~~~~~~~ -The ``PrintVisitor`` implements the abstract ``Functional::AbstractVisitor`` -class, described above in `What is FunctionalIR`_, with a return type of -``SExpr``. This class converts FunctionalIR functions into s-expressions, -including reading inputs/current state with the ``access`` method from the -`Struct`_. For most functions, the Rosette output is very similar to the -corresponding SMT-LIB function with minor adjustments for syntax. +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. .. literalinclude:: /generated/functional/rosette.diff :language: diff :caption: portion of ``Functional::AbstractVisitor`` implementation diff showing similarities :start-at: SExpr logical_shift_left - :end-before: SExpr input + :end-at: "list-set-bv" However there are some differences in the two formats with regards to how booleans are handled, with Rosette providing built-in functions for conversion. @@ -377,13 +393,30 @@ booleans are handled, with Rosette providing built-in functions for conversion. :start-at: SExpr from_bool :end-before: SExpr extract +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)``). + +.. literalinclude:: /generated/functional/rosette.diff + :language: diff + :caption: zero/sign extension implementation diff + :start-after: SExpr buf( + :end-before: SExpr concat( + :lines: 2-3, 5-6 + +.. note:: Be sure to check the source code for the full list of differences here. + Module ~~~~~~ -The ``Functional::IR`` is wrapped in the ``SmtModule`` class, with the mapping -from RTLIL module to FunctionalIR happening in the constructor. Each of the -three ``SmtStruct``\ s; inputs, outputs, and state; are created, with each value -in the corresponding lists in the IR being ``insert``\ ed. +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 ``SmtStruct``\ s; inputs, outputs, and state; +are also created in the constructor, with each value in the corresponding lists +in the IR being ``insert``\ ed. .. literalinclude:: /generated/functional/smtlib.cc :language: c++ @@ -403,7 +436,7 @@ uses an underscore for the name of the initial state. 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 mapping function ``(inputs, +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. @@ -414,33 +447,35 @@ that the ``pair`` declaration isn't needed. :start-at: void write(std::ostream &out) :end-at: } -For the ``write_eval`` method, the main differences are syntactical. First we -change the function declaration line for the Rosette style which drops the -explicit output typing and uses the ``define`` keyword instead of -``define-fun``. 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. Iteration over all of the -``Functional::Node``\ s in the IR is the same in both. +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. -.. inlined diff for showing the whole function while skipping the middle part -.. code-block:: diff - :caption: diff of ``Module::write_eval()`` method +.. literalinclude:: /generated/functional/smtlib.cc + :language: c++ + :caption: iterating over FunctionalIR nodes in ``SmtModule::write_eval()`` + :start-at: for(auto n : ir) + :end-at: } - 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"))); - ... - - 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(); - } +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. + +.. literalinclude:: /generated/functional/rosette.diff + :language: diff + :caption: diff of ``Module::write_eval()`` transfer function declaration + :start-at: w.open(list("define-fun" + :end-at: w.open(list("define" + +.. literalinclude:: /generated/functional/rosette.diff + :language: diff + :caption: diff of output/next state handling ``Module::write_eval()`` + :start-at: w.open(list("pair" + :end-at: w.pop(); For the ``write_initial`` method, the SMT-LIB backend uses ``declare-const`` and ``assert``\ s which must always hold true. For Rosette we instead define the @@ -458,12 +493,15 @@ whereas the SMT-LIB code can only verify that a given ``next_state`` is correct. Backend ~~~~~~~ -The final part is the ``Backend`` itself, which registers the command in Yosys. -The ``execute`` method is the part that runs when the user calls -`write_functional_rosette`, handling any options, preparing the output file for -writing, and iterating over selected modules in the design. For more on adding -new commands to Yosys and how they work, refer to -:doc:`/yosys_internals/extending_yosys/extensions`. +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. + +.. literalinclude:: /generated/functional/smtlib.cc + :language: c++ + :caption: The ``FunctionalSmtBackend`` + :start-at: struct FunctionalSmtBackend + :end-at: } 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 From b56e3ec6e407c75a67d26f9b1badee1b3b79d4de Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 1 Mar 2025 16:15:54 +1300 Subject: [PATCH 18/19] docs/functional: Minimal backend paragraphs I was thinking about compiling the dummy example and including a simple example usage, but it turns out functional.h isn't (currently) available for extensions. --- .../extending_yosys/functional_ir.rst | 67 ++++++++++--------- 1 file changed, 36 insertions(+), 31 deletions(-) diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst index 689d45d32..37a7e33e1 100644 --- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst +++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst @@ -149,44 +149,49 @@ S-expressions can be constructed with ``SExpr::list``, for example ``SExpr expr 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::Node``\ s 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: + .. literalinclude:: /code_examples/functional/dummy.cc :language: c++ - :caption: Example source code for a minimal functional backend + :caption: Example source code for a minimal functional backend, ``dummy.cc`` -- three main steps needed +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. - + convert to FunctionalIR - + handle nodes - + handle outputs and next state +.. note:: -- backend pass boiler plate gives us ``write_functional_dummy`` command + For more on adding new commands to Yosys and how they work, refer to + :doc:`/yosys_internals/extending_yosys/extensions`. -The final part is the ``Backend`` itself, which registers the command in Yosys. -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. For more on adding new commands to Yosys and -how they work, refer to :doc:`/yosys_internals/extending_yosys/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``. -- pointer ``f`` is a ``std::ostream`` we can write to, being either a file or - stdout -- FunctionalIR conversion done by ``Functional::IR::from_module()`` -- each node performs some function or operation (including reading input/current - state) - - + each variable is assigned exactly once before being used - + ``node.name()`` returns a ``RTLIL::IdString``, which we convert for - printing with ``id2cstr()`` - + ``node.to_string()`` converts the node into a string of the form - ``function(args)`` - - * ``function`` is the result of ``Functional::IR::fn_to_string(node.fn())`` - * ``args`` are the zero or more arguments passed to the function, most - commonly the name of another node - * wraps ``node.visit()`` with a private visitor with return type - ``std::string`` - -- ``Functional::IROutput::value()`` and ``Functional::IRState::next_value()`` - represent the outputs of our function +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 --------------------------------------------- From c9785584da449b55e3e0117bf178a58e237f09ef Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 7 Mar 2025 08:39:21 +1300 Subject: [PATCH 19/19] docs/rosette: Fix tenses --- docs/source/yosys_internals/extending_yosys/functional_ir.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst index 37a7e33e1..4f363623e 100644 --- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst +++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst @@ -229,14 +229,14 @@ semantics/syntax of the language. The major changes from the SMT-LIB backend are as follows: -- all of the ``Smt`` prefixes in names are replace with ``Smtr`` to mean +- all of the ``Smt`` prefixes in names are replaced with ``Smtr`` to mean ``smtlib_rosette``; - syntax is adjusted for Racket; - data structures for input/output/state are changed from using ``declare-datatype`` with statically typed fields, to using ``struct`` with no static typing; - the transfer function also loses its static typing; -- sign/zero extension in Rosette uses the output width instead of the number of +- 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;