Formal Design is a new approach in which the use of formal methods
starts at the earliest design stages. In the traditional approach,
verification started much later, with the RTL implementation. The new
approach allows us to assure global correctness of complex protocols
and also speeds up the overall development process. The Formal Design
approach has been applied successfully to hardware protocols for
System 390 and for IBM's ASCI Blue supercomputer.
In related work a new class of algorithms for reasoning about
correctness of processor Pipelines are being investigated. The new
algorithms use propositional logic to reason about formulas in the
logic of uninterpreted functions. More about this work can be found
in: Processor Verification Using an Efficient Decision Procedure for Logic with Uninterpreted Functions.
In the area of arithmetic hardware, interactive theorem proving
techniques have been used for some time to verify the arithmetic
algorithms used in processors. However, interactive theorem proving
techniques are very difficult to apply because theorem provers need
detailed user guidance. We recently developed a much more automatic
approach, in which the correctness of arithmetic hardware is stated as
a problem to be solved by algebraic manipulation. Algebraic
manipulations can be performed highly automatically by symbolic
algebra systems. We used the algebraic technique to verify the
correctness of SRT division, a hardware division method used in many
modern microprocessors.
