1
Как я могу перевести утверждения о силе PSL или SVA в verilog вручную или автоматически с помощью инструмента с открытым исходным кодом? я могу сделать простые свойства безопасности, но я не имею понятия о свойствах жизнеспособности. Я знаю, что некоторые коммерческие инструменты имеют эту функцию для проверки конструкций Verilog, но у меня нет доступа к ним.Как преобразовать утверждения/свойства PSL или SVA в Verilog?
Например, я хочу перевести утверждение о живучести в PSL, например assert always req -> eventually! ack;, в эквивалентную цепочку Verilog, чтобы я мог использовать некоторые инструменты для моделирования, проверяя, существует ли это свойство.
- Редактировать было сделано, чтобы перефразировать из «возможно ли перевести ...» на «как мне переводить» спасибо ira!
Если некоторые существующие коммерческие инструменты могут это сделать, то вы тоже можете. Каков ваш конкретный вопрос? [Есть неявный вопрос: «учитывая, что у вас есть алгоритм для реализации, какая лучшая инфраструктура для этого?»] –
перефразировал мой вопрос - спасибо за указание! – adrianX
Дешевый трюк заключается в том, чтобы предположить, что «в конечном итоге» означает некоторое ограниченное количество часов. Затем «req == false» содержит сброс счетчика, иначе счетчик подсчитывает часы; когда бит 2^N в счетчике идет верно, настаивайте, что «2^N подразумевает ack». Я думаю, вы можете обобщить эту идею на более сложные временные условия с большим количеством счетчиков и каскадной проверки. Если логика «ack» является чисто комбинационной, достаточно одного такта («N = 1»). Я уверен, что есть более умные вещи, которые вы можете сделать, поэтому это только комментарий, но это даст вам удобную отправную точку. –