// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // This module implements a full adder for radix-B numbers that makes use of a// // processors arithmetic where the full word size is used to represent radix-B// // digits. For this reason, the carry digit must be computed differently to // // the reference implementation of a full adder given in module FullAdd. // // The correctness of the module below is seen as follows: // // // // Case 1: 0<=x+y+cin<B: In this case, we must have cout=0, so that we have to// // prove that s<x will never happen, and that in case s==x, we have cin=0. To // // this end, we note that by the case assumption, we have s = x+y+cin, thus: // // // // * s<x <=> y+cin<0 <=> false // // * s=x <=> y+cin=0 <=> y=cin=0 // // // // Case 2: B<=x+y+cin<2B-1: In this case, we must have cout=1, so that we have// // to prove that s>x will never happen, and that in case s==x, we have cin=1. // // To this end, note that in this case, we have s = x+y+cin-B, and therefore: // // // // * s<x <=> y+cin<B <=> !(y=B-1 & cin=1) // // * s=x <=> y+cin=B <=> (y=B-1 & cin=1) // // * s>x <=> y+cin>B <=> false // // // // ************************************************************************** // macro B = 8; // machine arithmetic for unsigned integers macro umod(x) = (x%B); macro uadd(x,y) = umod(x+y); macro usub(x,y) = umod((B+x)-y); macro umul(x,y) = umod(x*y); module NatFullAdd(nat{B} ?x,?y,nat{2} ?cin,cout,nat{B} s) { s = uadd(x,uadd(y,cin)); cout = ((s<x)?1:((s==x)?cin:0)); assert(x+y+cin == cout * B + s); }