Формальная проверка с помощью Chisel

Можно ли выполнить формальную проверку с помощью языка HDL Chisel3? Если да, есть ли для этого программное обеспечение с открытым исходным кодом? Я знаю, что мы можем сделать формальную проверку Verilog с Yosys, но с chisel?


hdl formal-verification chisel
person FabienM    schedule 16.03.2018    source источник

Ответы (3)


arrow_upward
2
arrow_downward

SpaceCowboy задал тот же вопрос здесь. И Джокенинг ответил ему: не знаю, но, может быть, это будет сделано.

person FabienM    schedule 13.04.2018
comment
Мои извинения за то, что я пропустил этот вопрос, когда вы изначально его задали. - person Jack Koenig; 17.04.2018

arrow_upward
1
arrow_downward

Yosys-smtbmc можно использовать с небольшими хитростями, описанными здесь. для «внедрения» формальных свойств в созданный Verilog.

person FabienM    schedule 04.02.2020

arrow_upward
1
arrow_downward

Теперь есть пакет chisel с именем chisel-formal.

import chisel3.formal._

Это расширяет Module чертой с именем Formal.

class MyModule extends Module with Formal {
//...
      past(io.Mwrite, 1) (pMwrite => {
        when(io.Mwrite === true.B) {
          assert(pMwrite === false.B)
        }
      })
      cover(countreg === 10.U)
//...
}

Это позволяет использовать функции assert(), accept(), cover(), past(), ....

Полное руководство приведено в репозитории github.

person FabienM    schedule 19.10.2020