Example Projects

HAL comes with a set of example projects that are the fastest way to get a feel for the tool — they are real netlists with the analysis already set up, so you can start looking at something interesting within a minute of opening HAL.

All of these projects can be found in hal/examples. Each project is provided as a zipped HAL project file, which can be imported into the HAL GUI via File > Import Project. Most projects ship with one or more Python scripts in their py/ folder, available from the Python Editor as soon as the project is open. Each project page lists the plugins and external tools it needs.

The projects below are ordered by difficulty, and each one builds on the techniques of the last. If you are new to HAL, work through them from top to bottom. If a project needs a plugin marked opt-in, rebuild HAL with -DBUILD_ALL_PLUGINS=ON, see Building HAL — and note that such plugins additionally need to be activated in the Plugin Manager.

1. FSM

• Size — 21 gates, 27 nets
• Gate library — example_library
• Requirements — plugins netlist_preprocessing, solve_fsm and dot_viewer, all built by default; z3 has to be installed unless you use the solver's brute force mode

A stand-alone finite state machine, and the smallest netlist shipped with HAL — small enough to display in full and to understand gate by gate. Its page is a guided tour of the GUI for people opening HAL for the first time: the graph view, the module hierarchy, the selection details and the Python console. The netlist is flat and its gate names are meaningless, so you clean out its buffers and then recover the structure of the state machine by hand, before extracting its state transition graph with a script.

2. Simple ALU

• Size — 45 gates, 77 nets
• Gate library — Xilinx UNISIM
• Requirements — no plugins; the z3 solver binary has to be installed

An extremely simple 8-bit ALU with a 2-bit opcode. This is where HAL stops being a graph viewer: you reconstruct the Boolean function of a subcircuit and then prove what it computes using an SMT solver, rather than concluding it from how the gates look.

3. Toy Cipher

• Size — 135 gates, 169 nets
• Gate library — Xilinx UNISIM
• Requirements — plugins dataflow and netlist_simulator_controller, both opt-in; Verilator has to be installed

A small — and deliberately insecure — block cipher. The first design large enough that staring at the graph stops working, which is exactly why it introduces the two techniques you will reach for most often on real netlists: dataflow analysis to recover the register structure, and simulation to watch the circuit run.

4. UART

• Size — 407 gates, 409 nets
• Gate library — example_library
• Requirements — none

A UART core that receives 64 bit and echoes the same 64 bit back. Unlike the projects above it comes with no guided script — it is a realistic circuit with a specification you already know, which makes it the natural place to practice on your own and check your conclusions against what a UART is supposed to do.

5. Crypto Trojan

• Size — 10,526 gates, 11,441 nets
• Gate library — LSI 10K
• Requirements — plugins dataflow and hawkeye, both opt-in, plus netlist_preprocessing, built by default

An AES-128 encryption netlist that someone has tampered with. A full case study on a design of realistic size, combining several of the techniques above to locate a hardware Trojan and work out how it gets triggered.