Module controller_gen 

Designer → certified controller: turn a synthesized PhasePlan into a Verilog phase-FSM and let the existing RTL pipeline (parse_transition_system → prove_invariant) certify it.

The controller cycles a phase counter; on entering each phase it greens exactly that phase’s movements and reds the rest. Because the plan is a conflict-free colouring, no conflicting pair is ever green together — and because every transition fully rewrites all movement registers to a (safe) phase configuration, the safety property is 1-inductive, so prove_invariant(1) proves it with no extra invariant strengthening. This closes the loop: design (SAT) → generate (codegen) → prove (k-induction), entirely on our own stack.

Functions

generate_controller

Generate a synthesizable Verilog controller (one 1-bit mvN register per movement, a phase counter) whose conflict-freedom is provable by prove_invariant.