Синтезируемая задержка в Verilog

-1

Я хочу синтезировать код SystemVerilog, который имеет задержку, записанную как ## 1, но синтезатор дает синтаксические ошибки, поскольку задержка не может быть синтезирована. Я хочу знать, есть ли способ дать задержку, которая будет синтезирована? Например, это утверждение SystemVerilog в коде с задержкамиСинтезируемая задержка в Verilog

assert property ((req1 == 0) ## 1 (req1 == 1) ## 1! (Req2 == 1) || (gnt1 == 0));

Как я могу синтезировать это без потери его поведения?

источник

2016-11-22 mii9

Свойства не являются частью Verilog, а являются частью SystemVerilog. Более того, сами свойства не синтезируются. Свойства используются в операциях cover или assert в среде моделирования.

Что касается задержек, то ваш единственный вариант - использовать триггер для задержки сигнала. В вашей собственности ##1 означает «на следующем краю», предполагая, что ваше свойство имеет некоторые связанные с ним часы (либо в инструкции cover/assert, либо в том, что он находится в блоке синхронизации).

Для создания синтезируемого цикла задержки в противном случае синтезируемого код:

[email protected](posedge ck or posedge arst) begin 
    if(arst) 
    data_delayed <= '0; 
    else 
    data_delayed <= data; 
end

источник

2016-11-22 12:32:41 Hida

Да, вы правы, свойства в коде указаны с использованием утверждений SystemVerilog. Я на самом деле пытаюсь преобразовать код описания оборудования в формально проверяемый код. Вот почему я использую утверждения для указания свойств и передачи их на синтезатор, который нужно преобразовать для проверки. Синтезатор просто не принимает синтаксис задержки, используемый i.e ## 1 в свойствах. Вышеупомянутый единственный способ моделировать задержку для синтезатора? – mii9

Вы не можете синтезировать свойства, и я подозреваю, что это не так, как работает ваш официальный верификатор. В моем (ограниченном) опыте с формальной проверкой формальный инструмент берет вашу реализацию как один входной и HDL-свойства в качестве другого. Таким образом, свойства не синтезируются и могут быть записаны обычным способом. Возможно, вы должны задать другой вопрос, где вы предоставляете больше информации о том, какой инструмент вы используете, и о том, как вы пытаетесь его использовать. – Hida

Вы написали не имеет никакого смысла. Вы не можете добавлять задержки в середине булевого выражения. Вы имели в виду написать последовательность выражений? Тогда правильный синтаксис будет

sequence s1; 
((req1 == 0) ##1(req1 == 1) ##1 !(req2 == 1) || (gnt1 == 0)); 
endsequence

источник

2016-11-22 15:06:30

Да, вы правы. Это правильный путь, извините мою ошибку. Большое спасибо. Но все же синтаксис задержки должен использоваться для указанного поведения, и синтезатор дает синтаксические ошибки из-за этого. Он отлично работает для свойств без синтаксиса. – mii9

ответ

Смежные вопросы