A formal method for computer design verification
Vijay Pitchumani, Edward P. Stabler · Design Automation Conference · 1982
A formal computer design verification method based on Floyd's inductive assertion technique[9] is presented as an alternative or at least a supplement to simulation. The semantics of a register transfer language is defined formally. It specifies how machine variables and time change. Hardware descriptions in this language may contain assertions. The formal definition of the language can then be used for automatic verification of logical correctness and realtime performance of the design.