%
% Verification of DLX ALU
% as given in [MP95]
%
% The PVS proof is Copyright (C) 2000 Daniel Kroening
%

dlxalu_proof: THEORY
  BEGIN
    IMPORTING dlxalu_spec, dlxalu_imp, alu_shifter_proof;

    op1, op2: VAR bvec[32];
    f: VAR bvec[5];

    alu_correct_shifts: LEMMA
      f(4)=FALSE IMPLIES
      ALUf_imp(op1, op2, f)=ALUf_spec(op1, op2, f);

    alu_correct_bitwise: LEMMA
      f(4)=TRUE AND f(3)=FALSE AND f(2)=TRUE IMPLIES
      ALUf_imp(op1, op2, f)=ALUf_spec(op1, op2, f);

    alu_correct_addsub: LEMMA
      f(4)=TRUE AND f(3)=FALSE AND f(2)=FALSE IMPLIES
      ALUf_imp(op1, op2, f)=ALUf_spec(op1, op2, f);

    alu_not_neg_and_equal: LEMMA
      f(4)=TRUE AND f(3)=TRUE IMPLIES
      (NOT (ALUf_addsub(op1, op2, f)`is_neg AND equal_impl(op1, op2)));

    alu_neg_correct: LEMMA
      f(4)=TRUE AND f(3)=TRUE IMPLIES
        (ALUf_addsub(op1, op2, f)`is_neg <=> bv2int(op1)<bv2int(op2));

    alu_l_or_g_or_eq: LEMMA
      bv2int(op1)<bv2int(op2) OR 
      bv2int(op1)>bv2int(op2) OR
      equal_impl(op1, op2);

    alu_ALUf_comp_correct: LEMMA
      f(4)=TRUE AND f(3)=TRUE IMPLIES
        ALUf_imp(op1, op2, f)`result(0)=ALUf_spec(op1, op2, f)`result(0);

    alu_correct_comp: LEMMA
      f(4)=TRUE AND f(3)=TRUE IMPLIES
      ALUf_imp(op1, op2, f)=ALUf_spec(op1, op2, f);

    alu_correct: LEMMA 
      ALUf_imp(op1, op2, f)=ALUf_spec(op1, op2, f);

  END dlxalu_proof