SRC Research Report 78
SRC Research Report 78
We show how machine-checked verification can support an approach to circuit design based on transformations. This approach starts with a conceptually simple (but inefficient) initial design and uses a combination of {\it ad hoc} and algorithmic transformations to produce a design that is more efficient (but more complex).
We present an example in which we start with a simplified CPU design and derive an efficient pipelined form, including circuitry for reverting the effects of partially executed instructions when a successful branch is detected late in the pipeline. The algorithmic stage of our derivation applies a transformation, retiming, that has been proven to preserve functional behavior in the general case. The {\it ad hoc} stage requires special justification, which we supply in the form of a machine-checked formal verification.
Back to the SRC Research Reports main page.