//
// CBG SQUANDERER : Dining Philosophers In Bluespec
// (C) 2012 David Greaves, University of Cambridge

import StmtFSM::*;

interface Spoon_if;
  method Action pickup();
  method Action putdown();
endinterface


module spoon (Spoon_if) ;

  Reg#(Bool) inuse <- mkReg(?);    

     method Action pickup() if (!inuse);
      action
	inuse <= True;
      endaction
     endmethod

     method Action putdown();
      action
	inuse <= False;
      endaction
     endmethod

endmodule


(*synthesize *)
module philoBENCH (Empty) ;

       Spoon_if spoon0 <- spoon; 
       Spoon_if spoon1 <- spoon; 
       Spoon_if spoon2 <- spoon; 
       Spoon_if spoon3 <- spoon; 
       Spoon_if spoon4 <- spoon; 

       Diner_if din0 <- mkDiner (3, 7, spoon0, spoon1);
       Diner_if din1 <- mkDiner (4, 4, spoon1, spoon2);
       Diner_if din2 <- mkDiner (2, 9, spoon3, spoon2); // <---- Reverse pickup
       Diner_if din3 <- mkDiner (3, 6, spoon3, spoon4);
       Diner_if din4 <- mkDiner (3, 6, spoon4, spoon0);


endmodule: philoBENCH

//

interface Diner_if;

endinterface

interface Random_if;
  method ActionValue#(UInt#(15)) gen();
endinterface    

module mkRandom_gen #(UInt#(15) seed) (Random_if);

  Reg#(UInt#(15)) prbs <- mkReg(seed);

  method ActionValue#(UInt#(15)) gen();
     prbs <= (prbs << 1) | (((prbs >> 14) ^ (prbs >> 13)) & 1);   
     return prbs;
  endmethod

endmodule 

module mkDiner #(UInt#(15) on, UInt#(15) seed) (Spoon_if left, Spoon_if right, Diner_if i) ;

  Reg#(Bool) eating <- mkReg(?);    
  Reg#(UInt#(15)) timer <- mkReg(0);

  Random_if gen <- mkRandom_gen(seed);

  rule foo (timer != 0);
     timer <= timer - 1;
  endrule


  Stmt seq_behaviour =
  (seq while (True) seq
     action UInt#(15) x <- gen.gen(); timer<=x & 31; endaction await(timer== 0);

     left.pickup();
     noAction;

     action UInt#(15) x <- gen.gen(); timer<=x & 31; endaction await(timer== 0);

     right.pickup();

     eating <= True;
     timer <= on; await(timer==0);
     eating <= False;

     noAction;

     left.putdown(); 
     noAction;
     right.putdown();
     noAction;
  endseq endseq);

  FSM fsm <- mkFSM (seq_behaviour);
 
  rule kickoff  ;
     fsm.start;
  endrule


endmodule