SVA для рукопожатия

Question

Я пытаюсь написать утверждение SVA для процедуры рукопожатия.

В моих поисках я нашел следующий:

property p_handshake(clk,req,ack); 
@(posedge clk) 
req |=> !req [*1:max] ##0 ack; 
endproperty 
assert property(p_handshake(clock,valid,done)); 

Однако мой «сделано» сигнал разрешается приходить много циклов после того, как действует цикл переходит на высоком уровне. Как вы делаете это заявление, убедитесь, что «сделано» указано на любой точка после того, как действительный утверждается, без действительного удаления?

Answer 1

$rose(req) |=> req[*1:$] ##0 ack; 

$rose начнет утверждение на нарастающем фронте req. [*1:$] означает, что левая сторона должна быть верной для диапазона от 1 до неограниченного количества часов. Вы можете использовать [+], что эквивалентно [*1:$].

Некоторые другие стили написания проверки будет:

$rose(req) |-> req[*1:$] ##1 (ack && req); 
$rose(req) |-> ##1 req throughout ack[->1]; 

Answer 2

не вы нуждаетесь в СВА, чтобы гарантировать, что, когда действительный $ Роуза, то сделано, уже не утверждал? Если вы это сделаете, тогда pls считают это SVA- $ rose (valid) | -> ~ done ## 1 $ stable (~ done) [* 949: 950] ## [1: $] done;

Вышеизложенное требует, чтобы оно не было подтверждено на период, за которым следует утверждение в будущем.