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] 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