Hierarchial properties

SystemVerilog
1

Does anyone know, if it’s possible to do “hierarchial properties” with one systemverilog file?

For example: There’s design TOP and it references design SUB (instance name could be TOP_i.SUB_i). I can make an assume properties like these:

property A;
    top_signal == 1 && 
    $root.some_signal == 1;
endproperty

property B;
    $root.SUB_i.some_other_signal == 1;
endproperty

But is there way to point to inside of SUB without the $root.SUB_i.* part?

I now have different systemverilog “testbench” for the sub modules, but that’s not really convenient. When verifying small designs, it would be nice to do all with one file and one run. Also if there are multiple instances of SUB, then the same assumes/asserts would be automatically propagated.

2

Assertion binding concept (‘bind’) of SV will be of use here.

Group all the properties related to a specific module interface/module (say ‘mod1’) together in a module, say ‘asserts_mod1’. Then ‘asserts_mod’ can be binded to all instances (mod1_inst1, mod1_inst2) of the same module(mod1) in the tb top, so that the same set of assertions are active on all the instances.

This way(using ‘bind’), the paths to the signals used in the properties are not required anymore and hence no question of updating them.

3

In reply to S.P.Rajkumar.V:

Thanks you for the answer. This bind seems to be the way to go.

There seems to be a lot of information about systemverilog/assertion syntax etc. but very little on the methodology side. If you have a RTL module, then how do you really check it with formal tools. Now I am trying to split the design into smaller assertions sets and this binding could come handy.

4

In reply to Jarno:

There are books and dozens of papers written on using bind to place SystemVerilog assertions in RTL designs. Just seach the words in bold.