I'm currently choosing between the right formalization for a big hardware project.
I'm considering between SVA, TLA+ and Lean. With the former being more domain specific and the later more general.
Do you think we'll move towards "Lean for everything" or do domain specific formalisms still make sense?
Have you considered P? It feels like a good abstraction for engineers as it's "proper" code.
https://github.com/p-org/P
what's SVA?
SystemVerilog Assertions. Hardware (silicon ASICs, and also FPGAs often) are written in a language called SystemVerilog. It has a feature called "concurrent assertions" which is usually just called SVA.
These are sort of temporal regexes, e.g. you can write
Which means if the rst signal fell (changed to 0) then foo must be 1 and 1-20 cycles later it must be 0.The nice thing about them is that there are a few commercial tools that can formally verify them. They're super expensive (~$100k/year for one license), but fairly widely used because they work really well.
It's probably the most successful application of formal verification because it doesn't require much expertise to use. Unlike software formal verification which pretty much immediately requires you to become an expert on loop invariants, termination measures, hoare triples etc. At least that has been my experience.