Rework the Simple ALU page and align requirements across the example pages
The Simple ALU page now follows the same shape as the FSM page: a short intro,
a requirements table, opening the project, then a "Reverse engineering the
ALU" section holding what you are looking for and four numbered steps, and a
closing list. It is written in second person throughout rather than narrating
what "we" do.
The substance is the same walkthrough of smt.py, but the page now states the
claim being tested up front and explains why the check is phrased as an
inequality, so the trick of hoping for UnSat arrives as the answer to a
question rather than a rule to follow. The two lines that were previously left
unexplained, concatenating the eight output functions and constructing the
adder, are covered as well, including the bit order of the concatenation and
the fact that the addition wraps at eight bits like the circuit does.
Corrections along the way: the prose named a pin group "opcode" while the code
beside it used "op", the page never said how to open the project, and it
claimed that this approach scales to subcircuits nobody could read by hand,
which sits badly next to its own statement that solving is exponential.
All example pages now carry the same "Requirements" table with a column
separating plugins from external dependencies. Verilator moves out of the Toy
Cipher prose into its table, and the FSM page gains z3, which solve_fsm needs
because it calls the solver binary by default. The overview page uses the same
wording.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Rewrite the FSM page as a first-contact guide and list plugins per example
The FSM project is the smallest netlist shipped with HAL and the recommended
place to start, so its page is now written for someone who has never opened
HAL before rather than as a reference.
It comes in two parts. Part 1 walks through the window, explains what a view
is, and covers navigating one; nothing there changes the netlist, so it is a
warm-up. Part 2 is five numbered steps that take the netlist from a flat pile
of gates to the state transition graph: remove the buffers, find the state
register, the transition logic and the output logic, then extract the graph
with a script.
The project itself is now flat and anonymous, so the reader recovers the three
parts by hand from gate types and connectivity, using the graph view rather
than a script. Scripting arrives only at the last step, once there is
something worth automating.
Buffers get their own step and an explanation of why they exist and why they
are in the way. It is also the first destructive action on the page, which is
worth saying out loud.
Every example page now lists the plugins it requires, and the overview page
repeats them, so nobody discovers halfway through that something is missing.
Also corrected along the way: import is the recommended way to open a project
and never unpacking the archive by hand, the widget positions matched neither
the code nor each other, panning is shift and drag rather than plain drag,
and the modifier keys now name their macOS equivalents.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Align header style and refine the introduction and example pages
Headers:
- Convert all page headers to sentence case, preserving acronyms, proper
nouns, and code identifiers. GitHub derives anchors by lowercasing, so
existing #anchor links are unaffected.
Introduction to HAL:
- Link "plugins" to the plugin index
- Correct the claim about the university lecture: HAL underpins its
practical part, and the example projects overlap only part of it
- Describe recovering high-level structure as several complementary
steps rather than one dominant one
- Move "publish reproducible research" to the end of the applications
Using HAL:
- Introduce the top module before referring to it, and move its snippet
into the Python section so no code precedes the Python introduction
- Rewrite the Python examples for readers new to Python, pull the IDs
section to the front, and give every item the same paragraph form
- Explain that the gate library and Python scripts may live outside the
project directory, and that an export always collects them
- Turn the netlist import dialog fields into an enumerated list
- Correct why a recovered netlist has no hierarchy: it is a design-time
construct absent from the chip or bitstream, not something synthesis
necessarily removes
Example projects:
- List each project once instead of three times
- Replace the empty-header tables with definition lists
Crypto Trojan and HAWKEYE:
- Document the ready-to-run hawkeye.py, the preprocessing it needs, and
the S-box database now shipped with HAL
Updated Simple ALU (markdown)
Updated Simple ALU (markdown)
Updated Simple ALU (markdown)
Updated Simple ALU (markdown)
Updated Simple ALU (markdown)
Updated Simple ALU (markdown)
Updated Simple ALU (markdown)
Updated Simple ALU (markdown)
Updated Simple ALU (markdown)
Updated Simple ALU (markdown)
Updated Simple ALU (markdown)
Updated Simple ALU (markdown)
Created Simple ALU (markdown)