|
|
|
|
|
by dboreham
953 days ago
|
|
Formal methods have been used in CPU design for nearly 40 years [1] but not yet for everything, and the methods tend to not have "round-trip-engineering" properties (e.g. TLA+ is not actually proving validity of the code you will run in production, just your description of its behavior and your idea of exhaustive test cases). [1] https://www.academia.edu/60937699/The_IMS_T_800_Transputer |
|