Document SMT solving and symbolic execution as Boolean function sub-pages
Add two core-API pages under Boolean Function: SMT Solving covers the
hal_py.SMT interface — constraints, query configuration, results and
models — and Symbolic Execution covers the rewriting engine behind
simplify_local(), simplify() and evaluate().
Both were verified against a build rather than against the headers, which
turned up behavior worth documenting: the timeout is in seconds, solver
binaries are looked up at three fixed paths rather than on PATH, symbolic
state bindings are write-once, and SymbolicExecution.evaluate() currently
raises from Python. Correct the timeout units and the solver lookup on the
Simple ALU page accordingly.
Co-Authored-By: Claude Opus 5 (1M context) <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
Overhaul wiki: introduction, core, and plugin documentation
Rewrite the introduction and core sections and add dedicated pages for
every shipped plugin.
Introduction:
- Add motivation: what problem HAL solves and nine concrete applications
- Write "Using HAL" from scratch (was an empty stub)
- Document that dataflow, simulator, and HAWKEYE are opt-in, so a default
build cannot run the example projects
- Restructure the WSL section into ordered steps for WSL 2 and WSL 1
- Flesh out the FSM, Toy Cipher, and UART example project pages
Core:
- Fix incorrect API documentation: Data Container documented functions
that do not exist, GateTypeProperty values were missing their c_ prefix,
Endpoint.get_pin() returns an object rather than a name
- Complete Netlist Utilities (documented 1 of 13 functions) and Decorators
(1 of 5 decorators), and drop all deprecated functions in favor of their
decorator replacements
- Add missing API to Boolean Function, Gate, Net, Netlist, and Module
- Add background and motivation to every core page
Plugins:
- Add pages for module identification, Python shell, solve FSM, Boolean
influence, resynthesis, Z3 utilities, Xilinx toolbox, sequential
symbolic execution, and both parser/writer groups
- Fill the bitorder propagation stub
- Make Provided Plugins the single index of all plugins with their CMake
flags and default state, and remove the duplicate list from the build
instructions
- Split the simulator into its four constituent plugins
Housekeeping:
- Add a work-in-progress disclaimer to the wiki home page
- Delete the orphaned Getting Started and waveform viewer widget stubs,
moving the simulation wizard documentation into the simulator page
- Fix broken links and typos throughout
Updated Boolean Function (markdown)
Hint about special handling of spaces in the string parser
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Function (markdown)
Updated Boolean Functions (markdown)