Can't include defines from other module

[ssmolov]

I'm running SymbiYosys on https://github.com/ispras/hdl-benchmarks/blob/master/verilog/texas97/PI_BUS/multi_master/bus.v module. This module uses several defines from https://github.com/ispras/hdl-benchmarks/blob/master/verilog/texas97/PI_BUS/multi_master/main.v module. How to get them for 'bus.v' to be formally checked? Here is my SBY:

[options]
mode bmc
depth 100

[engines]
smtbmc

[script]
read -formal /home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master/bus.v
prep -top bus_cont

[files]
/home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master/bus.v

It seems to be impossible to add full path to main.v module, because the module inside it contains an instance of the bus module. I've tried to use -incdir option in the following way:

[options]
mode bmc
depth 100

[engines]
smtbmc

[script]
read -incdir /home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master -formal /home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master/bus.v
prep -top main

[files]
/home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master/bus.v

and the result was:

SBY 15:14:55 [test] Removing direcory 'test'.
SBY 15:14:55 [test] Copy '/home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master/bus.v' to 'test/src/bus.v'.
SBY 15:14:55 [test] engine_0: smtbmc
SBY 15:14:55 [test] base: starting process "cd test/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:14:55 [test] base: ERROR: Module `bus_cont' not found!
SBY 15:14:55 [test] base: finished (returncode=1)
SBY 15:14:55 [test] base: job failed. ERROR.
SBY 15:14:55 [test] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 15:14:55 [test] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 15:14:55 [test] DONE (ERROR, rc=16)

[daveshah1]

Try using read -incdir and read -formal as separate commands (with read -incdir first) rather than combining them into one line.

[ssmolov]

Thanks for your answer!

The error that was related to -incdir usage disappear now, but I still can't elaborate bus.v module properly. Here is the SymbiYosys log:

SBY 11:35:06 [test] Copy '/home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master/bus.v' to 'test/src/bus.v'.
SBY 11:35:06 [test] engine_0: smtbmc
SBY 11:35:06 [test] base: starting process "cd test/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 11:35:06 [test] base: /home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master/bus.v:143: ERROR: Unimplemented compiler directive or undefined macro `RDY.
SBY 11:35:06 [test] base: finished (returncode=1)
SBY 11:35:06 [test] base: job failed. ERROR.
SBY 11:35:06 [test] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 11:35:06 [test] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 11:35:06 [test] DONE (ERROR, rc=16)

The RDY macro is defined at /home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master/main.v

[daveshah1]

bus.v doesn't actually include main.v, that's why it doesn't import any of its macros. Either add

`include "main.v"

to bus.v; or add main.v to the read -formal line

[ssmolov]

I've checked both ideas. The first one hangs SymbiYosys - probably, "two modules that have includes on each other" situation is critical. The second approach produces the following log:

SBY 12:19:06 [test] Copy '/home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master/bus.v' to 'test/src/bus.v'.
SBY 12:19:06 [test] engine_0: smtbmc
SBY 12:19:06 [test] base: starting process "cd test/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 12:19:06 [test] base: /home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master/bus.v:14: ERROR: Re-definition of module `$abstract\bus_cont'!
SBY 12:19:06 [test] base: finished (returncode=1)
SBY 12:19:06 [test] base: job failed. ERROR.
SBY 12:19:06 [test] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 12:19:06 [test] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 12:19:06 [test] DONE (ERROR, rc=16)

It seems that _multimaster project is organised in such way that it's hard for SymbiYosys to check bus.v module separately without Verilog code modification.

[ksundara20]

Hi Sergey, I faced this issue when I was doing FV on SweRV model. I was able to solve it by having a brand new verilog file that includes all header ".vh" files first and then all model verilog files ".v". You can also try the same solution.