Hierarchically accessing a SVA module from TB_top

I have a SVA module (file sva_module.sv) as follows:


module sva_module(<port list>);
`define abc @(posedge clk)

// variables
logic req;
logic ack;

// assertions
assert property (`abc req |-> ##3 ack);
endmodule

I would like to be able to override the

 `define abc @(posedge clk) 

to

 `define abc @(posedge clk) disable iff rst 

But I would like to do this override from TB_top and not make any changes to the sva_module.sv file.

Is this possible? If not, is there another way by which I can control the assertions in the sva_module hierarchically from TB_top?

In reply to vk7715:

It is not possible to override the definition of abc the way you have written your sva_module.sv file from another file. You could if you had written it this way

module sva_module(<port list>);
`ifndef abc
  `define abc @(posedge clk)
`endif

AND you compile your module TB_top file with
`define abc
in it before the sva_module.sv file. You can also use a command line option
+define+abc=@(posedge clk) disable iff rst’
which overrides any compiler `define n the source code.

Because `define is a compiler directive, both these options apply to all instances of sva_module. You cannot have instance specific definitions of compiler directives.

If you require instance specific definitions, you need to provide a more complete example that describes how you plan instantiate sva_module.

In reply to dave_59:

Hi Dave, thank you for the answer. If not using defines, is there another way I can hierarchically control the assertions in the SVA module from TB_top?

To make it clear, this is the problem statement. I have some assertions in sva_module.sv, and I wish to control these assertions from TB_top and not make any changes to sva_module.sv (since this file is maintained by someone else).

Is there any way I can do this?

Please let me know.

Thanks,
VK

In reply to vk7715:

If all you want to do is disable the assertion, you can use $assertcontrol from the TB to turn on or off an assertion as some point in time. See section 20.11 Assertion control system tasks.

In reply to dave_59:

Hi Dave, thank you for your answer. I took a look at the section you mentioned, and I have two questions:


$assertcontrol ( control_type [ , [ assertion_type ] [ , [ directive_type ] [ , [ levels ]
[ , list_of_scopes_or_assertions ] ] ] ] ) ;

  1. In the above code, if I want to enable/disable all assertions in an SVA module, can I give the name of the module in the “list_of_scopes_or_assertions” field instead of individually naming all the assertions?

  2. If I want to enable/disable just 2 assertions, do I specify them as

 assert_1 && assert_2 

in the “list_of_scopes_or_assertions” field?

In reply to vk7715:

  1. A scope is an instance path name. The only time a module name works as a path name is an upwards reference (a top-level module is a kind of upward reference). You could use the bind construct to insert a module inside your sva_module.
  2. A list is comma separated: sva_module.assert_1, sva_module.assert_2

A better option might be to use your tools commands to turn on/off assertions which has much more flexibility in specifying paths (e.g. wildcards)

In reply to dave_59:

Hi Dave, thank you for your answer. I have two follow up questions.

1. Am I allowed to instantiate an SVA module like a design module in TB_top? What I mean is


module tb_top();

// some code here

sva_module i_sva; // ---> is this module instantiation allowed?

// or should it be something like this?
bind my_design sva_module i_sva (.*);

endmodule

2. In any case, if the sva_module instance name is i_sva, is this what I will have to enter in the “list_of_scopes_or_assertions” field?
For example:


module tb_top();

// some code here

// instantiate sva module here

$assert_control( control_type [ , [ assertion_type ] [ , [ directive_type ] [ , [ levels ]
[ , i_sva ] ] ] ] ) ; // turn on or turn off assertions within this module as needed

endmodule

In reply to vk7715:

The bind construct is just a syntactic shortcut making it easier to add assertions if that is what works for you.

//`define USE_BIND

module tb_top;
  bit clk;
  initial repeat(10) #5 clk=!clk;
  
  device dut(.*);
  
`ifdef USE_BIND
  bind subunit sva_module s(.clk, .A(sig1),.B(sig2));
`else  
  sva_module sva1(dut.u1.clk, dut.u1.sig1,dut.u1.sig2);
  sva_module sva2(dut.u2.clk, dut.u2.sig1,dut.u2.sig2);
  sva_module svaN(dut.uN.clk, dut.uN.sig1,dut.uN.sig2);
`endif  
endmodule

module device(input bit clk);
  
  subunit u1(.*);
  subunit u2(.*);
  subunit uN(.*);

endmodule

module subunit(input bit clk);
  
  wire sig1=0,sig2=1;
  
endmodule

module sva_module(input bit clk, wire A,B);

  A1: assert property (@(posedge clk) A == B);
  A2: assert property (@(posedge clk) B == A);

endmodule

You should try this both ways and look at the differences in the reported paths. The you can try different methods of controlling assertions.

In reply to dave_59:

Hi Dave, can you please clarify what you mean by “differences in the reported paths”?