Rework the FSM solver, scope the preprocessing functions, and clean up the examples

CHANGELOG.md

@@ -91,8 +91,26 @@ All notable changes to this project will be documented in this file.
     * added `NetlistGraph::from_gates` that builds a graph from a subset of the gates of a netlist, optionally representing a gate by a primary and a shadow vertex so that feedback through it does not close a cycle
   * dataflow analysis
     * fixed broken initialization of DANA plugin when starting via CLI
+  * FSM solver
+    * reworked the API of `solve_fsm` into a single function that is set up through a `Configuration` object, which also selects between the SMT and the brute force approach
+    * changed `solve_fsm` to report the value of each configured output of the FSM in each state, annotating the states of the DOT graph with it
+    * changed `solve_fsm` to no longer write a file on its own, the DOT graph is now rendered by calling `generate_dot_graph` on the returned state transition graph
+    * changed `solve_fsm` to no longer open the graph in the dot viewer behind the user's back, use `dot_viewer.load_dot_file` to display it
+    * added `to_string` and `write_txt` to the state transition graph, printing the full conditions of all transitions together with a legend that maps the state bits, the outputs, and every net variable of a Boolean function back to the netlist
+    * split the `solve_fsm` API into one header per struct, mirroring the layout of the dataflow analysis plugin
+    * removed the debug output that `solve_fsm` printed to stdout on every run
+    * fixed `solve_fsm` interpreting a user-provided initial state with the wrong bit order, which made the exploration start from a different state than the one requested
+    * added tests for the `solve_fsm` plugin, which had none so far
   * netlist preprocessing
     * fixed `remove_redundant_gates` treating two flip-flops as duplicates although they start out at different values, as the fingerprint it groups them by covers the gate type and the fan-in but not the initial value, and flip-flops are merged on that fingerprint alone without the equivalence check that combinational gates get. This affects 11 of the 13 flip-flop types of the Xilinx UNISIM library, all of which carry an `INIT` value
+    * added an optional gate scope to the preprocessing functions of `netlist_preprocessing` and `xilinx_toolbox`, restricting which gates may be modified or deleted and defaulting to the entire netlist
+    * changed `split_shift_registers` and `unify_ff_outputs` to assign newly created gates to the module of the gate they replace instead of always to the top module
+    * fixed `simplify_lut_inits` crashing on a LUT whose output pin is unconnected
+    * fixed `remove_unconnected_gates` looping forever if a gate could not be deleted
+  * Xilinx toolbox
+    * fixed `split_luts` crashing on a `LUT6_2` that only uses one of its two output pins, which is the common case the function is meant to handle
+    * fixed the documentation of `split_shift_registers`, which claimed that only `SRL16E` is supported although `SRLC32E` is handled as well
+    * added tests for the `xilinx_toolbox` plugin, which had none so far
   * bit-order propagation
     * changed the interface to speak in a `BitOrder`, which is the order of one module pin group, and a `BitOrderResult`, which is what a propagation reports, in place of a map from pairs of module and pin group to a map from net to index. A bit order is now an object rather than a container, so Python can be given one without losing track of the netlist it belongs to, and a result iterates by module and pin group ID rather than by the addresses they happen to sit at
     * added tests for the plugin, which had none
@@ -103,6 +121,7 @@ All notable changes to this project will be documented in this file.
     * fixed the documentation of `NetlistSimulatorController::initialize`, which described the behaviour of the legacy `NetlistSimulator`: it claimed that no gates or clocks may be added afterwards and that `simulate` calls it automatically, neither of which holds since its body became empty
   * dot viewer
     * added 'hover over node' feature in dot viewer
+    * fixed the DOT viewer drawing the line break escapes of a node label verbatim instead of breaking the line, and drawing a red debug rectangle around any label that does not fit its node
 * GUI
   * fixed the GUI hanging for minutes when a module with many gates is selected, `ModuleModel` emitted a row insert signal per item while the model was already being reset, which made the attached filter proxy remap its rows once per item
   * fixed the GUI stalling when a large module is unfolded, the tree views measured every row individually and shaped the text of each gate name just to learn how tall the row is
@@ -112,6 +131,9 @@ All notable changes to this project will be documented in this file.
   * added option to focus on pin in pin context menu
   * changed default order to 'descending' when creating a pin group via Python command
   * changed behavior of GUI plugin manager to keep only those plugins loaded which are requested by user
