/*****************************************************************************
 * assertion_examples.v      Shows different examples of how assertions
 *      may be used inside and outside of procedural code.
 *
 *      Written By:  Tom Thatcher
 *****************************************************************************/


module assertion_examples (
   input logic clk,
   input logic reset_n,

   input logic eg1_a,
   input logic [1:0] eg1_d,
   output logic [1:0] eg1_q,

   input logic eg2_req,
   input logic eg2_done,

   input logic eg3_req,
   input logic eg3_done,

   input logic eg4_sel1_in,
   input logic eg4_sel0_in,
   input logic [1:0] eg4_d0,
   input logic [1:0] eg4_d1,
   output logic [1:0] eg4_q

   );


    default clocking main_clock @(posedge clk);
    endclocking


    //  Example 1:  Normal, sequential always procedure
    always_ff @(posedge clk) begin
   if (eg1_a) begin
       eg1_q <= eg1_d;
       a_eg1_d_oh : assert property ($onehot(eg1_d));
   end
    end

    // Equivalent assertion placed outside the prodedural context
    a_eg1_a_d_oh : assert property ($onehot(eg1_d));


    // Example 2:  Two-procedure form state machine.
    //      Assertion in the combinational procedure
    //      Still a well-behaved example

    typedef enum { idle, busy } t_eg2_state;
    t_eg2_state eg2_state, eg2_nextstate;

    always_ff @(posedge clk or negedge reset_n) begin
   if (!reset_n) begin
       eg2_state <= idle;
   end
   else begin
       eg2_state <= eg2_nextstate;
   end
    end

    always_comb begin
   case (eg2_state)
       idle: begin
      if (eg2_req) eg2_nextstate = busy;
       end
       busy: begin
      a_eg2_no_req_while_busy : assert property (!eg2_req);
      if (eg2_done) eg2_nextstate = idle;
       end
       default:  begin
      eg2_nextstate = idle;
       end
   endcase
    end

    // Equivalent assertion from outside procedural block
    a_eg2_a_no_req_while_busy: assert property (eg2_state == busy |-> !eg2_req);

       
    // Example 3:  Two-procedure form state machine.
    //      Assertion in the combinational procedure
    //      Coded in a way which would admit glitches in comb process


    logic [2:0] eg3_state;
    logic [2:0] eg3_nextstate;
    logic       eg3_state0;

    always_ff @(posedge clk or negedge reset_n) begin
   if (!reset_n) begin
       eg3_state[2:1] <= 2'b00;   // All flops reset to 0
       eg3_state0     <= 1'b0;
   end
   else begin
       eg3_state[2:1] <= eg3_nextstate[2:1];
       eg3_state0   <= ~eg3_nextstate[0];
   end
    end

    assign eg3_state[0] = ~eg3_state0;

    always_comb begin
   case(1)
       eg3_state[0] : begin
      if (eg3_req)  eg3_nextstate = 3'b010;
      else eg3_nextstate = 3'b001;
       end
       eg3_state[1] : begin
      if (eg3_done) eg3_nextstate = 3'b100;
      else eg3_nextstate = 3'b010;

      a_eg3_req_during_busy : assert property (!eg3_req);
       end
       eg3_state[2] : begin
      eg3_nextstate = 3'b001;
       end
   endcase
    end
         
    // Equivalent assertion written outside procedural context
    a_eg3_a_req_during_busy : assert property (eg3_state[1] |-> !eg3_req);


    // Example 4:  Blocking assignment used as an intermediate calculation
    //      (Steven Sharp's example)

    logic eg4_sel1, eg4_sel0;
    logic [1:0] eg4_sel;

    // This just stages inputs by one cycle.
    always_ff @(posedge clk) begin
   eg4_sel1 <= eg4_sel1_in;
   eg4_sel0 <= eg4_sel0_in;
    end


    always @(posedge clk) begin
   eg4_sel = {eg4_sel1, eg4_sel0};
   case (eg4_sel)
     1:  begin
        eg4_q <= eg4_d0;
        a_eg4_d0_oh: assert property ($onehot(eg4_d0));
         end
     2:  begin
        eg4_q <= eg4_d1;
         end
     default: eg4_q <= eg4_d1;
   endcase
    end

    // Equivalent assertion from external
    // Note that assertion is using the intermediate value assigned by
    // the blocking assignment above
    a_eg4a_d0_oh :  assert property (eg4_sel[0] |-> $onehot(eg4_d0));



endmodule

-- ErikSeligman - 09 May 2008