Question

To facilitate verification separate from the design, it is possible to specify properties and bind them to specific modules or instances. The following are the goals of providing this feature:

• It allows verification engineers to verify with minimum changes to the design code/files.
• It allows a convenient mechanism to attach verification IP to a module or an instance.
• No semantic changes to the assertions are introduced due to this feature. It is equivalent to writing properties external to a module, using hierarchical path names.

With this feature, a user can bind a module, interface, or program instance to a module or a module instance.

The syntax of the bind construct is:

bind_directive ::= bind hierarchical_identifier constant_select bind_instantiation;
                                                                // from Annex A.1.5
bind_instantiation ::=
    program_instantiation
  | module_instantiation
  | interface_instantiation

Syntax 17-17—bind construct syntax (excerpt from Annex A)

The bind directive can be specified in

• a module
• an interface
• a compilation-unit scope

A program block contains non-design code (either testbench or properties) and executes in the Reactive region, as explained in Section 16.

Example of binding a program instance to a module:

bind cpu fpu_props fpu_rules_1(a,b,c);

Where:

• cpu is the name of module.
• fpu_props is the name of the program containing properties.
• fpu_rules_1 is the program instance name.
• Ports (a, b,c) get bound to signals (a,b,c) of module cpu.
• Every instance of cpu gets the properties.

Example of binding a program instance to a specific instance of a module:

bind cpu1 fpu_props fpu_rules_1(a,b,c);

By binding a program to a module or an instance, the program becomes part of the bound object. The names of assertion-related declarations can be referenced using the SystemVerilog hierarchical naming conventions.

Binding of a module instance or an interface instance works the same way as described for programs above.

interface range (input clk,enable, input int minval,expr);
    property crange_en;
        @(posedge clk) enable |-> (minval <= expr);
    endproperty

    range_chk: assert property (crange_en);
endinteface

bind cr_unit range r1(c_clk,c_en,v_low,(in1&&in2));

In this example, interface range is instantiated in the module cr_unit. Effectively, every instance of module cr_unit shall contain the interface instance r1.