Bind Assertion in SystemVerilog

When RTL is already written and it becomes responsibility of a verification engineer to add assertion. And RTL designer does not want verification engineer to modify his RTL for the sake of adding assertion then, bind feature of SystemVerilog comes for rescue.

One can write all the assertion he or she wants to write in a separate file and using bind, he or she can bind the ports of his assertion file with the port/signals of the RTL in his test-bench code. What a cool feature.

The bind directive can be specified in any of the following:

• A module
• An interface
• A compilation-unit scope

There are three forms of bind syntax.

1. Binding is done to ALL instances of a module.
2. Binding is done to single instance of a module.
3. Binding is done to list of (multiple) instance of a module.

//=================================================
// Actual DUT RTL
//=================================================
module dut (
            input  wire clk,
            input  wire req,
            input  wire reset,
            output reg  gnt
           );
  always @ (posedge clk)
  begin
    gnt <= req;
  end
endmodule : dut
//=================================================

//=================================================
// Assertion Module
//=================================================
module assertion_module(
                        input wire clk_ip,
                        input wire req_ip,
                        input wire reset_ip,
                        input wire gnt_ip
                       );
  //=================================================
  // Sequence Layer
  //=================================================
  sequence req_gnt_seq;
    (~req_ip & gnt_ip) ##1 (~req_ip & ~gnt_ip);
  endsequence
  //=================================================
  // Property Specification Layer
  //=================================================
  property req_gnt_prop;
    @ (posedge clk_ip)
      disable iff (reset_ip)
        req_ip |=> req_gnt_seq;
  endproperty
  //=================================================
  // Assertion Directive Layer
  //=================================================
  req_gnt_assert : assert property (req_gnt_prop)
                   else
                   begin
                     $display("@%0dns Assertion Failed", $time);
                   end
endmodule : assertion_module
//=================================================


//=================================================
// Bind Module
//=================================================
module binding_module();
//=================================================
// Bind by Module name : This will bind ALL instance of DUT
//=================================================
// Syntax:
//   bind   RTL_Module_Name   Assertion_module_Name   Instance_Name

  bind dut assertion_module U_assert_ip (
                                         .clk_ip   (clk),
                                         .req_ip   (req),
                                         .reset_ip (reset),
                                         .gnt_ip   (gnt)
                                        );

//=================================================
// Bind by instance name : This will bind only one particular instance of DUT
//=================================================
// Syntax:
//   bind   RTL_Module_Name   :Instance_Path   Assertion_module_Name   Instance_Name

//  bind dut :$root.bind_assertion_tb.DUT_INST_1 assertion_module U_assert_ip (
//                                                                             .clk_ip   (clk),
//                                                                             .req_ip   (req),
//                                                                             .reset_ip (reset),
//                                                                             .gnt_ip   (gnt)
//                                                                            );

//=================================================
// Bind by instance name list : This will bind multiple instances of DUT
//=================================================
// Syntax:
//   bind   RTL_Module_Name   :Instance1_Path, Instance2_Path   Assertion_module_Name   Instance_Name
//  bind dut :$root.bind_assertion_tb.DUT_INST_1, $root.bind_assertion_tb.DUT_INST_2 assertion_module U_assert_ip (
//                                             .clk_ip   (clk),
//                                             .req_ip   (req),
//                                             .reset_ip (reset),
//                                             .gnt_ip   (gnt)
//                                           );

//=================================================
endmodule : binding_module


//=================================================
// TEST Module
//=================================================
module bind_assertion_tb();

  reg clk = 0;
  reg reset, req = 0;
  wire gnt;
 
  always #3 clk ++;
 
  initial begin
    reset <= 1;
    #20 reset <= 0;

    // Make the assertion pass
    #100 @ (posedge clk) req  <= 1;
    @ (posedge clk) req <= 0;

    // Make the assertion fail
    #100 @ (posedge clk) req  <= 1;
    repeat (5) @ (posedge clk);
    req <= 0;

    #10 $finish;
  end
 
  dut DUT_INST_1 (clk,req,reset,gnt);
  dut DUT_INST_2 (clk,req,reset,gnt);
  dut DUT_INST_3 (clk,req,reset,gnt);
 
