Binding in Systemverilog

Assertions are written both by design engineers and verification engineers depending on what is being checked and wherein the design hierarchy. If Assertions reside inside design modules which are going to be synthesized then these assertions which solely meant for checking/verification have to be enclosed inside compilation directives like ifdef so they can be hidden from Synthesis tools. As an alternative, Systemverilog provides bind feature which allows specific modules which contain all the assertions to be bound during elaboration. This feature essentially instantiates assertion module inside design module and all the assertions behave as if they reside inside the design. This enables engineers to keep verification code separate from design code.

Syntax:

bind <target RTL module> [:<name of the target instances>] <assertion module> <binding instance name> (<port list>);

where
[<name of target instance>] is optional. If nothing is specified, binding is done on all the target RTL module instances

<assertion module> is the module which contains all the assertion code.

<port list> is the port connections from target RTL module to assertion module.

Assertion module is like any other module. Keep below points in mind:

• Define all the inputs required for assertions as input ports.
• No outputs from assertion module as it is strictly not for driving anything into the design
• Input Port names can be name. If you decide to keep the same port names as the net name of target design module then you while binding .* would automap the connections. Connect by name if the input port name is different from the net in the target design module
• If any internal probes from instances below target design module are required for the assertion then same can be made as input to the assertion module and passed as an argument while making assign hierarchical probing at the target module. This should be avoided for any synthesizable block and usage is mostly intended for bmod assertions which requires internal probing

Ex:
Binding to all modules with name module_name:
bind module_name inst2_assert inst2a(.mode(mode_value),
                                                               .order(order)
                                                             );


Binding to the specific instance with name inst2 (Instance binding):
bind module_name:inst2 inst2_assert inst2a(.mode(mode_value),
                                                                       .order(order)
                                                                       );

Ex:

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

view raw binding_assertion.sv hosted with ❤ by GitHub