TomProceduralAssertExamples < P1800

P1800 Web>SystemVerilogSpecialCommittee>TomProceduralAssertExamples (2008-05-09, ErikSeligman) (raw view)EditAttach
<verbatim>

/*****************************************************************************
 * 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


</verbatim>

-- Main.ErikSeligman - 09 May 2008
Topic revision: r1 - 2008-05-09 - 19:23:31 - ErikSeligman
P1800