search

YosysHQ / sby

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

fib liveness example : suprove command not found #205

Closed lzxqaq closed 2 years ago

lzxqaq commented 2 years ago

When I run this example "sby/docs/examples/demos/fib". I found no suprove command for oss-cad-suite-windows-x64-20220801.

SBY 11:15:16 [fib_live] engine_0: aiger suprove
SBY 11:15:16 [fib_live] base: starting process "cd fib_live/src& yosys -ql ../model/design.log ../model/design.ys"
SBY 11:15:17 [fib_live] base: finished (returncode=0)
SBY 11:15:17 [fib_live] aig: starting process "cd fib_live/model& yosys -ql design_aiger.log design_aiger.ys"
SBY 11:15:18 [fib_live] aig: finished (returncode=0)
SBY 11:15:18 [fib_live] engine_0: starting process "cd fib_live& suprove +simple_liveness model/design_aiger.aig"
SBY 11:15:18 [fib_live] engine_0: finished (returncode=9009)
SBY 11:15:18 [fib_live] engine_0: COMMAND NOT FOUND. ERROR.
SBY 11:15:18 [fib_live] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:01 (1)
SBY 11:15:18 [fib_live] summary: Elapsed process time unvailable on Windows
SBY 11:15:18 [fib_live] DONE (ERROR, rc=16)
SBY 11:15:18 The following tasks failed: ['live']
nakengelhardt commented 2 years ago

Unfortunately, the suprove solver is only available on linux (it's been unmaintained for years and it's a struggle to get it to work at all).