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.
Comments
Congrats on solving the challenge!
I also briefly wrote about my approach here, with less pictures but going into slightly more detail about how to convert circuits to z3 equations: https://gist.github.com/KarelPeeters/dba417c2690cf0505ac9079...
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.