search

YosysHQ / sby

SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
Other
379 stars 74 forks source link

Yosys doesn't work on btor pono engine. #257

Open CrazybinaryLi opened 6 months ago

CrazybinaryLi commented 6 months ago

I used SBY to verify the open-source processor core RIDECORE formally. The mode was set to BMC with a depth of 100 and a timeout of 3600. The engine selection was btor pono. However, I encountered errors every time I ran it. The error message is as follows: Elapsed clock time [H:MM:SS (secs)]: 0:04:55 (295) Elapsed process time [H:MM:SS (secs)]: 0:02:24 (144) engine_0 (btor pono) did not return a status engine_0 did not produce any traces

Gallagator commented 5 months ago

I think pono may have problems and hasn't been maintained for 2 years. I've spent some time trying to add it as a backend to https://github.com/ucb-bar/chiseltest and I reported the following issue: https://github.com/stanford-centaur/pono/issues/320. There seem to be other issues which I didn't report which you can see in my PR: https://github.com/ucb-bar/chiseltest/pull/702. It doesn't seem like btor pono will be working anytime soon.