Questions for stimulus

SystemVerilog
,
1

Hi All, I have a DUT which has 4 fifo, and I verify this DUT using FPV
there are two inputs , and one output

input       wr_vld;
input [1:0] id;
output [3:0] full;

When full[3:0]=4'b0001; it means fifo (id=0) is full, so we can not push data to that fifo(id=0), but we can push data to fifo(id=1,2,3)
There are assumptions to constraint two inputs. I don’t know which one is correct
Here are sudo code

A: 
for(int i=0;i<4;i++)
assume(wr_vld & (id==i) |-> !full[i])
B:
for(int i=0;i<4;i++)
assume(wr_vld & full[i] |-> id!=i)
C:
for(int i=0;i<4;i++)
assume(wr_vld  |-> !full[i] & (id==i))

Q1: Assumption A ,B,C are equivalent? Which one is correct?

Q2: In my tb, i also have a fifo model. And there is signal called full_model
what is the problem in this assumption?
assume(wr_vld & (id==i) |-> !full_model[i])

I am confused . Please explain to me in detail
Thanks a lot!

3

An overlapping implication X |-> Y as a constraint when A and B or both boolean expressions is the same as the expression !X || Y.
The first assume equation can be re-written

!(wr_vld & (id==i)) || !full[i] // becomes
!wr_vld || id!=i || !full[i]]

which is equivalent to the second assume expression. I’ll leave it to you to work out the third assumption.

Can’t answer your second question without knowing what the full_model signal represents.

4

here is fifo model

always@(posedge clk or negedge rst_n)
  if(~rst_n)
     cnt <='d0l
  else if(push)
     cnt <= cnt+1;
  else if(pop)
     cnt<= cnt-1;

wire full_model = cnt ==7;

Using assume(wr_vld & (id==i) |-> !full_model[i]) .
Q1:full_model will be multi-driven?
Q2:As I know, the formal tool will assign the value in the right side of assertion. In my case, wr_vld & id will be driven by tool?
Thank you