// ************************************************************************** // // // // eses eses // // eses eses // // eses eseses esesese eses Embedded Systems Group // // ese ese ese ese ese // // ese eseseses eseseses ese Department of Computer Science // // eses eses ese eses // // eses eseses eseseses eses University of Kaiserslautern // // eses eses // // // // ************************************************************************** // // The following module implements comparison of radix-2 numbers. // // The depth of the algorithm below is O(N), which can be obviously improved // // to O(log(N)) using a parallel prefix computation. Alternatively, we refer // // to NatSubCLA which has depth O(log(N)) and can also compare numbers. // // ************************************************************************** // macro N = 4; // number of digits used macro natval(x,m) = sum(i=0..m-1) ((x[i]?1:0) * exp(2,i)); module NatLes([N]bool ?x,?y,bool les,eqq) { event [N+1]bool ls,eq; ls[N] = false; // ls[i] := x[N-1..i] < y[N-1..i] eq[N] = true; // eq[i] := x[N-1..i] = y[N-1..i] for(i=0..N-1) LesCell(ls[i+1],eq[i+1],x[i],y[i],ls[i],eq[i]); les = ls[0]; eqq = eq[0]; s1 : assert(les <-> natval(x,N) < natval(y,N)); s2 : assert(eqq <-> natval(x,N) == natval(y,N)); }