Как написать свойство для формальной проверки?

property prop1;
@(posedge clk)
$fell(sig1) ##1 sequence1 |-> sequence2;
endproperty

Я хочу отключить свойство iff sig1=1'b1 после первого такта.

Переход от высокого уровня к низкому на sig1 является моим условием срабатывания. Если я сделаю disable iff(sig1) условие срабатывания не будет выполнено.

Также использование throughout невозможно как для разрешающих, так и для удовлетворяющих последовательностей в формальных верификаторах.

Как мне это сделать? Спасибо!


system-verilog formal-verification system-verilog-assertions
person kkdev    schedule 12.05.2016    source источник
comment
Пожалуйста, будьте подробнее. Почему нельзя использовать disable iff (sig1);?   -  person sharvil111    schedule 12.05.2016
comment
переход от высокого уровня к низкому на сигнале 1 является моим условием срабатывания. Если я отключу iff(sig1), условие срабатывания не будет выполнено.   -  person kkdev    schedule 12.05.2016
comment
Обновлено. Просто примечание. Можете ли вы использовать неперекрывающийся (|=›) оператор, чтобы только когда $fell(sig1) оценивается как TRUE, тогда оценивалась только sequence1? Нравится: $fell(sig1) |=> sequence1 |-> sequence2;   -  person sharvil111    schedule 12.05.2016
comment
Я совершенно уверен, что с точки зрения синтаксиса это невозможно, и мой вопрос отличается. отключение свойства после одного такта.   -  person kkdev    schedule 12.05.2016

Ответы (2)


arrow_upward
0
arrow_downward

Как насчет того, чтобы написать вспомогательный код для получения отложенной версии sig:

  always @(posedge clk) sig1d <= sig1;

  property prop1;
    @(posedge clk) disable iff(sig1d) 
    $fell(sig1) ##1 sequence1 |-> sequence2;
  endproperty

http://www.edaplayground.com/x/2tbX

person Matthew Taylor    schedule 12.05.2016
comment
если я не ошибаюсь, это все равно задерживает отключение iff на один такт от того, что я хочу сделать. - person kkdev; 13.05.2016
comment
Но заметьте, у меня все еще есть $fell(sig1) НЕ $fell(sig1d). Конечно, если бы вы хотели отключить его, даже если бы sig1 было высоким на первом такте, тогда $fell(sig1) никогда не было бы истинным? Возможно, нам нужна временная диаграмма? (Или изменить мой код, чтобы создать его?) - person Matthew Taylor; 13.05.2016
comment
@MatthewTaylor Вы должны быть осторожны с тем фактом, что выражение disable выбирается асинхронно и может привести к условиям гонки. Вы должны использовать disable iff ($sampled(sig1d)). - person Tudor Timi; 13.05.2016
comment
@MatthewTaylor: Кажется, приведенный вами код работает для моделирования (я не пробовал). Но на формальном инструменте это приводит к бессодержательному доказательству, что означает, что разрешающая последовательность не может быть реализована. - person kkdev; 14.05.2016
comment
@Тюдор Спасибо. Таким образом, sig1d будет управляться в регионе NBA, $fell(sig1) будет отбираться в регионе preponed и, предположительно, disable оцениваться (и, следовательно, sig1d отбираться) в наблюдаемом регион, отсюда и раса. - person Matthew Taylor; 15.05.2016

arrow_upward
0
arrow_downward

Вы можете переписать свое утверждение так, чтобы оно срабатывало только в том случае, если вы не видите sig1 high после первого цикла:

property prop1;
  @(posedge clk) disable iff(sig1d) 
    $fell(sig1) ##1 !sig1 ##0 sequence1 |-> sequence2;
endproperty
person Tudor Timi    schedule 13.05.2016
comment
Я уже пробовал это. Проблема в том, что я не могу сделать это на sequence2. Например: $fell(sig1) ##1 !sig1 повсюду (последовательность1) |->последовательность2; Но я не могу поставить на sequence2 (формальные инструменты этого не позволяют). Поэтому я подумал, что лучше всего отключить свойство на sig1 после одного цикла. Любые другие предложения приветствуются. - person kkdev; 14.05.2016
comment
@kkdev Из того, что я понял, вам следует перефразировать свой вопрос, потому что он неоднозначен. Вы не хотите отключать свойство, если sig1 становится высоким после первого цикла (что может быть истолковано как значение цикла после первых циклов). Вы хотите отключить его, если sig1 становится высоким в любом последующем цикле. Вы должны попробовать использовать ответ @MathewTaylor, так как это единственный способ. - person Tudor Timi; 15.05.2016