source: cegar_dev/cegar/concrete_model/machine_concret.v @ 13

/* ----- Symbolic variables ----- */
typedef enum {S0, S1, S2, S3} MState;

/* ----- Main Module ----- */
module machine_concret (clk, i1, o1, o2, r_i1);

input clk;
input i1;
output o1;
output o2;
output r_i1;

MState reg m_state;
reg o1, o2;
reg r_i1;

initial 
   begin
        m_state = S0;
        o1 = 0; 
        o2 = 0; 
       r_i1 = i1;
   end //initial 

always @ (posedge clk) begin

 r_i1 = i1;
 case (m_state)
   S0:
      if (i1==1)
        begin
                m_state = S1;
                o1 = 1;
                o2 = 0;
        end
     else 
        begin
                o1 = 0;
                o2 = 0;
                m_state = S0;
        end

    S1:
       begin
                m_state = S2;
                o1 = 0;
                o2 = 1;
       end

    S2:
       begin
                m_state = S3;
                o1 = 1;
                o2 = 1;
        end

    S3:
        begin
                o1 = 1;
                o2 = 1;
                m_state = S3;
        end

  endcase
//  r_i1 = i1;

end //always
  
endmodule