Technology-Independent DR Conversion
}For
each PI x, create xt and
xf representing the true and false evaluations of x.
}For each node implementing yi = fi(x1, …, xn), create two nodes:
}yti =
DR(fi(x1, …, xn)) and yfi =
DR(fi’(x1, …, xn))
}y = x’, special case, yt =
xf, yf =
xt
}Define DR recursively (based on Shannon Expansion Th.):
}DR(0) = 0, DR(1) = 1
}DR(x.fx + x’.fx’) = xt.DR(fx) + xf.DR(fx’)
}Theorem[DR Conversion]
}Given
function y = f(x1, …,xn), under the assumption that
xi = xti = xfi’ it holds that y = yt = yf’
xi = xti = xfi’ it holds that y = yt = yf’
}Proof: by induction on function DR
20/4/2014
50
CE-653 - Indicating Logic