Rework the FSM solver, scope the preprocessing functions, and clean up the examples - #649
Merged
Merged
Conversation
Net::remove_source(Gate*, const GatePin*) and its destination counterpart dereferenced the pin without checking it, so passing a nullptr crashed. The string overloads never reach that state because they reject unknown pin names first, but the pin overloads are called directly by netlist_preprocessing and netlist_utils, and they are exposed to Python, where net.remove_source(g, None) terminated the interpreter. Their is_a_source and is_a_destination counterparts already guarded both arguments, so add the same guards for consistency. While looking up an endpoint, Net and Gate compared the pin by value rather than by pointer identity, so a distinct but equal GatePin of another gate type would match. All pins of a gate come from its gate type, so identity is what these lookups mean. Net::operator== keeps comparing by value, since it compares endpoints of two different nets that do not share pin objects. Add direct tests for the pin overloads of remove_source and remove_destination covering removal, the wrong pin, a nullptr pin, a nullptr gate, a gate that is not connected, and removing twice. They previously had no direct coverage at all, which the removed TODOs asked for. The remaining six TODOs were stale: the string overloads, the endpoint overloads, and both pin overloads of is_a_source and is_a_destination are already covered. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Five of the seven Python binding TODOs in plugin_manager.h are addressed: * get_cli_plugin_flags() and get_ui_plugin_flags() are bound and return a dict. * add_model_changed_callback() and remove_model_changed_callback() are bound, so a Python callable can be notified about loaded and unloaded plugins. * get_plugin_instance() gained the initialize and silent parameters. The other half of that TODO, bindings for different plugin types, needs no work: pybind11 already returns the plugin's own type once the Python module of that plugin has been imported, and the base interface otherwise. The docstring now says so. The remaining two TODOs, add_existing_options_description() and get_cli_plugin_options(), both take or return a ProgramOptions, which has no Python bindings at all. They keep a TODO that names that prerequisite instead of just saying "TODO Python binding". Verified from Python: the callback fires once per plugin on load and stops after removal, both flag getters return a dict, get_plugin_instance(name, False) skips initialization, and get_plugin_instance(name, True, True) returns None for an unknown plugin without logging an error. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Completes the Python bindings of plugin_manager by binding the types it depends
on:
* ProgramOptions and ProgramArguments, needed by add_existing_options_description()
and get_cli_plugin_options().
* FacExtensionInterface including its Feature enum, and plugin_manager::PluginFeature,
needed by get_plugin_features().
With those in place, add_existing_options_description(), get_cli_plugin_options(),
get_plugin_path(), has_valid_file_extension(), and get_plugin_features() are bound,
and plugin_manager.h no longer carries any TODO.
Two points worth noting:
ProgramOptions::add() takes its flags as a std::initializer_list, which cannot be
built from a container at runtime and is therefore not bindable. Changing the
parameter to a std::vector is not an option either, because a call such as
add({"-h", "--help"}, "...") then becomes ambiguous: std::string has an
iterator-pair constructor, so the braced list is a viable argument for the
single-flag overload as well. The vector-based implementation is therefore
exposed under the new name add_flags(), to which both existing overloads
delegate, so that all 87 call sites keep working unchanged. Python binds
add_flags() as add().
ProgramArguments::get_original_arguments() is deliberately not bound.
ProgramArguments stores the argv pointer without owning the strings, which no
longer exist once parse() has returned to Python, so exposing it would hand out
a dangling pointer.
Verified from Python: options can be added with one or several flags, parsed
from an argument list, queried, removed, and merged into another set; plugin
features report the parser of the Verilog plugin with its .v extension.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Selecting a module made the GUI hang for minutes on large designs. Selecting the top module of the OpenTitan benchmark, which holds all of its 424866 gates directly, froze HAL indefinitely. ModuleModel::populateTree() correctly brackets the population with beginResetModel() and endResetModel(), but createChildItem() emitted beginInsertRows()/endInsertRows() for every single item in between. Besides being undefined per the QAbstractItemModel contract, it made the attached SelectionTreeProxyModel re-map its source rows once per inserted row, which is quadratic in the number of items. Measured with a QSortFilterProxyModel over a plain list model, populating with a row signal per item takes 0.84 s for 50000 items, 3.29 s for 100000 and 14.71 s for 200000, while populating within a plain model reset is too fast to measure. Extrapolated to 424866 items that is more than a minute of pure proxy bookkeeping for a bare model, and considerably more for real tree items. createChildItem() and removeChildItem() now skip their row signals while a reset is in progress, since the reset already tells the views to re-read everything. Both functions also reset mIsModifying to false unconditionally, clobbering the true that populateTree() had set, so the guard in ModuleWidget was only in effect for the very first item. They now restore the previous value. mIsModifying was never initialized in the constructor either. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Unfolding the top module of the OpenTitan benchmark, which holds all of its 424866 gates directly, kept the GUI busy for seconds. A sample of the GUI taken while unfolding shows 5094 of 8032 main thread samples below QTreeViewPrivate::itemHeight, reached from updateScrollBars() when the expand is applied. Without uniform row heights that function measures rows individually through QTreeView::indexRowSizeHint(), which asks the item delegate for a size hint, which lays out and shapes the item text. 2345 samples end up in QTextEngine::shapeText() and 821 in CTFontGetGlyphsForCharacters(), so the view spends most of the unfold shaping gate names just to learn how tall their rows are. All rows of these views are plain single line text in one font, so their height is constant and QTreeViewPrivate::itemHeight() can return it directly. Applies to the four views that can hold one item per gate or net of a netlist: the selection details tree, the module elements tree, the module widget tree and the module pins tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Add the S-box database from the HAWKEYE artifacts to the plugin and copy it into the build directory at build time, analogous to how the gate library definitions are handled. The plugin's .gitignore is an allowlist, so the database needs an explicit exception to be tracked. Turn the placeholder py/hawkeye.py of the crypto_trojan example into a working script that detects state register candidates, isolates the round function, and identifies its S-box. On this netlist it reports AES. Both crypto_trojan and toy_cipher shipped outdated copies of their gate library that predate the c_* gate type properties: 101 of 163 cells in lsi_10k and 44 of 273 in XILINX_UNISIM were missing them. As a result, any analysis selecting gates by property found nothing in those projects. In crypto_trojan this made netlist_preprocessing::unify_ff_outputs fail with "gate library does not contain an inverter gate", leaving the FD1 Q/QN dual outputs in place and causing errors during S-box identification. Both libraries are refreshed from the shipped definitions. Also correct the documentation of identify_sbox: it returns an empty string when no S-box of the database matches, and only reports an error if the candidate could not be analyzed. Both the C++ and the Python documentation previously described a no-match as an error.
Selecting the top module of the OpenTitan benchmark took over a second. A sample of the GUI shows ModuleModel::populateTree() running three times for a single selection, 321, 313 and 307 samples of 1358 in that branch. Once for the selection details tree and twice for the module elements tree, because SelectionDetailsWidget::handleSelectionUpdate() drives the details widget directly and also populates the selection tree, whose current index change drives the very same details widget through triggerSelection(). Each of those runs builds one tree item per gate and per net of the module, about 825000 items for the OpenTitan top module. Two thirds of the time goes into the net items in moduleAssignNets(), the rest into the gate items in addRecursively() and into destroying the previous tree. ModuleElementsTree already tracks the module it displays, so it can skip the rebuild if it is asked for the same one again. The model keeps itself up to date through the netlist relay, so the rebuild is not what refreshes it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A sample of a HAWKEYE S-box identification run spent 96% of the main thread in BooleanFunction::compute_truth_table(), which evaluates the function once per truth table row. Three fixes, measured on a 50 node function over 8 variables, 256 rows per truth table, 5.17 ms per table before: BooleanFunction::operator< compared two functions of equal node count by building their reverse polish notation strings and comparing those. The symbolic state keeps its variables in a std::map<BooleanFunction, BooleanFunction>, so every variable lookup during evaluation formatted several strings, and since all keys are single variable nodes the node count never discriminated. Comparing the nodes directly is equivalent, Node::operator< is already a field wise comparison consistent with Node::operator==. Neither of the two maps keyed by BooleanFunction is ever iterated, so the changed order is not observable. 5.17 ms -> 4.56 ms. SymbolicExecution::constant_propagation() copied the value vector of every operand twice, once into a local and once into the vector of values. Some of the cases modify the values in place so one copy is still needed. 4.56 ms -> 3.94 ms. BooleanFunction::evaluate() validated the input sizes by comparing every input name against every node, which is a string comparison per pair on every call. Walking the nodes once and looking up each variable is equivalent. 3.94 ms -> 3.81 ms. That is 26% overall. The remaining cost is dominated by allocation, every node evaluation builds a std::vector<BooleanFunction> of operands and a BooleanFunction result, each owning a vector of nodes that own a string and a vector of values. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Three corrections to constant folding of Boolean functions, all found while adding evaluation tests for the operators that had none. Addition and subtraction masked their result to 32 bit before truncating it to the width of the operands, so every addition or subtraction of 33 to 64 bit operands silently lost its upper bits. A 33 bit 2^31 + 2^31 returned 0 instead of 2^32, and a 33 bit 0 - 1 returned 0xffffffff instead of 0x1ffffffff. The mask is not only too narrow but redundant, since Const() already takes exactly as many bits as the operands are wide. Eq returned a definite "not equal" when an undefined bit was involved, even though the two values would have been equal had that bit turned out the other way. It now returns X in that case, unless another bit already tells the values apart, which is how the other comparisons already behave. Sdiv, Udiv, Srem and Urem were not implemented and made evaluation of any function containing them fail. They are translated to bvsdiv, bvudiv, bvsrem and bvurem when handed to an SMT solver, so the folding follows those definitions, including a division by zero yielding all ones as the quotient and the dividend as the remainder. Restoring long division is used rather than 64 bit integer arithmetic, so that the operations work at any width like Mul does. The tests evaluate the four new operations against reference implementations of the SMT-LIB definitions for every pair of 4 bit operands, and cover the operators that had no evaluation coverage at all before: shifts, rotates, slice, concat, zero and sign extension, the comparisons, Ite, and the propagation of undefined values. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Covers the four factory functions themselves rather than their evaluation: that they accept operands and a result of equal size, produce a node of the right type and size over the right variables, and reject operands that differ in size from each other or from the result. The Python bindings for Sdiv, Udiv, Srem and Urem, including the node type constants, already exist and work, verified by hand against the new constant folding. They are not covered by tests/python_binding/test_boolean_function.py since that file is not referenced by the build or by any workflow and still calls get_variables(), get_truth_table(), is_constant_zero(), to_dnf() and optimize(), none of which are bound any more. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
tests/python_binding/ is not referenced by the build or by any workflow, so nothing has run these files in a long time. They would not run either: they still call boolean_function(), value.ONE, get_variables(), get_truth_table(), is_constant_zero(), to_dnf() and optimize() on the netlist and Boolean function classes, none of which are bound any more. Rather than leave tests that cannot pass and are not executed, drop them. The C++ suite under tests/netlist covers the same ground. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Evaluating a Boolean function walks its nodes and hands each one to SymbolicExecution::simplify(), which builds a std::vector<BooleanFunction> of operands and returns a BooleanFunction result. Each of those owns a vector of nodes whose nodes own a string and a vector of values, so computing a single AND of two bits costs several heap allocations. A sample of a HAWKEYE S-box identification run spent 63% of the evaluation in malloc and free. Whenever every variable of a function is bound to a constant, which is the case for anything computing a truth table, no sub-expression can survive and the whole detour through Boolean functions is unnecessary. SymbolicExecution therefore folds such a function on a stack of plain values and only falls back to the general path when a variable turns out not to be constant. To avoid a second implementation of the operator semantics, the switch that applies a node to constant operands moved into ConstantPropagation::fold(), shared by the new path and by constant_propagation(), which wraps its result back into a Boolean function as before. The 18 helpers of that namespace now return the value vector they were computing all along instead of wrapping it. They are local to the translation unit, no public signature changes. Resolving the variables is now done through SymbolicState::get_bindings() as well. Going through get() per variable built a Boolean function to use as the key and looked it up in a std::map keyed by whole Boolean functions, comparing them node by node and therefore string by string. Measured on a 50 node function over 8 variables, 5.17 ms per truth table before and 1.94 ms after, 2.7x. Together with the changes already on the misc branch it comes to 1.64 ms, 3.15x. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Covers the changes of this branch that had no entry yet: the two GUI hangs on large designs, the duplicate rebuild of the module elements tree, the faster Boolean function comparison, the shipped HAWKEYE S-box database, and the removal of the stale Python binding tests. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The reference implementations of the SMT-LIB division semantics let the compiler deduce their return type. On macOS that works out, u64 and the unsigned long long of the ~0ull and 1ull literals are the same type there. On Linux u64 is unsigned long, so the branches of the signed variants deduced unsigned long from one helper and unsigned long long from another, which GCC rejects: error: inconsistent types 'long unsigned int' and 'long long unsigned int' deduced for lambda return type Spelling out u64 as the return type fixes it. The loop over the bit widths of the wide arithmetic test no longer relies on a narrowing conversion either. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
BooleanFunction::simplify() runs the rule set of SymbolicExecution::simplify() and then hands the result to ABC. ABC works on single bits, so it collapses things like A ^ (A ^ B) even though the rule set has no rule for it, but it cannot reach the word level operations. Those are exactly the ones the rule set covers least: Zext and Sext had no rules at all, Slice had two and each comparison had one. None of the following was simplified before: ZEXT(A, |A|) => A SEXT(A, |A|) => A ZEXT(ZEXT(A, n), m) => ZEXT(A, m) SEXT(SEXT(A, n), m) => SEXT(A, m) SLICE(SLICE(A, i, j), k, l) => SLICE(A, i+k, i+l) SLICE(CONCAT(A, B), i, j) => SLICE(B, i, j) or SLICE(A, i-|B|, j-|B|) 0 <=u A => 1 A <=u 111...1 => 1 111...1 <u A => 0 A == ~A => 0 A == 1, A == 0 => A, ~A for a single bit ITE(A, 1, 0), ITE(A, 0, 1) => A, ~A for a single bit Only extensions of the same kind collapse, ZEXT(SEXT(A, n), m) is not ZEXT(A, m). A slice of a concatenation is only reduced when it falls entirely into one of the two halves. The tests check that simplification does not change the value of a function for any assignment of its variables, rather than that it produces one particular shape, and that something was simplified at all. Also fixes the rule comments of Urem, which were copied from Srem and claimed to describe the signed operation. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
An extension leaves the bits of the original value untouched and pads above them, so a slice that does not cross the boundary only depends on one of the two parts: SLICE(ZEXT(X, n), i, j) => 0 for i >= |X|, the range is padding SLICE(ZEXT(X, n), i, j) => SLICE(X, i, j) for j < |X| SLICE(SEXT(X, n), i, j) => SLICE(X, i, j) for j < |X| A slice that crosses the boundary is left alone. For a zero extension it would become a zero extension of a slice, and for a sign extension the padding is the replicated sign bit rather than a constant, so neither case gets shorter. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The preprocessing functions of netlist_preprocessing and xilinx_toolbox
always worked on the entire netlist, so there was no way to clean up a
single module or a hand-picked set of gates.
They now take an optional vector of gates that restricts which gates may
be modified or deleted. An empty vector keeps the previous behaviour and
considers the whole netlist, and the function's own type filter is still
applied on top, so passing every gate of a module is always valid.
Where a rewrite involves more than one gate, the scope means:
- remove_consecutive_inverters requires both inverters of a pair to be
in scope, even if only the second one ends up being deleted
- remove_redundant_gates only deletes gates that are in scope, the
equivalent gate kept in their stead may lie outside of it
- remove_unconnected_gates and propagate_constants keep iterating to a
fixpoint, but never cascade into gates outside of the scope
Left out for now are the two redundancy passes, whose gate set doubles
as the boundary for building Boolean functions, manual_mux_optimizations,
which replaces subgraphs through the resynthesis plugin, and the parsers
and reconstruction passes, which have no gates to scope by.
Scoping also exposed that newly created gates always ended up in the top
module, which would silently move logic out of the module being worked
on. split_shift_registers and unify_ff_outputs now assign their
replacements to the module of the gate they replace, as split_luts
already did.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Running a preprocessing function required writing a script, even for the routine cases where the user has just selected the modules or gates they want cleaned up. Both plugins now contribute a GUI extension, so remove_buffers, unify_ff_outputs, split_luts, and split_shift_registers show up in the context menus of the graph view, the module tree, and the selection details. Which variant is offered depends on the selection: while modules or gates are selected the entries operate on that selection, otherwise they operate on the entire netlist. Only one of the two is ever shown, so the menu always reflects what a click would act on. A selected module contributes all of its gates including those of its submodules, and a gate selected both directly and through a parent module is only passed once. The gate list is handed to the preprocessing function as its scope, so the function's own type filter still decides what is actually touched and passing a whole module is always valid. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
solve_fsm had grown two entry points and a widening parameter list, wrote a DOT file as a side effect of solving, and pushed the resulting graph into the dot viewer without being asked. It also printed every transition to stdout on every run. The plugin now exposes a single solve_fsm(Configuration) that returns a StateTransitionGraph and touches nothing else. Rendering is a separate step on the result: generate_dot_graph for the picture, to_string for the full text, write_txt for that text in a file. Displaying the graph is left to the caller, which is what dot_viewer::load_dot_file is for. The configuration also carries a brute_force flag that replaces the separate solve_fsm_brute_force function. Brute forcing enumerates every state, so it now discards the states that are unreachable from the initial state and both approaches return the same graph for the same configuration. Beyond the restructuring, the solver can report what the FSM outputs. Given a list of named outputs, each a vector of nets with the first providing the least significant bit, it evaluates every output in every state. An output that only depends on the state (Moore) reduces to a constant, one that also depends on the inputs (Mealy) keeps the input variables in its function, so both kinds are described without having to split transitions. Outputs are taken as nets rather than gates because an output does not need a gate of its own, as in the FSM example project where a port is driven straight off a flip-flop. The text representation prints the full condition of every transition without truncating anything, preceded by a legend that maps each state bit to its flip-flop, each output to its nets, and each net variable of a Boolean function to the net it stands for. The last one matters because those variables are built from net IDs and match no net name. Also fixes the initial state being assembled with the opposite bit order to the state vector handed to the solver, which made a non-zero initial state start the exploration from a different state than the one requested. The first flip-flop of the state register now provides the least significant bit everywhere. The plugin had no tests. Eight are added, covering Moore and Mealy outputs, multi-bit outputs and their bit order, the initial state, the equivalence of the two approaches, invalid configurations, and both renderings. They skip rather than fail when no local SMT solver is available. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
SelectionRelay::handleNetRemoved took the removed net out of the gate set of the pending selection action instead of the net set. Deleting a selected net therefore left it selected, and additionally dropped whichever gate happened to carry the same numeric ID from the selection. handleModuleRemoved and handleGateRemoved were already correct. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Two problems in QGVNode::paint, both visible as soon as a node label is longer than the node is wide. The DOT format encodes a line break within a label as the escape sequence \n, which is kept verbatim in the attribute. Qt only breaks on an actual newline character, and the overflow branch additionally passed Qt::TextSingleLine, so the escape was drawn as two literal characters and the whole label ended up on one line. displayLabel() now resolves \n, \l and \r before drawing, the width check measures the widest line rather than the whole string, and the single line flag is gone. The overflow branch also stroked a red rectangle around the label. That is leftover debug drawing with no way to switch it off, so it is removed. The two interact: graphviz sizes a node for the label with its line breaks applied, Qt then drew it as one long line, which overflowed and triggered the red rectangle. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A preprocessing function invoked from a context menu deletes or replaces one gate at a time, and the GUI re-laid out its graph views after every one of them, which dominated the runtime of the operation itself. Both plugins now hold a GuiLayoutLocker for the duration of the call, which defers the affected views and updates each of them once at the end. The class mirrors the one the dataflow analysis and module identification plugins already use: it asks the plugin manager for the UI plugin and does nothing if none is running, so it is safe in headless runs as well. The lock is taken explicitly by the plugin rather than wrapped around every context menu action by the GUI, because not every action needs it and holding one has a cost of its own. Note this only covers the graph view. Widgets such as the selection details react to the individual netlist events and still update once per gate. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…eanup # Conflicts: # CHANGELOG.md
The FSM project is the entry point of the example projects, so it is now flat and anonymous like a netlist recovered from real hardware: one module holding all 21 gates, named U1 to U21, with no hierarchy to give the answer away. The structure is what the guide asks the reader to recover by hand. Its script follows from that. gate_info.py is gone, it printed the Boolean function of every LUT and taught nothing that the selection details do not show. fsm.py now identifies the modules the reader built by ID rather than by name, takes the nets carrying the outputs of the machine, and hands all of it to the reworked solve_fsm API. It prints the solver's own text representation instead of formatting the transitions itself, and renders the DOT graph as a separate step. The outputs are given as nets rather than being read off the output logic module, because OUTPUT_0 leaves its flip-flop and goes straight to the port without passing through any gate, so that module cannot describe it. The ignore list kept a README.md that does not exist and did not list crypto_trojan.zip, which is tracked. Both corrected. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The FSM wiki page no longer embeds it, and nothing else in the wiki or the repository references it. It also showed the old graph, whose states carried no output annotation. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The script closed with "if output is SAT, then verified adder for given opcode", which states the opposite of what it checks. The constraint it builds asserts that the ALU and the adder differ, so UnSat is the result that proves them equal and Sat is the counterexample. Both comments now say what the constraint means and what each result implies. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…eanup # Conflicts: # CHANGELOG.md # plugins/netlist_preprocessing/python/python_bindings.cpp # plugins/netlist_preprocessing/test/netlist_preprocessing.cpp
The merge from master brought the binding lifetime check, and it flags the four FSM solver bindings that hand out gates without keeping their netlist alive: the state register, the transition logic, the initial state, and the state register of the state transition graph. The outputs of the configuration and the output nets of the graph hand out nets the same way behind a tuple, which the check does not see through, so they get the policy as well. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
The branch started as a cleanup of the example projects and grew into the fixes the examples needed to run. Twenty-eight commits on top of master; the Boolean function work that was merged separately in #636 is already in master and does not reappear here.
FSM solver (
solve_fsm)Configurationobject, which also selects between the SMT and the brute-force approach.generate_dot_graph,to_string, andwrite_txt(with a legend mapping state bits, outputs, and net variables back to the netlist).Preprocessing (
netlist_preprocessing,xilinx_toolbox)split_shift_registersandunify_ff_outputsassign new gates to the module of the gate they replace instead of the top module.simplify_lut_initscrashing on a LUT with an unconnected output,split_lutscrashing on aLUT6_2using only one output, andremove_unconnected_gateslooping forever when a gate cannot be deleted.remove_buffers,unify_ff_outputs,split_luts, andsplit_shift_registers, on the selection or the whole netlist, with GUI layout updates held back while they run.xilinx_toolbox, which had none.GUI and DOT viewer
Core and bindings
NetandGate.Examples
Merge state
Master is merged in (merge commit resolves
CHANGELOG.md, the preprocessing Python bindings, and the preprocessing tests). The changelog entries are folded into master's grouped layout, with new sub-headings for the FSM solver and the Xilinx toolbox. The merge also brought master's binding lifetime check, which flagged the FSM solver bindings; those now carryhal::borrowed().Test plan
🤖 Generated with Claude Code