search

chipsalliance / UHDM

Universal Hardware Data Model. A complete modeling of the IEEE SystemVerilog Object Model with VPI Interface, Elaborator, Serialization, Visitor and Listener. Used as a compiled interchange format in between SystemVerilog tools. Compiles on Linux gcc, Windows msys2-gcc & msvc, OsX
Apache License 2.0
186 stars 38 forks source link

Is it possible write SMT2 file from UHDM(Bypassing Yosys)? #1077

Open easyformal opened 2 weeks ago

easyformal commented 2 weeks ago

I know that UHDM can be imported into Yosys AST, and after Yosys performs synthesis, it can generate an SMT2 file. But for some formal verification apps, synthesis is unnecessary, and importing into Yosys and synthesizing takes too much time. Is it possible to generate an SMT2 file directly from UHDM? If so, what do I need to do? Thank you.

alaindargelas commented 6 days ago

@easyformal , you'd have to write your own writer using the VPI (Or C++) APIs, probably a lot of work! When using Synthesis, you don't have to perform any of the optimizations when you want to run formal proofs (Unless you are trying to debug Synthesis itself, which does not seem to be your problem). Disabling all optimizations in Yosys might give you the speed you need, or using a faster Yosys: Yosys has some notoriously slow optimizations passes (Really silly N^2 behavior or worse). Most of them have been optimized in this Yosys Hard fork (Which also supports Synlig/Sulreog/UHDM): https://github.com/os-fpga/yosys_verific_rs