search

tdb-alcorn / chisel-formal

Other
23 stars 3 forks source link

FYI: firrtl's SMT backend #1

Open ekiwi opened 4 years ago

ekiwi commented 4 years ago

Hi Tom,

Thanks a lot for starting the model checking support and now this library effort.

Just wanted to let you know that I recently wrote a SMT backend for firrtl which made it into the 1.4 release candidate. So now you could use btormc or pono without having to go through yosys.

Checkout this PR and please ask me any questions that might come up: https://github.com/freechipsproject/firrtl/pull/1826

The PR also has a small smtbmc clone (with much reduced functionality) which shows how the generated SMTLib expressions can be used: https://github.com/freechipsproject/firrtl/blob/f1c314e6c7e116df33ffc215ec907212037292dc/src/test/scala/firrtl/backends/experimental/smt/end2end/EndToEndSMTSpec.scala#L161

ekiwi commented 3 years ago

@tdb-alcorn Just wanted to let you know that I am going to add simple BMC support with the firrtl SMT backend to chiseltest: https://github.com/ucb-bar/chisel-testers2/pull/356

tdb-alcorn commented 3 years ago

@ekiwi amazing!

ekiwi commented 3 years ago

@ekiwi amazing!

Working on a better past now :)

ekiwi commented 3 years ago

@tdb-alcorn Would love to hear your thoughts on: https://github.com/ucb-bar/chisel-testers2/pull/386