With this change we are getting AIG based solvers to work and proper detection of command not found for windows.
Issue was conversion of command line sequential commands separator, since that was applied to actual command parameters where it is not applicable. Also we are now properly quoting parameters instead of using apostrophe.
There is special case when actual solver return error code 1, in that case we need to track if something got displayed by solver, and in case it does it is regular error, otherwise it is command not found.
SBY 12:58:24 [fib_cover] DONE (PASS, rc=0)
SBY 12:58:24 [fib_prove] Removing directory 'fib_prove'.
SBY 12:58:24 [fib_prove] Copy 'fib.sv' to 'fib_prove/src/fib.sv'.
SBY 12:58:24 [fib_prove] engine_0: abc pdr
SBY 12:58:24 [fib_prove] nomem: starting process "cd fib_prove/src& yosys -ql ..
/model/design_nomem.log ../model/design_nomem.ys"
SBY 12:58:24 [fib_prove] nomem: VERIFIC-WARNING [VERI-1209] fib.sv:27: expressio
n size 5 truncated to fit in target size 4
SBY 12:58:24 [fib_prove] nomem: finished (returncode=0)
SBY 12:58:24 [fib_prove] aig: starting process "cd fib_prove/model& yosys -ql de
sign_aiger.log design_aiger.ys"
SBY 12:58:24 [fib_prove] aig: finished (returncode=0)
SBY 12:58:24 [fib_prove] engine_0: starting process "cd fib_prove& yosys-abc -c
"read_aiger model/design_aiger.aig; fold; strash; pdr; write_cex -a engine_0/tra
ce.aiw""
SBY 12:58:26 [fib_prove] engine_0: ABC command line: "read_aiger model/design_ai
ger.aig; fold; strash; pdr; write_cex -a engine_0/trace.aiw".
SBY 12:58:26 [fib_prove] engine_0: Cannot open file "abc.rc".
SBY 12:58:26 [fib_prove] engine_0: Cannot open file "..\abc.rc".
SBY 12:58:26 [fib_prove] engine_0: Cannot open file "..\..\abc.rc".
SBY 12:58:26 [fib_prove] engine_0: Warning: The last 2 outputs are interpreted a
s constraints.
SBY 12:58:26 [fib_prove] engine_0: Invariant F[25] : 115 clauses with 38 flops (
out of 44) (cex = 0, ave = 17.83)
SBY 12:58:26 [fib_prove] engine_0: Verification of invariant with 115 clauses wa
s successful. Time = 0.00 sec
SBY 12:58:26 [fib_prove] engine_0: Property proved. Time = 1.38 sec
SBY 12:58:26 [fib_prove] engine_0: Counter-example is not available.
SBY 12:58:26 [fib_prove] engine_0: finished (returncode=0)
SBY 12:58:26 [fib_prove] engine_0: Status returned by engine: PASS
SBY 12:58:26 [fib_prove] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:01 (
1)
SBY 12:58:26 [fib_prove] summary: Elapsed process time unvailable on Windows
SBY 12:58:26 [fib_prove] summary: engine_0 (abc pdr) returned PASS
SBY 12:58:26 [fib_prove] DONE (PASS, rc=0)
SBY 12:58:26 [fib_live] Removing directory 'fib_live'.
SBY 12:58:26 [fib_live] Copy 'fib.sv' to 'fib_live/src/fib.sv'.
SBY 12:58:26 [fib_live] engine_0: aiger suprove
SBY 12:58:26 [fib_live] nomem: starting process "cd fib_live/src& yosys -ql ../m
odel/design_nomem.log ../model/design_nomem.ys"
SBY 12:58:26 [fib_live] nomem: VERIFIC-WARNING [VERI-1209] fib.sv:27: expression
size 5 truncated to fit in target size 4
SBY 12:58:26 [fib_live] nomem: finished (returncode=0)
SBY 12:58:26 [fib_live] aig: starting process "cd fib_live/model& yosys -ql desi
gn_aiger.log design_aiger.ys"
SBY 12:58:26 [fib_live] aig: finished (returncode=0)
SBY 12:58:26 [fib_live] engine_0: starting process "cd fib_live& suprove +simple
_liveness model/design_aiger.aig"
SBY 12:58:27 [fib_live] engine_0: finished (returncode=1)
SBY 12:58:27 [fib_live] engine_0: COMMAND NOT FOUND. ERROR.
SBY 12:58:27 [fib_live] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0
)
SBY 12:58:27 [fib_live] summary: Elapsed process time unvailable on Windows
SBY 12:58:27 [fib_live] DONE (ERROR, rc=16)
SBY 12:58:27 One or more tasks produced a non-zero return code.
With this change we are getting AIG based solvers to work and proper detection of command not found for windows.
Issue was conversion of command line sequential commands separator, since that was applied to actual command parameters where it is not applicable. Also we are now properly quoting parameters instead of using apostrophe.
There is special case when actual solver return error code 1, in that case we need to track if something got displayed by solver, and in case it does it is regular error, otherwise it is command not found.