Binding Assertion Example

binding_assertion.sv

//design example
module design_module(
        input logic enable,
        input logic reset,
        input logic clk,
        output logic active);

    logic [1:0] fsm_cs;//current state
    logic [1:0] fsm_ns;//next state

    always @(posedge clk or posedge reset)
    begin
        if(reset)
            fsm_cs <= 2'b0;
        else
            fsm_cs <= fsm_ns;
    end

    always_comb
        case(fsm_cs)
            2'b00: if(enable==1'b1 && reset==1'b0)
                    fsm_ns=2'b1;
            2'b01: if(enable==1'b0 || reset==1'b1)
                    fsm_ns=2'b0;
            default: fsm_ns=2'b0;
        endcase

    assign active = (fsm_ns==2'b01) ? 1'b1:1'b0;
endmodule

//assertion module
module assertion_module(input logic fsm_state,input logic enable,input logic reset,input logic clk);

    property fsm_check();
        @(posedge clk)
            disable iff(reset) $rose(enable)|=> (fsm_state==2'b1);
    endproperty

    FSM_ASSERT:assert property(fsm_check) else `uvm_error("assertion_module", $sformatf("fsm assertion failed");

endmodule

//testbench top
module top();
    logic en,reset,tester_clk,active_out;

    initial
    begin
        tester_clk=1'b0;
        forever #10 tester_clk=~tester_clk;
    end

    design_module mydut(.enable(en),.reset(reset),.clk(tester_clk),.active(active_out));

    //binding assertion module(assertion_module) to design module(design_module)
    bind design_module assertion_module assert_instance(.fsm_state(fsm_cs),.enable(enable),.reset(reset),.clk(clk));

    initial
        begin
            #5;
            reset=1'b1;
            #10;
            reset=1'b0;
            #10
            en=1'b1;
            #100;
            $finish;
        end
endmodule