That's really interesting that you actually used z3 to extract the output from the circuit! It hadn't occurred to me that it would be possible to do that. I suppose I got a little fixated on my approach of running a verilog simulation, and I only used z3 to solve one part (though the hardest part I think). How did you get a $DAYJOB involving formal verification?

Yeah I briefly considered switching to a simulator to get the final output, but then luckily realized the Z3 setup I had was already acting as a super-powered simulator anyway!

I'm not actually using formal verification at $DAYJOB, there we're using MILP solvers (which are closely related to SAT solvers) as part of the compilation flow when scheduling operations onto hardware accelerators.

I have been interested in formal verification for hardware for a while, but so far haven't found an opportunity to apply it. There are some great resources online though: the ZipCpu blog at https://zipcpu.com/formal/formal.html and SymbiYosys website at https://symbiyosys.readthedocs.io/en/latest/. I hindsight I could probably have used SymbiYosys instead of Z3, it would have saved me from having to walk the graph and map the gates to equations myself.