source: vis_dev/vis-2.1/examples/eisenberg/eisenberg.v @ 14

/* the interleaving is emulated in the system process by permit variables */

`define N 2

/* to emulate program counter */
typedef enum { L1, L2, L3, L4, L5, L6, L7, L8, 
               L9, L10, L11, L12, L13, L14, L15, L16 } loc;

/* state of how hard a process want to enter critical section */
typedef enum { idle, want_in, in_cs } flag_type;

module system (clk);
input clk;

/* flag? and turn are shared memory */
flag_type reg flag0, flag1;
reg turn;

flag_type wire out_flag0, out_flag1;
wire out_turn0, out_turn1;

wire perm0, perm1;
reg st_perm0, st_perm1; 
// st_pterm? just show which process is chosen 

/* the current processes */
process p0(clk, perm0, flag0, flag1, out_flag0, turn, out_turn0, 0);
process p1(clk, perm1, flag0, flag1, out_flag1, turn, out_turn1, 1);

/* the processes are chosen to be executed by CPU nondeterministically */
assign perm0 = $NDset(@(posedge clk), 0, 1);
assign perm1 = ~perm0;

/* only OS/CPU can update system memory */
initial begin flag0=idle; flag1=idle; turn=0; end
initial st_perm0 = $ND(0,1);
initial st_perm1 = $ND(0,1);
always @(posedge clk) begin
    st_perm0 = perm0; st_perm1 = perm1;
    if (perm0==1)     begin flag0 = out_flag0; turn = out_turn0; end
    else if(perm1==1) begin flag1 = out_flag1; turn = out_turn1; end
end

endmodule


/* individual process */
module process (clk, perm, flag0, flag1, out_flag, turn, out_turn, i);
input clk;
input perm;
input flag0, flag1;
output out_flag;
input turn;
output out_turn;
input i;

flag_type wire flag0, flag1;
flag_type wire out_flag;
 
// pc and j are local to each process
loc reg pc;
reg j;

flag_type wire flagj, flagturn;
wire nond_exit;

assign flagj = (j==0) ?       flag0 : flag1,
       flagturn = (turn==0) ? flag0 : flag1;

/* if the process decide to change system wide data */
assign out_flag = (pc==L1) ? want_in : 
                  (pc==L7) ? in_cs : 
                  (pc==L16)? idle :
                  (i==0) ? flag0 : flag1;
assign out_turn = (pc==L11) ? i : (pc==L15) ? j : turn;
assign nond_exit = $NDset(@(posedge clk), 0, 1);

initial begin j=0; pc=L1; end

// ----- the program is executed forever -----
always @(posedge clk) begin                                            
    if (perm==1) begin
        case (pc)
// repeat   flag[i]=want_in;
            L1: begin pc=L2; end                                       
//     j=turn;
            L2: begin j=turn; pc=L3; end                               
//     while (j != i)
            L3: begin if (j!=i) pc=L4; else pc=L7; end                 
//         do if (flag[j] != idle)
            L4: begin if (flagj != idle) pc=L5; else pc=L6; end        
//                then j = turn;
            L5: begin j=turn; pc=L3; end                               
//                else j = j+1 mod `N;
            L6: begin if (j==`N-1) j=0; else j=j+1; pc=L3; end         
//     flag[i] = in_cs;
            L7: begin pc=L8; end                                       
//     j=0;
            L8: begin j=0; pc=L9; end                                  
//     while ((j<`N) && (j==i || flag[j] != in_cs)) do j=j+1;
            L9: begin                                                  
                if ((j<`N) && ((j==i) || (flagj!=in_cs)))       
                    begin j=j+1; pc=L9; end
                else pc=L10;
                end
// until (j>=`N) && ((turn==i) || flag[turn] == idle);
            L10: begin                                                 
                 if ((j>=`N) && ((turn==i) || (flagturn==idle)))
                     pc=L11;
                 else 
                     pc=L1;
                 end
// turn = i;
            L11: begin pc=L12; end                                     
// critical section
            
// ----- CRITICAL SECTION -----
            L12: begin if (nond_exit==1) pc=L13; else pc=L12; end      
// j = turn+1 mod `N;
            L13: begin if (turn==`N-1) j=0; else j=turn+1; pc=L14; end 
// while (flag[j] == idle) do j=j+1 mod `N;
            L14: begin if (flagj==idle)                                
                           begin
                           if (j==`N-1) j=0;
                           else j=j+1;
                           pc=L14;
                           end
                       else pc=L15;
                 end
// turn = j;
            L15: begin pc=L16; end                                     
// flag[i] = idle;
            L16: begin if (nond_exit==1) pc=L1; else pc=L16; end       
                                                                       
// ----- REMAINDER SECTION -----
            default: ;
        endcase
    end
end

endmodule