Mechanical Verification of Adder Circuits using Rewrite Rule Laboratory

摘要

A methodology for mechanically verifying generic adder circuits is proposed using the rewrite-rule based theorem prover Rewrite Rule Laboratory (RRL). Proofs of properties of adder circuit descriptions are done by rewriting and induction. Carry lookahead adder circuit is described using powerlists, a data structure introduced by Misra to support divide-and-conquer strategy used for designing data-parallel algorithms. This description uses an algorithm for parallel prefix computation on powerlists due to Adams. Reasoning about properties of this algorithm can be of independent interest since parallel prefix operator has been found useful in many data-parallel algorithms.