endmodule : bind_assertion_tb


//=================================================
//Output:  Bind by Module name : This will bind ALL instance of DUT
//=================================================
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_1.U_assert_ip.req_gnt_assert: started at 237s failed at 243s
//        Offending '((~req_ip) & gnt_ip)'
//@243ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_2.U_assert_ip.req_gnt_assert: started at 237s failed at 243s
//        Offending '((~req_ip) & gnt_ip)'
//@243ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_3.U_assert_ip.req_gnt_assert: started at 237s failed at 243s
//        Offending '((~req_ip) & gnt_ip)'
//@243ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_1.U_assert_ip.req_gnt_assert: started at 243s failed at 249s
//        Offending '((~req_ip) & gnt_ip)'
//@249ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_2.U_assert_ip.req_gnt_assert: started at 243s failed at 249s
//        Offending '((~req_ip) & gnt_ip)'
//@249ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_3.U_assert_ip.req_gnt_assert: started at 243s failed at 249s
//        Offending '((~req_ip) & gnt_ip)'
//@249ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_1.U_assert_ip.req_gnt_assert: started at 249s failed at 255s
//        Offending '((~req_ip) & gnt_ip)'
//@255ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_2.U_assert_ip.req_gnt_assert: started at 249s failed at 255s
//        Offending '((~req_ip) & gnt_ip)'
//@255ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_3.U_assert_ip.req_gnt_assert: started at 249s failed at 255s
//        Offending '((~req_ip) & gnt_ip)'
//@255ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_1.U_assert_ip.req_gnt_assert: started at 255s failed at 261s
//        Offending '((~req_ip) & gnt_ip)'
//@261ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_2.U_assert_ip.req_gnt_assert: started at 255s failed at 261s
//        Offending '((~req_ip) & gnt_ip)'
//@261ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_3.U_assert_ip.req_gnt_assert: started at 255s failed at 261s
//        Offending '((~req_ip) & gnt_ip)'



//=================================================
//Output: Bind by instance name : This will bind only one particular instance of DUT
//=================================================
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST.U_assert_ip.req_gnt_assert: started at 237s failed at 243s
//        Offending '((~req_ip) & gnt_ip)'
//@243ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST.U_assert_ip.req_gnt_assert: started at 243s failed at 249s
//        Offending '((~req_ip) & gnt_ip)'
//@249ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST.U_assert_ip.req_gnt_assert: started at 249s failed at 255s
//        Offending '((~req_ip) & gnt_ip)'
//@255ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST.U_assert_ip.req_gnt_assert: started at 255s failed at 261s
//        Offending '((~req_ip) & gnt_ip)'
//@261ns Assertion Failed



//=================================================
//Output: Bind by instance name list : This will bind multiple instances of DUT
//=================================================
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_1.U_assert_ip.req_gnt_assert: started at 237s failed at 243s
//        Offending '((~req_ip) & gnt_ip)'
//@243ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_2.U_assert_ip.req_gnt_assert: started at 237s failed at 243s
//        Offending '((~req_ip) & gnt_ip)'
//@243ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_1.U_assert_ip.req_gnt_assert: started at 243s failed at 249s
//        Offending '((~req_ip) & gnt_ip)'
//@249ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_2.U_assert_ip.req_gnt_assert: started at 243s failed at 249s
//        Offending '((~req_ip) & gnt_ip)'
//@249ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_1.U_assert_ip.req_gnt_assert: started at 249s failed at 255s
//        Offending '((~req_ip) & gnt_ip)'
//@255ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_2.U_assert_ip.req_gnt_assert: started at 249s failed at 255s
//        Offending '((~req_ip) & gnt_ip)'
//@255ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_1.U_assert_ip.req_gnt_assert: started at 255s failed at 261s
//        Offending '((~req_ip) & gnt_ip)'
//@261ns Assertion Failed
//"bind_top.sv", 43: bind_assertion_tb.DUT_INST_2.U_assert_ip.req_gnt_assert: started at 255s failed at 261s
//        Offending '((~req_ip) & gnt_ip)'
//@261ns Assertion Failed