diff --git a/CHANGELOG.md b/CHANGELOG.md index 0ce0af35cfa7..bb4a51e5740b 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/examples/.gitignore b/examples/.gitignore index 98f3c62e1c8a..37dc9c6d9ce9 100644 --- a/examples/.gitignore +++ b/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 \ No newline at end of file +!toy_cipher.zip diff --git a/examples/fsm.zip b/examples/fsm.zip index dc30d92f9222..5f2de0fb6e15 100644 Binary files a/examples/fsm.zip and b/examples/fsm.zip differ diff --git a/examples/simple_alu.zip b/examples/simple_alu.zip index 04ab4316e81e..16d3002785a8 100644 Binary files a/examples/simple_alu.zip and b/examples/simple_alu.zip differ diff --git a/plugins/dot_viewer/deps/QGVCore/QGVNode.cpp b/plugins/dot_viewer/deps/QGVCore/QGVNode.cpp index 78c8132eb57e..689bf1e43cad 100644 --- a/plugins/dot_viewer/deps/QGVCore/QGVNode.cpp +++ b/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); diff --git a/plugins/dot_viewer/deps/QGVCore/QGVNode.h b/plugins/dot_viewer/deps/QGVCore/QGVNode.h index 0496bfca02dd..4b37415acbe2 100644 --- a/plugins/dot_viewer/deps/QGVCore/QGVNode.h +++ b/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; diff --git a/plugins/gui/src/selection_relay/selection_relay.cpp b/plugins/gui/src/selection_relay/selection_relay.cpp index 4072b908856f..4d47fe6315dc 100644 --- a/plugins/gui/src/selection_relay/selection_relay.cpp +++ b/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(); } } diff --git a/plugins/netlist_preprocessing/include/netlist_preprocessing/netlist_preprocessing.h b/plugins/netlist_preprocessing/include/netlist_preprocessing/netlist_preprocessing.h index d02da34bdabc..90c5f1a3e069 100644 --- a/plugins/netlist_preprocessing/include/netlist_preprocessing/netlist_preprocessing.h +++ b/plugins/netlist_preprocessing/include/netlist_preprocessing/netlist_preprocessing.h @@ -49,9 +49,10 @@ 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 remove_unused_lut_inputs(Netlist* nl); + Result remove_unused_lut_inputs(Netlist* nl, const std::vector& gates = {}); /** * Removes buffer gates from the netlist and connect their fan-in to their fan-out nets. @@ -59,18 +60,21 @@ namespace hal * 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 remove_buffers(Netlist* nl); + Result remove_buffers(Netlist* nl, const std::vector& 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 remove_redundant_gates(Netlist* nl, const std::function& filter = nullptr); + Result remove_redundant_gates(Netlist* nl, const std::function& filter = nullptr, const std::vector& 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 remove_unconnected_gates(Netlist* nl); + Result remove_unconnected_gates(Netlist* nl, const std::vector& 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 propagate_constants(Netlist* nl); + Result propagate_constants(Netlist* nl, const std::vector& 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 remove_consecutive_inverters(Netlist* nl); + Result remove_consecutive_inverters(Netlist* nl, const std::vector& 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 simplify_lut_inits(Netlist* nl); + Result simplify_lut_inits(Netlist* nl, const std::vector& 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_`. * * @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> create_nets_at_unconnected_pins(Netlist* nl); + Result> create_nets_at_unconnected_pins(Netlist* nl, const std::vector& 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. diff --git a/plugins/netlist_preprocessing/include/netlist_preprocessing/plugin_netlist_preprocessing.h b/plugins/netlist_preprocessing/include/netlist_preprocessing/plugin_netlist_preprocessing.h index e6159ba97266..af0aa0f7ca81 100644 --- a/plugins/netlist_preprocessing/include/netlist_preprocessing/plugin_netlist_preprocessing.h +++ b/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 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 get_context_contribution(const Netlist* nl, const std::vector& mods, const std::vector& gats, const std::vector& 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& mods, const std::vector& gats, const std::vector& nets) override; + }; + } // namespace hal diff --git a/plugins/netlist_preprocessing/include/netlist_preprocessing/utils/gui_layout_locker.h b/plugins/netlist_preprocessing/include/netlist_preprocessing/utils/gui_layout_locker.h new file mode 100644 index 000000000000..253e7db580fc --- /dev/null +++ b/plugins/netlist_preprocessing/include/netlist_preprocessing/utils/gui_layout_locker.h @@ -0,0 +1,72 @@ +// MIT License +// +// Copyright (c) 2019 Ruhr University Bochum, Chair for Embedded Security. All Rights reserved. +// Copyright (c) 2019 Marc Fyrbiak, Sebastian Wallat, Max Hoffmann ("ORIGINAL AUTHORS"). All rights reserved. +// Copyright (c) 2021 Max Planck Institute for Security and Privacy. All Rights reserved. +// Copyright (c) 2021 Jörn Langheinrich, Julian Speith, Nils Albartus, René Walendy, Simon Klix ("ORIGINAL AUTHORS"). All Rights reserved. +// +// Permission is hereby granted, free of charge, to any person obtaining a copy +// of this software and associated documentation files (the "Software"), to deal +// in the Software without restriction, including without limitation the rights +// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +// copies of the Software, and to permit persons to whom the Software is +// furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all +// copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +// SOFTWARE. + +/** + * @file gui_layout_locker.h + * @brief This file contains a helper that suppresses layout updates of the GUI. + */ + +#pragma once + +#include "hal_core/defines.h" + +namespace hal +{ + class UIPluginInterface; + + namespace netlist_preprocessing + { + /** + * @class GuiLayoutLocker + * @brief Suppresses layout updates of the GUI for as long as the object exists. + * + * A netlist modification that touches many gates makes the GUI re-layout its graph views once per change, + * which can dominate the runtime of the modification itself. Holding a locker defers those updates until it + * goes out of scope, at which point every affected view is updated once. + * + * Locks nest, so it is safe to hold more than one at a time. Does nothing if no GUI is running, which makes + * it safe to use from code that also runs headless. + */ + class GuiLayoutLocker + { + public: + /** + * @brief Suppress layout updates of the GUI until the locker is destroyed. + */ + GuiLayoutLocker(); + + /** + * @brief Release the lock and let the GUI update the views that changed in the meantime. + */ + ~GuiLayoutLocker(); + + GuiLayoutLocker(const GuiLayoutLocker&) = delete; + GuiLayoutLocker& operator=(const GuiLayoutLocker&) = delete; + + private: + UIPluginInterface* m_gui_plugin; + }; + } // namespace netlist_preprocessing +} // namespace hal diff --git a/plugins/netlist_preprocessing/python/python_bindings.cpp b/plugins/netlist_preprocessing/python/python_bindings.cpp index 4bd80e35d22d..f38d02bddc16 100644 --- a/plugins/netlist_preprocessing/python/python_bindings.cpp +++ b/plugins/netlist_preprocessing/python/python_bindings.cpp @@ -80,8 +80,8 @@ namespace hal m.def( "remove_unused_lut_inputs", - [](Netlist* nl) -> std::optional { - auto res = netlist_preprocessing::remove_unused_lut_inputs(nl); + [](Netlist* nl, const std::vector& gates) -> std::optional { + auto res = netlist_preprocessing::remove_unused_lut_inputs(nl, gates); if (res.is_ok()) { return res.get(); @@ -93,18 +93,20 @@ namespace hal } }, py::arg("nl"), + py::arg("gates") = std::vector(), R"( 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 hal_py.Netlist nl: The netlist to operate on. + :param list[hal_py.Gate] gates: The gates to consider. Defaults to an empty list, in which case all gates of the netlist are considered. :returns: The number of removed LUT endpoints on success, ``None`` otherwise. :rtype: int or ``None`` )"); m.def( "remove_buffers", - [](Netlist* nl) -> std::optional { - auto res = netlist_preprocessing::remove_buffers(nl); + [](Netlist* nl, const std::vector& gates) -> std::optional { + auto res = netlist_preprocessing::remove_buffers(nl, gates); if (res.is_ok()) { return res.get(); @@ -116,20 +118,22 @@ namespace hal } }, py::arg("nl"), + py::arg("gates") = std::vector(), R"( 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 hal_py.Netlist nl: The netlist to operate on. + :param list[hal_py.Gate] gates: The gates to consider. Defaults to an empty list, in which case all gates of the netlist are considered. :returns: The number of removed buffers on success, ``None`` otherwise. :rtype: int or ``None`` )"); m.def( "remove_redundant_gates", - [](Netlist* nl, const std::function& filter = nullptr) -> std::optional { - auto res = netlist_preprocessing::remove_redundant_gates(nl, filter); + [](Netlist* nl, const std::function& filter = nullptr, const std::vector& gates = {}) -> std::optional { + auto res = netlist_preprocessing::remove_redundant_gates(nl, filter, gates); if (res.is_ok()) { return res.get(); @@ -142,11 +146,14 @@ namespace hal }, py::arg("nl"), py::arg("filter") = nullptr, + py::arg("gates") = std::vector(), R"( 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 hal_py.Netlist nl: The netlist to operate on. :param lambda filter: Optional filter to fine-tune which gates are being replaced. Default to a ``None``. + :param list[hal_py.Gate] gates: The gates to consider. Defaults to an empty list, in which case all gates of the netlist are considered. :returns: The number of removed gates on success, ``None`` otherwise. :rtype: int or ``None`` )"); @@ -204,8 +211,8 @@ namespace hal m.def( "remove_unconnected_gates", - [](Netlist* nl) -> std::optional { - auto res = netlist_preprocessing::remove_unconnected_gates(nl); + [](Netlist* nl, const std::vector& gates) -> std::optional { + auto res = netlist_preprocessing::remove_unconnected_gates(nl, gates); if (res.is_ok()) { return res.get(); @@ -217,10 +224,13 @@ namespace hal } }, py::arg("nl"), + py::arg("gates") = std::vector(), R"( 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 hal_py.Netlist nl: The netlist to operate on. + :param list[hal_py.Gate] gates: The gates to consider. Defaults to an empty list, in which case all gates of the netlist are considered. :returns: The number of removed gates on success, ``None`` otherwise. :rtype: int or ``None`` )"); @@ -302,8 +312,8 @@ namespace hal m.def( "propagate_constants", - [](Netlist* nl) -> std::optional { - auto res = netlist_preprocessing::propagate_constants(nl); + [](Netlist* nl, const std::vector& gates) -> std::optional { + auto res = netlist_preprocessing::propagate_constants(nl, gates); if (res.is_ok()) { return res.get(); @@ -315,19 +325,22 @@ namespace hal } }, py::arg("nl"), + py::arg("gates") = std::vector(), R"( 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 static 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 hal_py.Netlist nl: The netlist to operate on. + :param list[hal_py.Gate] gates: The gates to consider. Defaults to an empty list, in which case all gates of the netlist are considered. :returns: The number of rerouted nets on success, ``None`` otherwise. :rtype: int or ``None`` )"); m.def( "remove_consecutive_inverters", - [](Netlist* nl) -> std::optional { - auto res = netlist_preprocessing::remove_consecutive_inverters(nl); + [](Netlist* nl, const std::vector& gates) -> std::optional { + auto res = netlist_preprocessing::remove_consecutive_inverters(nl, gates); if (res.is_ok()) { return res.get(); @@ -339,19 +352,22 @@ namespace hal } }, py::arg("nl"), + py::arg("gates") = std::vector(), R"( 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 hal_py.Netlist nl: The netlist to operate on. + :param list[hal_py.Gate] gates: The gates to consider. Defaults to an empty list, in which case all gates of the netlist are considered. :returns: The number of removed inverter gates on success, ``None`` otherwise. :rtype: int or ``None`` )"); m.def( "simplify_lut_inits", - [](Netlist* nl) -> std::optional { - auto res = netlist_preprocessing::simplify_lut_inits(nl); + [](Netlist* nl, const std::vector& gates) -> std::optional { + auto res = netlist_preprocessing::simplify_lut_inits(nl, gates); if (res.is_ok()) { return res.get(); @@ -363,10 +379,12 @@ namespace hal } }, py::arg("nl"), + py::arg("gates") = std::vector(), R"( Replaces pins connected to GND/VCC with constants and simplifies the boolean function of a LUT by recomputing the INIT string. :param hal_py.Netlist nl: The netlist to operate on. + :param list[hal_py.Gate] gates: The gates to consider. Defaults to an empty list, in which case all gates of the netlist are considered. :returns: The number of simplified INIT strings on success, ``None`` otherwise. :rtype: int or ``None`` )"); @@ -474,8 +492,8 @@ namespace hal m.def( "create_nets_at_unconnected_pins", - [](Netlist* nl) -> std::vector { - auto res = netlist_preprocessing::create_nets_at_unconnected_pins(nl); + [](Netlist* nl, const std::vector& gates) -> std::vector { + auto res = netlist_preprocessing::create_nets_at_unconnected_pins(nl, gates); if (res.is_ok()) { return res.get(); @@ -487,12 +505,14 @@ namespace hal } }, py::arg("nl"), + py::arg("gates") = std::vector(), borrowed(), R"( Create a new net for every unconnected output pin of every gate of the netlist. The new nets are named ``HAL_UNCONNECTED_``. :param hal_py.Netlist nl: The netlist to operate on. + :param list[hal_py.Gate] gates: The gates to consider. Defaults to an empty list, in which case all gates of the netlist are considered. :returns: The created nets on success, an empty list otherwise. :rtype: list[hal_py.Net] )"); @@ -517,7 +537,8 @@ namespace hal R"( 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. + 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 hal_py.Netlist nl: The netlist to operate on. :param list[hal_py.Gate] ffs: The flip-flops to operate on. Defaults to an empty vector, in which case all flip-flops of the netlist are considered. diff --git a/plugins/netlist_preprocessing/src/netlist_preprocessing.cpp b/plugins/netlist_preprocessing/src/netlist_preprocessing.cpp index 8e1c45f2a4b0..7cfb51b11f0e 100644 --- a/plugins/netlist_preprocessing/src/netlist_preprocessing.cpp +++ b/plugins/netlist_preprocessing/src/netlist_preprocessing.cpp @@ -16,6 +16,7 @@ #include "resynthesis/resynthesis.h" #include "z3_utils/netlist_comparison.h" +#include #include #include #include @@ -24,7 +25,61 @@ namespace hal { namespace netlist_preprocessing { - Result remove_unused_lut_inputs(Netlist* nl) + namespace + { + /** + * The set of gates a preprocessing function is allowed to modify or delete. An empty gate vector means the + * entire netlist, which is what all of these functions default to. + */ + struct GateScope + { + GateScope(const std::vector& gates) : m_all(gates.empty()) + { + // duplicates are dropped, but the caller's order is preserved so that results stay reproducible + for (auto* g : gates) + { + if (m_lookup.insert(g).second) + { + m_gates.push_back(g); + } + } + } + + bool contains(const Gate* g) const + { + return m_all || m_lookup.find(g) != m_lookup.end(); + } + + /** + * All gates within the scope that also pass the caller's type filter. The scope only ever restricts + * which gates are considered, it never widens what a function operates on. + */ + std::vector gates(const Netlist* nl, const std::function& type_filter = nullptr) const + { + if (m_all) + { + return type_filter ? nl->get_gates(type_filter) : nl->get_gates(); + } + + std::vector res; + for (auto* g : m_gates) + { + if (!type_filter || type_filter(g)) + { + res.push_back(g); + } + } + return res; + } + + private: + bool m_all; + std::vector m_gates; + std::unordered_set m_lookup; + }; + } // namespace + + Result remove_unused_lut_inputs(Netlist* nl, const std::vector& gates) { u32 num_eps = 0; @@ -36,8 +91,10 @@ namespace hal } Net* gnd_net = gnd_gates.front()->get_fan_out_nets().front(); + const GateScope scope(gates); + // iterate all LUT gates - for (const auto& gate : nl->get_gates([](const Gate* g) { return g->get_type()->has_property(GateTypeProperty::c_lut); })) + for (const auto& gate : scope.gates(nl, [](const Gate* g) { return g->get_type()->has_property(GateTypeProperty::c_lut); })) { std::vector fan_in = gate->get_fan_in_endpoints(); std::unordered_map functions = gate->get_boolean_functions(); @@ -91,13 +148,15 @@ namespace hal // TODO make this check every pin of a gate and check whether the generated boolean function (with replaced gnd and vcc nets) is just a variable. // Afterwards just connect input net to buffer destination. Do this for all pins and delete gate if it has no more successors and not global outputs - Result remove_buffers(Netlist* nl) + Result remove_buffers(Netlist* nl, const std::vector& gates) { u32 num_gates = 0; std::queue gates_to_be_deleted; - for (const auto& gate : nl->get_gates()) + const GateScope scope(gates); + + for (const auto& gate : scope.gates(nl)) { std::vector fan_out = gate->get_fan_out_endpoints(); @@ -376,8 +435,12 @@ namespace hal } } // namespace - Result remove_redundant_gates(Netlist* nl, const std::function& filter) + Result remove_redundant_gates(Netlist* nl, const std::function& filter, const std::vector& gates) { + // NOTE: the scope restricts which gates may be deleted, not which gates are compared. The gate that is + // kept in place of a duplicate is allowed to lie outside of it, so the candidate pool below stays global. + const GateScope scope(gates); + auto config = hal::SMT::QueryConfig(); #ifdef BITWUZLA_LIBRARY @@ -482,6 +545,12 @@ namespace hal continue; } + // no gate of this group may be deleted, so skip the equivalence checks altogether + if (std::none_of(gates.begin(), gates.end(), [&scope](const Gate* g) { return scope.contains(g); })) + { + continue; + } + if (fingerprint.type->has_property(GateTypeProperty::combinational)) { std::set visited; @@ -542,6 +611,10 @@ namespace hal { std::sort(current_duplicates.begin(), current_duplicates.end(), [](const auto& g1, const auto& g2) { return g1->get_name().length() < g2->get_name().length(); }); + // a gate outside of the scope must never be deleted, so move such gates to the front to make one + // of them the survivor. Without a scope this is a no-op and the shortest name survives as before. + std::stable_partition(current_duplicates.begin(), current_duplicates.end(), [&scope](const Gate* g) { return !scope.contains(g); }); + auto* survivor_gate = current_duplicates.front(); std::map out_pins_to_nets; for (auto* ep : survivor_gate->get_fan_out_endpoints()) @@ -562,6 +635,13 @@ namespace hal for (u32 k = 1; k < current_duplicates.size(); k++) { auto* current_gate = current_duplicates.at(k); + + // a group can hold more than one gate outside of the scope, none of which may be deleted + if (!scope.contains(current_gate)) + { + continue; + } + for (auto* ep : current_gate->get_fan_out_endpoints()) { auto* ep_net = ep->get_net(); @@ -1030,15 +1110,20 @@ namespace hal return OK(clean_up_res.get() + counter); } - Result remove_unconnected_gates(Netlist* nl) + Result remove_unconnected_gates(Netlist* nl, const std::vector& gates) { u32 num_gates = 0; + const GateScope scope(gates); + + // gates outside of the scope are never deleted, so the candidates can only shrink from here on + std::vector candidates = scope.gates(nl); + std::vector to_delete; do { to_delete.clear(); - for (const auto& g : nl->get_gates()) + for (const auto& g : candidates) { bool is_unconnected = true; for (const auto& on : g->get_fan_out_nets()) @@ -1066,6 +1151,14 @@ namespace hal num_gates++; } } + + // drop every gate that was handled so that the next round neither dereferences a deleted gate nor + // retries one that could not be deleted + if (!to_delete.empty()) + { + const std::unordered_set handled(to_delete.begin(), to_delete.end()); + candidates.erase(std::remove_if(candidates.begin(), candidates.end(), [&handled](Gate* g) { return handled.find(g) != handled.end(); }), candidates.end()); + } } while (!to_delete.empty()); log_info("netlist_preprocessing", "removed {} unconnected gates from netlist with ID {}.", num_gates, nl->get_id()); @@ -1643,13 +1736,15 @@ namespace hal return OK(res_count); } - Result propagate_constants(Netlist* nl) + Result propagate_constants(Netlist* nl, const std::vector& gates) { if (nl == nullptr) { return ERR("netlist is a nullptr"); } + const GateScope scope(gates); + Net* gnd_net = nl->get_gnd_gates().empty() ? nullptr : nl->get_gnd_gates().front()->get_fan_out_nets().front(); Net* vcc_net = nl->get_vcc_gates().empty() ? nullptr : nl->get_vcc_gates().front()->get_fan_out_nets().front(); @@ -1659,8 +1754,10 @@ namespace hal { u32 replaced_dst_count = 0; std::vector to_delete; - for (const auto g : nl->get_gates([](const auto g) { - return g->get_type()->has_property(GateTypeProperty::combinational) && !g->get_type()->has_property(GateTypeProperty::ground) + // re-queried every round so that gates deleted in a previous round are never revisited, the scope + // keeps the propagation from cascading into gates the caller did not select + for (const auto g : nl->get_gates([&scope](const auto g) { + return scope.contains(g) && g->get_type()->has_property(GateTypeProperty::combinational) && !g->get_type()->has_property(GateTypeProperty::ground) && !g->get_type()->has_property(GateTypeProperty::power); })) { @@ -1755,15 +1852,17 @@ namespace hal return OK(total_replaced_dst_count); } - Result remove_consecutive_inverters(Netlist* nl) + Result remove_consecutive_inverters(Netlist* nl, const std::vector& gates) { if (nl == nullptr) { return ERR("netlist is a nullptr"); } + const GateScope scope(gates); + std::set gates_to_delete; - for (auto* inv_gate : nl->get_gates([](const Gate* g) { return g->get_type()->has_property(GateTypeProperty::c_inverter); })) + for (auto* inv_gate : scope.gates(nl, [](const Gate* g) { return g->get_type()->has_property(GateTypeProperty::c_inverter); })) { if (gates_to_delete.find(inv_gate) != gates_to_delete.end()) { @@ -1786,6 +1885,12 @@ namespace hal } auto* pred_gate = middle_net->get_sources().front()->get_gate(); + // both inverters of the pair have to be in scope, even if only the second one ends up being deleted + if (!scope.contains(pred_gate)) + { + continue; + } + if (pred_gate->get_type()->has_property(GateTypeProperty::c_inverter)) { const auto& fan_in = pred_gate->get_fan_in_endpoints(); @@ -1870,11 +1975,13 @@ namespace hal } } // namespace - Result simplify_lut_inits(Netlist* nl) + Result simplify_lut_inits(Netlist* nl, const std::vector& gates) { u32 num_inits = 0; - for (auto g : nl->get_gates([](const auto& g) { return g->get_type()->has_property(GateTypeProperty::c_lut); })) + const GateScope scope(gates); + + for (auto g : scope.gates(nl, [](const auto& g) { return g->get_type()->has_property(GateTypeProperty::c_lut); })) { auto res = g->get_init_data(); if (res.is_error()) @@ -1899,6 +2006,12 @@ namespace hal continue; } + // skip if the output pin is not connected, there is nothing to simplify then + if (g->get_fan_out_endpoints().empty()) + { + continue; + } + const auto out_ep = g->get_fan_out_endpoints().front(); // skip if the gate has more than one boolean function @@ -2467,11 +2580,13 @@ namespace hal return OK(all_modules); } - Result> create_nets_at_unconnected_pins(Netlist* nl) + Result> create_nets_at_unconnected_pins(Netlist* nl, const std::vector& gates) { std::vector created_nets; - for (const auto& g : nl->get_gates()) + const GateScope scope(gates); + + for (const auto& g : scope.gates(nl)) { for (const auto& p : g->get_type()->get_output_pins()) { @@ -2578,6 +2693,13 @@ namespace hal } auto* inv = nl->create_gate(inverter_type, ff->get_name() + "__NEG_STATE_INVERT__"); + + // keep the new inverter within the module of the flip-flop it belongs to instead of the top module + if (auto* mod = ff->get_module(); !mod->is_top_module()) + { + mod->assign_gate(inv); + } + state_net->add_destination(inv, inv_in_pin); neg_state_net->remove_source(neg_state_ep); neg_state_net->add_source(inv, inv_out_pin); diff --git a/plugins/netlist_preprocessing/src/plugin_netlist_preprocessing.cpp b/plugins/netlist_preprocessing/src/plugin_netlist_preprocessing.cpp index 2a1aa5e8caf7..ee2c0798a416 100644 --- a/plugins/netlist_preprocessing/src/plugin_netlist_preprocessing.cpp +++ b/plugins/netlist_preprocessing/src/plugin_netlist_preprocessing.cpp @@ -1,7 +1,20 @@ #include "netlist_preprocessing/plugin_netlist_preprocessing.h" +#include "hal_core/netlist/gate.h" +#include "hal_core/netlist/module.h" +#include "hal_core/netlist/netlist.h" +#include "netlist_preprocessing/utils/gui_layout_locker.h" +#include "netlist_preprocessing/netlist_preprocessing.h" + +#include + namespace hal { + NetlistPreprocessingPlugin::NetlistPreprocessingPlugin() + { + m_extensions.push_back(new GuiExtensionNetlistPreprocessing()); + } + extern std::unique_ptr create_plugin_instance() { return std::make_unique(); @@ -29,4 +42,117 @@ namespace hal retval.insert("z3_utils"); return retval; } + + namespace + { + /** + * The gates of the selected modules, including those of their submodules, together with the selected gates. + * Duplicates are dropped, which matters when a gate is selected both directly and through a parent module. + */ + std::vector gates_from_selection(Netlist* nl, const std::vector& mods, const std::vector& gats) + { + std::vector res; + std::unordered_set seen; + + const auto collect = [&res, &seen](Gate* g) { + if (g != nullptr && seen.insert(g).second) + { + res.push_back(g); + } + }; + + for (u32 id : gats) + { + collect(nl->get_gate_by_id(id)); + } + + for (u32 id : mods) + { + if (const Module* m = nl->get_module_by_id(id); m != nullptr) + { + for (Gate* g : m->get_gates(nullptr, true)) + { + collect(g); + } + } + } + + return res; + } + } // namespace + + std::vector GuiExtensionNetlistPreprocessing::get_context_contribution(const Netlist*, const std::vector& mods, const std::vector& gats, const std::vector&) + { + std::vector retval; + + const auto add = [this, &retval](const std::string& tag, const std::string& entry) { + ContextMenuContribution cmc; + cmc.mContributer = this; + cmc.mTagname = tag; + cmc.mEntry = entry; + retval.push_back(cmc); + }; + + // a selection is what the user is pointing at, so do not offer to run on the entire netlist next to it + if (!mods.empty() || !gats.empty()) + { + add("remove_buffers_selection", "Remove buffers from selection"); + add("unify_ff_outputs_selection", "Unify flip-flop outputs of selection"); + } + else + { + add("remove_buffers_netlist", "Remove buffers from netlist"); + add("unify_ff_outputs_netlist", "Unify flip-flop outputs of netlist"); + } + + return retval; + } + + void GuiExtensionNetlistPreprocessing::execute_function(std::string tag, Netlist* nl, const std::vector& mods, const std::vector& gats, const std::vector&) + { + if (nl == nullptr) + { + log_warning("netlist_preprocessing", "cannot run preprocessing: no netlist loaded."); + return; + } + + // deleting or replacing a gate makes the GUI re-layout its graph views, which would otherwise happen once + // per gate and dominate the runtime of the preprocessing itself + const netlist_preprocessing::GuiLayoutLocker layout_locker; + + // an empty scope makes the preprocessing functions consider the entire netlist + std::vector scope; + if (tag == "remove_buffers_selection" || tag == "unify_ff_outputs_selection") + { + scope = gates_from_selection(nl, mods, gats); + if (scope.empty()) + { + log_warning("netlist_preprocessing", "cannot run preprocessing on the selection: no gates selected."); + return; + } + } + + if (tag == "remove_buffers_selection" || tag == "remove_buffers_netlist") + { + if (const auto res = netlist_preprocessing::remove_buffers(nl, scope); res.is_error()) + { + log_error("netlist_preprocessing", "failed to remove buffers: {}", res.get_error().get()); + } + } + else if (tag == "unify_ff_outputs_selection" || tag == "unify_ff_outputs_netlist") + { + if (const auto res = netlist_preprocessing::unify_ff_outputs(nl, scope); res.is_error()) + { + log_error("netlist_preprocessing", "failed to unify flip-flop outputs: {}", res.get_error().get()); + } + else + { + log_info("netlist_preprocessing", "rerouted {} 'neg_state' outputs.", res.get()); + } + } + else + { + log_warning("netlist_preprocessing", "unknown context menu tag '{}'.", tag); + } + } } // namespace hal diff --git a/plugins/netlist_preprocessing/src/utils/gui_layout_locker.cpp b/plugins/netlist_preprocessing/src/utils/gui_layout_locker.cpp new file mode 100644 index 000000000000..f25ab7dd0182 --- /dev/null +++ b/plugins/netlist_preprocessing/src/utils/gui_layout_locker.cpp @@ -0,0 +1,51 @@ +// MIT License +// +// Copyright (c) 2019 Ruhr University Bochum, Chair for Embedded Security. All Rights reserved. +// Copyright (c) 2019 Marc Fyrbiak, Sebastian Wallat, Max Hoffmann ("ORIGINAL AUTHORS"). All rights reserved. +// Copyright (c) 2021 Max Planck Institute for Security and Privacy. All Rights reserved. +// Copyright (c) 2021 Jörn Langheinrich, Julian Speith, Nils Albartus, René Walendy, Simon Klix ("ORIGINAL AUTHORS"). All Rights reserved. +// +// Permission is hereby granted, free of charge, to any person obtaining a copy +// of this software and associated documentation files (the "Software"), to deal +// in the Software without restriction, including without limitation the rights +// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +// copies of the Software, and to permit persons to whom the Software is +// furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all +// copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +// SOFTWARE. + +#include "netlist_preprocessing/utils/gui_layout_locker.h" + +#include "hal_core/plugin_system/plugin_interface_ui.h" +#include "hal_core/plugin_system/plugin_manager.h" + +namespace hal +{ + namespace netlist_preprocessing + { + GuiLayoutLocker::GuiLayoutLocker() : m_gui_plugin(plugin_manager::get_plugin_instance("hal_gui")) + { + if (m_gui_plugin != nullptr) + { + m_gui_plugin->set_layout_locker(true); + } + } + + GuiLayoutLocker::~GuiLayoutLocker() + { + if (m_gui_plugin != nullptr) + { + m_gui_plugin->set_layout_locker(false); + } + } + } // namespace netlist_preprocessing +} // namespace hal diff --git a/plugins/netlist_preprocessing/test/netlist_preprocessing.cpp b/plugins/netlist_preprocessing/test/netlist_preprocessing.cpp index b5dc2c50e09a..6c31ab265102 100644 --- a/plugins/netlist_preprocessing/test/netlist_preprocessing.cpp +++ b/plugins/netlist_preprocessing/test/netlist_preprocessing.cpp @@ -1,5 +1,7 @@ #include "netlist_preprocessing/netlist_preprocessing.h" +#include "netlist_preprocessing/plugin_netlist_preprocessing.h" + #include "netlist_test_utils.h" #include "gate_library_test_utils.h" @@ -309,6 +311,686 @@ namespace hal { TEST_END } + /** + * Test that the gate scope restricts which buffers are removed. + * + * Functions: remove_buffers + */ + TEST_F(NetlistPreprocessingTest, check_remove_buffers_scoped) + { + TEST_START + { + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + const GateLibrary* gl = nl->get_gate_library(); + ASSERT_NE(gl, nullptr); + + Gate* g0 = nl->create_gate(gl->get_gate_type_by_name("AND2"), "g0"); + Gate* b1 = nl->create_gate(gl->get_gate_type_by_name("BUF"), "b1"); + Gate* b2 = nl->create_gate(gl->get_gate_type_by_name("BUF"), "b2"); + Gate* g3 = nl->create_gate(gl->get_gate_type_by_name("AND2"), "g3"); + + Net* n0 = nl->create_net("n0"); + n0->add_destination(g0, "I0"); + n0->mark_global_input_net(); + + Net* n1 = nl->create_net("n1"); + n1->add_destination(g0, "I1"); + n1->mark_global_input_net(); + + Net* n2 = nl->create_net("n2"); + n2->add_destination(g3, "I1"); + n2->mark_global_input_net(); + + test_utils::connect(nl.get(), g0, "O", b1, "I"); + test_utils::connect(nl.get(), b1, "O", b2, "I"); + test_utils::connect(nl.get(), b2, "O", g3, "I0"); + + // only the buffer within the scope is removed, the second one is left untouched + auto res = netlist_preprocessing::remove_buffers(nl.get(), {b1}); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 1); + + ASSERT_EQ(nl->get_gates().size(), 3); + ASSERT_NE(nl->get_gate_by_id(b2->get_id()), nullptr); + ASSERT_NE(g0->get_successor("O"), nullptr); + EXPECT_EQ(g0->get_successor("O")->get_gate(), b2); + + // without a scope the remaining buffer is removed as well + res = netlist_preprocessing::remove_buffers(nl.get()); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 1); + + ASSERT_EQ(nl->get_gates().size(), 2); + ASSERT_NE(g0->get_successor("O"), nullptr); + EXPECT_EQ(g0->get_successor("O")->get_gate(), g3); + } + TEST_END + } + + /** + * Test that the gate scope restricts which LUT fan-in endpoints are removed. + * + * Functions: remove_unused_lut_inputs + */ + TEST_F(NetlistPreprocessingTest, check_remove_unused_lut_inputs_scoped) + { + TEST_START + { + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + const GateLibrary* gl = nl->get_gate_library(); + ASSERT_NE(gl, nullptr); + + Gate* gnd_gate = nl->create_gate(gl->get_gate_type_by_name("GND"), "gnd"); + nl->mark_gnd_gate(gnd_gate); + Net* gnd_net = nl->create_net("gnd"); + gnd_net->add_source(gnd_gate, "O"); + + GateType* lut4 = gl->get_gate_type_by_name("LUT4"); + + Gate* l0 = nl->create_gate(lut4, "l0"); + Gate* l1 = nl->create_gate(lut4, "l1"); + Gate* l2 = nl->create_gate(lut4, "l2"); + Gate* l3 = nl->create_gate(lut4, "l3"); + Gate* l4 = nl->create_gate(lut4, "l4"); + Gate* l5 = nl->create_gate(lut4, "l5"); + l4->add_boolean_function("O", BooleanFunction::Var("I2")); + l5->add_boolean_function("O", BooleanFunction::Var("I2")); + + for (Gate* dst : {l4, l5}) + { + test_utils::connect(nl.get(), l0, "O", dst, "I0"); + test_utils::connect(nl.get(), l1, "O", dst, "I1"); + test_utils::connect(nl.get(), l2, "O", dst, "I2"); + test_utils::connect(nl.get(), l3, "O", dst, "I3"); + } + + // both LUTs ignore three of their inputs, but only the one within the scope is cleaned up + auto res = netlist_preprocessing::remove_unused_lut_inputs(nl.get(), {l5}); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 3); + + EXPECT_EQ(l4->get_predecessor("I0")->get_gate(), l0); + EXPECT_EQ(l4->get_predecessor("I1")->get_gate(), l1); + EXPECT_EQ(l4->get_predecessor("I2")->get_gate(), l2); + EXPECT_EQ(l4->get_predecessor("I3")->get_gate(), l3); + + EXPECT_EQ(l5->get_predecessor("I0")->get_gate(), gnd_gate); + EXPECT_EQ(l5->get_predecessor("I1")->get_gate(), gnd_gate); + EXPECT_EQ(l5->get_predecessor("I2")->get_gate(), l2); + EXPECT_EQ(l5->get_predecessor("I3")->get_gate(), gnd_gate); + } + { + // a scope that contains no LUT at all leaves the netlist alone + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + const GateLibrary* gl = nl->get_gate_library(); + ASSERT_NE(gl, nullptr); + + Gate* gnd_gate = nl->create_gate(gl->get_gate_type_by_name("GND"), "gnd"); + nl->mark_gnd_gate(gnd_gate); + Net* gnd_net = nl->create_net("gnd"); + gnd_net->add_source(gnd_gate, "O"); + + GateType* lut4 = gl->get_gate_type_by_name("LUT4"); + Gate* l0 = nl->create_gate(lut4, "l0"); + Gate* l1 = nl->create_gate(lut4, "l1"); + l1->add_boolean_function("O", BooleanFunction::Var("I2")); + test_utils::connect(nl.get(), l0, "O", l1, "I0"); + + auto res = netlist_preprocessing::remove_unused_lut_inputs(nl.get(), {gnd_gate}); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 0); + EXPECT_EQ(l1->get_predecessor("I0")->get_gate(), l0); + } + TEST_END + } + + /** + * Test that the gate scope restricts which redundant gates are removed, that the gate kept in their stead may lie + * outside of the scope, and that the scope is not the same as the filter. + * + * Functions: remove_redundant_gates + */ + TEST_F(NetlistPreprocessingTest, check_remove_redundant_gates_scoped) + { + // builds two functionally equivalent AND2 gates 'g0' and 'g1' driving an XOR2 gate + auto build = [](Netlist* nl) -> std::vector { + const GateLibrary* gl = nl->get_gate_library(); + + Gate* g0 = nl->create_gate(gl->get_gate_type_by_name("AND2"), "g0"); + Gate* g1 = nl->create_gate(gl->get_gate_type_by_name("AND2"), "g1"); + Gate* x = nl->create_gate(gl->get_gate_type_by_name("XOR2"), "x"); + + Net* n0 = nl->create_net("n0"); + n0->add_destination(g0, "I0"); + n0->add_destination(g1, "I0"); + n0->mark_global_input_net(); + + Net* n1 = nl->create_net("n1"); + n1->add_destination(g0, "I1"); + n1->add_destination(g1, "I1"); + n1->mark_global_input_net(); + + test_utils::connect(nl, g0, "O", x, "I0"); + test_utils::connect(nl, g1, "O", x, "I1"); + + return {g0, g1, x}; + }; + + TEST_START + { + // the gate inside the scope is deleted, the equivalent gate outside of it survives + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + auto gates = build(nl.get()); + Gate *g0 = gates[0], *g1 = gates[1]; + + auto res = netlist_preprocessing::remove_redundant_gates(nl.get(), nullptr, {g1}); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 1); + + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_name() == "g0"; }).size(), 1); + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_name() == "g1"; }).size(), 0); + } + { + // the survivor is determined by the scope, not by the gate name + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + auto gates = build(nl.get()); + Gate* g0 = gates[0]; + + auto res = netlist_preprocessing::remove_redundant_gates(nl.get(), nullptr, {g0}); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 1); + + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_name() == "g0"; }).size(), 0); + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_name() == "g1"; }).size(), 1); + } + { + // the filter and the scope are not interchangeable: the filter also hides a gate from being used as the + // survivor, so restricting it to a single gate leaves that gate without an equivalent partner + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + auto gates = build(nl.get()); + Gate* g1 = gates[1]; + + auto res = netlist_preprocessing::remove_redundant_gates(nl.get(), [g1](const Gate* g) { return g == g1; }); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 0); + + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_name() == "g0"; }).size(), 1); + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_name() == "g1"; }).size(), 1); + } + { + // a scope holding both gates behaves like an unscoped call + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + auto gates = build(nl.get()); + Gate *g0 = gates[0], *g1 = gates[1]; + + auto res = netlist_preprocessing::remove_redundant_gates(nl.get(), nullptr, {g0, g1}); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 1); + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "AND2"; }).size(), 1); + } + TEST_END + } + + /** + * Test that the removal of unconnected gates does not cascade beyond the gate scope. + * + * Functions: remove_unconnected_gates + */ + TEST_F(NetlistPreprocessingTest, check_remove_unconnected_gates_scoped) + { + // builds a chain 'g0' -> 'g1' -> 'g2' whose last gate has no fan-out at all + auto build = [](Netlist* nl) -> std::vector { + const GateLibrary* gl = nl->get_gate_library(); + + Gate* g0 = nl->create_gate(gl->get_gate_type_by_name("AND2"), "g0"); + Gate* g1 = nl->create_gate(gl->get_gate_type_by_name("AND2"), "g1"); + Gate* g2 = nl->create_gate(gl->get_gate_type_by_name("AND2"), "g2"); + + for (const auto& [gate, pin] : std::vector>{{g0, "I0"}, {g0, "I1"}, {g1, "I1"}, {g2, "I1"}}) + { + Net* n = nl->create_net("in_" + gate->get_name() + "_" + pin); + n->add_destination(gate, pin); + n->mark_global_input_net(); + } + + test_utils::connect(nl, g0, "O", g1, "I0"); + test_utils::connect(nl, g1, "O", g2, "I0"); + + return {g0, g1, g2}; + }; + + TEST_START + { + // without a scope the whole chain collapses + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + build(nl.get()); + + auto res = netlist_preprocessing::remove_unconnected_gates(nl.get()); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 3); + EXPECT_TRUE(nl->get_gates().empty()); + } + { + // the cascade stops at the scope boundary, so 'g0' survives even though it is unconnected afterwards + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + auto gates = build(nl.get()); + Gate *g1 = gates[1], *g2 = gates[2]; + + auto res = netlist_preprocessing::remove_unconnected_gates(nl.get(), {g1, g2}); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 2); + + ASSERT_EQ(nl->get_gates().size(), 1); + EXPECT_EQ(nl->get_gates().front()->get_name(), "g0"); + } + TEST_END + } + + /** + * Test that constant propagation does not cascade beyond the gate scope. + * + * Functions: propagate_constants + */ + TEST_F(NetlistPreprocessingTest, check_propagate_constants_scoped) + { + TEST_START + { + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + const GateLibrary* gl = nl->get_gate_library(); + ASSERT_NE(gl, nullptr); + + Gate* gnd_gate = nl->create_gate(gl->get_gate_type_by_name("GND"), "gnd"); + nl->mark_gnd_gate(gnd_gate); + Net* gnd_net = nl->create_net("gnd"); + gnd_net->add_source(gnd_gate, "O"); + Gate* vcc_gate = nl->create_gate(gl->get_gate_type_by_name("VCC"), "vcc"); + nl->mark_vcc_gate(vcc_gate); + Net* vcc_net = nl->create_net("vcc"); + vcc_net->add_source(vcc_gate, "O"); + + // both AND2 gates have one input tied to GND, so both outputs are constant 0 + Gate* g0 = nl->create_gate(gl->get_gate_type_by_name("AND2"), "g0"); + Gate* g1 = nl->create_gate(gl->get_gate_type_by_name("AND2"), "g1"); + Gate* x = nl->create_gate(gl->get_gate_type_by_name("XOR2"), "x"); + + gnd_net->add_destination(g0, "I0"); + gnd_net->add_destination(g1, "I0"); + + Net* n0 = nl->create_net("n0"); + n0->add_destination(g0, "I1"); + n0->mark_global_input_net(); + + Net* n1 = nl->create_net("n1"); + n1->add_destination(g1, "I1"); + n1->mark_global_input_net(); + + test_utils::connect(nl.get(), g0, "O", x, "I0"); + test_utils::connect(nl.get(), g1, "O", x, "I1"); + + auto res = netlist_preprocessing::propagate_constants(nl.get(), {g0}); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 1); + + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_name() == "g0"; }).size(), 0); + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_name() == "g1"; }).size(), 1); + ASSERT_NE(x->get_predecessor("I0"), nullptr); + EXPECT_EQ(x->get_predecessor("I0")->get_gate(), gnd_gate); + } + TEST_END + } + + /** + * Test that both inverters of a pair have to be inside the gate scope for the pair to be removed. + * + * Functions: remove_consecutive_inverters + */ + TEST_F(NetlistPreprocessingTest, check_remove_consecutive_inverters_scoped) + { + // builds 'i0' -> 'i1' followed by an AND2 gate consuming the result + auto build = [](Netlist* nl) -> std::vector { + const GateLibrary* gl = nl->get_gate_library(); + + Gate* i0 = nl->create_gate(gl->get_gate_type_by_name("INV"), "i0"); + Gate* i1 = nl->create_gate(gl->get_gate_type_by_name("INV"), "i1"); + Gate* g = nl->create_gate(gl->get_gate_type_by_name("AND2"), "g"); + + Net* n0 = nl->create_net("n0"); + n0->add_destination(i0, "I"); + n0->mark_global_input_net(); + + Net* n1 = nl->create_net("n1"); + n1->add_destination(g, "I1"); + n1->mark_global_input_net(); + + test_utils::connect(nl, i0, "O", i1, "I"); + test_utils::connect(nl, i1, "O", g, "I0"); + + return {i0, i1, g}; + }; + + TEST_START + { + // only the second inverter is in scope, so the pair is left alone + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + auto gates = build(nl.get()); + Gate* i1 = gates[1]; + + auto res = netlist_preprocessing::remove_consecutive_inverters(nl.get(), {i1}); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 0); + EXPECT_EQ(nl->get_gates().size(), 3); + } + { + // with both inverters in scope the pair is removed and the AND2 gate is fed directly + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + auto gates = build(nl.get()); + Gate *i0 = gates[0], *i1 = gates[1], *g = gates[2]; + + auto res = netlist_preprocessing::remove_consecutive_inverters(nl.get(), {i0, i1}); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 2); + + ASSERT_EQ(nl->get_gates().size(), 1); + ASSERT_NE(g->get_fan_in_net("I0"), nullptr); + EXPECT_TRUE(g->get_fan_in_net("I0")->is_global_input_net()); + } + TEST_END + } + + /** + * Test that the gate scope restricts which LUT INIT strings are simplified. + * + * Functions: simplify_lut_inits + */ + TEST_F(NetlistPreprocessingTest, check_simplify_lut_inits_scoped) + { + TEST_START + { + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + const GateLibrary* gl = nl->get_gate_library(); + ASSERT_NE(gl, nullptr); + + Gate* gnd_gate = nl->create_gate(gl->get_gate_type_by_name("GND"), "gnd"); + nl->mark_gnd_gate(gnd_gate); + Net* gnd_net = nl->create_net("gnd"); + gnd_net->add_source(gnd_gate, "O"); + + GateType* lut2 = gl->get_gate_type_by_name("LUT2"); + + // both LUTs compute 'I0 & I1' with 'I0' tied to GND, so both are constant 0 + Gate* l0 = nl->create_gate(lut2, "l0"); + Gate* l1 = nl->create_gate(lut2, "l1"); + ASSERT_TRUE(l0->set_init_data({"8"}).is_ok()); + ASSERT_TRUE(l1->set_init_data({"8"}).is_ok()); + + gnd_net->add_destination(l0, "I0"); + gnd_net->add_destination(l1, "I0"); + + Net* n0 = nl->create_net("n0"); + n0->add_destination(l0, "I1"); + n0->add_destination(l1, "I1"); + n0->mark_global_input_net(); + + Gate* x = nl->create_gate(gl->get_gate_type_by_name("XOR2"), "x"); + test_utils::connect(nl.get(), l0, "O", x, "I0"); + test_utils::connect(nl.get(), l1, "O", x, "I1"); + + auto res = netlist_preprocessing::simplify_lut_inits(nl.get(), {l0}); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 1); + + auto l0_init = l0->get_init_data(); + ASSERT_TRUE(l0_init.is_ok()); + EXPECT_NE(l0_init.get().front(), "8"); + + auto l1_init = l1->get_init_data(); + ASSERT_TRUE(l1_init.is_ok()); + EXPECT_EQ(l1_init.get().front(), "8"); + } + { + // a LUT whose output pin is unconnected is skipped instead of crashing + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + const GateLibrary* gl = nl->get_gate_library(); + ASSERT_NE(gl, nullptr); + + Gate* gnd_gate = nl->create_gate(gl->get_gate_type_by_name("GND"), "gnd"); + nl->mark_gnd_gate(gnd_gate); + Net* gnd_net = nl->create_net("gnd"); + gnd_net->add_source(gnd_gate, "O"); + + Gate* l0 = nl->create_gate(gl->get_gate_type_by_name("LUT2"), "l0"); + ASSERT_TRUE(l0->set_init_data({"8"}).is_ok()); + gnd_net->add_destination(l0, "I0"); + + Net* n0 = nl->create_net("n0"); + n0->add_destination(l0, "I1"); + n0->mark_global_input_net(); + + auto res = netlist_preprocessing::simplify_lut_inits(nl.get()); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 0); + + auto l0_init = l0->get_init_data(); + ASSERT_TRUE(l0_init.is_ok()); + EXPECT_EQ(l0_init.get().front(), "8"); + } + TEST_END + } + + /** + * Test that the gate scope restricts which gates get nets created at their unconnected output pins. + * + * Functions: create_nets_at_unconnected_pins + */ + TEST_F(NetlistPreprocessingTest, check_create_nets_at_unconnected_pins_scoped) + { + TEST_START + { + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + const GateLibrary* gl = nl->get_gate_library(); + ASSERT_NE(gl, nullptr); + + Gate* g0 = nl->create_gate(gl->get_gate_type_by_name("AND2"), "g0"); + Gate* g1 = nl->create_gate(gl->get_gate_type_by_name("AND2"), "g1"); + + auto res = netlist_preprocessing::create_nets_at_unconnected_pins(nl.get(), {g0}); + ASSERT_TRUE(res.is_ok()); + ASSERT_EQ(res.get().size(), 1); + + EXPECT_NE(g0->get_fan_out_net("O"), nullptr); + EXPECT_EQ(g1->get_fan_out_net("O"), nullptr); + + // without a scope the remaining pin is covered as well + res = netlist_preprocessing::create_nets_at_unconnected_pins(nl.get()); + ASSERT_TRUE(res.is_ok()); + ASSERT_EQ(res.get().size(), 1); + EXPECT_NE(g1->get_fan_out_net("O"), nullptr); + } + TEST_END + } + + /** + * Test that the inverter created for a 'neg_state' output is assigned to the module of its flip-flop. + * + * Functions: unify_ff_outputs + */ + TEST_F(NetlistPreprocessingTest, check_unify_ff_outputs_module_assignment) + { + TEST_START + { + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + const GateLibrary* gl = nl->get_gate_library(); + ASSERT_NE(gl, nullptr); + + Gate* ff = nl->create_gate(gl->get_gate_type_by_name("DFF"), "ff"); + Gate* g = nl->create_gate(gl->get_gate_type_by_name("XOR2"), "g"); + + Net* clk = nl->create_net("clk"); + clk->add_destination(ff, "CLK"); + clk->mark_global_input_net(); + + Net* d = nl->create_net("d"); + d->add_destination(ff, "D"); + d->mark_global_input_net(); + + test_utils::connect(nl.get(), ff, "Q", g, "I0"); + test_utils::connect(nl.get(), ff, "QN", g, "I1"); + + Module* mod = nl->create_module("mod", nl->get_top_module(), {ff}); + ASSERT_NE(mod, nullptr); + + auto res = netlist_preprocessing::unify_ff_outputs(nl.get(), {ff}); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 1); + + auto inverters = nl->get_gates([](const Gate* g) { return g->get_type()->has_property(GateTypeProperty::c_inverter); }); + ASSERT_EQ(inverters.size(), 1); + + // the new inverter belongs to the flip-flop it was created for, not to the top module + EXPECT_EQ(inverters.front()->get_module(), mod); + } + TEST_END + } + + /** + * Test the context menu entries contributed to the GUI. + * + * Functions: GuiExtensionNetlistPreprocessing::get_context_contribution, GuiExtensionNetlistPreprocessing::execute_function + */ + TEST_F(NetlistPreprocessingTest, check_gui_extension) + { + TEST_START + { + NetlistPreprocessingPlugin plugin; + + GuiExtensionNetlistPreprocessing* gui = nullptr; + for (auto* ext : plugin.get_extensions()) + { + if (auto* casted = dynamic_cast(ext); casted != nullptr) + { + gui = casted; + } + } + ASSERT_NE(gui, nullptr); + + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + const GateLibrary* gl = nl->get_gate_library(); + ASSERT_NE(gl, nullptr); + + Gate* g0 = nl->create_gate(gl->get_gate_type_by_name("AND2"), "g0"); + Gate* b1 = nl->create_gate(gl->get_gate_type_by_name("BUF"), "b1"); + Gate* b2 = nl->create_gate(gl->get_gate_type_by_name("BUF"), "b2"); + Gate* g3 = nl->create_gate(gl->get_gate_type_by_name("AND2"), "g3"); + + Net* n0 = nl->create_net("n0"); + n0->add_destination(g0, "I0"); + n0->mark_global_input_net(); + + Net* n1 = nl->create_net("n1"); + n1->add_destination(g0, "I1"); + n1->mark_global_input_net(); + + Net* n2 = nl->create_net("n2"); + n2->add_destination(g3, "I1"); + n2->mark_global_input_net(); + + test_utils::connect(nl.get(), g0, "O", b1, "I"); + test_utils::connect(nl.get(), b1, "O", b2, "I"); + test_utils::connect(nl.get(), b2, "O", g3, "I0"); + + // without a selection the netlist-wide entries are offered + auto without_selection = gui->get_context_contribution(nl.get(), {}, {}, {}); + ASSERT_EQ(without_selection.size(), 2); + for (const auto& cmc : without_selection) + { + EXPECT_EQ(cmc.mContributer, gui); + EXPECT_FALSE(cmc.mEntry.empty()); + EXPECT_NE(cmc.mTagname.find("_netlist"), std::string::npos); + } + + // with a selection only the entries operating on it are offered + auto with_selection = gui->get_context_contribution(nl.get(), {}, {b1->get_id()}, {}); + ASSERT_EQ(with_selection.size(), 2); + for (const auto& cmc : with_selection) + { + EXPECT_EQ(cmc.mContributer, gui); + EXPECT_FALSE(cmc.mEntry.empty()); + EXPECT_NE(cmc.mTagname.find("_selection"), std::string::npos); + } + + // running the entry on the selected gate removes only that buffer + gui->execute_function("remove_buffers_selection", nl.get(), {}, {b1->get_id()}, {}); + EXPECT_EQ(nl->get_gates().size(), 3); + ASSERT_NE(g0->get_successor("O"), nullptr); + EXPECT_EQ(g0->get_successor("O")->get_gate(), b2); + + // the netlist-wide entry then removes the remaining one + gui->execute_function("remove_buffers_netlist", nl.get(), {}, {}, {}); + EXPECT_EQ(nl->get_gates().size(), 2); + ASSERT_NE(g0->get_successor("O"), nullptr); + EXPECT_EQ(g0->get_successor("O")->get_gate(), g3); + } + { + // a module selection is expanded into the gates it contains + NetlistPreprocessingPlugin plugin; + auto* gui = dynamic_cast(plugin.get_extensions().front()); + ASSERT_NE(gui, nullptr); + + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + const GateLibrary* gl = nl->get_gate_library(); + ASSERT_NE(gl, nullptr); + + Gate* g0 = nl->create_gate(gl->get_gate_type_by_name("AND2"), "g0"); + Gate* b1 = nl->create_gate(gl->get_gate_type_by_name("BUF"), "b1"); + Gate* b2 = nl->create_gate(gl->get_gate_type_by_name("BUF"), "b2"); + Gate* g3 = nl->create_gate(gl->get_gate_type_by_name("AND2"), "g3"); + + Net* n0 = nl->create_net("n0"); + n0->add_destination(g0, "I0"); + n0->mark_global_input_net(); + + Net* n1 = nl->create_net("n1"); + n1->add_destination(g0, "I1"); + n1->mark_global_input_net(); + + Net* n2 = nl->create_net("n2"); + n2->add_destination(g3, "I1"); + n2->mark_global_input_net(); + + test_utils::connect(nl.get(), g0, "O", b1, "I"); + test_utils::connect(nl.get(), b1, "O", b2, "I"); + test_utils::connect(nl.get(), b2, "O", g3, "I0"); + + // only the first buffer lives inside the module + Module* mod = nl->create_module("mod", nl->get_top_module(), {b1}); + ASSERT_NE(mod, nullptr); + + gui->execute_function("remove_buffers_selection", nl.get(), {mod->get_id()}, {}, {}); + EXPECT_EQ(nl->get_gates().size(), 3); + ASSERT_NE(g0->get_successor("O"), nullptr); + EXPECT_EQ(g0->get_successor("O")->get_gate(), b2); + } + TEST_END + } + /** * Test that two flip-flops which differ only in the value they start out at are not treated as * duplicates of one another. diff --git a/plugins/solve_fsm/CMakeLists.txt b/plugins/solve_fsm/CMakeLists.txt index 050922e10ee2..579a57bd9fd6 100644 --- a/plugins/solve_fsm/CMakeLists.txt +++ b/plugins/solve_fsm/CMakeLists.txt @@ -12,4 +12,6 @@ if(PL_SOLVE_FSM OR BUILD_ALL_PLUGINS) SOURCES ${SOLVE_FSM_SRC} ${SOLVE_FSM_PYTHON_SRC} PYDOC SPHINX_DOC_INDEX_FILE ${CMAKE_CURRENT_SOURCE_DIR}/documentation/solve_fsm.rst ) + + add_subdirectory(test) endif() diff --git a/plugins/solve_fsm/include/solve_fsm/configuration.h b/plugins/solve_fsm/include/solve_fsm/configuration.h new file mode 100644 index 000000000000..0da58749ba62 --- /dev/null +++ b/plugins/solve_fsm/include/solve_fsm/configuration.h @@ -0,0 +1,167 @@ +// MIT License +// +// Copyright (c) 2019 Ruhr University Bochum, Chair for Embedded Security. All Rights reserved. +// Copyright (c) 2019 Marc Fyrbiak, Sebastian Wallat, Max Hoffmann ("ORIGINAL AUTHORS"). All rights reserved. +// Copyright (c) 2021 Max Planck Institute for Security and Privacy. All Rights reserved. +// Copyright (c) 2021 Jörn Langheinrich, Julian Speith, Nils Albartus, René Walendy, Simon Klix ("ORIGINAL AUTHORS"). All Rights reserved. +// +// Permission is hereby granted, free of charge, to any person obtaining a copy +// of this software and associated documentation files (the "Software"), to deal +// in the Software without restriction, including without limitation the rights +// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +// copies of the Software, and to permit persons to whom the Software is +// furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all +// copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +// SOFTWARE. + +/** + * @file configuration.h + * @brief This file contains the struct that holds the configuration of a run of the FSM solver. + */ + +#pragma once + +#include "hal_core/defines.h" + +#include +#include +#include +#include + +namespace hal +{ + class Gate; + class Net; + class Netlist; + + namespace solve_fsm + { + /** + * @struct Configuration + * @brief The configuration of a run of the FSM solver. + * + * Holds everything the solver needs to know about the FSM, including the netlist that implements it. The state + * register and the transition logic are mandatory, everything else is optional. + * + * States are encoded as integers, with the first flip-flop of the state register providing the least + * significant bit. + */ + struct Configuration + { + /** + * @brief Construct a new FSM solver configuration for the given netlist. + * + * @param[in] nl - The netlist that implements the FSM. + */ + Configuration(Netlist* nl); + + /** + * @brief The netlist that implements the FSM. + */ + Netlist* netlist; + + /** + * @brief The flip-flops that make up the state register of the FSM. + * + * The first flip-flop provides the least significant bit of the state. Defaults to an empty vector, but a + * state register is required for the solver to run. + */ + std::vector state_register = {}; + + /** + * @brief The combinational gates that compute the next state of the FSM. + * + * Defaults to an empty vector, but transition logic is required for the solver to run. + */ + std::vector transition_logic = {}; + + /** + * @brief The outputs of the FSM, each given as a name and the nets that make up that output. + * + * The first net of an output provides its least significant bit, so a single-bit output is a vector + * holding one net. Defaults to an empty vector, in which case no outputs are computed. + */ + std::vector>> outputs = {}; + + /** + * @brief The initial value of each flip-flop of the state register. + * + * Only states reachable from the resulting initial state are explored. Defaults to an empty map, in which + * case the FSM starts in state 0. + */ + std::map initial_state = {}; + + /** + * @brief The timeout for the underlying SMT solver in milliseconds. Defaults to 600000 ms. + * + * Has no effect when `brute_force` is set, as no SMT solver is used then. + */ + u32 timeout = 600000; + + /** + * @brief Enumerate all states instead of using an SMT solver. Defaults to `false`. + * + * Brute forcing needs no external solver and is faster for small state registers, but its runtime doubles + * with every additional flip-flop. Both approaches produce the same state transition graph. + */ + bool brute_force = false; + + /** + * @brief Set the flip-flops that make up the state register of the FSM. + * + * @param[in] state_register - The flip-flops of the state register, least significant bit first. + * @returns The updated FSM solver configuration. + */ + Configuration& with_state_register(const std::vector& state_register); + + /** + * @brief Set the combinational gates that compute the next state of the FSM. + * + * @param[in] transition_logic - The gates of the transition logic. + * @returns The updated FSM solver configuration. + */ + Configuration& with_transition_logic(const std::vector& transition_logic); + + /** + * @brief Set the outputs of the FSM that the solver should evaluate in each state. + * + * @param[in] outputs - The outputs, each given as a name and the nets that make up that output, least significant bit first. + * @returns The updated FSM solver configuration. + */ + Configuration& with_outputs(const std::vector>>& outputs); + + /** + * @brief Set the initial value of each flip-flop of the state register. + * + * @param[in] initial_state - The initial value of each flip-flop of the state register. + * @returns The updated FSM solver configuration. + */ + Configuration& with_initial_state(const std::map& initial_state); + + /** + * @brief Set the timeout for the underlying SMT solver. + * + * @param[in] timeout - The timeout in milliseconds. + * @returns The updated FSM solver configuration. + */ + Configuration& with_timeout(const u32 timeout); + + /** + * @brief Set whether to enumerate all states instead of using an SMT solver. + * + * @param[in] brute_force - Set `true` to enumerate all states, `false` to use an SMT solver. Defaults to `true`. + * @returns The updated FSM solver configuration. + */ + Configuration& with_brute_force(const bool brute_force = true); + }; + } // namespace solve_fsm +} // namespace hal diff --git a/plugins/solve_fsm/include/solve_fsm/solve_fsm.h b/plugins/solve_fsm/include/solve_fsm/solve_fsm.h index ada58a2d85f8..be37ad9d232a 100644 --- a/plugins/solve_fsm/include/solve_fsm/solve_fsm.h +++ b/plugins/solve_fsm/include/solve_fsm/solve_fsm.h @@ -24,77 +24,35 @@ // SOFTWARE. /** - * @file solve_fsm.h - * @brief This file contains functions to generate the state transition graph of a given FSM. + * @file solve_fsm.h + * @brief This file contains the function to recover the state transition graph of a finite state machine. */ #pragma once -#include "hal_core/defines.h" -#include "hal_core/netlist/boolean_function.h" #include "hal_core/utilities/result.h" - -#include +#include "solve_fsm/configuration.h" +#include "solve_fsm/state_transition_graph.h" namespace hal { - class Netlist; - class Gate; - /** - * Recovers the state transition graph of a finite state machine from the gate-level netlist that implements it. + * @brief Recovers the state transition graph of a finite state machine from the gate-level netlist that implements it. */ namespace solve_fsm { /** - * Generate the state transition graph of a given FSM using SMT solving. - * The result is a map from each state of the FSM to all of its transitions. - * A transition is given as each successor state as well as the Boolean condition that needs to be fulfilled for the transition to take place. - * Optionally also produces a DOT file representing the state transition graph. - * - * @param[in] nl - The netlist to operate on. - * @param[in] state_reg - A vector of flip-flop gates that make up the state register of the FSM. - * @param[in] transition_logic - A vector of combinational gates that make up the transition logic of the FSM. - * @param[in] initial_state - A map from the state register flip-flops to their initial (Boolean) value. If an empty map is provided, the initial state is set to 0. Defaults to an empty map. - * @param[in] graph_path - File path at which to store the DOT state transition graph. No file is created if the path is left empty. Defaults to an empty path. - * @param[in] timeout - Timeout for the underlying SAT solvers. Defaults to 600000 ms. - * @returns OK() and a map from each state to its successor states as well as the condition for the respective transition to be taken, an error otherwise. - */ - Result>> solve_fsm(Netlist* nl, - const std::vector& state_reg, - const std::vector& transition_logic, - const std::map& initial_state = {}, - const std::filesystem::path& graph_path = "", - const u32 timeout = 600000); - - /** - * Generate the state transition graph of a given FSM using brute force. - * The result is a map from each state of the FSM to all of its transitions. - * A transition is given as each successor state as well as the Boolean condition that needs to be fulfilled for the transition to take place. - * Optionally also produces a DOT file representing the state transition graph. - * - * @param[in] nl - The netlist to operate on. - * @param[in] state_reg - A vector of flip-flop gates that make up the state register of the FSM. - * @param[in] transition_logic - A vector of combinational gates that make up the transition logic of the FSM. - * @param[in] graph_path - File path at which to store the DOT state transition graph. No file is created if the path is left empty. Defaults to an empty path. - */ - Result>> - solve_fsm_brute_force(Netlist* nl, const std::vector& state_reg, const std::vector& transition_logic, const std::filesystem::path& graph_path = ""); - - /** - * Generates the state graph of a finite state machine from the transitions of that fsm. + * @brief Recover the state transition graph of an FSM from the netlist that implements it. + * + * Explores the states that are reachable from the initial state and determines, for each of them, which + * successor states it can reach and under which condition. If outputs are configured, the value of each output + * in each state is computed as well. + * + * No file is written. Use `StateTransitionGraph::generate_dot_graph` on the result to render the graph. * - * @param[in] state_reg - Vector contianing the state registers. - * @param[in] transitions - Transitions of the fsm given as a map from origin state to all possible successor states and the corresponding condition. - * @param[in] graph_path - Path where the transition state graph in dot format is saved. - * @param[in] max_condition_length - The maximum character length that is printed for boolean functions representing the conditions. - * @param[in] base - The base with that the states are formatted and printed. - * @returns A string representing the dot graph. + * @param[in] config - The configuration of the FSM solver run. + * @returns OK() and the state transition graph of the FSM on success, an error otherwise. */ - Result generate_dot_graph(const std::vector& state_reg, - const std::map>& transitions, - const std::filesystem::path& graph_path = "", - const u32 max_condition_length = 128, - const u32 base = 10); + Result solve_fsm(const Configuration& config); } // namespace solve_fsm -} // namespace hal \ No newline at end of file +} // namespace hal diff --git a/plugins/solve_fsm/include/solve_fsm/state_transition_graph.h b/plugins/solve_fsm/include/solve_fsm/state_transition_graph.h new file mode 100644 index 000000000000..87a7653d5c6e --- /dev/null +++ b/plugins/solve_fsm/include/solve_fsm/state_transition_graph.h @@ -0,0 +1,139 @@ +// MIT License +// +// Copyright (c) 2019 Ruhr University Bochum, Chair for Embedded Security. All Rights reserved. +// Copyright (c) 2019 Marc Fyrbiak, Sebastian Wallat, Max Hoffmann ("ORIGINAL AUTHORS"). All rights reserved. +// Copyright (c) 2021 Max Planck Institute for Security and Privacy. All Rights reserved. +// Copyright (c) 2021 Jörn Langheinrich, Julian Speith, Nils Albartus, René Walendy, Simon Klix ("ORIGINAL AUTHORS"). All Rights reserved. +// +// Permission is hereby granted, free of charge, to any person obtaining a copy +// of this software and associated documentation files (the "Software"), to deal +// in the Software without restriction, including without limitation the rights +// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +// copies of the Software, and to permit persons to whom the Software is +// furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all +// copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +// SOFTWARE. + +/** + * @file state_transition_graph.h + * @brief This file contains the struct that holds the state transition graph of an FSM. + */ + +#pragma once + +#include "hal_core/defines.h" +#include "hal_core/netlist/boolean_function.h" +#include "hal_core/utilities/result.h" + +#include +#include +#include +#include +#include + +namespace hal +{ + class Gate; + class Net; + class Netlist; + + namespace solve_fsm + { + /** + * @struct StateTransitionGraph + * @brief The state transition graph of an FSM, i.e., the behavior that its netlist implements. + * + * States are encoded as integers, with the first flip-flop of the state register providing the least + * significant bit. The same holds for the nets of a multi-bit output. + */ + struct StateTransitionGraph + { + /** + * @brief The netlist that implements the FSM. + */ + Netlist* netlist = nullptr; + + /** + * @brief The flip-flops that make up the state register, in the order that determines the encoding of a state. + * + * The first flip-flop provides the least significant bit, so this is what maps a state back to the netlist. + */ + std::vector state_register; + + /** + * @brief The outputs of the FSM, each given as a name and the nets that make up that output. + * + * The first net of an output provides its least significant bit. Empty unless outputs were configured. + */ + std::vector>> output_nets; + + /** + * @brief A map from each state to its successor states, together with the condition under which the respective transition is taken. + */ + std::map> transitions; + + /** + * @brief A map from each state to the value of every output of the FSM in that state. + * + * The outputs of a state are given in the order in which they were configured. An output of a Moore FSM + * only depends on the state, so its Boolean function is constant. An output of a Mealy FSM may also depend + * on the inputs of the FSM, in which case its Boolean function still contains the input variables. + * + * Empty unless outputs were configured. + */ + std::map>> outputs; + + /** + * @brief Get the number of flip-flops that make up the state register, i.e., the bit-size of a state. + * + * @returns The bit-size of a state. + */ + u32 get_state_size() const; + + /** + * @brief Render the state transition graph in the DOT format. + * + * Each state becomes a node labeled with its value and, if outputs were computed, with the value of every + * output in that state. Each transition becomes an edge labeled with its condition. Boolean functions are + * truncated to keep the graph readable, use `to_string` to get them in full. + * + * @param[in] graph_path - The file path at which to store the graph. No file is written if the path is left empty. Defaults to an empty path. + * @param[in] max_condition_length - The maximum number of characters printed for a Boolean function. Defaults to 128. + * @param[in] base - The base in which state and output values are printed, either 2 or 10. Defaults to 10. + * @returns OK() and the graph in the DOT format on success, an error otherwise. + */ + Result generate_dot_graph(const std::filesystem::path& graph_path = "", const u32 max_condition_length = 128, const u32 base = 10) const; + + /** + * @brief Render the state transition graph as human-readable text, without truncating anything. + * + * Starts with a legend that maps each bit of the state to the flip-flop holding it, each output to the + * nets that make it up, and every net variable appearing in a Boolean function to the net it stands for. + * The legend is followed by one block per state holding its outputs and all of its outgoing transitions + * together with the full condition of each. + * + * @param[in] base - The base in which state and output values are printed, either 2 or 10. Defaults to 10. + * @returns OK() and the state transition graph as text on success, an error otherwise. + */ + Result to_string(const u32 base = 10) const; + + /** + * @brief Write the state transition graph to a text file, without truncating anything. + * + * @param[in] file_path - The file path at which to store the text representation. + * @param[in] base - The base in which state and output values are printed, either 2 or 10. Defaults to 10. + * @returns OK() on success, an error otherwise. + */ + Result write_txt(const std::filesystem::path& file_path, const u32 base = 10) const; + }; + } // namespace solve_fsm +} // namespace hal diff --git a/plugins/solve_fsm/python/python_bindings.cpp b/plugins/solve_fsm/python/python_bindings.cpp index 4fae40577673..29e2538179e6 100644 --- a/plugins/solve_fsm/python/python_bindings.cpp +++ b/plugins/solve_fsm/python/python_bindings.cpp @@ -68,11 +68,184 @@ namespace hal :rtype: str )"); - m.def( - "solve_fsm_brute_force", - [](Netlist* nl, const std::vector& state_reg, const std::vector& transition_logic, const std::string& graph_path = "") - -> std::optional>> { - auto res = solve_fsm::solve_fsm_brute_force(nl, state_reg, transition_logic, graph_path); + py::class_ py_solve_fsm_configuration(m, "Configuration", R"( + The configuration of a run of the FSM solver. + + Holds everything the solver needs to know about the FSM, including the netlist that implements it. + The state register and the transition logic are mandatory, everything else is optional. + + States are encoded as integers, with the first flip-flop of the state register providing the least significant bit. + )"); + + py_solve_fsm_configuration.def(py::init(), py::arg("nl"), R"( + Construct a new FSM solver configuration for the given netlist. + + :param hal_py.Netlist nl: The netlist that implements the FSM. + )"); + + py_solve_fsm_configuration.def_readwrite("netlist", &solve_fsm::Configuration::netlist, R"( + The netlist that implements the FSM. + + :type: hal_py.Netlist + )"); + + py_solve_fsm_configuration.def_readwrite("state_register", &solve_fsm::Configuration::state_register, borrowed(), R"( + The flip-flops that make up the state register of the FSM. + + The first flip-flop provides the least significant bit of the state. + Defaults to an empty list, but a state register is required for the solver to run. + + :type: list[hal_py.Gate] + )"); + + py_solve_fsm_configuration.def_readwrite("transition_logic", &solve_fsm::Configuration::transition_logic, borrowed(), R"( + The combinational gates that compute the next state of the FSM. + + Defaults to an empty list, but transition logic is required for the solver to run. + + :type: list[hal_py.Gate] + )"); + + py_solve_fsm_configuration.def_readwrite("outputs", &solve_fsm::Configuration::outputs, borrowed(), R"( + The outputs of the FSM, each given as a name and the nets that make up that output. + + The first net of an output provides its least significant bit, so a single-bit output is a list holding one net. + Defaults to an empty list, in which case no outputs are computed. + + :type: list[tuple(str,list[hal_py.Net])] + )"); + + py_solve_fsm_configuration.def_readwrite("initial_state", &solve_fsm::Configuration::initial_state, borrowed(), R"( + The initial value of each flip-flop of the state register. + + Only states reachable from the resulting initial state are explored. + Defaults to an empty dict, in which case the FSM starts in state 0. + + :type: dict[hal_py.Gate,bool] + )"); + + py_solve_fsm_configuration.def_readwrite("timeout", &solve_fsm::Configuration::timeout, R"( + The timeout for the underlying SMT solver in milliseconds. Defaults to 600000 ms. + + Has no effect when ``brute_force`` is set, as no SMT solver is used then. + + :type: int + )"); + + py_solve_fsm_configuration.def_readwrite("brute_force", &solve_fsm::Configuration::brute_force, R"( + Enumerate all states instead of using an SMT solver. Defaults to ``False``. + + Brute forcing needs no external solver and is faster for small state registers, but its runtime doubles with every additional flip-flop. + Both approaches produce the same state transition graph. + + :type: bool + )"); + + py_solve_fsm_configuration.def("with_state_register", &solve_fsm::Configuration::with_state_register, py::arg("state_register"), R"( + Set the flip-flops that make up the state register of the FSM. + + :param list[hal_py.Gate] state_register: The flip-flops of the state register, least significant bit first. + :returns: The updated FSM solver configuration. + :rtype: solve_fsm.Configuration + )"); + + py_solve_fsm_configuration.def("with_transition_logic", &solve_fsm::Configuration::with_transition_logic, py::arg("transition_logic"), R"( + Set the combinational gates that compute the next state of the FSM. + + :param list[hal_py.Gate] transition_logic: The gates of the transition logic. + :returns: The updated FSM solver configuration. + :rtype: solve_fsm.Configuration + )"); + + py_solve_fsm_configuration.def("with_outputs", &solve_fsm::Configuration::with_outputs, py::arg("outputs"), R"( + Set the outputs of the FSM that the solver should evaluate in each state. + + :param list[tuple(str,list[hal_py.Net])] outputs: The outputs, each given as a name and the nets that make up that output, least significant bit first. + :returns: The updated FSM solver configuration. + :rtype: solve_fsm.Configuration + )"); + + py_solve_fsm_configuration.def("with_initial_state", &solve_fsm::Configuration::with_initial_state, py::arg("initial_state"), R"( + Set the initial value of each flip-flop of the state register. + + :param dict[hal_py.Gate,bool] initial_state: The initial value of each flip-flop of the state register. + :returns: The updated FSM solver configuration. + :rtype: solve_fsm.Configuration + )"); + + py_solve_fsm_configuration.def("with_timeout", &solve_fsm::Configuration::with_timeout, py::arg("timeout"), R"( + Set the timeout for the underlying SMT solver. + + :param int timeout: The timeout in milliseconds. + :returns: The updated FSM solver configuration. + :rtype: solve_fsm.Configuration + )"); + + py_solve_fsm_configuration.def("with_brute_force", &solve_fsm::Configuration::with_brute_force, py::arg("brute_force") = true, R"( + Set whether to enumerate all states instead of using an SMT solver. + + :param bool brute_force: Set ``True`` to enumerate all states, ``False`` to use an SMT solver. Defaults to ``True``. + :returns: The updated FSM solver configuration. + :rtype: solve_fsm.Configuration + )"); + + py::class_ py_state_transition_graph(m, "StateTransitionGraph", R"( + The state transition graph of an FSM, i.e., the behavior that its netlist implements. + + States are encoded as integers, with the first flip-flop of the state register providing the least significant bit. + )"); + + py_state_transition_graph.def_readonly("transitions", &solve_fsm::StateTransitionGraph::transitions, R"( + A dict from each state to its successor states, together with the condition under which the respective transition is taken. + + :type: dict[int,dict[int,hal_py.BooleanFunction]] + )"); + + py_state_transition_graph.def_readonly("outputs", &solve_fsm::StateTransitionGraph::outputs, R"( + A dict from each state to the value of every output of the FSM in that state. + + The outputs of a state are given in the order in which they were configured. + An output of a Moore FSM only depends on the state, so its Boolean function is constant. + An output of a Mealy FSM may also depend on the inputs of the FSM, in which case its Boolean function still contains the input variables. + + Empty unless outputs were configured. + + :type: dict[int,list[tuple(str,hal_py.BooleanFunction)]] + )"); + + py_state_transition_graph.def_readonly("netlist", &solve_fsm::StateTransitionGraph::netlist, R"( + The netlist that implements the FSM. + + :type: hal_py.Netlist + )"); + + py_state_transition_graph.def_readonly("state_register", &solve_fsm::StateTransitionGraph::state_register, borrowed(), R"( + The flip-flops that make up the state register, in the order that determines the encoding of a state. + + The first flip-flop provides the least significant bit, so this is what maps a state back to the netlist. + + :type: list[hal_py.Gate] + )"); + + py_state_transition_graph.def_readonly("output_nets", &solve_fsm::StateTransitionGraph::output_nets, borrowed(), R"( + The outputs of the FSM, each given as a name and the nets that make up that output. + + The first net of an output provides its least significant bit. Empty unless outputs were configured. + + :type: list[tuple(str,list[hal_py.Net])] + )"); + + py_state_transition_graph.def("get_state_size", &solve_fsm::StateTransitionGraph::get_state_size, R"( + Get the number of flip-flops that make up the state register, i.e., the bit-size of a state. + + :returns: The bit-size of a state. + :rtype: int + )"); + + py_state_transition_graph.def( + "generate_dot_graph", + [](const solve_fsm::StateTransitionGraph& self, const std::filesystem::path& graph_path, const u32 max_condition_length, const u32 base) -> std::optional { + auto res = self.generate_dot_graph(graph_path, max_condition_length, base); if (res.is_ok()) { return res.get(); @@ -83,33 +256,27 @@ namespace hal return std::nullopt; } }, - py::arg("nl"), - py::arg("state_reg"), - py::arg("transition_logic"), - py::arg("graph_path") = std::string(""), + py::arg("graph_path") = "", + py::arg("max_condition_length") = 128, + py::arg("base") = 10, R"( - Generate the state transition graph of a given FSM using brute force. - The result is a map from each state of the FSM to all of its transitions. - A transition is given as each successor state as well as the Boolean condition that needs to be fulfilled for the transition to take place. - Optionally also produces a DOT file representing the state transition graph. - - :param hal_py.Netlist nl: The netlist to operate on. - :param list[hal_py.Gate] state_reg: A list of flip-flop gates that make up the state register of the FSM. - :param list[hal_py.Gate] transition_logic: A list of combinational gates that make up the transition logic of the FSM. - :param pathlib.Path graph_path: File path at which to store the DOT state transition graph. No file is created if the path is left empty. Defaults to an empty path. - :returns: A dict from each state to its successor states as well as the condition for the respective transition to be taken on success, ``None`` otherwise. - :rtype: dict[int,dict[int,hal_py.BooleanFunction]] or None - )"); + Render the state transition graph in the DOT format. - m.def( - "solve_fsm", - [](Netlist* nl, - const std::vector& state_reg, - const std::vector& transition_logic, - const std::map& initial_state = {}, - const std::filesystem::path& graph_path = "", - const u32 timeout = 600000) -> std::optional>> { - auto res = solve_fsm::solve_fsm(nl, state_reg, transition_logic, initial_state, graph_path, timeout); + Each state becomes a node labeled with its value and, if outputs were computed, with the value of every output in that state. + Each transition becomes an edge labeled with its condition. + If the ``dot_viewer`` plugin is available, the written graph is additionally offered to it for display. + + :param pathlib.Path graph_path: The file path at which to store the graph. No file is written if the path is left empty. Defaults to an empty path. + :param int max_condition_length: The maximum number of characters printed for a Boolean function. Defaults to 128. + :param int base: The base in which state and output values are printed, either 2 or 10. Defaults to 10. + :returns: The graph in the DOT format on success, ``None`` otherwise. + :rtype: str or None + )"); + + py_state_transition_graph.def( + "to_string", + [](const solve_fsm::StateTransitionGraph& self, const u32 base) -> std::optional { + auto res = self.to_string(base); if (res.is_ok()) { return res.get(); @@ -120,36 +287,44 @@ namespace hal return std::nullopt; } }, - py::arg("nl"), - py::arg("state_reg"), - py::arg("transition_logic"), - py::arg("initial_state") = std::map(), - py::arg("graph_path") = "", - py::arg("timeout") = 600000, + py::arg("base") = 10, + R"( + Render the state transition graph as human-readable text, without truncating anything. + + Starts with a legend that maps each bit of the state to the flip-flop holding it, each output to the nets that make it up, and every net variable appearing in a Boolean function to the net it stands for. + The legend is followed by one block per state holding its outputs and all of its outgoing transitions together with the full condition of each. + + :param int base: The base in which state and output values are printed, either 2 or 10. Defaults to 10. + :returns: The state transition graph as text on success, ``None`` otherwise. + :rtype: str or None + )"); + + py_state_transition_graph.def( + "write_txt", + [](const solve_fsm::StateTransitionGraph& self, const std::filesystem::path& file_path, const u32 base) -> bool { + auto res = self.write_txt(file_path, base); + if (res.is_ok()) + { + return true; + } + log_error("python_context", "{}", res.get_error().get()); + return false; + }, + py::arg("file_path"), + py::arg("base") = 10, R"( - Generate the state transition graph of a given FSM using SMT solving. - The result is a map from each state of the FSM to all of its transitions. - A transition is given as each successor state as well as the Boolean condition that needs to be fulfilled for the transition to take place. - Optionally also produces a DOT file representing the state transition graph. - - :param hal_py.Netlist nl: The netlist to operate on. - :param list[hal_py.Gate] state_reg: A list of flip-flop gates that make up the state register of the FSM. - :param list[hal_py.Gate] transition_logic: A list of combinational gates that make up the transition logic of the FSM. - :param dict[hal_py.Gate,bool] initial_state: A dict from the state register flip-flops to their initial (Boolean) value. If an empty dict is provided, the initial state is set to 0. Defaults to an empty dict. - :param pathlib.Path graph_path: File path at which to store the DOT state transition graph. No file is created if the path is left empty. Defaults to an empty path. - :param int timeout: Timeout for the underlying SAT solvers. Defaults to 600000 ms. - :returns: A dict from each state to its successor states as well as the condition for the respective transition to be taken on success, ``None`` otherwise. - :rtype: dict[int,dict[int,hal_py.BooleanFunction]] or None - )"); + Write the state transition graph to a text file, without truncating anything. + + :param pathlib.Path file_path: The file path at which to store the text representation. + :param int base: The base in which state and output values are printed, either 2 or 10. Defaults to 10. + :returns: ``True`` on success, ``False`` otherwise. + :rtype: bool + )"); m.def( - "generate_dot_graph", - [](const std::vector& state_reg, - const std::map>& transitions, - const std::string& graph_path = "", - const u32 max_condition_length = 128, - const u32 base = 10) -> std::optional { - auto res = solve_fsm::generate_dot_graph(state_reg, transitions, graph_path, max_condition_length, base); + "solve_fsm", + [](const solve_fsm::Configuration& config) -> std::optional { + auto res = solve_fsm::solve_fsm(config); if (res.is_ok()) { return res.get(); @@ -160,23 +335,21 @@ namespace hal return std::nullopt; } }, - py::arg("state_reg"), - py::arg("transitions"), - py::arg("graph_path") = std::string(), - py::arg("max_condition_length") = 128, - py::arg("base") = 10, + py::arg("config"), R"( - Generates the state graph of a finite state machine from the transitions of that fsm. - - :param list[hal_py.Gate] state_reg: Vector contianing the state registers. - :param dict[int, dict[int, hal_py.BooleanFunction]] transitions: Transitions of the fsm given as a map from origin state to all possible successor states and the corresponding condition. - :param str graph_path: Path to the location where the state graph is saved in dot format. - :param int max_condition_length: The maximum character length that is printed for boolean functions representing the conditions. - :param int base: The base with that the states are formatted and printed. - :returns: A string representing the dot graph. - :rtype: str + Recover the state transition graph of an FSM from the netlist that implements it. + + Explores the states that are reachable from the initial state and determines, for each of them, which successor states it can reach and under which condition. + If outputs are configured, the value of each output in each state is computed as well. + + No file is written. Use ``StateTransitionGraph.generate_dot_graph`` on the result to render the graph. + + :param solve_fsm.Configuration config: The configuration of the FSM solver run. + :returns: The state transition graph of the FSM on success, ``None`` otherwise. + :rtype: solve_fsm.StateTransitionGraph or None )"); + #ifndef PYBIND11_MODULE return m.ptr(); #endif // PYBIND11_MODULE diff --git a/plugins/solve_fsm/src/configuration.cpp b/plugins/solve_fsm/src/configuration.cpp new file mode 100644 index 000000000000..78bf1da4bb24 --- /dev/null +++ b/plugins/solve_fsm/src/configuration.cpp @@ -0,0 +1,72 @@ +// MIT License +// +// Copyright (c) 2019 Ruhr University Bochum, Chair for Embedded Security. All Rights reserved. +// Copyright (c) 2019 Marc Fyrbiak, Sebastian Wallat, Max Hoffmann ("ORIGINAL AUTHORS"). All rights reserved. +// Copyright (c) 2021 Max Planck Institute for Security and Privacy. All Rights reserved. +// Copyright (c) 2021 Jörn Langheinrich, Julian Speith, Nils Albartus, René Walendy, Simon Klix ("ORIGINAL AUTHORS"). All Rights reserved. +// +// Permission is hereby granted, free of charge, to any person obtaining a copy +// of this software and associated documentation files (the "Software"), to deal +// in the Software without restriction, including without limitation the rights +// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +// copies of the Software, and to permit persons to whom the Software is +// furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all +// copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +// SOFTWARE. + +#include "solve_fsm/configuration.h" + +namespace hal +{ + namespace solve_fsm + { + Configuration::Configuration(Netlist* nl) : netlist(nl) + { + } + + Configuration& Configuration::with_state_register(const std::vector& state_register) + { + this->state_register = state_register; + return *this; + } + + Configuration& Configuration::with_transition_logic(const std::vector& transition_logic) + { + this->transition_logic = transition_logic; + return *this; + } + + Configuration& Configuration::with_outputs(const std::vector>>& outputs) + { + this->outputs = outputs; + return *this; + } + + Configuration& Configuration::with_initial_state(const std::map& initial_state) + { + this->initial_state = initial_state; + return *this; + } + + Configuration& Configuration::with_timeout(const u32 timeout) + { + this->timeout = timeout; + return *this; + } + + Configuration& Configuration::with_brute_force(const bool brute_force) + { + this->brute_force = brute_force; + return *this; + } + } // namespace solve_fsm +} // namespace hal diff --git a/plugins/solve_fsm/src/solve_fsm.cpp b/plugins/solve_fsm/src/solve_fsm.cpp index 250ed047e011..847546d0fcb2 100644 --- a/plugins/solve_fsm/src/solve_fsm.cpp +++ b/plugins/solve_fsm/src/solve_fsm.cpp @@ -1,5 +1,31 @@ +// MIT License +// +// Copyright (c) 2019 Ruhr University Bochum, Chair for Embedded Security. All Rights reserved. +// Copyright (c) 2019 Marc Fyrbiak, Sebastian Wallat, Max Hoffmann ("ORIGINAL AUTHORS"). All rights reserved. +// Copyright (c) 2021 Max Planck Institute for Security and Privacy. All Rights reserved. +// Copyright (c) 2021 Jörn Langheinrich, Julian Speith, Nils Albartus, René Walendy, Simon Klix ("ORIGINAL AUTHORS"). All Rights reserved. +// +// Permission is hereby granted, free of charge, to any person obtaining a copy +// of this software and associated documentation files (the "Software"), to deal +// in the Software without restriction, including without limitation the rights +// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +// copies of the Software, and to permit persons to whom the Software is +// furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all +// copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +// SOFTWARE. #include "solve_fsm/solve_fsm.h" +#include "hal_core/netlist/net.h" + #include "hal_core/netlist/boolean_function/solver.h" #include "hal_core/netlist/decorators/boolean_function_decorator.h" #include "hal_core/netlist/decorators/boolean_function_net_decorator.h" @@ -8,13 +34,12 @@ #include "hal_core/netlist/gate_library/gate_type.h" #include "hal_core/netlist/gate_library/gate_type_component/ff_component.h" #include "hal_core/netlist/gate_library/gate_type_component/state_component.h" -#include "hal_core/plugin_system/plugin_manager.h" -#include "hal_core/plugin_system/gui_extension_interface.h" #include "hal_core/netlist/net.h" #include #include #include +#include namespace hal { @@ -90,8 +115,6 @@ namespace hal + " of state register has an unhandeled type " + ff->get_type()->get_name()); } - std::cout << complete_bf << std::endl; - for (const auto& pin_var : complete_bf.get_variable_names()) { // The complete Boolean function of a flip flop will contain the internal state and negated internal state. @@ -158,8 +181,6 @@ namespace hal } } - std::cout << complete_bf << std::endl; - bf = complete_bf; } else @@ -232,6 +253,112 @@ namespace hal } // takes a map of unconditional transitions and reconstructs the conditions under which each condition is taken + /** + * Build one Boolean function per output of the FSM, concatenating the nets of a multi-bit output into a + * single function with the first net as the least significant bit, matching how the state is encoded. + */ + Result>> generate_output_bfs(Netlist* nl, const std::vector>>& outputs) + { + // the combinational gates of the netlist bound the subgraph, so expansion stops at the flip-flop + // output nets and at the inputs of the FSM, which is exactly where the output logic ends + const std::vector comb_gates = nl->get_gates([](const Gate* g) { return g->get_type()->has_property(GateTypeProperty::combinational); }); + const SubgraphNetlistDecorator dec(*nl); + + std::vector> res; + for (const auto& [name, nets] : outputs) + { + if (nets.empty()) + { + return ERR("failed to generate output functions: output '" + name + "' does not contain any nets."); + } + + BooleanFunction bf; + for (u32 i = 0; i < nets.size(); i++) + { + if (nets.at(i) == nullptr) + { + return ERR("failed to generate output functions: output '" + name + "' contains a nullptr net at index " + std::to_string(i) + "."); + } + + auto bit_res = dec.get_subgraph_function(comb_gates, nets.at(i)); + if (bit_res.is_error()) + { + return ERR_APPEND(bit_res.get_error(), "failed to generate output functions: could not generate function for net " + std::to_string(nets.at(i)->get_id()) + "."); + } + + if (i == 0) + { + bf = bit_res.get(); + continue; + } + + auto concat_res = BooleanFunction::Concat(bit_res.get(), std::move(bf), i + 1); + if (concat_res.is_error()) + { + return ERR_APPEND(concat_res.get_error(), "failed to generate output functions: could not concatenate the nets of output '" + name + "'."); + } + bf = concat_res.get(); + } + + res.push_back({name, std::move(bf)}); + } + + return OK(res); + } + + /** + * The substitution that pins the state register to the given state, so that a function reading the state + * can be reduced to what it computes while the FSM is in that state. + */ + std::map generate_state_substitution(const std::vector& state_reg, const u64 state) + { + std::map res; + + for (u32 i = 0; i < state_reg.size(); i++) + { + const bool bit = (state >> i) & 0x1; + const Gate* ff = state_reg.at(i); + const auto pins = ff->get_type()->get_pins([](const GatePin* p) { + return (p->get_direction() == PinDirection::output) && ((p->get_type() == PinType::state) || (p->get_type() == PinType::neg_state)); + }); + + for (const auto* pin : pins) + { + if (const Net* n = ff->get_fan_out_net(pin); n != nullptr) + { + const bool val = (pin->get_type() == PinType::neg_state) ? !bit : bit; + res.insert({BooleanFunctionNetDecorator(*n).get_boolean_variable_name(), BooleanFunction::Const(val ? 1 : 0, 1)}); + } + } + } + + return res; + } + + /** + * Reduce every output of the FSM to what it computes in the given state. Outputs of a Moore FSM become + * constants, outputs of a Mealy FSM keep the input variables they depend on. + */ + Result>> + evaluate_outputs_in_state(const std::vector>& output_bfs, const std::vector& state_reg, const u64 state) + { + const auto substitution = generate_state_substitution(state_reg, state); + + std::vector> res; + for (const auto& [name, bf] : output_bfs) + { + auto sub_res = bf.substitute(substitution); + if (sub_res.is_error()) + { + return ERR_APPEND(sub_res.get_error(), "failed to evaluate outputs: could not substitute the state register in output '" + name + "'."); + } + + res.push_back({name, sub_res.get().simplify()}); + } + + return OK(res); + } + Result>> generate_conditional_transitions(const std::vector>& state_bfs, const std::map>& transitions) { @@ -282,332 +409,324 @@ namespace hal } - void open_dot_in_viewer(const std::filesystem::path& out_path) - { - BasePluginInterface* bpif = plugin_manager::get_plugin_instance("dot_viewer"); - if (!bpif) - { - log_info("solve_fsm", "Cannot find 'dot_viewer' plugin, dot graph not displayed."); - return; - } - GuiExtensionInterface* geif = bpif->get_first_extension(); - if (!geif) - { - log_info("solve_fsm", "Cannot find dot_viewer GUI interface, dot graph not displayed."); - return; - } - std::vector params; - params.push_back(PluginParameter(PluginParameter::ExistingFile, "filename", "", out_path.string())); - params.push_back(PluginParameter(PluginParameter::String, "plugin", "", "solve_fsm")); - params.push_back(PluginParameter(PluginParameter::PushButton, "exec", "", "clicked")); - geif->set_parameter(params); - log_info("solve_fsm", "Request to display graph '{}' send to dot viewer.", out_path.string()); - } - - } // namespace - - Result>> - solve_fsm_brute_force(Netlist* nl, const std::vector& state_reg, const std::vector& transition_logic, const std::filesystem::path& graph_path) - { - const u32 state_size = state_reg.size(); - if (state_size > 64) - { - return ERR("failed to solve fsm: Currently only supports fsm with up to 64 state flip-flops but got " + std::to_string(state_size) + "."); - } - - // extract Boolean functions for each state flip-flop - const auto state_bfs_res = generate_state_bfs(nl, state_reg, transition_logic, true); - if (state_bfs_res.is_error()) - { - return ERR_APPEND(state_bfs_res.get_error(), "failed to solve fsm: unable to generate Boolean functions for state."); - } - const std::vector> state_bfs = state_bfs_res.get(); - - // bitvector including all the functions to calculate the next state - BooleanFunction next_state_vec = state_bfs.front().second; - for (u32 i = 1; i < state_reg.size(); i++) - { - next_state_vec = BooleanFunction::Concat(state_bfs.at(i).second.clone(), std::move(next_state_vec), next_state_vec.size() + 1).get(); - } - - std::map> all_transitions; - - for (u64 state = 0; state < (u64(1) << state_size); state++) + /** + * Determine the successors of every state by enumerating every state and every input combination. Needs no + * external solver, but the runtime doubles with every additional flip-flop of the state register. + */ + Result>> generate_transitions_brute_force(const std::vector>& state_bfs, const u32 state_size) { - // generate state map - std::map var_to_val; - for (u32 state_index = 0; state_index < state_size; state_index++) - { - std::string var = BooleanFunctionNetDecorator(*(state_bfs.at(state_index).first)).get_boolean_variable_name(); - BooleanFunction val = ((state >> state_index) & 0x1) ? BooleanFunction::Const(1, 1) : BooleanFunction::Const(0, 1); - var_to_val.insert({var, val}); - } - - const auto sub_res = next_state_vec.substitute(var_to_val); - if (sub_res.is_error()) + // bitvector including all the functions to calculate the next state + BooleanFunction next_state_vec = state_bfs.front().second; + for (u32 i = 1; i < state_size; i++) { - return ERR_APPEND(sub_res.get_error(), "failed to solve fsm: unable to substitute variables in next state vec."); + next_state_vec = BooleanFunction::Concat(state_bfs.at(i).second.clone(), std::move(next_state_vec), next_state_vec.size() + 1).get(); } - const auto state_bf = sub_res.get().simplify(); - const auto inputs = utils::to_vector(state_bf.get_variable_names()); + std::map> all_transitions; - // brute force over all external inputs - for (u64 input_val = 0; input_val < (u64(1) << inputs.size()); input_val++) + for (u64 state = 0; state < (u64(1) << state_size); state++) { - // generate input map - std::unordered_map> input_mapping; - for (u32 input_index = 0; input_index < inputs.size(); input_index++) + // generate state map + std::map var_to_val; + for (u32 state_index = 0; state_index < state_size; state_index++) { - std::string input_var = inputs.at(input_index); - BooleanFunction::Value val = ((input_val >> input_index) & 0x1) ? BooleanFunction::Value::ONE : BooleanFunction::Value::ZERO; - input_mapping.insert({input_var, {val}}); + std::string var = BooleanFunctionNetDecorator(*(state_bfs.at(state_index).first)).get_boolean_variable_name(); + BooleanFunction val = ((state >> state_index) & 0x1) ? BooleanFunction::Const(1, 1) : BooleanFunction::Const(0, 1); + var_to_val.insert({var, val}); } - const auto& eval_res = state_bf.evaluate(input_mapping); + const auto sub_res = next_state_vec.substitute(var_to_val); if (sub_res.is_error()) { - return ERR_APPEND(sub_res.get_error(), "failed to solve fsm: unable to evaluate next state function."); + return ERR_APPEND(sub_res.get_error(), "failed to solve fsm: unable to substitute variables in next state vec."); } - const auto eval = eval_res.get(); + const auto state_bf = sub_res.get().simplify(); + const auto inputs = utils::to_vector(state_bf.get_variable_names()); - if (eval.front() == BooleanFunction::Value::X) + // brute force over all external inputs + for (u64 input_val = 0; input_val < (u64(1) << inputs.size()); input_val++) { - return ERR("failed to solve fsm: evaluating state function resulted in X state."); - } - - const u64 suc_state = BooleanFunction::to_u64(eval).get(); - all_transitions[state].insert(suc_state); - } - } - - const auto conditional_transitions = generate_conditional_transitions(state_bfs, all_transitions).get(); - - /* DEBUG PRINTING */ - for (const auto& [org, successors] : conditional_transitions) - { - std::cout << org << ": " << std::endl; - for (const auto& [suc, condition] : successors) - { - std::cout << "\t" << suc << ": " << condition.to_string() << std::endl; - } - } - /* END DEBUG PRINTING */ - - if (auto graph_res = generate_dot_graph(state_reg, conditional_transitions, graph_path); graph_res.is_error()) - { - return ERR_APPEND(graph_res.get_error(), "failed to solve fsm: unable to generate dot graph."); - } + // generate input map + std::unordered_map> input_mapping; + for (u32 input_index = 0; input_index < inputs.size(); input_index++) + { + std::string input_var = inputs.at(input_index); + BooleanFunction::Value val = ((input_val >> input_index) & 0x1) ? BooleanFunction::Value::ONE : BooleanFunction::Value::ZERO; + input_mapping.insert({input_var, {val}}); + } - return OK(conditional_transitions); - } + const auto& eval_res = state_bf.evaluate(input_mapping); + if (sub_res.is_error()) + { + return ERR_APPEND(sub_res.get_error(), "failed to solve fsm: unable to evaluate next state function."); + } - Result>> solve_fsm(Netlist* nl, - const std::vector& state_reg, - const std::vector& transition_logic, - const std::map& initial_state, - const std::filesystem::path& graph_path, - const u32 timeout) - { - const u32 state_size = state_reg.size(); - if (state_size > 64) - { - return ERR("failed to solve fsm: Currently only supports fsm with up to 64 state flip-flops but got " + std::to_string(state_size) + "."); - } + const auto eval = eval_res.get(); - // extract Boolean functions for each state flip-flop - const auto state_bfs_res = generate_state_bfs(nl, state_reg, transition_logic, true); - if (state_bfs_res.is_error()) - { - return ERR_APPEND(state_bfs_res.get_error(), "failed to solve fsm: unable to generate Boolean functions for state."); - } - const std::vector> state_bfs = state_bfs_res.get(); + if (eval.front() == BooleanFunction::Value::X) + { + return ERR("failed to solve fsm: evaluating state function resulted in X state."); + } - BooleanFunction prev_state_vec = BooleanFunctionNetDecorator(*(state_bfs.front().first)).get_boolean_variable(); - BooleanFunction next_state_vec = state_bfs.front().second; - for (u32 i = 1; i < state_reg.size(); i++) - { - // bitvector representing the previous state - prev_state_vec = BooleanFunction::Concat(BooleanFunctionNetDecorator(*(state_bfs.at(i).first)).get_boolean_variable(), std::move(prev_state_vec), i + 1).get(); + const u64 suc_state = BooleanFunction::to_u64(eval).get(); + all_transitions[state].insert(suc_state); + } + } - // bitvector including all the functions to calculate the next state - next_state_vec = BooleanFunction::Concat(state_bfs.at(i).second.clone(), std::move(next_state_vec), i + 1).get(); + return OK(all_transitions); } - // generate initial state - u64 initial_state_num = 0; - if (!initial_state.empty()) + /** + * Determine the successors of the states reachable from the initial state by querying an SMT solver for + * one successor at a time, excluding the ones already found until the solver runs out of solutions. + */ + Result>> + generate_transitions_smt(const std::vector>& state_bfs, const u32 state_size, const u64 initial_state_num, const u32 timeout) { - for (const auto& gate : state_reg) + BooleanFunction prev_state_vec = BooleanFunctionNetDecorator(*(state_bfs.front().first)).get_boolean_variable(); + BooleanFunction next_state_vec = state_bfs.front().second; + for (u32 i = 1; i < state_size; i++) { - if (initial_state.find(gate) == initial_state.end()) - { - return ERR("failed to solve fsm: Unable to find intial value for gate " + std::to_string(gate->get_id()) + " in the provided initial state map."); - } + // bitvector representing the previous state + prev_state_vec = BooleanFunction::Concat(BooleanFunctionNetDecorator(*(state_bfs.at(i).first)).get_boolean_variable(), std::move(prev_state_vec), i + 1).get(); - initial_state_num = initial_state_num << 1; - initial_state_num += initial_state.at(gate); + // bitvector including all the functions to calculate the next state + next_state_vec = BooleanFunction::Concat(state_bfs.at(i).second.clone(), std::move(next_state_vec), i + 1).get(); } - } - // generate all transitions that are reachable from the inital state. - std::map> all_transitions; + std::map> all_transitions; - std::deque q; - std::unordered_set visited; + std::deque q; + std::unordered_set visited; - q.push_back(initial_state_num); + q.push_back(initial_state_num); - while (!q.empty()) - { - std::vector successor_states; - - u64 n = q.front(); - q.pop_front(); - - if (visited.find(n) != visited.end()) + while (!q.empty()) { - continue; - } - visited.insert(n); + std::vector successor_states; - // generate new transitions and add them to the queue - SMT::Solver s; + u64 n = q.front(); + q.pop_front(); - // set prev_state_vec to starting state - s = s.with_constraint(SMT::Constraint{prev_state_vec.clone(), BooleanFunction::Const(n, state_size)}); - - while (true) - { - if (auto res = s.query(SMT::QueryConfig().with_model_generation().with_timeout(timeout)); res.is_error()) + if (visited.find(n) != visited.end()) { - return ERR_APPEND(res.get_error(), "failed to solve fsm: failed to querry SMT solver for state " + std::to_string(n) + "."); + continue; } - else - { - auto s_res = res.get(); - - if (s_res.is_unsat()) - { - break; - } + visited.insert(n); - if (s_res.is_unknown()) - { - return ERR("failed to solve fsm: received an unknown solver result for state " + std::to_string(n) + "."); - } + // generate new transitions and add them to the queue + SMT::Solver s; - auto m = s_res.model.value(); - auto suc = m.evaluate(next_state_vec).get(); - auto suc_num = 0; + // set prev_state_vec to starting state + s = s.with_constraint(SMT::Constraint{prev_state_vec.clone(), BooleanFunction::Const(n, state_size)}); - // a constant (numeral) successor state - if (suc.is_constant()) + while (true) + { + if (auto res = s.query(SMT::QueryConfig().with_model_generation().with_timeout(timeout)); res.is_error()) { - suc_num = suc.get_constant_value_u64().get(); + return ERR_APPEND(res.get_error(), "failed to solve fsm: failed to querry SMT solver for state " + std::to_string(n) + "."); } - // a successor state that includes boolean functions (for example in form of input variables) else { - // to resolve such a successor state, we simpply set all variables left in the state to zero (which is one possible solution) and continue to search for more valid solutions - std::unordered_map> zero_mapping; - for (const auto& var : suc.get_variable_names()) + auto s_res = res.get(); + + if (s_res.is_unsat()) { - zero_mapping.insert({var, {BooleanFunction::Value::ZERO}}); + break; } - if (auto eval_res = suc.evaluate(zero_mapping); eval_res.is_error()) + if (s_res.is_unknown()) { - return ERR_APPEND(eval_res.get_error(), "failed to solve fsm: could not evaluate successor state to constant."); + return ERR("failed to solve fsm: received an unknown solver result for state " + std::to_string(n) + "."); } + + auto m = s_res.model.value(); + auto suc = m.evaluate(next_state_vec).get(); + auto suc_num = 0; + + // a constant (numeral) successor state + if (suc.is_constant()) + { + suc_num = suc.get_constant_value_u64().get(); + } + // a successor state that includes boolean functions (for example in form of input variables) else { - suc_num = BooleanFunction::to_u64(eval_res.get()).get(); + // to resolve such a successor state, we simpply set all variables left in the state to zero (which is one possible solution) and continue to search for more valid solutions + std::unordered_map> zero_mapping; + for (const auto& var : suc.get_variable_names()) + { + zero_mapping.insert({var, {BooleanFunction::Value::ZERO}}); + } + + if (auto eval_res = suc.evaluate(zero_mapping); eval_res.is_error()) + { + return ERR_APPEND(eval_res.get_error(), "failed to solve fsm: could not evaluate successor state to constant."); + } + else + { + suc_num = BooleanFunction::to_u64(eval_res.get()).get(); + } } - } - q.push_back(suc_num); - all_transitions[n].insert(suc_num); - s = s.with_constraint(SMT::Constraint(BooleanFunction::Not(BooleanFunction::Eq(next_state_vec.clone(), BooleanFunction::Const(suc_num, suc.size()), 1).get(), 1).get())); + q.push_back(suc_num); + all_transitions[n].insert(suc_num); + s = s.with_constraint(SMT::Constraint(BooleanFunction::Not(BooleanFunction::Eq(next_state_vec.clone(), BooleanFunction::Const(suc_num, suc.size()), 1).get(), 1).get())); + } } } - } - const auto conditional_transitions = generate_conditional_transitions(state_bfs, all_transitions).get(); + return OK(all_transitions); + } - /* DEBUG PRINTING */ - for (const auto& [org, successors] : conditional_transitions) + /** + * Restrict the transitions to the states that are actually reachable from the initial state. Brute forcing + * enumerates every state, including those the FSM can never enter from where it starts. + */ + std::map> restrict_to_reachable(const std::map>& all_transitions, const u64 initial_state_num) { - std::cout << org << ": " << std::endl; - for (const auto& [suc, condition] : successors) + std::map> res; + + std::deque q = {initial_state_num}; + std::unordered_set visited; + + while (!q.empty()) { - std::cout << "\t" << suc << ": " << condition.to_string() << std::endl; + const u64 state = q.front(); + q.pop_front(); + + if (!visited.insert(state).second) + { + continue; + } + + const auto it = all_transitions.find(state); + if (it == all_transitions.end()) + { + continue; + } + + res[state] = it->second; + for (const u64 successor : it->second) + { + q.push_back(successor); + } } + + return res; } - /* END DEBUG PRINTING */ + } // namespace - if (auto graph_res = generate_dot_graph(state_reg, conditional_transitions, graph_path); graph_res.is_error()) + + Result solve_fsm(const Configuration& config) + { + if (config.netlist == nullptr) { - return ERR_APPEND(graph_res.get_error(), "failed to solve fsm: unable to generate dot graph."); + return ERR("failed to solve FSM: netlist is a nullptr."); } - return OK(conditional_transitions); - } + if (config.state_register.empty()) + { + return ERR("failed to solve FSM: no state register configured."); + } + if (config.transition_logic.empty()) + { + return ERR("failed to solve FSM: no transition logic configured."); + } - Result generate_dot_graph(const std::vector& state_reg, - const std::map>& transitions, - const std::filesystem::path& graph_path, - const u32 max_condition_length, - const u32 base) - { - std::string graph_str = "digraph {\ncomment=\"created by HAL plugin solve_fsm\"\n"; + const u32 state_size = config.state_register.size(); + if (state_size > 64) + { + return ERR("failed to solve FSM: only up to 64 state flip-flops are supported, but got " + std::to_string(state_size) + "."); + } - for (const auto& [org, successors] : transitions) + // extract Boolean functions for each state flip-flop + const auto state_bfs_res = generate_state_bfs(config.netlist, config.state_register, config.transition_logic, true); + if (state_bfs_res.is_error()) { - for (const auto& [suc, cond] : successors) - { - std::string start_name; - std::string end_name; + return ERR_APPEND(state_bfs_res.get_error(), "failed to solve FSM: unable to generate the Boolean functions of the state."); + } + const std::vector> state_bfs = state_bfs_res.get(); - switch (base) - { - case 2: - start_name = std::bitset<64>(org).to_string().substr(64 - state_reg.size(), 64); - end_name = std::bitset<64>(suc).to_string().substr(64 - state_reg.size(), 64); - break; - case 10: - start_name = std::to_string(org); - end_name = std::to_string(suc); - break; - default: - return ERR("failed to generate DOT graph: base " + std::to_string(base) + "not implemented."); - } + // the first flip-flop of the state register provides the least significant bit + u64 initial_state_num = 0; + for (u32 i = 0; i < state_size; i++) + { + Gate* gate = config.state_register.at(i); + if (config.initial_state.empty()) + { + break; + } - graph_str += - start_name + " -> " + end_name + "[label=\"" + cond.to_string().substr(0, max_condition_length) + "\", weight=\"" + cond.to_string().substr(0, max_condition_length) + "\"];\n"; - ; + if (config.initial_state.find(gate) == config.initial_state.end()) + { + return ERR("failed to solve FSM: unable to find an initial value for gate '" + gate->get_name() + "' with ID " + std::to_string(gate->get_id()) + + " in the provided initial state."); } + + initial_state_num |= u64(config.initial_state.at(gate) ? 1 : 0) << i; } - graph_str += "}"; + std::map> all_transitions; + if (config.brute_force) + { + auto transitions_res = generate_transitions_brute_force(state_bfs, state_size); + if (transitions_res.is_error()) + { + return ERR_APPEND(transitions_res.get_error(), "failed to solve FSM: unable to determine the transitions by brute force."); + } - // write to file - if (!graph_path.empty()) + // brute forcing visits every state, so the ones the FSM can never enter have to be dropped to match + // what the SMT approach returns for the same configuration + all_transitions = restrict_to_reachable(transitions_res.get(), initial_state_num); + } + else { - std::ofstream ofs(graph_path); - if (!ofs.is_open()) + auto transitions_res = generate_transitions_smt(state_bfs, state_size, initial_state_num, config.timeout); + if (transitions_res.is_error()) { - return ERR("failed to generate DOT graph: could not open file '" + graph_path.string() + "' for writing."); + return ERR_APPEND(transitions_res.get_error(), "failed to solve FSM: unable to determine the transitions using the SMT solver."); } - ofs << graph_str; - ofs.close(); + + all_transitions = transitions_res.get(); } - open_dot_in_viewer(graph_path); + StateTransitionGraph res; + res.netlist = config.netlist; + res.state_register = config.state_register; + res.output_nets = config.outputs; + + auto conditional_res = generate_conditional_transitions(state_bfs, all_transitions); + if (conditional_res.is_error()) + { + return ERR_APPEND(conditional_res.get_error(), "failed to solve FSM: unable to determine the conditions of the transitions."); + } + res.transitions = conditional_res.get(); + + if (!config.outputs.empty()) + { + const auto output_bfs_res = generate_output_bfs(config.netlist, config.outputs); + if (output_bfs_res.is_error()) + { + return ERR_APPEND(output_bfs_res.get_error(), "failed to solve FSM: unable to generate the Boolean functions of the outputs."); + } + const auto output_bfs = output_bfs_res.get(); + + for (const auto& [state, _] : all_transitions) + { + auto state_outputs_res = evaluate_outputs_in_state(output_bfs, config.state_register, state); + if (state_outputs_res.is_error()) + { + return ERR_APPEND(state_outputs_res.get_error(), "failed to solve FSM: unable to evaluate the outputs in state " + std::to_string(state) + "."); + } + + res.outputs[state] = state_outputs_res.get(); + } + } - return OK(graph_str); + return OK(res); } } // namespace solve_fsm } // namespace hal diff --git a/plugins/solve_fsm/src/state_transition_graph.cpp b/plugins/solve_fsm/src/state_transition_graph.cpp new file mode 100644 index 000000000000..03103f079fd1 --- /dev/null +++ b/plugins/solve_fsm/src/state_transition_graph.cpp @@ -0,0 +1,305 @@ +// MIT License +// +// Copyright (c) 2019 Ruhr University Bochum, Chair for Embedded Security. All Rights reserved. +// Copyright (c) 2019 Marc Fyrbiak, Sebastian Wallat, Max Hoffmann ("ORIGINAL AUTHORS"). All rights reserved. +// Copyright (c) 2021 Max Planck Institute for Security and Privacy. All Rights reserved. +// Copyright (c) 2021 Jörn Langheinrich, Julian Speith, Nils Albartus, René Walendy, Simon Klix ("ORIGINAL AUTHORS"). All Rights reserved. +// +// Permission is hereby granted, free of charge, to any person obtaining a copy +// of this software and associated documentation files (the "Software"), to deal +// in the Software without restriction, including without limitation the rights +// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +// copies of the Software, and to permit persons to whom the Software is +// furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all +// copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +// SOFTWARE. + +#include "solve_fsm/state_transition_graph.h" + +#include "hal_core/netlist/decorators/boolean_function_net_decorator.h" +#include "hal_core/netlist/gate.h" +#include "hal_core/netlist/net.h" +#include "hal_core/netlist/netlist.h" + +#include +#include +#include +#include + +namespace hal +{ + namespace solve_fsm + { + namespace + { + /** + * Print a value in the requested base, zero-padded to the given bit-size when printed as binary. + */ + std::string format_value(const u64 value, const u32 size, const u32 base) + { + if (base == 2) + { + return std::bitset<64>(value).to_string().substr(64 - size, 64); + } + return std::to_string(value); + } + + /** + * A Boolean function rendered either as the value it evaluates to or, if it still depends on the inputs of + * the FSM, as the function itself. + */ + std::string format_function(const BooleanFunction& bf, const u32 base) + { + if (bf.is_constant()) + { + if (const auto res = bf.get_constant_value_u64(); res.is_ok()) + { + return format_value(res.get(), bf.size(), base); + } + } + return bf.to_string(); + } + + /** + * The name and ID of a netlist element, as printed in the legend of the text representation. + */ + template + std::string format_element(const T* element) + { + return "'" + element->get_name() + "' with ID " + std::to_string(element->get_id()); + } + } // namespace + + u32 StateTransitionGraph::get_state_size() const + { + return state_register.size(); + } + + Result StateTransitionGraph::generate_dot_graph(const std::filesystem::path& graph_path, const u32 max_condition_length, const u32 base) const + { + std::string graph_str = "digraph {\ncomment=\"created by HAL plugin solve_fsm\"\n"; + + const auto format_state = [this, base](const u64 state) -> std::string { + if (base == 2) + { + return std::bitset<64>(state).to_string().substr(64 - this->get_state_size(), 64); + } + return std::to_string(state); + }; + + if (base != 2 && base != 10) + { + return ERR("failed to generate DOT graph: base " + std::to_string(base) + "not implemented."); + } + + // states only carry an explicit node statement if there is something to annotate them with + if (!outputs.empty()) + { + std::set states; + for (const auto& [org, successors] : transitions) + { + states.insert(org); + for (const auto& [suc, _] : successors) + { + states.insert(suc); + } + } + + for (const auto& state : states) + { + std::string label = format_state(state); + + if (const auto it = outputs.find(state); it != outputs.end()) + { + for (const auto& [name, bf] : it->second) + { + // an output that only depends on the state has a constant value, one that also depends on + // the inputs of the FSM is printed as the function that it is + std::string value; + if (bf.is_constant()) + { + if (const auto val_res = bf.get_constant_value_u64(); val_res.is_ok()) + { + value = (base == 2) ? std::bitset<64>(val_res.get()).to_string().substr(64 - bf.size(), 64) : std::to_string(val_res.get()); + } + } + if (value.empty()) + { + value = bf.to_string().substr(0, max_condition_length); + } + + label += "\\n" + name + " = " + value; + } + } + + graph_str += format_state(state) + " [label=\"" + label + "\"];\n"; + } + } + + for (const auto& [org, successors] : transitions) + { + for (const auto& [suc, cond] : successors) + { + const std::string start_name = format_state(org); + const std::string end_name = format_state(suc); + + graph_str += + start_name + " -> " + end_name + "[label=\"" + cond.to_string().substr(0, max_condition_length) + "\", weight=\"" + cond.to_string().substr(0, max_condition_length) + "\"];\n"; + ; + } + } + + graph_str += "}"; + + // write to file + if (!graph_path.empty()) + { + std::ofstream ofs(graph_path); + if (!ofs.is_open()) + { + return ERR("failed to generate DOT graph: could not open file '" + graph_path.string() + "' for writing."); + } + ofs << graph_str; + ofs.close(); + + } + + return OK(graph_str); + } + Result StateTransitionGraph::to_string(const u32 base) const + { + if (base != 2 && base != 10) + { + return ERR("failed to print state transition graph: base " + std::to_string(base) + " is not implemented."); + } + + const u32 state_size = get_state_size(); + std::stringstream ss; + + ss << "FSM with " << state_size << " state bits and " << transitions.size() << " reachable states" << std::endl << std::endl; + + // the legend maps a state and its outputs back to the netlist elements they are made of + ss << "state register (least significant bit first):" << std::endl; + for (u32 i = 0; i < state_register.size(); i++) + { + ss << " bit " << i << ": " << format_element(state_register.at(i)) << std::endl; + } + ss << std::endl; + + if (!output_nets.empty()) + { + ss << "outputs (least significant bit first):" << std::endl; + for (const auto& [name, nets] : output_nets) + { + ss << " " << name << ":"; + for (u32 i = 0; i < nets.size(); i++) + { + ss << (i == 0 ? " " : ", ") << format_element(nets.at(i)); + } + ss << std::endl; + } + ss << std::endl; + } + + // the Boolean functions refer to nets by a variable derived from the net ID, which matches no name in the + // netlist, so every variable that appears anywhere below is resolved here + std::set variables; + for (const auto& [state, successors] : transitions) + { + for (const auto& [successor, condition] : successors) + { + const auto vars = condition.get_variable_names(); + variables.insert(vars.begin(), vars.end()); + } + } + for (const auto& [state, state_outputs] : outputs) + { + for (const auto& [name, bf] : state_outputs) + { + const auto vars = bf.get_variable_names(); + variables.insert(vars.begin(), vars.end()); + } + } + + if (!variables.empty()) + { + ss << "nets referenced in the Boolean functions below:" << std::endl; + for (const auto& variable : variables) + { + ss << " " << variable << ": "; + if (netlist == nullptr) + { + ss << "unknown, the netlist is not available" << std::endl; + continue; + } + + if (const auto net_res = BooleanFunctionNetDecorator::get_net_from(netlist, variable); net_res.is_ok()) + { + ss << "'" << net_res.get()->get_name() << "' with ID " << net_res.get()->get_id() << std::endl; + } + else + { + ss << "not a net of this netlist" << std::endl; + } + } + ss << std::endl; + } + + for (const auto& [state, successors] : transitions) + { + ss << "state " << format_value(state, state_size, base) << std::endl; + + if (const auto it = outputs.find(state); it != outputs.end() && !it->second.empty()) + { + ss << " outputs:" << std::endl; + for (const auto& [name, bf] : it->second) + { + ss << " " << name << " = " << format_function(bf, base) << std::endl; + } + } + + ss << " transitions:" << std::endl; + if (successors.empty()) + { + ss << " none" << std::endl; + } + for (const auto& [successor, condition] : successors) + { + ss << " to " << format_value(successor, state_size, base) << " if " << condition.to_string() << std::endl; + } + + ss << std::endl; + } + + return OK(ss.str()); + } + + Result StateTransitionGraph::write_txt(const std::filesystem::path& file_path, const u32 base) const + { + auto res = to_string(base); + if (res.is_error()) + { + return ERR_APPEND(res.get_error(), "failed to write state transition graph to '" + file_path.string() + "'."); + } + + std::ofstream ofs(file_path); + if (!ofs.is_open()) + { + return ERR("failed to write state transition graph: could not open file '" + file_path.string() + "' for writing."); + } + ofs << res.get(); + ofs.close(); + + return OK({}); + } + } // namespace solve_fsm +} // namespace hal diff --git a/plugins/solve_fsm/test/CMakeLists.txt b/plugins/solve_fsm/test/CMakeLists.txt new file mode 100644 index 000000000000..0ba164034b19 --- /dev/null +++ b/plugins/solve_fsm/test/CMakeLists.txt @@ -0,0 +1,13 @@ +if(BUILD_TESTS) + include_directories(${gtest_SOURCE_DIR}/include ${gtest_SOURCE_DIR} ${CMAKE_SOURCE_DIR}/include ${CMAKE_SOURCE_DIR}/tests ${CMAKE_SOURCE_DIR}/plugins/solve_fsm/include) + + add_executable(runTest-solve_fsm solve_fsm.cpp) + + target_link_libraries(runTest-solve_fsm solve_fsm pthread gtest hal::core hal::netlist test_utils) + + add_test(runTest-solve_fsm ${CMAKE_BINARY_DIR}/bin/hal_plugins/runTest-solve_fsm --gtest_output=xml:${CMAKE_BINARY_DIR}/gtestresults-runBasicTests.xml) + + if(${CMAKE_BUILD_TYPE} STREQUAL "Debug") + add_sanitizers(runTest-solve_fsm) + endif() +endif() diff --git a/plugins/solve_fsm/test/solve_fsm.cpp b/plugins/solve_fsm/test/solve_fsm.cpp new file mode 100644 index 000000000000..3399bf80381d --- /dev/null +++ b/plugins/solve_fsm/test/solve_fsm.cpp @@ -0,0 +1,630 @@ +#include "solve_fsm/solve_fsm.h" + +#include "hal_core/netlist/gate.h" + +#include "hal_core/netlist/boolean_function/solver.h" +#include "hal_core/netlist/gate.h" +#include "hal_core/netlist/net.h" +#include "hal_core/netlist/netlist.h" +#include "netlist_test_utils.h" + +namespace hal +{ + class SolveFsmTest : public ::testing::Test + { + protected: + virtual void SetUp() + { + NO_COUT_BLOCK; + test_utils::init_log_channels(); + test_utils::create_sandbox_directory(); + } + + virtual void TearDown() + { + test_utils::remove_sandbox_directory(); + } + + /** + * The solver is an external dependency that is not present in every environment, so the tests below are + * skipped rather than failed when it cannot be found. + */ + static bool solver_available() + { + return SMT::Solver::has_local_solver_for(SMT::SolverType::Z3, SMT::SolverCall::Binary); + } + + /** + * A two bit state register clocked by a global input, with 'ff0' holding the least significant bit. + */ + struct StateRegister + { + Gate* ff0; + Gate* ff1; + Net* q0; + Net* q1; + + std::vector gates() const + { + return {ff0, ff1}; + } + }; + + StateRegister create_state_register(Netlist* nl) + { + const GateLibrary* gl = nl->get_gate_library(); + + StateRegister sr; + sr.ff0 = nl->create_gate(gl->get_gate_type_by_name("DFF"), "ff0"); + sr.ff1 = nl->create_gate(gl->get_gate_type_by_name("DFF"), "ff1"); + + Net* clk = nl->create_net("clk"); + clk->add_destination(sr.ff0, "CLK"); + clk->add_destination(sr.ff1, "CLK"); + clk->mark_global_input_net(); + + sr.q0 = nl->create_net("q0"); + sr.q0->add_source(sr.ff0, "Q"); + sr.q1 = nl->create_net("q1"); + sr.q1->add_source(sr.ff1, "Q"); + + return sr; + } + + /** + * Transition logic of a two bit counter, i.e. 0 -> 1 -> 2 -> 3 -> 0. + */ + std::vector create_counter_logic(Netlist* nl, const StateRegister& sr) + { + const GateLibrary* gl = nl->get_gate_library(); + + // next bit 0 is the inverse of bit 0 + Gate* inv = nl->create_gate(gl->get_gate_type_by_name("INV"), "inv_d0"); + sr.q0->add_destination(inv, "I"); + Net* d0 = nl->create_net("d0"); + d0->add_source(inv, "O"); + d0->add_destination(sr.ff0, "D"); + + // next bit 1 flips whenever bit 0 is set + Gate* xor2 = nl->create_gate(gl->get_gate_type_by_name("XOR2"), "xor_d1"); + sr.q0->add_destination(xor2, "I0"); + sr.q1->add_destination(xor2, "I1"); + Net* d1 = nl->create_net("d1"); + d1->add_source(xor2, "O"); + d1->add_destination(sr.ff1, "D"); + + return {inv, xor2}; + } + + /** + * Transition logic of a saturating counter, i.e. 0 -> 1 -> 2 -> 3 -> 3. Unlike the wrapping counter above, + * which state the FSM starts in decides which states are reachable at all. + */ + std::vector create_saturating_counter_logic(Netlist* nl, const StateRegister& sr) + { + const GateLibrary* gl = nl->get_gate_library(); + + // next bit 0 is '!q0 | q1' + Gate* inv = nl->create_gate(gl->get_gate_type_by_name("INV"), "inv_q0"); + sr.q0->add_destination(inv, "I"); + Net* not_q0 = nl->create_net("not_q0"); + not_q0->add_source(inv, "O"); + + Gate* or_d0 = nl->create_gate(gl->get_gate_type_by_name("OR2"), "or_d0"); + not_q0->add_destination(or_d0, "I0"); + sr.q1->add_destination(or_d0, "I1"); + Net* d0 = nl->create_net("d0"); + d0->add_source(or_d0, "O"); + d0->add_destination(sr.ff0, "D"); + + // next bit 1 is 'q0 | q1' + Gate* or_d1 = nl->create_gate(gl->get_gate_type_by_name("OR2"), "or_d1"); + sr.q0->add_destination(or_d1, "I0"); + sr.q1->add_destination(or_d1, "I1"); + Net* d1 = nl->create_net("d1"); + d1->add_source(or_d1, "O"); + d1->add_destination(sr.ff1, "D"); + + return {inv, or_d0, or_d1}; + } + + /** + * The constant value of an output, or an empty optional if the output still depends on the inputs of the FSM. + */ + static std::optional constant_value(const std::vector>& outputs, const std::string& name) + { + for (const auto& [output_name, bf] : outputs) + { + if (output_name != name) + { + continue; + } + if (!bf.is_constant()) + { + return std::nullopt; + } + if (auto res = bf.get_constant_value_u64(); res.is_ok()) + { + return res.get(); + } + } + return std::nullopt; + } + }; + + /** + * Test that the outputs of a Moore FSM evaluate to a constant in every state, both for an output driven by + * combinational logic and for one that is driven by a flip-flop directly. + * + * Functions: solve_fsm + */ + TEST_F(SolveFsmTest, check_moore_outputs) + { + TEST_START + if (!solver_available()) + { + GTEST_SKIP() << "no local SMT solver available"; + } + { + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + const GateLibrary* gl = nl->get_gate_library(); + + const StateRegister sr = create_state_register(nl.get()); + const auto transition_logic = create_counter_logic(nl.get(), sr); + + // one output computed from both state bits, one taken straight off a flip-flop + Gate* out_xor = nl->create_gate(gl->get_gate_type_by_name("XOR2"), "out_xor"); + sr.q0->add_destination(out_xor, "I0"); + sr.q1->add_destination(out_xor, "I1"); + Net* out_b = nl->create_net("out_b"); + out_b->add_source(out_xor, "O"); + out_b->mark_global_output_net(); + + const auto config = solve_fsm::Configuration(nl.get()).with_state_register(sr.gates()).with_transition_logic(transition_logic).with_outputs({{"OUT_A", {sr.q0}}, {"OUT_B", {out_b}}}); + const auto res = solve_fsm::solve_fsm(config); + ASSERT_TRUE(res.is_ok()); + const auto graph = res.get(); + + // the counter walks through all four states + ASSERT_EQ(graph.transitions.size(), 4); + for (u64 state = 0; state < 4; state++) + { + ASSERT_EQ(graph.transitions.at(state).size(), 1); + EXPECT_EQ(graph.transitions.at(state).begin()->first, (state + 1) % 4); + } + + // 'OUT_A' is state bit 0, 'OUT_B' is the XOR of both state bits + ASSERT_EQ(graph.outputs.size(), 4); + for (u64 state = 0; state < 4; state++) + { + const auto& outputs = graph.outputs.at(state); + ASSERT_EQ(outputs.size(), 2); + + // the outputs keep the order in which they were passed in + EXPECT_EQ(outputs.at(0).first, "OUT_A"); + EXPECT_EQ(outputs.at(1).first, "OUT_B"); + + EXPECT_EQ(constant_value(outputs, "OUT_A"), std::optional(state & 0x1)); + EXPECT_EQ(constant_value(outputs, "OUT_B"), std::optional((state & 0x1) ^ ((state >> 1) & 0x1))); + } + } + TEST_END + } + + /** + * Test that an output of a Mealy FSM keeps the input it depends on instead of collapsing to a constant. + * + * Functions: solve_fsm + */ + TEST_F(SolveFsmTest, check_mealy_outputs) + { + TEST_START + if (!solver_available()) + { + GTEST_SKIP() << "no local SMT solver available"; + } + { + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + const GateLibrary* gl = nl->get_gate_library(); + + const StateRegister sr = create_state_register(nl.get()); + const auto transition_logic = create_counter_logic(nl.get(), sr); + + // the output depends on an input of the FSM as well as on the state + Net* in0 = nl->create_net("in0"); + in0->mark_global_input_net(); + + Gate* out_xor = nl->create_gate(gl->get_gate_type_by_name("XOR2"), "out_xor"); + sr.q0->add_destination(out_xor, "I0"); + in0->add_destination(out_xor, "I1"); + Net* out = nl->create_net("out"); + out->add_source(out_xor, "O"); + out->mark_global_output_net(); + + const auto config = solve_fsm::Configuration(nl.get()).with_state_register(sr.gates()).with_transition_logic(transition_logic).with_outputs({{"OUT", {out}}}); + const auto res = solve_fsm::solve_fsm(config); + ASSERT_TRUE(res.is_ok()); + const auto graph = res.get(); + + ASSERT_EQ(graph.outputs.size(), 4); + for (u64 state = 0; state < 4; state++) + { + const auto& outputs = graph.outputs.at(state); + ASSERT_EQ(outputs.size(), 1); + const auto& bf = outputs.at(0).second; + + // the state alone does not determine the output, so the input variable has to survive + EXPECT_FALSE(bf.is_constant()); + ASSERT_EQ(bf.get_variable_names().size(), 1); + + // 'OUT' is 'in0' XOR state bit 0, so evaluating the input reproduces both possible outputs + const std::string var = *(bf.get_variable_names().begin()); + for (const auto in_val : {BooleanFunction::Value::ZERO, BooleanFunction::Value::ONE}) + { + const std::unordered_map inputs = {{var, in_val}}; + const auto eval_res = bf.evaluate(inputs); + ASSERT_TRUE(eval_res.is_ok()); + + const auto expected = ((in_val == BooleanFunction::Value::ONE) != ((state & 0x1) == 1)) ? BooleanFunction::Value::ONE : BooleanFunction::Value::ZERO; + EXPECT_EQ(eval_res.get(), expected); + } + } + } + TEST_END + } + + /** + * Test that a multi-bit output is reported as a single value, with the first net providing the least significant bit. + * + * Functions: solve_fsm + */ + TEST_F(SolveFsmTest, check_multi_bit_output) + { + TEST_START + if (!solver_available()) + { + GTEST_SKIP() << "no local SMT solver available"; + } + { + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + + const StateRegister sr = create_state_register(nl.get()); + const auto transition_logic = create_counter_logic(nl.get(), sr); + + // the FSM publishes its state register, so the value of the output must equal the state itself + const auto config = solve_fsm::Configuration(nl.get()).with_state_register(sr.gates()).with_transition_logic(transition_logic).with_outputs({{"OUT", {sr.q0, sr.q1}}}); + const auto res = solve_fsm::solve_fsm(config); + ASSERT_TRUE(res.is_ok()); + const auto graph = res.get(); + + ASSERT_EQ(graph.outputs.size(), 4); + for (u64 state = 0; state < 4; state++) + { + const auto& outputs = graph.outputs.at(state); + ASSERT_EQ(outputs.size(), 1); + EXPECT_EQ(outputs.at(0).second.size(), 2); + EXPECT_EQ(constant_value(outputs, "OUT"), std::optional(state)); + } + } + { + // reversing the nets of the output reverses its bits + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + + const StateRegister sr = create_state_register(nl.get()); + const auto transition_logic = create_counter_logic(nl.get(), sr); + + const auto config = solve_fsm::Configuration(nl.get()).with_state_register(sr.gates()).with_transition_logic(transition_logic).with_outputs({{"OUT", {sr.q1, sr.q0}}}); + const auto res = solve_fsm::solve_fsm(config); + ASSERT_TRUE(res.is_ok()); + const auto graph = res.get(); + + for (u64 state = 0; state < 4; state++) + { + const u64 reversed = ((state & 0x1) << 1) | ((state >> 1) & 0x1); + EXPECT_EQ(constant_value(graph.outputs.at(state), "OUT"), std::optional(reversed)); + } + } + TEST_END + } + + /** + * Test that a non-zero initial state is interpreted with the first flip-flop of the state register providing the + * least significant bit, and that the exploration starts from that state. + * + * Functions: solve_fsm + */ + TEST_F(SolveFsmTest, check_initial_state) + { + TEST_START + if (!solver_available()) + { + GTEST_SKIP() << "no local SMT solver available"; + } + { + // the saturating counter never returns to a lower state, so the set of reachable states pins down which + // state the solver actually started from + const std::vector, std::set>> cases = { + {{{0, false}, {1, false}}, {0, 1, 2, 3}}, // state 0 + {{{0, true}, {1, false}}, {1, 2, 3}}, // state 1, only the first flip-flop is set + {{{0, false}, {1, true}}, {2, 3}}, // state 2, only the second flip-flop is set + {{{0, true}, {1, true}}, {3}}, // state 3 + }; + + for (const auto& [initial_bits, expected_states] : cases) + { + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + + const StateRegister sr = create_state_register(nl.get()); + const auto transition_logic = create_saturating_counter_logic(nl.get(), sr); + + const std::map initial_state = {{sr.ff0, initial_bits.at(0)}, {sr.ff1, initial_bits.at(1)}}; + + const auto config = solve_fsm::Configuration(nl.get()) + .with_state_register(sr.gates()) + .with_transition_logic(transition_logic) + .with_outputs({{"OUT", {sr.q0, sr.q1}}}) + .with_initial_state(initial_state); + const auto res = solve_fsm::solve_fsm(config); + ASSERT_TRUE(res.is_ok()); + const auto graph = res.get(); + + std::set reached; + for (const auto& [state, successors] : graph.transitions) + { + reached.insert(state); + for (const auto& [successor, _] : successors) + { + reached.insert(successor); + } + } + + EXPECT_EQ(reached, expected_states); + } + } + TEST_END + } + + /** + * Test that brute forcing and SMT solving produce the same state transition graph, including for a non-zero + * initial state, where brute forcing has to discard the states that the FSM can never enter. + * + * Functions: solve_fsm + */ + TEST_F(SolveFsmTest, check_brute_force) + { + TEST_START + if (!solver_available()) + { + GTEST_SKIP() << "no local SMT solver available"; + } + { + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + + const StateRegister sr = create_state_register(nl.get()); + const auto transition_logic = create_saturating_counter_logic(nl.get(), sr); + + // starting in state 1 leaves state 0 unreachable, which brute forcing has to notice + const std::map initial_state = {{sr.ff0, true}, {sr.ff1, false}}; + + const auto base_config = solve_fsm::Configuration(nl.get()) + .with_state_register(sr.gates()) + .with_transition_logic(transition_logic) + .with_outputs({{"OUT", {sr.q0, sr.q1}}}) + .with_initial_state(initial_state); + + auto smt_config = base_config; + const auto smt_res = solve_fsm::solve_fsm(smt_config); + ASSERT_TRUE(smt_res.is_ok()); + const auto smt = smt_res.get(); + + auto brute_config = base_config; + brute_config.with_brute_force(); + const auto brute_res = solve_fsm::solve_fsm(brute_config); + ASSERT_TRUE(brute_res.is_ok()); + const auto brute = brute_res.get(); + + EXPECT_EQ(smt.get_state_size(), brute.get_state_size()); + + // the same states are reached + ASSERT_EQ(smt.transitions.size(), brute.transitions.size()); + EXPECT_EQ(smt.transitions.size(), 3); + + for (const auto& [state, successors] : smt.transitions) + { + ASSERT_NE(brute.transitions.find(state), brute.transitions.end()); + ASSERT_EQ(successors.size(), brute.transitions.at(state).size()); + for (const auto& [successor, _] : successors) + { + EXPECT_NE(brute.transitions.at(state).find(successor), brute.transitions.at(state).end()); + } + + // and report the same outputs + EXPECT_EQ(constant_value(smt.outputs.at(state), "OUT"), constant_value(brute.outputs.at(state), "OUT")); + } + } + TEST_END + } + + /** + * Test that the solver rejects a configuration that does not describe an FSM. + * + * Functions: solve_fsm + */ + TEST_F(SolveFsmTest, check_invalid_configuration) + { + TEST_START + { + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + + const StateRegister sr = create_state_register(nl.get()); + const auto transition_logic = create_counter_logic(nl.get(), sr); + + EXPECT_TRUE(solve_fsm::solve_fsm(solve_fsm::Configuration(nullptr).with_state_register(sr.gates()).with_transition_logic(transition_logic)).is_error()); + EXPECT_TRUE(solve_fsm::solve_fsm(solve_fsm::Configuration(nl.get()).with_transition_logic(transition_logic)).is_error()); + EXPECT_TRUE(solve_fsm::solve_fsm(solve_fsm::Configuration(nl.get()).with_state_register(sr.gates())).is_error()); + + // an initial state that does not cover the whole state register is rejected as well + const auto incomplete = solve_fsm::Configuration(nl.get()) + .with_state_register(sr.gates()) + .with_transition_logic(transition_logic) + .with_initial_state({{sr.ff0, true}}); + EXPECT_TRUE(solve_fsm::solve_fsm(incomplete).is_error()); + } + TEST_END + } + + /** + * Test that the text representation contains the legend mapping the state and the outputs back to the netlist, + * and the full condition of every transition. + * + * Functions: StateTransitionGraph::to_string + */ + TEST_F(SolveFsmTest, check_to_string) + { + TEST_START + if (!solver_available()) + { + GTEST_SKIP() << "no local SMT solver available"; + } + { + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + + const StateRegister sr = create_state_register(nl.get()); + const auto transition_logic = create_counter_logic(nl.get(), sr); + + const auto config = solve_fsm::Configuration(nl.get()).with_state_register(sr.gates()).with_transition_logic(transition_logic).with_outputs({{"OUT", {sr.q0, sr.q1}}}); + const auto res = solve_fsm::solve_fsm(config); + ASSERT_TRUE(res.is_ok()); + const auto graph = res.get(); + + const auto str_res = graph.to_string(); + ASSERT_TRUE(str_res.is_ok()); + const std::string str = str_res.get(); + + // the legend maps every bit of the state and every output back to the netlist + EXPECT_NE(str.find("FSM with 2 state bits and 4 reachable states"), std::string::npos); + EXPECT_NE(str.find("bit 0: 'ff0' with ID " + std::to_string(sr.ff0->get_id())), std::string::npos); + EXPECT_NE(str.find("bit 1: 'ff1' with ID " + std::to_string(sr.ff1->get_id())), std::string::npos); + EXPECT_NE(str.find("OUT: 'q0' with ID " + std::to_string(sr.q0->get_id()) + ", 'q1' with ID " + std::to_string(sr.q1->get_id())), std::string::npos); + + // every state carries its outputs and its transitions + for (u64 state = 0; state < 4; state++) + { + EXPECT_NE(str.find("state " + std::to_string(state) + "\n"), std::string::npos); + EXPECT_NE(str.find("OUT = " + std::to_string(state)), std::string::npos); + EXPECT_NE(str.find("to " + std::to_string((state + 1) % 4) + " if "), std::string::npos); + } + + // this FSM has no inputs at all, so no Boolean function holds a variable and there is nothing to resolve + EXPECT_EQ(str.find("nets referenced in the Boolean functions below:"), std::string::npos); + + // nothing is truncated, so the conditions appear in full + for (const auto& [state, successors] : graph.transitions) + { + for (const auto& [successor, condition] : successors) + { + EXPECT_NE(str.find(condition.to_string()), std::string::npos); + } + } + + // binary state labels are zero-padded to the size of the state register + const auto bin_res = graph.to_string(2); + ASSERT_TRUE(bin_res.is_ok()); + EXPECT_NE(bin_res.get().find("state 10"), std::string::npos); + + EXPECT_TRUE(graph.to_string(16).is_error()); + } + { + // the variables inside the Boolean functions are derived from net IDs and match no name in the netlist, + // so an FSM that actually depends on an input needs the legend to resolve them + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + const GateLibrary* gl = nl->get_gate_library(); + + const StateRegister sr = create_state_register(nl.get()); + const auto transition_logic = create_counter_logic(nl.get(), sr); + + Net* in0 = nl->create_net("some_input_net"); + in0->mark_global_input_net(); + + Gate* out_xor = nl->create_gate(gl->get_gate_type_by_name("XOR2"), "out_xor"); + sr.q0->add_destination(out_xor, "I0"); + in0->add_destination(out_xor, "I1"); + Net* out = nl->create_net("out"); + out->add_source(out_xor, "O"); + out->mark_global_output_net(); + + const auto config = solve_fsm::Configuration(nl.get()).with_state_register(sr.gates()).with_transition_logic(transition_logic).with_outputs({{"OUT", {out}}}); + const auto res = solve_fsm::solve_fsm(config); + ASSERT_TRUE(res.is_ok()); + + const auto str_res = res.get().to_string(); + ASSERT_TRUE(str_res.is_ok()); + const std::string str = str_res.get(); + + const std::string variable = "net_" + std::to_string(in0->get_id()); + EXPECT_NE(str.find("nets referenced in the Boolean functions below:"), std::string::npos); + EXPECT_NE(str.find(" " + variable + ": 'some_input_net' with ID " + std::to_string(in0->get_id())), std::string::npos); + + // the variable really is the net ID rather than the net name, which is what makes the legend necessary + EXPECT_NE(str.find(variable), std::string::npos); + EXPECT_EQ(nl->get_nets([&variable](const Net* n) { return n->get_name() == variable; }).size(), 0); + } + TEST_END + } + + /** + * Test that the DOT graph carries a node for every state, annotated with the outputs of that state. + * + * Functions: StateTransitionGraph::generate_dot_graph + */ + TEST_F(SolveFsmTest, check_generate_dot_graph) + { + TEST_START + if (!solver_available()) + { + GTEST_SKIP() << "no local SMT solver available"; + } + { + std::unique_ptr nl = test_utils::create_empty_netlist(); + ASSERT_NE(nl, nullptr); + + const StateRegister sr = create_state_register(nl.get()); + const auto transition_logic = create_counter_logic(nl.get(), sr); + + const auto config = solve_fsm::Configuration(nl.get()).with_state_register(sr.gates()).with_transition_logic(transition_logic).with_outputs({{"OUT", {sr.q0, sr.q1}}}); + const auto res = solve_fsm::solve_fsm(config); + ASSERT_TRUE(res.is_ok()); + const auto graph = res.get(); + + const auto dot_res = graph.generate_dot_graph(); + ASSERT_TRUE(dot_res.is_ok()); + const std::string dot = dot_res.get(); + + // solving does not write a graph on its own, rendering it is a separate step + for (u64 state = 0; state < 4; state++) + { + const std::string node = std::to_string(state) + " [label=\"" + std::to_string(state) + "\\nOUT = " + std::to_string(state) + "\"];"; + EXPECT_NE(dot.find(node), std::string::npos) << "missing node statement: " << node; + } + + // without outputs the states carry no annotation + const auto plain_config = solve_fsm::Configuration(nl.get()).with_state_register(sr.gates()).with_transition_logic(transition_logic); + const auto plain_res = solve_fsm::solve_fsm(plain_config); + ASSERT_TRUE(plain_res.is_ok()); + + const auto plain_dot_res = plain_res.get().generate_dot_graph(); + ASSERT_TRUE(plain_dot_res.is_ok()); + EXPECT_EQ(plain_dot_res.get().find("label=\"0\\nOUT"), std::string::npos); + } + TEST_END + } +} // namespace hal diff --git a/plugins/xilinx_toolbox/CMakeLists.txt b/plugins/xilinx_toolbox/CMakeLists.txt index c665bca0d17b..76a0d5e36448 100644 --- a/plugins/xilinx_toolbox/CMakeLists.txt +++ b/plugins/xilinx_toolbox/CMakeLists.txt @@ -12,4 +12,6 @@ if(PL_XILINX_TOOLBOX OR BUILD_ALL_PLUGINS) SOURCES ${XILINX_TOOLBOX_SRC} ${XILINX_TOOLBOX_PYTHON_SRC} PYDOC SPHINX_DOC_INDEX_FILE ${CMAKE_CURRENT_SOURCE_DIR}/documentation/xilinx_toolbox.rst ) + + add_subdirectory(test) endif() diff --git a/plugins/xilinx_toolbox/include/xilinx_toolbox/plugin_xilinx_toolbox.h b/plugins/xilinx_toolbox/include/xilinx_toolbox/plugin_xilinx_toolbox.h index eb33d2b6637f..8c4749be1f66 100644 --- a/plugins/xilinx_toolbox/include/xilinx_toolbox/plugin_xilinx_toolbox.h +++ b/plugins/xilinx_toolbox/include/xilinx_toolbox/plugin_xilinx_toolbox.h @@ -30,6 +30,7 @@ #pragma once +#include "hal_core/plugin_system/gui_extension_interface.h" #include "hal_core/plugin_system/plugin_interface_base.h" namespace hal @@ -45,10 +46,10 @@ namespace hal class PLUGIN_API XilinxToolboxPlugin : public BasePluginInterface { public: - /** - * @brief Default constructor for `XilinxToolboxPlugin`. + /** + * @brief Constructor for `XilinxToolboxPlugin` that registers the GUI extension. */ - XilinxToolboxPlugin() = default; + XilinxToolboxPlugin(); /** * @brief Default destructor for `XilinxToolboxPlugin`. @@ -83,4 +84,47 @@ namespace hal */ std::set get_dependencies() const override; }; + + /** + * @class GuiExtensionXilinxToolbox + * @brief GUI extension interface for the Xilinx toolbox plugin. + * + * Contributes the preprocessing steps for Xilinx primitives 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 GuiExtensionXilinxToolbox : public GuiExtensionInterface + { + public: + /** + * @brief Default constructor for `GuiExtensionXilinxToolbox`. + */ + GuiExtensionXilinxToolbox() : GuiExtensionInterface("Xilinx Toolbox") + { + } + + /** + * @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 get_context_contribution(const Netlist* nl, const std::vector& mods, const std::vector& gats, const std::vector& 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& mods, const std::vector& gats, const std::vector& nets) override; + }; } // namespace hal diff --git a/plugins/xilinx_toolbox/include/xilinx_toolbox/preprocessing.h b/plugins/xilinx_toolbox/include/xilinx_toolbox/preprocessing.h index d76a5ec13f95..880084eb4fdb 100644 --- a/plugins/xilinx_toolbox/include/xilinx_toolbox/preprocessing.h +++ b/plugins/xilinx_toolbox/include/xilinx_toolbox/preprocessing.h @@ -33,8 +33,11 @@ #include "hal_core/defines.h" #include "hal_core/utilities/result.h" +#include + namespace hal { + class Gate; class Netlist; namespace xilinx_toolbox @@ -45,19 +48,22 @@ namespace hal * Replaces `LUT6_2` with a `LUT6` and a `LUT5` gate if the respective outputs of the `LUT6_2` are actually used, i.e., connected to other gates. * * @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 The number of split `LUT6_2` gates on success, an error otherwise. */ - Result split_luts(Netlist* nl); + Result split_luts(Netlist* nl, const std::vector& gates = {}); /** * @brief Split shift register primitives and replaces them with equivalent flip-flops chains. * - * Currently only implemented for gate type `SRL16E`. + * Currently only implemented for gate types `SRL16E` and `SRLC32E`. + * The created flip-flops are assigned to the module of the shift register gate that they replace. * * @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 The number of split shift registers on success, an error otherwise. */ - Result split_shift_registers(Netlist* nl); + Result split_shift_registers(Netlist* nl, const std::vector& gates = {}); /** * @brief Parse an `.xdc` file and extract the position LOC and BEL data of each gate. diff --git a/plugins/xilinx_toolbox/include/xilinx_toolbox/utils/gui_layout_locker.h b/plugins/xilinx_toolbox/include/xilinx_toolbox/utils/gui_layout_locker.h new file mode 100644 index 000000000000..c1b4a531b784 --- /dev/null +++ b/plugins/xilinx_toolbox/include/xilinx_toolbox/utils/gui_layout_locker.h @@ -0,0 +1,72 @@ +// MIT License +// +// Copyright (c) 2019 Ruhr University Bochum, Chair for Embedded Security. All Rights reserved. +// Copyright (c) 2019 Marc Fyrbiak, Sebastian Wallat, Max Hoffmann ("ORIGINAL AUTHORS"). All rights reserved. +// Copyright (c) 2021 Max Planck Institute for Security and Privacy. All Rights reserved. +// Copyright (c) 2021 Jörn Langheinrich, Julian Speith, Nils Albartus, René Walendy, Simon Klix ("ORIGINAL AUTHORS"). All Rights reserved. +// +// Permission is hereby granted, free of charge, to any person obtaining a copy +// of this software and associated documentation files (the "Software"), to deal +// in the Software without restriction, including without limitation the rights +// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +// copies of the Software, and to permit persons to whom the Software is +// furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all +// copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +// SOFTWARE. + +/** + * @file gui_layout_locker.h + * @brief This file contains a helper that suppresses layout updates of the GUI. + */ + +#pragma once + +#include "hal_core/defines.h" + +namespace hal +{ + class UIPluginInterface; + + namespace xilinx_toolbox + { + /** + * @class GuiLayoutLocker + * @brief Suppresses layout updates of the GUI for as long as the object exists. + * + * A netlist modification that touches many gates makes the GUI re-layout its graph views once per change, + * which can dominate the runtime of the modification itself. Holding a locker defers those updates until it + * goes out of scope, at which point every affected view is updated once. + * + * Locks nest, so it is safe to hold more than one at a time. Does nothing if no GUI is running, which makes + * it safe to use from code that also runs headless. + */ + class GuiLayoutLocker + { + public: + /** + * @brief Suppress layout updates of the GUI until the locker is destroyed. + */ + GuiLayoutLocker(); + + /** + * @brief Release the lock and let the GUI update the views that changed in the meantime. + */ + ~GuiLayoutLocker(); + + GuiLayoutLocker(const GuiLayoutLocker&) = delete; + GuiLayoutLocker& operator=(const GuiLayoutLocker&) = delete; + + private: + UIPluginInterface* m_gui_plugin; + }; + } // namespace xilinx_toolbox +} // namespace hal diff --git a/plugins/xilinx_toolbox/python/python_bindings.cpp b/plugins/xilinx_toolbox/python/python_bindings.cpp index 46ebbb50bb16..333a6db5430c 100644 --- a/plugins/xilinx_toolbox/python/python_bindings.cpp +++ b/plugins/xilinx_toolbox/python/python_bindings.cpp @@ -82,8 +82,8 @@ namespace hal m.def( "split_luts", - [](Netlist* nl) -> std::optional { - auto res = xilinx_toolbox::split_luts(nl); + [](Netlist* nl, const std::vector& gates) -> std::optional { + auto res = xilinx_toolbox::split_luts(nl, gates); if (res.is_ok()) { return res.get(); @@ -95,19 +95,21 @@ namespace hal } }, py::arg("nl"), + py::arg("gates") = std::vector(), R"( Split LUTs with two outputs into two separate LUT gates. Replaces ``LUT6_2`` with a ``LUT6`` and a ``LUT5`` gate if the respective outputs of the ``LUT6_2`` are actually used, i.e., connected to other gates. :param hal_py.Netlist nl: The netlist to operate on. + :param list[hal_py.Gate] gates: The gates to consider. Defaults to an empty list, in which case all gates of the netlist are considered. :returns: The number of split ``LUT6_2`` gates on success, ``None`` otherwise. :rtype: int or None )"); m.def( "split_shift_registers", - [](Netlist* nl) -> std::optional { - auto res = xilinx_toolbox::split_shift_registers(nl); + [](Netlist* nl, const std::vector& gates) -> std::optional { + auto res = xilinx_toolbox::split_shift_registers(nl, gates); if (res.is_ok()) { return res.get(); @@ -119,11 +121,14 @@ namespace hal } }, py::arg("nl"), + py::arg("gates") = std::vector(), R"( Split shift register primitives and replaces them with equivalent flip-flops chains. - Currently only implemented for gate type ``SRL16E``. + Currently only implemented for gate types ``SRL16E`` and ``SRLC32E``. + The created flip-flops are assigned to the module of the shift register gate that they replace. :param hal_py.Netlist nl: The netlist to operate on. + :param list[hal_py.Gate] gates: The gates to consider. Defaults to an empty list, in which case all gates of the netlist are considered. :returns: The number of split shift registers on success, ``None`` otherwise. :rtype: int or None )"); diff --git a/plugins/xilinx_toolbox/src/plugin_xilinx_toolbox.cpp b/plugins/xilinx_toolbox/src/plugin_xilinx_toolbox.cpp index fc959c775aec..d9a11239ab8f 100644 --- a/plugins/xilinx_toolbox/src/plugin_xilinx_toolbox.cpp +++ b/plugins/xilinx_toolbox/src/plugin_xilinx_toolbox.cpp @@ -1,7 +1,20 @@ #include "xilinx_toolbox/plugin_xilinx_toolbox.h" +#include "hal_core/netlist/gate.h" +#include "hal_core/netlist/module.h" +#include "hal_core/netlist/netlist.h" +#include "xilinx_toolbox/preprocessing.h" +#include "xilinx_toolbox/utils/gui_layout_locker.h" + +#include + namespace hal { + XilinxToolboxPlugin::XilinxToolboxPlugin() + { + m_extensions.push_back(new GuiExtensionXilinxToolbox()); + } + extern std::unique_ptr create_plugin_instance() { return std::make_unique(); @@ -26,4 +39,121 @@ namespace hal { return {}; } + + namespace + { + /** + * The gates of the selected modules, including those of their submodules, together with the selected gates. + * Duplicates are dropped, which matters when a gate is selected both directly and through a parent module. + */ + std::vector gates_from_selection(Netlist* nl, const std::vector& mods, const std::vector& gats) + { + std::vector res; + std::unordered_set seen; + + const auto collect = [&res, &seen](Gate* g) { + if (g != nullptr && seen.insert(g).second) + { + res.push_back(g); + } + }; + + for (u32 id : gats) + { + collect(nl->get_gate_by_id(id)); + } + + for (u32 id : mods) + { + if (const Module* m = nl->get_module_by_id(id); m != nullptr) + { + for (Gate* g : m->get_gates(nullptr, true)) + { + collect(g); + } + } + } + + return res; + } + } // namespace + + std::vector GuiExtensionXilinxToolbox::get_context_contribution(const Netlist*, const std::vector& mods, const std::vector& gats, const std::vector&) + { + std::vector retval; + + const auto add = [this, &retval](const std::string& tag, const std::string& entry) { + ContextMenuContribution cmc; + cmc.mContributer = this; + cmc.mTagname = tag; + cmc.mEntry = entry; + retval.push_back(cmc); + }; + + // a selection is what the user is pointing at, so do not offer to run on the entire netlist next to it + if (!mods.empty() || !gats.empty()) + { + add("split_luts_selection", "Split LUTs of selection"); + add("split_shift_registers_selection", "Split shift registers of selection"); + } + else + { + add("split_luts_netlist", "Split LUTs of netlist"); + add("split_shift_registers_netlist", "Split shift registers of netlist"); + } + + return retval; + } + + void GuiExtensionXilinxToolbox::execute_function(std::string tag, Netlist* nl, const std::vector& mods, const std::vector& gats, const std::vector&) + { + if (nl == nullptr) + { + log_warning("xilinx_toolbox", "cannot run preprocessing: no netlist loaded."); + return; + } + + // deleting or replacing a gate makes the GUI re-layout its graph views, which would otherwise happen once + // per gate and dominate the runtime of the preprocessing itself + const xilinx_toolbox::GuiLayoutLocker layout_locker; + + // an empty scope makes the preprocessing functions consider the entire netlist + std::vector scope; + if (tag == "split_luts_selection" || tag == "split_shift_registers_selection") + { + scope = gates_from_selection(nl, mods, gats); + if (scope.empty()) + { + log_warning("xilinx_toolbox", "cannot run preprocessing on the selection: no gates selected."); + return; + } + } + + if (tag == "split_luts_selection" || tag == "split_luts_netlist") + { + if (const auto res = xilinx_toolbox::split_luts(nl, scope); res.is_error()) + { + log_error("xilinx_toolbox", "failed to split LUTs: {}", res.get_error().get()); + } + else + { + log_info("xilinx_toolbox", "split {} LUTs.", res.get()); + } + } + else if (tag == "split_shift_registers_selection" || tag == "split_shift_registers_netlist") + { + if (const auto res = xilinx_toolbox::split_shift_registers(nl, scope); res.is_error()) + { + log_error("xilinx_toolbox", "failed to split shift registers: {}", res.get_error().get()); + } + else + { + log_info("xilinx_toolbox", "split {} shift registers.", res.get()); + } + } + else + { + log_warning("xilinx_toolbox", "unknown context menu tag '{}'.", tag); + } + } } // namespace hal diff --git a/plugins/xilinx_toolbox/src/preprocessing.cpp b/plugins/xilinx_toolbox/src/preprocessing.cpp index 9fd1b9ece48a..f55d83d0ca8a 100644 --- a/plugins/xilinx_toolbox/src/preprocessing.cpp +++ b/plugins/xilinx_toolbox/src/preprocessing.cpp @@ -4,11 +4,39 @@ #include "hal_core/netlist/netlist.h" #include "xilinx_toolbox/plugin_xilinx_toolbox.h" +#include + namespace hal { namespace xilinx_toolbox { - Result split_luts(Netlist* nl) + namespace + { + /** + * All gates within the caller's scope that also pass the given type filter. An empty scope means the + * entire netlist, which is what the preprocessing functions default to. The scope only ever restricts + * which gates are considered, it never widens what a function operates on. + */ + std::vector gates_in_scope(const Netlist* nl, const std::vector& gates, const std::function& type_filter) + { + if (gates.empty()) + { + return nl->get_gates(type_filter); + } + + std::vector res; + for (auto* g : gates) + { + if (type_filter(g)) + { + res.push_back(g); + } + } + return res; + } + } // namespace + + Result split_luts(Netlist* nl, const std::vector& gates) { u32 deleted_gates = 0; u32 new_gates = 0; @@ -17,7 +45,7 @@ namespace hal const auto lut6_type = nl->get_gate_library()->get_gate_type_by_name("LUT6"); const auto lut5_type = nl->get_gate_library()->get_gate_type_by_name("LUT5"); - const auto lut6_2_gates = nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "LUT6_2"; }); + const auto lut6_2_gates = gates_in_scope(nl, gates, [](const Gate* g) { return g->get_type()->get_name() == "LUT6_2"; }); for (const auto& g : lut6_2_gates) { @@ -38,7 +66,8 @@ namespace hal continue; } - if (o5->get_num_of_destinations() > 0) + // 'O5' or 'O6' may be entirely unconnected, which is the common case this function is meant to handle + if (o5 != nullptr && o5->get_num_of_destinations() > 0) { // create LUT5 auto* lut5 = nl->create_gate(lut5_type, g->get_name() + "_split_O5"); @@ -64,7 +93,7 @@ namespace hal o5->add_source(lut5, "O"); } - if (o6->get_num_of_destinations() > 0) + if (o6 != nullptr && o6->get_num_of_destinations() > 0) { // create LUT6 auto* lut6 = nl->create_gate(lut6_type, g->get_name() + "_split_O6"); @@ -109,7 +138,7 @@ namespace hal return OK(deleted_gates); } - Result split_shift_registers(Netlist* nl) + Result split_shift_registers(Netlist* nl, const std::vector& gates) { u32 deleted_gates = 0; u32 new_gates = 0; @@ -122,7 +151,7 @@ namespace hal } // iterate over all shift registers of type 'SRL16E' or 'SRLC32E' - for (const auto& gate : nl->get_gates([](const auto& g) { return g->get_type()->get_name() == "SRL16E" || g->get_type()->get_name() == "SRLC32E"; })) + for (const auto& gate : gates_in_scope(nl, gates, [](const Gate* g) { return g->get_type()->get_name() == "SRL16E" || g->get_type()->get_name() == "SRLC32E"; })) { auto control_pins = gate->get_type()->get_pins([](const auto& pg) { return (pg->get_direction() == PinDirection::input) && (pg->get_type() == PinType::control); }); if (control_pins.size() != 4 && gate->get_type()->get_name() == "SRLC16E" || control_pins.size() != 5 && gate->get_type()->get_name() == "SRLC32E") @@ -242,6 +271,12 @@ namespace hal Gate* new_gate = nl->create_gate(ff_gt, ff_name); new_gates++; + // keep the replacement within the module of the gate it replaces instead of the top module + if (auto* mod = gate->get_module(); !mod->is_top_module()) + { + mod->assign_gate(new_gate); + } + clk_in->add_destination(new_gate, "C"); enable_in->add_destination(new_gate, "CE"); diff --git a/plugins/xilinx_toolbox/src/utils/gui_layout_locker.cpp b/plugins/xilinx_toolbox/src/utils/gui_layout_locker.cpp new file mode 100644 index 000000000000..2121e692215e --- /dev/null +++ b/plugins/xilinx_toolbox/src/utils/gui_layout_locker.cpp @@ -0,0 +1,51 @@ +// MIT License +// +// Copyright (c) 2019 Ruhr University Bochum, Chair for Embedded Security. All Rights reserved. +// Copyright (c) 2019 Marc Fyrbiak, Sebastian Wallat, Max Hoffmann ("ORIGINAL AUTHORS"). All rights reserved. +// Copyright (c) 2021 Max Planck Institute for Security and Privacy. All Rights reserved. +// Copyright (c) 2021 Jörn Langheinrich, Julian Speith, Nils Albartus, René Walendy, Simon Klix ("ORIGINAL AUTHORS"). All Rights reserved. +// +// Permission is hereby granted, free of charge, to any person obtaining a copy +// of this software and associated documentation files (the "Software"), to deal +// in the Software without restriction, including without limitation the rights +// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +// copies of the Software, and to permit persons to whom the Software is +// furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all +// copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +// SOFTWARE. + +#include "xilinx_toolbox/utils/gui_layout_locker.h" + +#include "hal_core/plugin_system/plugin_interface_ui.h" +#include "hal_core/plugin_system/plugin_manager.h" + +namespace hal +{ + namespace xilinx_toolbox + { + GuiLayoutLocker::GuiLayoutLocker() : m_gui_plugin(plugin_manager::get_plugin_instance("hal_gui")) + { + if (m_gui_plugin != nullptr) + { + m_gui_plugin->set_layout_locker(true); + } + } + + GuiLayoutLocker::~GuiLayoutLocker() + { + if (m_gui_plugin != nullptr) + { + m_gui_plugin->set_layout_locker(false); + } + } + } // namespace xilinx_toolbox +} // namespace hal diff --git a/plugins/xilinx_toolbox/test/CMakeLists.txt b/plugins/xilinx_toolbox/test/CMakeLists.txt new file mode 100644 index 000000000000..f0ef3240f3ef --- /dev/null +++ b/plugins/xilinx_toolbox/test/CMakeLists.txt @@ -0,0 +1,13 @@ +if(BUILD_TESTS) + include_directories(${gtest_SOURCE_DIR}/include ${gtest_SOURCE_DIR} ${CMAKE_SOURCE_DIR}/include ${CMAKE_SOURCE_DIR}/tests ${CMAKE_SOURCE_DIR}/plugins/xilinx_toolbox/include ${CMAKE_SOURCE_DIR}/plugins/hgl_parser/include) + + add_executable(runTest-xilinx_toolbox xilinx_toolbox.cpp) + + target_link_libraries(runTest-xilinx_toolbox xilinx_toolbox hgl_parser pthread gtest hal::core hal::netlist test_utils) + + add_test(runTest-xilinx_toolbox ${CMAKE_BINARY_DIR}/bin/hal_plugins/runTest-xilinx_toolbox --gtest_output=xml:${CMAKE_BINARY_DIR}/gtestresults-runBasicTests.xml) + + if(${CMAKE_BUILD_TYPE} STREQUAL "Debug") + add_sanitizers(runTest-xilinx_toolbox) + endif() +endif() diff --git a/plugins/xilinx_toolbox/test/xilinx_toolbox.cpp b/plugins/xilinx_toolbox/test/xilinx_toolbox.cpp new file mode 100644 index 000000000000..73760ea163d3 --- /dev/null +++ b/plugins/xilinx_toolbox/test/xilinx_toolbox.cpp @@ -0,0 +1,317 @@ +#include "hal_core/netlist/gate.h" +#include "hal_core/netlist/module.h" +#include "hal_core/netlist/net.h" +#include "hal_core/netlist/netlist.h" +#include "hal_core/netlist/netlist_factory.h" +#include "hgl_parser/hgl_parser.h" +#include "netlist_test_utils.h" +#include "xilinx_toolbox/plugin_xilinx_toolbox.h" +#include "xilinx_toolbox/preprocessing.h" + +namespace hal +{ + class XilinxToolboxTest : public ::testing::Test + { + protected: + std::unique_ptr m_gl_owner; + GateLibrary* m_gl = nullptr; + + virtual void SetUp() + { + NO_COUT_BLOCK; + test_utils::init_log_channels(); + test_utils::create_sandbox_directory(); + + // the gate library manager relies on the parser plugins being registered, so parse the library directly + const std::string path = utils::get_base_directory().string() + "/share/hal/gate_libraries/XILINX_UNISIM.hgl"; + + HGLParser parser; + if (auto res = parser.parse(path); res.is_ok()) + { + m_gl_owner = res.get(); + m_gl = m_gl_owner.get(); + } + } + + virtual void TearDown() + { + test_utils::remove_sandbox_directory(); + } + + /** + * A netlist using the Xilinx UNISIM gate library, with GND and VCC gates already marked. + */ + std::unique_ptr create_netlist(Net** gnd_net, Net** vcc_net) + { + if (m_gl == nullptr) + { + return nullptr; + } + + auto nl = netlist_factory::create_netlist(m_gl); + if (nl == nullptr) + { + return nullptr; + } + + Gate* gnd_gate = nl->create_gate(m_gl->get_gate_type_by_name("GND"), "gnd"); + nl->mark_gnd_gate(gnd_gate); + *gnd_net = nl->create_net("gnd_net"); + (*gnd_net)->add_source(gnd_gate, "G"); + + Gate* vcc_gate = nl->create_gate(m_gl->get_gate_type_by_name("VCC"), "vcc"); + nl->mark_vcc_gate(vcc_gate); + *vcc_net = nl->create_net("vcc_net"); + (*vcc_net)->add_source(vcc_gate, "P"); + + return nl; + } + }; + + /** + * Test that the gate scope restricts which 'LUT6_2' gates are split, and that a 'LUT6_2' with an unconnected + * output is handled gracefully. + * + * Functions: split_luts + */ + TEST_F(XilinxToolboxTest, check_split_luts_scoped) + { + TEST_START + { + Net *gnd_net = nullptr, *vcc_net = nullptr; + std::unique_ptr nl = create_netlist(&gnd_net, &vcc_net); + ASSERT_NE(nl, nullptr); + + GateType* lut6_2 = m_gl->get_gate_type_by_name("LUT6_2"); + ASSERT_NE(lut6_2, nullptr); + + std::vector luts; + for (const std::string& name : {"l0", "l1"}) + { + Gate* l = nl->create_gate(lut6_2, name); + ASSERT_TRUE(l->set_init_data({"ABCDEF0123456789"}).is_ok()); + + for (u32 i = 0; i < 6; i++) + { + Net* n = nl->create_net(name + "_i" + std::to_string(i)); + n->add_destination(l, "I" + std::to_string(i)); + n->mark_global_input_net(); + } + + for (const std::string& pin : {"O5", "O6"}) + { + Net* n = nl->create_net(name + "_" + pin); + n->add_source(l, pin); + n->mark_global_output_net(); + // the outputs have to be used, otherwise there is nothing to split off + n->add_destination(nl->create_gate(m_gl->get_gate_type_by_name("INV"), name + "_" + pin + "_sink"), "I"); + } + + luts.push_back(l); + } + + // only the LUT within the scope is split into a 'LUT6' and a 'LUT5' + auto res = xilinx_toolbox::split_luts(nl.get(), {luts.at(0)}); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 1); + + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "LUT6_2"; }).size(), 1); + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "LUT6"; }).size(), 1); + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "LUT5"; }).size(), 1); + + // without a scope the remaining LUT is split as well + res = xilinx_toolbox::split_luts(nl.get()); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 1); + + EXPECT_TRUE(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "LUT6_2"; }).empty()); + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "LUT6"; }).size(), 2); + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "LUT5"; }).size(), 2); + } + { + // a 'LUT6_2' that only uses 'O6' is split into a single 'LUT6' instead of crashing + Net *gnd_net = nullptr, *vcc_net = nullptr; + std::unique_ptr nl = create_netlist(&gnd_net, &vcc_net); + ASSERT_NE(nl, nullptr); + + Gate* l = nl->create_gate(m_gl->get_gate_type_by_name("LUT6_2"), "l0"); + ASSERT_TRUE(l->set_init_data({"ABCDEF0123456789"}).is_ok()); + + for (u32 i = 0; i < 6; i++) + { + Net* n = nl->create_net("i" + std::to_string(i)); + n->add_destination(l, "I" + std::to_string(i)); + n->mark_global_input_net(); + } + + Net* o6 = nl->create_net("o6"); + o6->add_source(l, "O6"); + o6->add_destination(nl->create_gate(m_gl->get_gate_type_by_name("INV"), "sink"), "I"); + + auto res = xilinx_toolbox::split_luts(nl.get()); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 1); + + EXPECT_TRUE(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "LUT6_2"; }).empty()); + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "LUT6"; }).size(), 1); + EXPECT_TRUE(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "LUT5"; }).empty()); + } + TEST_END + } + + /** + * Test that the gate scope restricts which shift registers are split, and that the created flip-flops are assigned + * to the module of the gate they replace. + * + * Functions: split_shift_registers + */ + TEST_F(XilinxToolboxTest, check_split_shift_registers_scoped) + { + // creates an 'SRL16E' gate with all control pins tied to GND, i.e. a shift register of length one + auto create_srl = [](Netlist* nl, GateLibrary* gl, const std::string& name, Net* gnd_net, Net* vcc_net) -> Gate* { + Gate* srl = nl->create_gate(gl->get_gate_type_by_name("SRL16E"), name); + + for (u32 i = 0; i < 4; i++) + { + gnd_net->add_destination(srl, "A" + std::to_string(i)); + } + vcc_net->add_destination(srl, "CE"); + + Net* clk = nl->create_net(name + "_clk"); + clk->add_destination(srl, "CLK"); + clk->mark_global_input_net(); + + Net* d = nl->create_net(name + "_d"); + d->add_destination(srl, "D"); + d->mark_global_input_net(); + + Net* q = nl->create_net(name + "_q"); + q->add_source(srl, "Q"); + q->add_destination(nl->create_gate(gl->get_gate_type_by_name("INV"), name + "_sink"), "I"); + + return srl; + }; + + TEST_START + { + Net *gnd_net = nullptr, *vcc_net = nullptr; + std::unique_ptr nl = create_netlist(&gnd_net, &vcc_net); + ASSERT_NE(nl, nullptr); + + Gate* s0 = create_srl(nl.get(), m_gl, "s0", gnd_net, vcc_net); + Gate* s1 = create_srl(nl.get(), m_gl, "s1", gnd_net, vcc_net); + + // only the shift register within the scope is replaced by flip-flops + auto res = xilinx_toolbox::split_shift_registers(nl.get(), {s0}); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 1); + + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "SRL16E"; }).size(), 1); + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "FDE"; }).size(), 1); + + // without a scope the remaining shift register is replaced as well + res = xilinx_toolbox::split_shift_registers(nl.get()); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 1); + + EXPECT_TRUE(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "SRL16E"; }).empty()); + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "FDE"; }).size(), 2); + } + { + // the created flip-flops belong to the module of the shift register, not to the top module + Net *gnd_net = nullptr, *vcc_net = nullptr; + std::unique_ptr nl = create_netlist(&gnd_net, &vcc_net); + ASSERT_NE(nl, nullptr); + + Gate* s0 = create_srl(nl.get(), m_gl, "s0", gnd_net, vcc_net); + + Module* mod = nl->create_module("mod", nl->get_top_module(), {s0}); + ASSERT_NE(mod, nullptr); + + auto res = xilinx_toolbox::split_shift_registers(nl.get(), {s0}); + ASSERT_TRUE(res.is_ok()); + EXPECT_EQ(res.get(), 1); + + auto ffs = nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "FDE"; }); + ASSERT_EQ(ffs.size(), 1); + EXPECT_EQ(ffs.front()->get_module(), mod); + } + TEST_END + } + + /** + * Test the context menu entries contributed to the GUI. + * + * Functions: GuiExtensionXilinxToolbox::get_context_contribution, GuiExtensionXilinxToolbox::execute_function + */ + TEST_F(XilinxToolboxTest, check_gui_extension) + { + TEST_START + { + XilinxToolboxPlugin plugin; + + GuiExtensionXilinxToolbox* gui = nullptr; + for (auto* ext : plugin.get_extensions()) + { + if (auto* casted = dynamic_cast(ext); casted != nullptr) + { + gui = casted; + } + } + ASSERT_NE(gui, nullptr); + + Net *gnd_net = nullptr, *vcc_net = nullptr; + std::unique_ptr nl = create_netlist(&gnd_net, &vcc_net); + ASSERT_NE(nl, nullptr); + + std::vector luts; + for (const std::string& name : {"l0", "l1"}) + { + Gate* l = nl->create_gate(m_gl->get_gate_type_by_name("LUT6_2"), name); + ASSERT_TRUE(l->set_init_data({"ABCDEF0123456789"}).is_ok()); + + for (u32 i = 0; i < 6; i++) + { + Net* n = nl->create_net(name + "_i" + std::to_string(i)); + n->add_destination(l, "I" + std::to_string(i)); + n->mark_global_input_net(); + } + + Net* o6 = nl->create_net(name + "_o6"); + o6->add_source(l, "O6"); + o6->add_destination(nl->create_gate(m_gl->get_gate_type_by_name("INV"), name + "_sink"), "I"); + + luts.push_back(l); + } + + // without a selection the netlist-wide entries are offered + auto without_selection = gui->get_context_contribution(nl.get(), {}, {}, {}); + ASSERT_EQ(without_selection.size(), 2); + for (const auto& cmc : without_selection) + { + EXPECT_NE(cmc.mTagname.find("_netlist"), std::string::npos); + } + + // with a selection only the entries operating on it are offered + auto with_selection = gui->get_context_contribution(nl.get(), {}, {luts.at(0)->get_id()}, {}); + ASSERT_EQ(with_selection.size(), 2); + for (const auto& cmc : with_selection) + { + EXPECT_EQ(cmc.mContributer, gui); + EXPECT_FALSE(cmc.mEntry.empty()); + EXPECT_NE(cmc.mTagname.find("_selection"), std::string::npos); + } + + // running the entry on the selected gate splits only that LUT + gui->execute_function("split_luts_selection", nl.get(), {}, {luts.at(0)->get_id()}, {}); + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "LUT6_2"; }).size(), 1); + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "LUT6"; }).size(), 1); + + // the netlist-wide entry then splits the remaining one + gui->execute_function("split_luts_netlist", nl.get(), {}, {}, {}); + EXPECT_TRUE(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "LUT6_2"; }).empty()); + EXPECT_EQ(nl->get_gates([](const Gate* g) { return g->get_type()->get_name() == "LUT6"; }).size(), 2); + } + TEST_END + } +} // namespace hal diff --git a/wiki_images/examples/fsm.png b/wiki_images/examples/fsm.png deleted file mode 100644 index 98b3e050ba8b..000000000000 Binary files a/wiki_images/examples/fsm.png and /dev/null differ