alu_rf.mzn

%
% First version of constraint model for add-example on alu-rf configuration
%

include "globals.mzn";

  int: N = 10;
  int: vregs = 3;
  int: buses = 2;
  int: registers = 3;
  int: instrs = 6;
  int: FUs = 2;

  int: ALU = 1;
  int: RF = 2;

% For precedences
  int: nop    = 1;
  int: pass   = 2;
  int: load_a = 3;
  int: load_b = 4;
  int: add    = 5;
  int: store  = 6;

% For text output
  array[1..instrs] of string: instructions = ["nop", "pass", "load_a", "load_b", "add", "store"];
  array[1..FUs] of string: units = ["ALU", "RF"];

% State array
  array[0..N-1,1..buses+registers,1..vregs] of var 0..1: S;
  array[1..N-1, 1..FUs] of var 1..instrs: op;

% TODO: This
  solve maximize sum(n in 1..N-1) (n*S[n,3,3]);

  constraint
% Single value per bus/register
  forall(n in 1..N-1) (
   forall(j in 1..buses) (
    (sum(i in 1..vregs) (S[n,j,i]) )<= 1
    ))
/\
% Transport constraints
forall(n in 1..N-1, i in 1..vregs) (
  ((S[n,1,i] = 1) -> (
  % The load-instructions might need some kind of set-syntax
  ((S[n+1,1,i] = 1     /\ op[n,RF] != load_a /\ op[n,RF] != load_b )
    \/ (S[n+1,2,i] = 1 /\ op[n,ALU] = pass)
    \/ (S[n+1,1,i] = 0 /\ (op[n,RF] = load_a \/ op[n,RF] = load_b)))))
/\
  ((S[n,2,i] = 1) -> (
  (S[n+1,2,i] = 1           /\ ((op[n,RF] != load_a /\ op[n,RF] != load_b /\ op[n,ALU]  = nop))
   \/ (S[n+1,2,i] = 1       /\ (op[n,ALU] = pass    /\ op[n,ALU] != nop))
   \/ (S[n+1,buses+1,i] = 0 /\ op[n,RF] = store))))
)
/\
forall(n in 1..N-1, i in 1..vregs) (
  ((S[n,1,i] = 1) /\ (op[n,RF] != load_a) /\ (op[n,RF] != load_b)) <-> (S[n+1,1,i] = 1)
/\(((S[n,2,i] = 1) /\ (op[n,ALU] != add /\ op[n,ALU] != pass))     <-> (S[n+1,2,i] = 1))
/\ ((S[n,3,i] = 1) /\ (op[n,RF] != store)                          <-> (S[n+1,3,i] = 1))
/\ ((S[n,4,i] = 1)                                                 <-> (S[n+1,4,i] = 1))
  )

/\
% input constraints
forall(i in 1..vregs, j in 1..buses) (
   (S[0,j,i] = 0)
/\ (S[0,3,1] = 1)
/\ (S[0,4,2] = 1))
/\
forall (n in 1..N) (
  ((op[n,ALU] = add) -> (S[n,1,1] = 1 /\ S[n,2,2] = 1) \/ (S[n,2,1] = 1 /\ S[n,1,2] = 1))
/\
  ((op[n,RF] = store) -> (S[n,2,3] = 1))
)
/\
% output constraints
forall(n in 1..N) (
  ((op[n,RF] = load_a) -> (S[n+1,1,1] = 1))
/\ ((op[n,RF] = load_b) -> (S[n+1,1,2] = 1))
/\ ((op[n,ALU] = add) -> (S[n+1,2,3] = 1))
/\ ((op[n,RF] = store) -> (S[n+1,3,3] = 1))
);

% output
% forall(n in 1..N-1) (
% [ show_int(1, S[n,j,i]) ++ " " ++
%   if i == vregs then "\n" else "" endif
% | j in 1..buses, i in 1..vregs]
% )