Hardware Retiming

# Correctness of a Hardware Retiming Transformation

This example applies BOBJ's circular coinductive rewriting algorithm with case analysis, to a hardware verification example, taken from the thesis of Paul Miner at Indiana University (1998), written under the direction of Prof. Steven Johnson; this thesis applies explicit coinduction to many hardware examples, and inspired us to try our approach on the same domain. A diagram for the circuit is given below, and the code in the next section is due to Kai Lin, as is the idea of enhancing circular coinductive rewriting with case analysis; the syntax was designed by Joseph Goguen.

The problem is to prove that the second circuit has the same behavior as the first; this means proving correctness of a "retiming transformation," done to minimize the longest (i.e., critical) path through the first circuit. The approach in the thesis of Paul Miner was to translate the logic of a hardware description language named DRS into the higher order logic of the PVS theorem prover, which then required some rather non-trivial interactions with the user in order to complete the proof. Our approach here is much more direct, expressing both the circuit and the proof task in BOBJ, and then applying the CCRW algorithm with one case analysis and one lemma. Although less than entirely trivial, these are standard tricks that can be learned from experience; actually, these Boolean case analyses are entirely standard for hardware and could be automated, and the cobasis used is also standard.

### 1. BOBJ Source Code

*** file: /tatami/bobj/examples/mux.bob *** hardware retiming transformation correctness bth STREAM is sort Stream . op _&_ : Bool Stream -> Stream . op hd : Stream -> Bool . op tl : Stream -> Stream . var S : Stream . var B : Bool . eq hd(B & S) = B . eq tl(B & S) = S . end bth FUN is pr STREAM . op f : Bool -> Bool . op mapf : Stream -> Stream . op mux : Stream Stream Stream -> Stream . op mux : Bool Bool Bool -> Bool . op feedback : Stream Stream Bool -> Stream . vars B B1 B2 : Bool . vars S S1 S2 S3 : Stream . eq hd(mapf(S)) = f(hd(S)) . eq tl(mapf(S)) = mapf(tl(S)) . eq hd(mux(S1, S2, S3)) = hd(S2) if hd(S1) . eq hd(mux(S1, S2, S3)) = hd(S3) if not hd(S1). eq tl(mux(S1, S2, S3)) = tl(S2) if hd(S1) . eq tl(mux(S1, S2, S3)) = tl(S3) if not hd(S1) . eq mux(true, B1, B2) = B1 . eq mux(false, B1, B2) = B2 . eq hd(feedback(S1, S2, B)) = B . eq tl(feedback(S1, S2, B)) = feedback(tl(S1), tl(S2), mux(hd(S1), hd(S2), B)) . end bth SYSTEM is pr FUN . ops old new : Stream Stream Bool -> Stream . vars B B1 B2 : Bool . vars S S1 S2 : Stream . eq hd(old(S1, S2, B)) = f(B) . eq tl(old(S1, S2, B)) = mapf(mux(S1, S2, feedback(S1, S2, B))) . eq hd(new(S1, S2, B)) = B . eq tl(new(S1, S2, B)) = mux(S1, mapf(S2), feedback(S1, mapf(S2), B)) . end cobasis SYSTEM-COBASIS from SYSTEM is op hd : Stream -> Bool . op tl : Stream -> Stream . end cases MUX-STREAM-CASE-ANALYSE for SYSTEM is vars S1 S2 S3 : Stream . context mux(S1, S2, S3) . case eq hd(S1) = true . case eq hd(S1) = false . end cases MUX-CASE-ANALYSE for SYSTEM is vars B1 B2 B3 : Bool . context mux(B1, B2, B3) . case eq B1 = true . case eq B1 = false . end set cob SYSTEM-COBASIS . set cred trace on . ***> a lemma cred with MUX-CASE-ANALYSE mapf(feedback(S1, S2, B)) == feedback(S1, mapf(S2), f(B)) . ***> main result open . eq mapf(feedback(S1, S2, B)) = feedback(S1, mapf(S2), f(B)) . cred with MUX-STREAM-CASE-ANALYSE old(S1, S2, B) == new(S1, S2, f(B)) . close

### 2. BOBJ Output

