Error `Option skip is only valid for smtbmc and btor engines` running riscv-formal

[carlosedp]

I'm trying to add riscv-formal to my core and while running it, I'm getting:

❯ ./start_formal.sh
Reading checks.cfg.
Creating checks directory.
Generated 43 checks.
make: Entering directory '/src/cores/chiselv/checks'
sby causal_ch0.sby
sby liveness_ch0.sby
sby pc_bwd_ch0.sby
sby pc_fwd_ch0.sby
sby reg_ch0.sby
sby unique_ch0.sby
sby insn_add_ch0.sby
sby insn_addi_ch0.sby
sby insn_and_ch0.sby
sby insn_andi_ch0.sby
sby insn_auipc_ch0.sby
sby insn_beq_ch0.sby
WARNING: Could not connect to jobserver specified in MAKEFLAGS, disabling parallel execution.
WARNING: Could not connect to jobserver specified in MAKEFLAGS, disabling parallel execution.
SBY 13:30:01 [pc_bwd_ch0] ERROR: Option skip is only valid for smtbmc and btor engines.
SBY 13:30:01 [liveness_ch0] ERROR: Option skip is only valid for smtbmc and btor engines.
make: *** [makefile:12: pc_bwd_ch0/status] Error 1
make: *** Waiting for unfinished jobs....
WARNING: Could not connect to jobserver specified in MAKEFLAGS, disabling parallel execution.
SBY 13:30:01 [unique_ch0] ERROR: Option skip is only valid for smtbmc and btor engines.
make: *** [makefile:8: liveness_ch0/status] Error 1
make: *** [makefile:24: unique_ch0/status] Error 1
WARNING: Could not connect to jobserver specified in MAKEFLAGS, disabling parallel execution.
SBY 13:30:01 [reg_ch0] ERROR: Option skip is only valid for smtbmc and btor engines.
WARNING: Could not connect to jobserver specified in MAKEFLAGS, disabling parallel execution.
make: *** [makefile:20: reg_ch0/status] Error 1
SBY 13:30:01 [insn_addi_ch0] ERROR: Option skip is only valid for smtbmc and btor engines.
WARNING: Could not connect to jobserver specified in MAKEFLAGS, disabling parallel execution.
WARNING: Could not connect to jobserver specified in MAKEFLAGS, disabling parallel execution.
SBY 13:30:01 [causal_ch0] ERROR: Option skip is only valid for smtbmc and btor engines.
WARNING: Could not connect to jobserver specified in MAKEFLAGS, disabling parallel execution.
SBY 13:30:01 [pc_fwd_ch0] ERROR: Option skip is only valid for smtbmc and btor engines.
WARNING: Could not connect to jobserver specified in MAKEFLAGS, disabling parallel execution.
make: *** [makefile:32: insn_addi_ch0/status] Error 1
SBY 13:30:01 [insn_and_ch0] ERROR: Option skip is only valid for smtbmc and btor engines.
WARNING: Could not connect to jobserver specified in MAKEFLAGS, disabling parallel execution.
SBY 13:30:01 [insn_andi_ch0] ERROR: Option skip is only valid for smtbmc and btor engines.
SBY 13:30:01 [insn_auipc_ch0] ERROR: Option skip is only valid for smtbmc and btor engines.
make: *** [makefile:4: causal_ch0/status] Error 1
make: *** [makefile:16: pc_fwd_ch0/status] Error 1
make: *** [makefile:40: insn_andi_ch0/status] Error 1
WARNING: Could not connect to jobserver specified in MAKEFLAGS, disabling parallel execution.
SBY 13:30:01 [insn_add_ch0] ERROR: Option skip is only valid for smtbmc and btor engines.
WARNING: Could not connect to jobserver specified in MAKEFLAGS, disabling parallel execution.
make: *** [makefile:36: insn_and_ch0/status] Error 1
SBY 13:30:01 [insn_beq_ch0] ERROR: Option skip is only valid for smtbmc and btor engines.
make: *** [makefile:28: insn_add_ch0/status] Error 1
make: *** [makefile:44: insn_auipc_ch0/status] Error 1
make: *** [makefile:48: insn_beq_ch0/status] Error 1
make: Leaving directory '/src/cores/chiselv/checks'

My config is:

[options]
isa rv32i

[depth]
insn            20
reg       15    30
pc_fwd    10    30
pc_bwd    10    30
liveness  1  10 30
unique    1  10 30
causal    10    30

[defines]
`define RISCV_FORMAL_ALIGNED_MEM

[script-sources]
read_verilog -sv @basedir@/cores/@core@/wrapper.sv
read_verilog @basedir@/cores/@core@/RVFITop.v

This also happens to existing cores like vexriscv or picorv32.

I'm running yosys and sby from gcr.io/hdl-containers/formal container which uses:

root@6f4ae94e1682:/src/cores/chiselv# yosys --version
Yosys 0.20+74 (git sha1 9313549cd, clang 11.0.1-2 -fPIC -Os)

Latest SBY from https://github.com/YosysHQ/sby.

[jix]

This seems to be a bug in SBY which slipped through the automated tests after some recent refactoring. The SBY commit 9a14f4d238 is the latest one before that refactoring and should still work.

[carlosedp]

Thanks @jix ... got an image from the beginning of august and it worked! On some image (during august too) I got the error: SBY 14:07:17 [insn_auipc_ch0] prep: ERROR: No such command: formalff (type 'help' for a command overview) ~Want me to open an issue over SBY there referencing this one?~

[jix]

That No such command: formalff error means that the used Yosys version is too old for the used SBY version. In general SBY requires an up to date Yosys version.

[carlosedp]

Ah ok.. so it's probably a mismatch midways in the container image . The one I'm using(gcr.io/hdl-containers/formal@sha256:ff660de17fb8847f01fb33c1b4bd8bf08eebfd9e3fdaa9dd844a71f7c54b42a7) works fine and I'll wait for this fix to bump it.