PVS dump file adder.dmp

To extract the specifications and proofs, download this file to adder.dmp and from a running PVS type the command
   M-x undump-pvs-files
You will be prompted for the dump file name (adder.dmp) and the directory in which to dump the extracted files.
%Patch files loaded: (patch2-test patch2) version 2.394 $$$adder.pvs % This treatment of a ripple-carry adder follows that given in % Harald Ruess. "Hierarchical verification of two-dimensional high-speed % multiplication in PVS: A case study." In M. Srivas, editor, Formal % Methods in Computer-Aided Design (FMCAD '96), Palo Alto, CA, % November 1996. To appear. % Available at http://www.csl.sri.com/reports/postscript/fmcad96-ruess.ps.gz % % The notations bitvector@bit, bitvectors@bv[N], bitvectors@bv_nat % indicate the theories bit, bv[N], and bv_nat from the bitvector library % that is distributed with PVS full_adder: THEORY BEGIN IMPORTING bitvectors@bit x, y, cin: VAR bit FA(x, y, cin): [# carry, sum: bit #] = (# carry := (x AND y) OR ((x XOR y) AND cin), sum := (x XOR y) XOR cin #) FA_char: LEMMA sum(FA(x, y, cin)) = x + y + cin - 2 * carry(FA(x, y, cin)) END full_adder ripple_adder[N: posnat] : THEORY BEGIN IMPORTING full_adder, bitvectors@bv[N], bitvectors@bv_nat n: VAR below[N] bv1, bv2: VAR bvec[N] j: VAR upto[N] nth_cin(j, bv1, bv2): RECURSIVE bit = IF j = 0 THEN 0 ELSE carry(FA(bv1(j-1), bv2(j-1), nth_cin(j-1, bv1, bv2))) ENDIF MEASURE j adder(bv1, bv2): [# carry: bit, sum :bvec[N] #] = (# carry := nth_cin(N, bv1, bv2), sum := (LAMBDA n: sum(FA(bv1(n), bv2(n), nth_cin(n, bv1,bv2)))) #) adder_invariant: LEMMA bv2nat_rec(j, sum(adder(bv1, bv2))) = bv2nat_rec(j, bv1) + bv2nat_rec(j, bv2) - nth_cin(j, bv1, bv2) * exp2(j) bv_nat(bv1): nat = bv2nat(bv1) CONVERSION bv_nat adder_correct: THEOREM sum(adder(bv1, bv2)) = bv1 + bv2 - carry(adder(bv1, bv2)) * exp2(N) END ripple_adder $$$adder.prf (|full_adder| (|FA_char| "" (GRIND) NIL))(|ripple_adder| (|nth_cin_TCC1| "" (SUBTYPE-TCC) NIL) (|nth_cin_TCC2| "" (SUBTYPE-TCC) NIL) (|nth_cin_TCC3| "" (SUBTYPE-TCC) NIL) (|nth_cin_TCC4| "" (TERMINATION-TCC) NIL) (|adder_TCC1| "" (SUBTYPE-TCC) NIL) (|adder_TCC2| "" (SUBTYPE-TCC) NIL) (|adder_invariant| "" (INDUCT-AND-SIMPLIFY "j" :EXCLUDE "FA" :THEORIES "full_adder") NIL) (|adder_correct| "" (LEMMA "adder_invariant") (("" (GRIND :EXCLUDE "FA") NIL))))