Browse by author
Lookup NU author(s): Dr Albert Koelmans, Professor David Kinniment
Timing verification of digital systems is usually performed by analytical tools. It can also be done by the use of formal transformations of the system structure. We show that there are significant advantages in using the Boyer Moore theorem prover, as opposed to special purpose tools. By modelling waveforms and timing functions in the Boyer Moore logic, it is possible to prove very general theorems about timing properties of combinatorial and feeback systems. Such theorems look quite natural to hardware designers, and allow a simpler, yet more powerful data base for timing verification to be built up.
Author(s): Koelmans AM, Kinniment DJ
Publication type: Report
Publication status: Published
Series Title: Computing Laboratory Technical Report Series
Year: 1991
Pages: 16
Print publication date: 01/10/1991
Source Publication Date: October 1991
Report Number: 347
Institution: Computing Laboratory, University of Newcastle upon Tyne
Place Published: Newcastle upon Tyne
URL: http://www.cs.ncl.ac.uk/publications/trs/papers/347.pdf