Inherit in PSL for VUNIT (IFV verification)

A PSL vunit is bound to a Verilog instance or module, so you can't use it multiple times on a signal by signal basis. But you do have a couple of options that you can use to keep from having to repeat the assertions multiple times.

The easiest would be to use paramterized properties and assertions.

property no_grant_wo_req ( boolean gnt, req ) = never ( gnt && !req );
no_grant_port1: assert no_grant_wo_req ( gnt[1], req[1] );
no_grant_port2: assert no_grant_wo_req ( gnt[2], req[2] );
...

Another common method is to create a "verification component" (also commonly called a "vcomp") to check the protocol. This is a Verilog module that will check the operation of the protocol. It can be instantiated as many times as necessary and wired up to each of the ports or signals in question. This is the way that the OVL and IAL assertion libraries work.

module protocol_checker ( input clk, gnt, req, ... );
  // psl no_grant_wo_req: assert never ( gnt && !req ) @(posedge clk);
  ...
endmodule

These checker modules could then be instantiated and wired-up in the DUT's HDL (perhaps surrounded with some `defines or systhesis pragmas).

If you didn't want to edit the original HDL source code, you could use a single vunit to create multiple copies of this vcomp and wire them up to the ports of the DUT.  We can use a vunit for more than just PSL, we can actually put the HDL statements that will instantiate the checker into our vunit.

vunit dut_checker(dut) {
  protocol_checker chk1 ( clk, gnt[1], req[1], ... );
  protocol_checker chk2 ( clk, gnt[2], req[2], ... );
}

 Thanks!

You helped a lot!