i need to write an assertion for an and gate with valid and enable on its inputs and outputs
inputs: a, b, valid_in, enable_in
outputs z, valid_out, enable_out
always @(posedge clk) begin
if (valid_in && enable_in)
tmp <= a&b;
if(valid_out && enable_out)
z <= tmp;
end
@t=0 : a=1 b=1
@t=1 : a=0, b=1
@t=3 : a=1,b=0 (@t=7 enable was low, so a,b inputs were not received)
@t=6: z=1
@t=8: z=0 (@t=7 enable was low, so z didnt receive output)
@t=9: z=0
i tried to write something like below as i dont know when exactly the valid_out and enable_out will be triggered, but this assertion passes only the first time and fails for subsequent a and b as it is always matching with the first valid_enable.
property check_and_1
@(posedge clk)
valid_in == 1 && enable_in ==1 && a==1 && b==1 |-> ##[1:$]valid_out ==1 && enable_out ==1 and z==1;
endproperty
property check_and_0
@(posedge clk)
valid_in == 1 && enable_in ==1 && (a!=1 || b!=1) |-> ##[1:$]valid_out ==1 && enable_out ==1 and z==0;
endproperty