awk% bobj \|||||||||||||||||/ --- Welcome to BOBJ --- /|||||||||||||||||\ BOBJ version 0.9.196 built: Tue Oct 29 16:43:36 PST 2002 University of California, San Diego Mon Nov 04 12:15:28 PST 2002 BOBJ> in mux ========================================== bth STREAM ========================================== bth FUN ========================================== bth SYSTEM ========================================== cases MUX-STREAM-CASE-ANALYSE ========================================== cases MUX-CASE-ANALYSE ========================================== set cobasis SYSTEM-COBASIS ========================================== ***> a lemma ========================================== c-reduce in SYSTEM : mapf(feedback(S1, S2, B)) == feedback(S1, mapf(S2), f(B)) use: MUX-CASE-ANALYSE using cobasis SYSTEM-COBASIS for SYSTEM reduced to: mapf(feedback(S1, S2, B)) == feedback(S1, mapf(S2), f(B)) ----------------------------------------- add rule (C1) : mapf(feedback(S1, S2, B)) = feedback(S1, mapf(S2), f(B)) ----------------------------------------- target is: mapf(feedback(S1, S2, B)) == feedback(S1, mapf(S2), f(B)) expand by: op hd : Stream -> Bool reduced to: true nf: f(B) ----------------------------------------- target is: mapf(feedback(S1, S2, B)) == feedback(S1, mapf(S2), f(B)) expand by: op tl : Stream -> Stream deduced using (C1) : feedback(tl(S1), mapf(tl(S2)), f(mux(hd(S1), hd(S2), B))) == feedback(tl(S1), mapf(tl(S2)), mux(hd(S1), f(hd(S2)), f(B))) ------------------------------------------- case analysis by MUX-CASE-ANALYSE ------------------------------------------- introduce constant(s): s1 for the variable S1 s for the variable S2 b for the variable B ------------------------------- case 1 : assume: hd(s1) = true reduce: feedback(tl(s1), mapf(tl(s)), f(mux(hd(s1), hd(s), b))) == feedback(tl(s1), mapf(tl(s)), mux(hd(s1), f(hd(s)), f(b))) nf: true ------------------------------- case 2 : assume: hd(s1) = false reduce: feedback(tl(s1), mapf(tl(s)), f(mux(hd(s1), hd(s), b))) == feedback(tl(s1), mapf(tl(s)), mux(hd(s1), f(hd(s)), f(b))) nf: true ----------------------------------------- result: true c-rewrite time: 287ms parse time: 8ms ========================================== ***> main result ========================================== open ========================================== eq mapf(feedback(S1, S2, B)) = feedback(S1, mapf(S2), f(B)) ========================================== c-reduce in SYSTEM : old(S1, S2, B) == new(S1, S2, f(B)) use: MUX-STREAM-CASE-ANALYSE using cobasis SYSTEM-COBASIS for SYSTEM reduced to: old(S1, S2, B) == new(S1, S2, f(B)) ----------------------------------------- add rule (C1) : old(S1, S2, B) = new(S1, S2, f(B)) ----------------------------------------- target is: old(S1, S2, B) == new(S1, S2, f(B)) expand by: op hd : Stream -> Bool reduced to: true nf: f(B) ----------------------------------------- target is: old(S1, S2, B) == new(S1, S2, f(B)) expand by: op tl : Stream -> Stream reduced to: mapf(mux(S1, S2, feedback(S1, S2, B))) == mux(S1, mapf(S2), feedback(S1, mapf(S2), f(B))) ------------------------------------------- case analysis by MUX-STREAM-CASE-ANALYSE ------------------------------------------- introduce constant(s): s for the variable S1 s1 for the variable S2 b for the variable B ------------------------------- case 1 : assume: hd(s) = true reduce: mapf(mux(s, s1, feedback(s, s1, b))) == mux(s, mapf(s1), feedback(s, mapf(s1), f(b))) nf: mapf(mux(s, s1, feedback(s, s1, b))) == mux(s, mapf(s1), feedback(s, mapf(s1), f(b))) ------------------------------- case analysis failed ----------------------------------------- add rule (C2) : mapf(mux(S1, S2, feedback(S1, S2, B))) = mux(S1, mapf(S2), feedback(S1, mapf(S2), f(B))) ----------------------------------------- target is: mapf(mux(S1, S2, feedback(S1, S2, B))) == mux(S1, mapf(S2), feedback(S1, mapf(S2), f(B))) expand by: op hd : Stream -> Bool reduced to: f(hd(mux(S1, S2, feedback(S1, S2, B)))) == hd(mux(S1, mapf(S2), feedback(S1, mapf(S2), f(B)))) ------------------------------------------- case analysis by MUX-STREAM-CASE-ANALYSE ------------------------------------------- introduce constant(s): s for the variable S1 s1 for the variable S2 b for the variable B ------------------------------- case 1 : assume: hd(s) = true reduce: f(hd(mux(s, s1, feedback(s, s1, b)))) == hd(mux(s, mapf(s1), feedback(s, mapf(s1), f(b)))) nf: true ------------------------------- case 2 : assume: hd(s) = false reduce: f(hd(mux(s, s1, feedback(s, s1, b)))) == hd(mux(s, mapf(s1), feedback(s, mapf(s1), f(b)))) nf: true ----------------------------------------- target is: mapf(mux(S1, S2, feedback(S1, S2, B))) == mux(S1, mapf(S2), feedback(S1, mapf(S2), f(B))) expand by: op tl : Stream -> Stream reduced to: mapf(tl(mux(S1, S2, feedback(S1, S2, B)))) == tl(mux(S1, mapf(S2), feedback(S1, mapf(S2), f(B)))) ------------------------------------------- case analysis by MUX-STREAM-CASE-ANALYSE ------------------------------------------- introduce constant(s): s for the variable S1 s1 for the variable S2 b for the variable B ------------------------------- case 1 : assume: hd(s) = true reduce: mapf(tl(mux(s, s1, feedback(s, s1, b)))) == tl(mux(s, mapf(s1), feedback(s, mapf(s1), f(b)))) nf: true ------------------------------- case 2 : assume: hd(s) = false reduce: mapf(tl(mux(s, s1, feedback(s, s1, b)))) == tl(mux(s, mapf(s1), feedback(s, mapf(s1), f(b)))) nf: true ----------------------------------------- result: true c-rewrite time: 154ms parse time: 7ms ========================================== close BOBJ> q Bye. awk%

To the BOBJ Examples homepage
To the Tatami project homepage
Maintained by Joseph Goguen