I was asked to verify a DUT, it has a single input and 2 outputs.
Packet entering the DUT on input and can leave through one of the outputs but not through both of them.
How can I identify and issue an error when same packet is monitored on same clk on both output ports?
On different clock cycles it is easy to catch.
In reply to Michael54:
What bit of information controls which output is selected?
You can’t just look at the data and say it should be that one and not this one, unless that bit of info is in the header of the packet.
In any case, you need to get access to that control bit of info and then make a decision by evaluating the activity of the packets in the outputs.
Each packet has pkt_id field, and let’s assume we don’t have any further info which could help us to determine through which output port it should leave the DUT.
Packet itself leaves through the output port with minor change in the packet header.
We just want to check packet leaves only from a single output port and not through both ports.
In reply to Michael54:
Here is a possible way using the sync signals that detect the start of packet.
module pkt(input bit clk, din, output bit do1, do2);
endmodule
module top;
/* Each packet has pkt_id field, and let's assume we don't have any further info
which could help us to determine through which output port it should leave the DUT.
Packet itself leaves through the output port with minor change in the packet header.
We just want to check packet leaves only from a single output port and not through both ports. */
bit clk, clk1, cl2, sync1, sync2, id1, id2;
// Instantiate packet module here
pkt pkt1(.*);
// Logic to detect sync1, sync2
ap_synchronous_no2outputs: assert property(@ (posedge clk)
$rose(sync1) || $rose(sync2) |-> not(sync1 && sync2));
// Can also write assertions on IDs if needed.
// For asynconous, if both outsputs are source, they'll do that with 10 cycle
// (am assumeing 10
let max_async_distance = 10;
ap_Asynchronous_no2outputs1_2: assert property(@ (posedge clk1)
$rose(sync1) |-> not(##[1:max_async_distance] sync2));
ap_Asynchronous_no2outputs2_1: assert property(@ (posedge clk1)
$rose(sync2) |-> not(##[1:max_async_distance] sync1));
endmodule