YosysHQ / sby

SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
Other
388 stars 73 forks source link

Tags persist across section boundaries #188

Closed KrystalDelusion closed 4 months ago

KrystalDelusion commented 2 years ago

When using multiline configurations as described in the reference page of the docs, missing a trailing -- before changing sections will cause other tasks to fail. For example, in the code below only the bmc task will function, while the cover task fails with the message config file is lacking engine configuration.

...
[options]
cover:
mode cover
--
bmc: 
mode bmc

[engines]
cover: smtbmc boolector
bmc: smtbmc boolector
...

This is not unique to the [options] section either, I've also had it happen in the [engines] section and getting an error for not having a top module defined.

Having had a quick look at the code in sby.py it seems like in the above code example, the [engines] line is only included in the config for bmc by the time it gets passed to sby_core.py. So while the cover: smtbmc boolector line is included, it appears to the code as though it is still in the [options] section.

If this is by design then maybe make that clear in the instructions, otherwise adding a line.startswith("[") or similar might be nice.

nakengelhardt commented 1 year ago

Claire confirmed this is in fact a feature.