imm_bus.mzn

include "globals.mzn";

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  Model Settings
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Upper bound on #cycles
  int: N = 5;

% Configuration
  int: vregs = 1;
  int: buses = 1;

% Instructions
  int: num_instrs = 1; % excluding nop
  int: nop    = 0;
  int: imm_a  = 1;

% Functional units
  int: num_FUs = 1;
  int: IMM = 1;

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  Variables
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% State array
  array[1..N,1..buses,1..vregs] of var bool: S;
  array[1..N,1..num_FUs] of var 0..num_instrs: op;
  var 1..N: end;

%
%  Find all satisfying schedules
%

  solve satisfy;
% solve minimize end;

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  Architecture Constraints
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Buses hold their values on nop
  constraint forall(n in 1..N-1, i in 1..vregs, j in 1..buses) (
  op[n,IMM] = nop -> (S[n,j,i] = S[n+1,j,i])
);

% Remove garbage at end of schedule
  constraint forall(n in end..N, f in 1..num_FUs) (op[n,f] = nop);

% vreg 1 is not active in cycle 1
  constraint S[1,1,1] = false;


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  Architecture Constraints
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Terminating constraints
  constraint forall(n in 1..N) (
    (S[n,1,1] = true) <- (end = n)
  );

  constraint S[end,1,1] = true;

% imm_a produces vreg 1 on bus 1
  constraint forall(n in 1..N-1) (
    op[n,IMM] = imm_a <-> ((S[n,1,1] = false) /\ (S[n+1,1,1] = true))
  );