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