Chisel / Firrtl Verilog backend доказательство работы

Есть ли какие-то встроенные тесты или инструменты для формальной проверки дизайна chisel или firrtl по сравнению с сгенерированным verilog? На каких концепциях построен бэкэнд Verilog? Есть ли в нем баги?


chisel
person SpaceCowboy max    schedule 12.04.2018    source источник

Ответы (2)


arrow_upward
5
arrow_downward

В Chisel и FIRRTL нет встроенной формальной поддержки верификации. Нет никаких доказательств работы для компилятора или серверной части. Как и в любом традиционном компиляторе, здесь, безусловно, есть ошибки, хотя мы делаем все возможное, чтобы их отловить и исправить.

В настоящее время мы используем Yosys для выполнения LEC на нескольких экземплярах цепей FIRRTL между любыми изменениями, которые мы вносим в Кодовая база FIRRTL. Я хотел бы расширить использование формальной проверки, чтобы гарантировать, что различные преобразования в компиляторе не изменят семантику схем, на которых они работают. Мы также экспериментируем с серверными модулями проверки моделей, чтобы улучшить интеграцию с формальными инструментами проверки.

person Jack Koenig    schedule 12.04.2018

arrow_upward
2
arrow_downward

Начиная с FIRRTL v1.4 и Chisel v3.4, будет базовая поддержка примитивов проверки.

Если вы импортируете chisel3.experimental.verification, вы получите assert, assume и cover, которые генерируют соответствующие конструкции в Verilog.

import chisel3.experimental.{verification => v}

class Foo extends Module {
  val predicate: Bool
  v.assert(predicate)
}

Обратите внимание, что это довольно низкоуровневый интерфейс. В настоящее время я работаю над вспомогательной библиотекой, чтобы сделать формальную проверку в Chisel более доступной: https://github.com/tdb-alcorn/chisel-formal

person alcorn    schedule 24.08.2020