+  * fixed the GUI dropping an unrelated gate from the selection instead of the net itself when a selected net is deleted
+  * fixed the GUI re-laying out its graph views once per gate while a preprocessing function invoked from a context menu deletes or replaces many of them
+  * added context menu entries to the GUI for `remove_buffers`, `unify_ff_outputs`, `split_luts`, and `split_shift_registers`, each applicable to the current selection or to the entire netlist
   * module pin groups
     * fixed bug in pin model which must not crash when deleting a non-empty pin group
     * fixed bug by disallowing deletion of group comprising a single pin with same name

examples/.gitignore

@@ -1,7 +1,7 @@
 # Created by .ignore support plugin (hsz.mobi)
 *
-!README.md
+!crypto_trojan.zip
 !fsm.zip
 !uart.zip
 !simple_alu.zip
-!toy_cipher.zip
+!toy_cipher.zip

plugins/dot_viewer/deps/QGVCore/QGVNode.cpp

@@ -46,6 +46,17 @@ QString QGVNode::label() const
     return QString();
 }
 
+QString QGVNode::displayLabel() const
+{
+    /* The DOT format encodes line breaks within a label as the escape sequences \n, \l and \r, which are kept
+     * verbatim in the attribute and would be drawn as literal characters. */
+    QString retval = label();
+    retval.replace("\\n", "\n");
+    retval.replace("\\l", "\n");
+    retval.replace("\\r", "\n");
+    return retval;
+}
+
 void QGVNode::setLabel(const QString &label)
 {
     setAttribute("label", label);
@@ -83,10 +94,15 @@ void QGVNode::paint(QPainter * painter, const QStyleOptionGraphicsItem *, QWidge
     painter->setPen(QGVCore::toColor(getAttribute("labelfontcolor")));
 
     const QRectF rect = boundingRect().adjusted(2,2,-2,-2); //Margin
+    const QString text = displayLabel();
     if(_icon.isNull())
     {
+        /* A label may span several lines, so the widest of them decides whether it still fits. */
         QFontMetrics fm(painter->font());
-        qreal fw = fm.horizontalAdvance(label());
+        qreal fw = 0;
+        for (const QString& line : text.split('\n'))
+            fw = qMax(fw, (qreal) fm.horizontalAdvance(line));
+
         if (fw > rect.width())
         {
             qreal scl = rect.width()/fw;
@@ -96,18 +112,15 @@ void QGVNode::paint(QPainter * painter, const QStyleOptionGraphicsItem *, QWidge
             painter->translate(tx,ty);
             painter->scale(scl, scl);
             painter->translate(-tx/scl, -ty);
-            painter->drawText(rect, Qt::AlignLeft | Qt::AlignVCenter | Qt::TextDontClip | Qt::TextSingleLine, label());
-            painter->setPen( QPen(Qt::red,1) );
-            painter->setBrush ( Qt::NoBrush );
-            painter->drawRect(rect);
+            painter->drawText(rect, Qt::AlignLeft | Qt::AlignVCenter | Qt::TextDontClip, text);
             painter->restore();
         }
         else
-            painter->drawText(rect, Qt::AlignCenter , QGVNode::label());
+            painter->drawText(rect, Qt::AlignCenter, text);
     }
     else
     {
-        painter->drawText(rect.adjusted(0,0,0, -rect.height()*2/3), Qt::AlignCenter , QGVNode::label());
+        painter->drawText(rect.adjusted(0,0,0, -rect.height()*2/3), Qt::AlignCenter, text);
 
         const QRectF img_rect = rect.adjusted(0, rect.height()/3,0, 0);
         QImage img = _icon.scaled(img_rect.size().toSize(), Qt::KeepAspectRatio, Qt::SmoothTransformation);

plugins/dot_viewer/deps/QGVCore/QGVNode.h

@@ -36,6 +36,11 @@ class QGVCORE_EXPORT QGVNode : public QGraphicsItem
     ~QGVNode();
 
     QString label() const;
+
+    /**
+     * The label as it should be drawn, with the line break escapes of the DOT format resolved.
+     */
+    QString displayLabel() const;
     void setLabel(const QString &label);
 
     QRectF boundingRect() const override;

plugins/gui/src/selection_relay/selection_relay.cpp

@@ -418,7 +418,7 @@ namespace hal
         if (it != mSelectedNets.end())
         {
             initializeAction();
-            mAction->mGates.remove(id);
+            mAction->mNets.remove(id);
             executeAction();
         }
     }

plugins/netlist_preprocessing/include/netlist_preprocessing/netlist_preprocessing.h

@@ -49,28 +49,32 @@ namespace hal
          * Removes all LUT fan-in endpoints that do not correspond to a variable within the Boolean function that determines the output of a gate.
          * 
          * @param[in] nl - The netlist to operate on. 
+         * @param[in] gates - The gates to consider. Defaults to an empty vector, in which case all gates of the netlist are considered.
          * @returns OK() and the number of removed LUT endpoints on success, an error otherwise.
          */
-        Result<u32> remove_unused_lut_inputs(Netlist* nl);
+        Result<u32> remove_unused_lut_inputs(Netlist* nl, const std::vector<Gate*>& gates = {});
 
         /**
          * Removes buffer gates from the netlist and connect their fan-in to their fan-out nets.
          * Considers all combinational gates and takes their inputs into account.
          * For example, a 2-input AND gate with one input being connected to constant `1` will also be removed.
          * 
          * @param[in] nl - The netlist to operate on. 
+         * @param[in] gates - The gates to consider. Defaults to an empty vector, in which case all gates of the netlist are considered.
          * @returns OK() and the number of removed buffers on success, an error otherwise.
          */
-        Result<u32> remove_buffers(Netlist* nl);
+        Result<u32> remove_buffers(Netlist* nl, const std::vector<Gate*>& gates = {});
 
         /**
          * Removes redundant gates from the netlist, i.e., gates that are functionally equivalent and are connected to the same input nets.
+         * Only gates contained in `gates` are removed, the equivalent gate that is kept in their stead may lie outside of `gates`.
          * 
          * @param[in] nl - The netlist to operate on. 
          * @param[in] filter - Optional filter to fine-tune which gates are being replaced. Default to a `nullptr`.
+         * @param[in] gates - The gates to consider. Defaults to an empty vector, in which case all gates of the netlist are considered.
          * @return OK() and the number of removed gates on success, an error otherwise.
          */
-        Result<u32> remove_redundant_gates(Netlist* nl, const std::function<bool(const Gate*)>& filter = nullptr);
+        Result<u32> remove_redundant_gates(Netlist* nl, const std::function<bool(const Gate*)>& filter = nullptr, const std::vector<Gate*>& gates = {});
 
         /**
          * Removes redundant sequential feedback loops.
@@ -95,11 +99,13 @@ namespace hal
 
         /**
          * Removes gates for which all fan-out nets do not have a destination and are not global output nets.
+         * The removal is repeated until no further gates can be removed, but gates outside of `gates` are never removed, even if they become unconnected in the process.
          * 
          * @param[in] nl - The netlist to operate on. 
+         * @param[in] gates - The gates to consider. Defaults to an empty vector, in which case all gates of the netlist are considered.
          * @return OK() and the number of removed gates on success, an error otherwise.
          */
-        Result<u32> remove_unconnected_gates(Netlist* nl);
+        Result<u32> remove_unconnected_gates(Netlist* nl, const std::vector<Gate*>& gates = {});
 
         /**
          * Removes nets who have neither a source, nor a destination.
@@ -132,28 +138,33 @@ namespace hal
         /**
          * Builds for all gate output nets the Boolean function and substitutes all variables connected to vcc/gnd nets with the respective boolean value.
          * If the function simplifies to a  boolean constant cut the connection to the nets destinations and directly connect it to vcc/gnd. 
+         * The propagation is repeated until no further gates can be substituted, but gates outside of `gates` are never substituted, even if they become constant in the process.
          * 
          * @param[in] nl - The netlist to operate on.
+         * @param[in] gates - The gates to consider. Defaults to an empty vector, in which case all gates of the netlist are considered.
          * @return OK() and the number rerouted destinations on success, an error otherwise.
          */
-        Result<u32> propagate_constants(Netlist* nl);
+        Result<u32> propagate_constants(Netlist* nl, const std::vector<Gate*>& gates = {});
 
         /**
          * Removes two consecutive inverters and reconnects the input of the first inverter to the output of the second one.
          * If the first inverter has additional successors, only the second inverter is deleted.
+         * Both inverters must be contained in `gates` for the pair to be considered, even if only the second one ends up being deleted.
          * 
          * @param[in] nl - The netlist to operate on.
+         * @param[in] gates - The gates to consider. Defaults to an empty vector, in which case all gates of the netlist are considered.
          * @returns OK() and the number of removed inverter gates on success, an error otherwise.
          */
-        Result<u32> remove_consecutive_inverters(Netlist* nl);
+        Result<u32> remove_consecutive_inverters(Netlist* nl, const std::vector<Gate*>& gates = {});
 
         /**
          * Replaces pins connected to GND/VCC with constants and simplifies the Boolean function of a LUT by recomputing the INIT string.
          * 
          * @param[in] nl - The netlist to operate on. 
+         * @param[in] gates - The gates to consider. Defaults to an empty vector, in which case all gates of the netlist are considered.
          * @return OK() and the number of simplified INIT strings on success, an error otherwise.
          */
-        Result<u32> simplify_lut_inits(Netlist* nl);
+        Result<u32> simplify_lut_inits(Netlist* nl, const std::vector<Gate*>& gates = {});
 
         /**
          * Tries to reconstruct a name and index for each flip flop that was part of a multi-bit wire in the verilog code.
@@ -202,14 +213,16 @@ namespace hal
          * The new nets are named `HAL_UNCONNECTED_<net_id>`.
          *
          * @param[in] nl - The netlist to operate on.
+         * @param[in] gates - The gates to consider. Defaults to an empty vector, in which case all gates of the netlist are considered.
          * @returns OK() and the created nets on success, an error otherwise.
          */
-        Result<std::vector<Net*>> create_nets_at_unconnected_pins(Netlist* nl);
+        Result<std::vector<Net*>> create_nets_at_unconnected_pins(Netlist* nl, const std::vector<Gate*>& gates = {});
 
         /**
          * Iterates all flip-flops of the netlist or specified by the user.
          * If a flip-flop has a `state` and a `neg_state` output, a new inverter gate is created and connected to the `state` output net as an additional destination.
          * Finally, the `neg_state` output net is disconnected from the `neg_state` pin and re-connected to the new inverter gate's output. 
+         * The new inverter gate is assigned to the module of the respective flip-flop.
          * 
          * @param[in] nl - The netlist to operate on.
          * @param[in] ffs - The flip-flops to operate on. Defaults to an empty vector, in which case all flip-flops of the netlist are considered.

plugins/netlist_preprocessing/include/netlist_preprocessing/plugin_netlist_preprocessing.h

@@ -30,23 +30,26 @@
 
 #pragma once
 
+#include "hal_core/plugin_system/gui_extension_interface.h"
 #include "hal_core/plugin_system/plugin_interface_base.h"
 
 namespace hal
 {
+    class Netlist;
+
     /**
      * @class NetlistPreprocessingPlugin
      * @brief Plugin interface for netlist preprocessing.
-     * 
+     *
      * This class provides an interface to integrate the netlist preprocessing as a plugin within the HAL framework.
      */
     class PLUGIN_API NetlistPreprocessingPlugin : public BasePluginInterface
     {
     public:
-        /** 
-         * @brief Default constructor for `NetlistPreprocessingPlugin`.
+        /**
+         * @brief Constructor for `NetlistPreprocessingPlugin` that registers the GUI extension.
          */
-        NetlistPreprocessingPlugin() = default;
+        NetlistPreprocessingPlugin();
 
         /** 
          * @brief Default destructor for `NetlistPreprocessingPlugin`.
@@ -81,4 +84,48 @@ namespace hal
          */
         std::set<std::string> get_dependencies() const override;
     };
+
+    /**
+     * @class GuiExtensionNetlistPreprocessing
+     * @brief GUI extension interface for the netlist preprocessing plugin.
+     *
+     * Contributes the most commonly used preprocessing steps to the context menus of the GUI, so that they can be
+     * applied to the current selection or to the entire netlist without writing a script.
+     */
+    class PLUGIN_API GuiExtensionNetlistPreprocessing : public GuiExtensionInterface
+    {
+    public:
+        /**
+         * @brief Default constructor for `GuiExtensionNetlistPreprocessing`.
+         */
+        GuiExtensionNetlistPreprocessing() : GuiExtensionInterface("Netlist Preprocessing")
+        {
+        }
+
+        /**
+         * @brief Get the context menu entries contributed for the given selection.
+         *
+         * If modules or gates are selected, only the entries operating on that selection are contributed. The entries
+         * operating on the entire netlist are contributed when nothing is selected.
+         *
+         * @param[in] nl - The netlist that is currently open.
+         * @param[in] mods - The IDs of the currently selected modules.
+         * @param[in] gats - The IDs of the currently selected gates.
+         * @param[in] nets - The IDs of the currently selected nets.
+         * @returns The contributed context menu entries.
+         */
+        std::vector<ContextMenuContribution> get_context_contribution(const Netlist* nl, const std::vector<u32>& mods, const std::vector<u32>& gats, const std::vector<u32>& nets) override;
+
+        /**
+         * @brief Execute the context menu entry identified by the given tag.
+         *
+         * @param[in] tag - The tag of the entry to execute.
+         * @param[in] nl - The netlist that is currently open.
+         * @param[in] mods - The IDs of the currently selected modules.
+         * @param[in] gats - The IDs of the currently selected gates.
+         * @param[in] nets - The IDs of the currently selected nets.
+         */
+        void execute_function(std::string tag, Netlist* nl, const std::vector<u32>& mods, const std::vector<u32>& gats, const std::vector<u32>& nets) override;
+    };
+
 }    // namespace hal