%
% Specification of Shifter for the DLX ALU
%
% PVS Formalization (C) 2000-2001 Daniel Kroening
%

alu_shifter_spec[N: posnat, logN: posnat]: THEORY
  BEGIN

    IMPORTING bitvectors@top;

    op: VAR bvec[N];
    distance: VAR bvec[logN];
    right, arithmetic: VAR bit;

    arith_right_shift(i: nat, bv: bvec[N]): bvec[N] =
      IF i=0 THEN
        bv
      ELSIF i<N THEN
        fill[i](bv(N-1)) o bv^(N-1, i)
      ELSE
        fill[N](TRUE)
      ENDIF;

    alu_shifter_spec(op, distance, right, arithmetic):bvec[N]=
      IF right THEN
        IF arithmetic THEN
          arith_right_shift(bv2nat(distance), op)
        ELSE
          right_shift(bv2nat(distance), op)
        ENDIF
      ELSE
        left_shift(bv2nat(distance), op)
      ENDIF;

  END alu_shifter_spec