Issues while running with smtbmc in MacOS X

[jdesiloniz]

Hi. I'm going back to study formal verification following @ZipCPU's course, and I've just installed all the tools in a brand new laptop running MacOS X Catalina. AFAIK I'm running the latest version of yosys (Yosys 0.9+2406 (git sha1 773b056, clang 12.0.0 -fPIC -Os)) and Symbiyosys. But when attempting to run a simple example with sby, I get the following:

SBY 23:45:23 [counter] Removing directory 'counter'.
SBY 23:45:23 [counter] Copy 'counter.v' to 'counter/src/counter.v'.
SBY 23:45:23 [counter] engine_0: smtbmc z3
SBY 23:45:23 [counter] base: starting process "cd counter/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 23:45:23 [counter] base: finished (returncode=0)
SBY 23:45:23 [counter] smt2: starting process "cd counter/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 23:45:23 [counter] smt2: ERROR: No such command: dffunmap (type 'help' for a command overview)
SBY 23:45:23 [counter] smt2: finished (returncode=1)
SBY 23:45:23 [counter] smt2: job failed. ERROR.
SBY 23:45:23 [counter] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 23:45:23 [counter] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 23:45:23 [counter] DONE (ERROR, rc=16)

I've seen that the reference to dffunmap was added 3 days ago on https://github.com/YosysHQ/SymbiYosys/commit/b172357161ea16a0734be6782b0744cf6b7108b6. I've googled it to see if it could be an issue in my environment (a missing tool/dependency) but I only find references to that single commit. Is it possible there's an issue with Symbiyosys, or if it's with my install... do you know what could I do to make sby work? Thanks!

EDIT: it may sound obvious but commenting the aforementioned line in my current installation made sby work without apparent issues. In any case I guess this is just a temporal hack on my end :).

[mwkmwkmwk]

Updating to the current yosys master should fix the issue — your version doesn't include the new command yet.

In the future we'll need to figure out some proper versioned interface between yosys and sby, but in the meantime either upgrading your yosys or downgrading sby will work as a workaround.

[jdesiloniz]

Thanks for clarifying, @mwkmwkmwk. Then it's probably an issue on the homebrew repository, as I tried upgrading yosys through brew and it seemed like it had the latest version (they probably didn't update to the latest changes?).

Closing.