Looking at your assertion, it won't capture the immediate ACK because you are expecting a sequence excluding an immediate ACK with !ack
. I would re-write your assertion as:
sequence seq;
$stable({address, data}) ##[0:63] (val && ack && $stable({address, data})) ##1 !ack ##1 !val;
endsequence
property p;
@(posedge clk)
$rose(val) |=> seq;
endproperty
as_protocol : assert property(p);
与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…