Title :
A formal method for computer design verification
Author :
Pitchumani, Vijay ; Stabler, Edward P.
Author_Institution :
Syracuse University, Syracuse, NY
Abstract :
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.
Keywords :
Computational modeling; Computer simulation; Design engineering; Design methodology; Formal verification; Hardware; Logic design; Registers; Testing;
Conference_Titel :
Design Automation, 1982. 19th Conference on
Conference_Location :
Las Vegas, NV, USA
Print_ISBN :
0-89791-020-6
DOI :
10.1109/DAC.1982.1585588
