Given that a DUT uses a modport in its interface definition shown below -
module DUT
(
input clk,
input resetn,
dut_if.initiator if1
);
endmodule
And interface itself looks like -
interface dut_if ;
logic req;
logic gnt;
modport initiator {output req, input gnt};
modport responder {input req, output gnt};
endinterface
If I have write a SVA module with some properties, conventional wisdom says - all ports of a DUT are inputs to a SVA module that’s supposed to be bound to the DUT.
How do I define the ports of SVA module (specifically the signals in modport) so that I can bind successfully?
PS: I did checkout the various other questions in the forum. Most of the examples were using only 'input' ports in the interface/modport.. Didnt find one modport with both direction ports..
I do not understand why the dut_if modport directions matter here. The SVA module that gets bound inside the DUT module would still be inputs.
Hi @dave_59 ,
Here if the DUT interface were -
input clk,
input resetn,
input req,
output gnt
And the SVA module ports were are all inputs, then SVA bind works. That’s traditional formal bench.
there are 2 issues -
1… But with the DUT having a modport at the interface, SVA input ports (sepa**rate req/gnt signals**) can’t be bound to the modport, because they dont match the modport type.
2… And SVA needs all signals as inputs, and there is no such modport to instantiate…
3… Even if there was a modport with all inputs, to be used in SVA, can’t bind that modport to the DUT’s modport, because they are different…
Hope it makes it clear…
Your issue has nothing to do with the bind construct. You can always instantiate a module without an interface with signals from members of an interface. Let’s say your SVA module looked like:
module sva (
input clk,
input resetn,
input req,
input gnt);
// ...
endmodule
Then inside your DUT module, you can instantiate this module as:
sva s1(clk,resetn,if1.req,if1.gnt);
Oh yes. That is what I ended up doing.
But that’s not the ideal solution. RTL designers dont want to modify their file to include verification files.
That is where - bind - comes in handy. Your file is very much separated from RTL files. And won’t compile/bind, if the SVA file is specifically not passed for compilation.
And looks like the bind in this case doesn’t work. I was trying to see if I am missing something?
I think we need support in SystemVerilog to be able to bind directly to a modport, for formal verification purposes.
bind should have worked. Please show a complete example using
bind DUT sva s1(clk,resetn,if1.req,if1.gnt);
Hi Dave,
Yes, for a single dimension, that might work.
My design has multiple dimensions of the modport instance - as shown below…
module DUT
(
input clk,
input resetn,
dut_if.initiator if1[3:0]
);
endmodule
And interface itself looks like - as shown before in the thread above…
interface dut_if ;
logic req;
logic gnt;
modport initiator {output req, input gnt};
modport responder {input req, output gnt};
endinterface
In this case, how would I write the binds…?
- the (.*) won’t work
- Something like this -
sva s1(clk,resetn,if1.req,if1.gnt); won’t work as well…?
because here you would have to make sure to bind to - if1[0].req, if1[0].gnt, if1[1].req, if1[1].gnt etc…
It would really help to show a complete example. If you have
module sva (input wire clk,resetn,req,gnt);
//...
endmodule
Then you have multiple binds:
bind DUT sva s0(clk,resetn,if1[0].req,if1[0].gnt);
bind DUT sva s1(clk,resetn,if1[1].req,if1[1].gnt);
But if you have
module sva (input wire clk,resetn,req[4],gnt[4]);
//...
endmodule
The you can use an array assignment pattern
bind DUT sva s0(clk,resetn,
'{if1[0].req, if1[1].req, ...[2]...,...[3]...},
'{if1[0].gnt, if1[1].gnt, ...[2]...,...[3]...}
);
There might be other ways to accomplish this if you gave a more complete example.
Thanks Dave.
This solution isn’t scalable if we want to override different values to the bus width when based on parameters.
In my case, the dut.if1 is sized using a parameter with a default value of 64… and can be a bigger value in the places of instantiation.
Is there a more cleaner parameterized way of achieving this for scalability?
@varunr86, with every post, you add missing information.
If you want people to help you, please show us a minimal, complete example of the what the code looks like before the bind. And then show us some example of the SVA modules you want to add using bind with the port connections you would like to see.
Apologies on the delay to follow up @dave_59
DUT module is same as previous example, except parameterized.
Here are the SVA, interface, and DUT…
Interface - from before…
interface dut_if ;
logic [NUM_REQS-1:0] req; //// Each bit pair of req/gnt is a handshake.. and there are NUM_REQs of them..
logic [NUM_REQS-1:0] gnt;
modport initiator {output req, input gnt};
modport responder {input req, output gnt};
endinterface
DUT - updated…
module DUT
(
input clk,
input resetn,
dut_if.initiator if1[NUM_PORTS-1:0]
);
endmodule
SVA code (mainly port is what I am looking for…
SVA - ??
module sva (
input clk,
input resetn,
// What's this line going to be??
input logic [NUM_REQS-1:0] req [NUM_PORTS-1:0],
/// What's this line going to be..??
input logic [NUM_REQS-1:0] gnt [NUM_PORTS-1:0] );
// ...
endmodule
and how will the bind look…?
Hi @dave_59 , any thoughts on the query shared above. Let me know if feel anything more is needed from my side. Would appreciate your inputs. Keen on knowing if this could be done in a scalable manner.
As I Said before, If you want people to help you, please show us a minimal, complete example of the what the code looks like before the bind.
Show all the interface connections. Why not have NUM_PORTS a parameter of the interface creating arrays of req/gnt?
@dave_59 I am not sure, what you are not finding complete here. Can you elaborate, what else you think is missing?
As for having NUM_PORTS be a parameter of the interface, thats not how the RTL looks on my end. It looks exactly like how I pasted above…
Your question is a design implementation question.
I am trying to see how I can write SVA for the RTL at-hand.