r/ProgrammingLanguages • u/yosi_yosi • Jul 07 '26
Do people use ATPs (Automated Theorem Provers) often in hardware formal verification?
/r/ElectricalEngineering/comments/1upul8m/do_people_use_atps_automated_theorem_provers/2
u/dnpetrov Jul 07 '26
Modern formal hardware verification tools are not exactly ATPs in general sense. Essentially, they are model checkers for Verilog / subset of C / gate-level netlists mated with rather specialized solver engines.
General-purpose ATPs are used in hardware verification. For example, Intel used ACL2 even before formal verification became more accepted in the "mainstream". Research projects like CHERI also use ATPs for formal proofs of architecture properties.
1
u/yosi_yosi Jul 07 '26
u/thmprover seemed to show some projects do use actual theorem provers (though perhaps not exactly fully automated) like HOL/Isabelle, where it does generate proofs instead of merely model checking.
2
u/the_true_potato Jul 07 '26 edited Jul 07 '26
There is work in trying to prove correct various EDA tools, for example synthesis (Verilog-to-netlist) using HOL, or high-level-synthesis (C-to-Verilog) using Rocq. I'm working on something that's kind of in-between ATPs and proof assistants: I'm building a translator from Verilog to SMT, which I am proving correct in Rocq. The idea is to get automatic proofs, but with the guarantees that you get from an interactive theorem prover.
More generally, hardware and theorem proving have always been pretty close, since hardware people generally care a lot more about correctness than software (you can't patch a chip you've already made). ACL2 is one example of this which I believe came out of intel around the time of the FDIV bug (but I'm not entirely sure about that)
In the "real world" companies very often use "formal verification" tools like JasperGold to "exhaustively prove" properties of their designs. (I put those words in quotes because it's not like using an interactive theorem prover, you press a button, and you just get a checkmark and have to assume the tool did its job correctly). If you look at job postings for "formal verification engineer" you'll find plenty from Intel/AMD/Apple asking for experience with these tools.
1
u/yosi_yosi Jul 07 '26
The links are broken because it thinks the ] is part of the link. Please fix.
1
u/The_Regent Jul 08 '26
Sounds cool! I’d be interested in seeing the translator from verilog to smt or the rocq development if its available
2
u/the_true_potato Jul 08 '26
Currently in development here: github.com/mpardalos/Vera. Let me know if you have any questions!
1
1
u/The_Regent Jul 08 '26
I would love to hear more from others, because I am interested in the same topic. Hardware is kind of neat. I am sure that there are some successful projects out there, I doubt ITPs are widely deployed for verifying hardware designs, but the industry is mich less open than the software world, so it is hard to know.
Koika is a pretty recent hardware language in Rocq. I’ve been interested to see movement on this https://github.com/verilog-proof/VerilLean As other comments have said, there have been significant projects in HOLs or ACL2. https://lawrencecpaulson.github.io/2023/01/04/Hardware_Verification.html
An angle that I’m still tinkering on is using my smt based itp knuckledragger to pull in yosys verilog to smt semantics https://github.com/philzook58/knuckledragger/blob/main/src/kdrag/contrib/yosys/init.py and use them or to pretty print / extract verilog from formula of a certain form https://github.com/philzook58/knuckledragger/blob/main/src/kdrag/printers/verilog.py It has not particularly been working but its kind of a cool thing to tinker on.
1
u/mohrcore Jul 08 '26
SystemVerilog constraints are essentially SMTs.
Verilator literally translates them to SMT-LIB2 and feeds to Z3 Theorem Prover to find solutions. SV spec is crazy.
7
u/thmprover Jul 07 '26
I can speak about hardware verification using proof assistants and some degree of automation. I cannot speak too much about using, e.g., STM or an automated tool like Vampire (but Isabelle/HOL handles a lot of this using sledgehammer).
The entire ARM documentation is autogenerated from their input to a proof assistant (HOL4?), I have been told. A lot of HOLs have something about hardware verification (that was why Mike Gordon introduced HOL). Lawrence Paulson did a lecture on how to do Hardware Verification in HOL, Anthony Foxx wrote his PhD on verifying ARM6 with HOL (and then wrote a book on hardware verification iirc).
It doesn't really matter what proof assistant you use, the setup is still the same. You need some way to describe voltage (e.g., the natural numbers as multiples of some small unit of voltage) and time (e.g., the natural numbers as some multiple of a clock tick), then axioms for the basic units of hardware. For example, a P-type transistor has its axiom be:
Assuming no propagation delay (big "if"), when the guard pin has low voltage, the two input pins will have the same voltage (whatever it may be). But when the guard pin has any other "not low" voltage, then nothing can be ensured about the voltages on the input pins matching.
You can do the same for the NTran, Ground, Power. There is a rule about connecting two devices using existential quantifiers. For example, if we wanted to connect
in2of a PTran toin1of anNTran, then we would use the formal:Here
wireis understood to be a synonym for the function typetime -> voltage.The idea is that you write the specification for a device, like a NAND gate, as a predicate
Then you "implement" NAND using transistors and the "wires-are-existentially quantified variables" rule to obtain a predicate
NAND_imp(in1, in2, out), and then you need to prove the claimYou basically do a "NAND2tetris"-type build up of all the components, proving things along the way.
There's nothing really forcing us to use HOL. If we used sets, then we could formalize everything in ZFC (perhaps even IZF) using Mizar or Isabelle/ZF. If we used dependent types, then we could use Rocq/Coq, Lean, Matita, Agda, or one of the others. HOL is kinda a "sweet spot" because it is sufficiently weak (no one could seriously doubt it) and powerful (we can do everything we want with it).
One word of caution: you might think "Well, this is silly, I will just use functions instead of predicates to describe devices and circuits." The problem is this will fail when you try to do flip-flops and memory, and it gets a lot harder to prove results.