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

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

В своих поисках я обнаружил следующее:

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

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


system-verilog system-verilog-assertions
person user1220086    schedule 08.07.2013    source источник

Ответы (2)


arrow_upward
2
arrow_downward 

$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];
person Greg    schedule 08.07.2013
comment
Интересным моментом здесь является то, что вы (правильно) используете $rose() для условия включения. Причина, по которой вы делаете это, а не только req |-> ..., заключается в том, что вы не создаете поток утверждения каждый цикл, когда req высокий, а только первый. Это большая победа в производительности. - person Paul S; 11.07.2013

arrow_upward
0
arrow_downward

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

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

person V from QC    schedule 19.07.2013