%
% Shifter for the DLX ALU from [MP95]
%
% PVS Formalization (C) 2000-2001 Daniel Kroening
%

alu_shifter_impl[N: above(1), logN: posnat]: THEORY
  BEGIN
    ASSUMING

      logN_is_logN: ASSUMPTION N=2^logN;

    ENDASSUMING

    basicslib: LIBRARY="../basics";
    %IMPORTING basicslib@basics;
    IMPORTING basicslib@shifter;
    IMPORTING basicslib@halfdecoder;
    IMPORTING basicslib@carry_chain_inc;

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

    shifter_distance(distance: bvec[logN], right: bool):bvec[logN]=
      IF right THEN
        carry_chain_inc_impl(logN, NOT distance, TRUE)^(logN-1, 0)

      ELSE
        distance
      ENDIF;

    shifter_mask(distance: bvec[logN], right: bool):bvec[N]=
      LET dec=halfdecoder_impl[logN, N](distance) IN
      LAMBDA (i: below(N)):
        IF right THEN
          dec(N-i-1)
        ELSE
          dec(i)
        ENDIF;

    alu_shifter_impl(op, distance, right, arithmetic):bvec[N]=
      LET dist=shifter_distance[N, logN](distance, right) IN
      LET cls_out=cls_impl(logN, op, dist) IN
      LET mask=shifter_mask[N, logN](distance, right) IN
      LET fill=right AND arithmetic AND op(N-1) IN
      LAMBDA (i: below(N)):
        (cls_out(i) AND NOT mask(i)) OR
        (mask(i) AND fill);

  END alu_shifter_impl