Binding with assertions

Binding is the process of associating assertions, written in SystemVerilog Assertion (SVA) constructs, with a design module or interface without directly modifying the source code of the DUT. This approach is particularly beneficial in:

  • Keeping the design and verification code separate.
  • Facilitating modular verification.
  • Reusing assertions across multiple designs or configurations.

Why Use Binding?

Binding assertions provides several advantages:

  • Non-intrusive Verification: Assertions can be added without altering the original design code.
  • Modularity: Assertions can be written in separate files or modules, making them easier to manage.
  • Reusability: The same assertion can be reused across multiple modules or configurations.
  • Flexibility: Assertions can be selectively enabled or disabled during simulation.

Syntax

bind <design_module name/design_instance name> <assertion_module name> <bind_instance_name> (port_list);

Example:

We design a simple 4-bit counter that increments on every positive clock edge when enable is high. The counter resets to 0 when rst_n is low. In assertion module we define a property no_overflow that ensures the counter doesn’t overflow when enable is high. An assert statement checks the property and reports an error if violated.

// Design Module: Simple counter module
module counter(
    input logic clk,
    input logic rst_n,
    input logic enable,
    output logic [3:0] count
);
    always_ff @(posedge clk or negedge rst_n) begin
        if (!rst_n)
            count <= 4'b0;
        else if (enable)
            count <= count + 1;
    end
endmodule

// Assertion Module: Checks counter overflow condition
module counter_assertions(input logic clk, input logic rst_n, input logic enable, input logic [3:0] count);
    // Assertion: Counter should not overflow (count < 4'b1111)
    property no_overflow;
        @(posedge clk) disable iff (!rst_n) (enable && count == 4'b1111) |-> (count < 4'b1111);
    endproperty
    
    assert property(no_overflow) else $error("Counter overflow detected!");
endmodule

TB code:

// Testbench
`include "assertion.sv"

module tb;
    // Testbench signals
    logic clk;
    logic rst_n;
    logic enable;
    logic [3:0] count;

    // Instantiate the design under test (DUT)
    counter uut (
        .clk(clk),
        .rst_n(rst_n),
        .enable(enable),
        .count(count)
    );

    // Bind the assertion module to the DUT
    bind counter counter_assertions assertions_inst (.clk(clk), .rst_n(rst_n), .enable(enable), .count(count));

    // Clock generation
    initial begin
        clk = 0;
        forever #5 clk = ~clk;
    end

    // Test stimulus
    initial begin
        rst_n = 0;
        enable = 0;
        #10 rst_n = 1;   // Release reset
        #10 enable = 1;  // Enable the counter
        #100 enable = 0; // Disable the counter
        #20 enable = 1;  // Re-enable the counter
        #100;
        $stop;
    end
  
  initial begin
    $monitor("at time %0t, rst = %0d, enable=%0d, count=%0d",$time,rst_n,enable,count);
  end
  
endmodule

Output:

at time 0, rst = 0, enable=0, count=0
at time 10, rst = 1, enable=0, count=0
at time 20, rst = 1, enable=1, count=0
at time 25, rst = 1, enable=1, count=1
at time 35, rst = 1, enable=1, count=2
at time 45, rst = 1, enable=1, count=3
at time 55, rst = 1, enable=1, count=4
at time 65, rst = 1, enable=1, count=5
at time 75, rst = 1, enable=1, count=6
at time 85, rst = 1, enable=1, count=7
at time 95, rst = 1, enable=1, count=8
at time 105, rst = 1, enable=1, count=9
at time 115, rst = 1, enable=1, count=10
at time 120, rst = 1, enable=0, count=10
at time 140, rst = 1, enable=1, count=10
at time 145, rst = 1, enable=1, count=11
at time 155, rst = 1, enable=1, count=12
at time 165, rst = 1, enable=1, count=13
at time 175, rst = 1, enable=1, count=14
at time 185, rst = 1, enable=1, count=15
"assertion.sv", 7: tb.uut.assertions_inst.unnamed$$_0: started at 195ns failed at 195ns
	Offending '(count < 4'b1111)'
Error: "assertion.sv", 7: tb.uut.assertions_inst.unnamed$$_0: at time 195 ns
Counter overflow detected!
Execute on

Binding Assertions to an Interface

Interfaces are often used to encapsulate communication signals in a design. Binding assertions to an interface allows you to monitor and verify protocol compliance directly at the interface level.

Example: Binding with an Interface

Consider a simple AXI-like interface:

interface axi_interface;
    logic clk;
    logic reset_n;
    logic valid;
    logic ready;
endinterface

You want to assert that when valid is high, ready must eventually go high.

  1. Write the Assertion Module
    Create a module containing the assertions:
module axi_assertions (
    axi_interface axi_if
);
    property valid_to_ready;
        @(posedge axi_if.clk) disable iff (!axi_if.reset_n)
        axi_if.valid |=> axi_if.ready;
    endproperty

    assert property (valid_to_ready) else $error("ready not asserted after valid");
endmodule

Bind the Assertion Module to the Interface Instance in top level module.

module top;
    axi_interface axi_if();

    my_design dut (
        .clk(axi_if.clk),
        .reset_n(axi_if.reset_n),
        .valid(axi_if.valid),
        .ready(axi_if.ready)
    );

    bind axi_interface axi_assertions u_axi_assertions (.*);
endmodule

Here, the axi_assertions module is bound to the axi_interface instance, ensuring that all signals within the interface adhere to the defined assertion.

Previous
Next