imm_bus_rf.mzn

include "globals.mzn";

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

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

% Instructions
  int: num_instrs = 2; % excluding nop

  int: nop    = 0;
  int: imm_1  = 1;
  int: store  = 2;

% Functional units
  int: num_FUs = 2;

  int: IMM = 1;
  int: RF = 2;

  set of int: IMM_ops = {nop, imm_1};
  set of int: RF_ops = {nop, store};

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

  var 1..N: end;
  solve minimize end;
  % or maximize the number of cycles in the terminating state?
  % solve maximize sum(n in 1..N) (bool2int(R[n,1,1]));

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

  constraint forall(n in 1..N) (
   op[n,IMM] in IMM_ops
/\ op[n,RF]  in RF_ops
  );

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

% store copies the vreg on bus 1 to reg 1, if it's there
  constraint forall(n in 1..N-1, i in 1..vregs) (
    (op[n,RF] = store <-> (B[n,1,1] = true))
    /\
    (op[n,RF] = store <-> ((R[n,1,i] = false /\ (R[n+1,1,i] = true))))
  );

% Buses and Registers hold their values on nop
  % constraint forall(n in 1..N-1, i in 1..vregs, j in 1..buses) (
  %   op[n,IMM] = nop -> (B[n,j,i] = B[n+1,j,i])
  % );
  constraint forall(n in 1..N-1, i in 1..vregs, r in 1..registers) (
    op[n,RF] = nop  -> (R[n,r,i] = R[n+1,r,i])
  );

% at cycle N the terminating state should be true
  % constraint R[N,1,1] = true;
% all registers and buses are empty in cycle 1
  constraint forall (r in 1..registers, i in 1..vregs) (R[1,r,i] = false);
  constraint forall (j in 1..buses, i in 1..vregs) (B[1,j,i] = false);