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
<![CDATA[
*** 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
<![CDATA[
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
Last modified: Sat Dec 29 11:20:41 PST 2001
