Formal verifiation: SymbiYosys of SpinalTemplateSbt fails with "RG_WIDTH > 1 is not support by async2sync, use clk2fflogic." when using async reset

[janschiefer]

SpinalHDL: 1.10.1
Scala version: 2.12.18
sbt version: 1.9.8
SymbiYosys version: Giit 19.02.204

Problem:

• when using a async reset in your design you generate Verilog like "always @(posedge clk or posedge reset) begin"
• SymbiYosys "async2sync" chokes on designs with multiple asynchronous clocks or a async reset signal

Fix:

• this is fixed by adding the configuration option "multiclock on" in the .sby configuration file
• Pull request: Use multiclock mode in formal verification #38

SymbiYosys logfile:

SBY  1:11:48 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] Removing directory '/home/jschiefer/Code/SpinalTemplateSbt/simWorkspace/unamed/unamed_bmc'.
SBY  1:11:48 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] Copy '/home/jschiefer/Code/SpinalTemplateSbt/simWorkspace/unamed/rtl/unamed.sv' to '/home/jschiefer/Code/SpinalTemplateSbt/simWorkspace/unamed/unamed_bmc/src/unamed.sv'.
SBY  1:11:48 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] engine_0: smtbmc --progress yices
SBY  1:11:48 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] base: starting process "cd /home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc/src; yosys -ql ../model/design.log ../model/design.ys"
SBY  1:11:48 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] base: finished (returncode=0)
SBY  1:11:48 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] prep: starting process "cd /home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc/model; yosys -ql design_prep.log design_prep.ys"
SBY  1:11:48 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] prep: ERROR: $check cell $assert$unamed.sv:41$5 with TRG_WIDTH > 1 is not support by async2sync, use clk2fflogic.
SBY  1:11:48 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] prep: finished (returncode=1)
SBY  1:11:48 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] prep: task failed. ERROR.
SBY  1:11:48 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  1:11:48 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  1:11:48 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] summary: engine_0 (smtbmc --progress yices) did not return a status
SBY  1:11:48 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] summary: engine_0 did not produce any traces
SBY  1:11:48 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] DONE (ERROR, rc=16)