3 ms·

So I don't understand. Why make the "formal" specification for the processor rather then one in verilog (or some other immediately testable system) to start wit

So I don't understand. Why make the "formal" specification for the processor rather then one in verilog (or some other immediately testable system) to start with? If you can't directly check from a provable formal system then it doesn't really help with validation and you have to jump through a lot of hoops to get there (like OP did).

jlg23 10y ago
The "formal" specification is the goal, but the starting point is a rather informal specification. So it is an iterative process where you discover a bug and then have to figure out whether the bug is in the implementation or the interpretation of the presentation (i.e. the test).
adreid 10y ago
It takes a lot of effort to write a specification. Just think how much software you have ever seen complete specifications for - and how close that number is to zero. So if you are going to write a specification, you really want to get maximum bang per buck out of the effort. Which means that it has to be good for many purposes: - documentation - verifying processors - dynamic verification (i.e., testing) - formal verification - testing test suites - verifying application software - dynamic and formal verification - verifying OSes, RTOSes, microkernels and other bare-metal software - verifying compilers - generating machine readable descriptions Verilog is great for one of these - but less good for all the others. Starting with a relatively neutral language gives you a lot more flexibility. It makes any individual task a bit harder than if that was your only goal but you save effort overall. There is also the virtuous cycle that bug fixes and improvements that help any one goal are folded into the master copy - so all other sub-projects benefit.