SymbiYosys has a feature within it to allow you to use Python code to generate arbitrary SymbiYosys script material. We can use this code to generate a long (and potentially very complex) hierarchy command to configure our design for whatever purpose we have. In this case, we configure it for one of four configurations. Now, when we run SymbiYosys, all four of these configurations will be checked.

The first step is to create a task in our SBY file, one for each configuration we want to test.

[tasks]
A
B
other

The next step is to adjust the Yosys script to adjust the proof depending upon the task we are running.

read -formal toplvl.v
--pycode-begin--
cmd = "hierarchy -top toplvl.v"
cmd += " -chparam A %d" % (1 if "A" in tags else 0)
cmd += " -chparam B %d" % (1 if "B" in tags else 0)
output(cmd)
--pycode-end--
prep -top toplvl

We can do one better by using a Makefile and creating a separate PASS target for each of these configurations.

.PHONY: toplvl
toplvl: toplvl_A/PASS toplvl_B/PASS toplvl_other/PASS

toplvl_A/PASS: toplvl.v toplvl.sby # and other dependencies
	sby -f toplvl.sby A

toplvl_B/PASS: toplvl.v toplvl.sby # and other dependencies
	sby -f toplvl.sby B

toplvl_other/PASS: toplvl.v toplvl.sby # and other dependencies
	sby -f toplvl.sby Other

This works because of how SymbiYosys works: SymbiYosys creates a separate directory for the files associated with every proof. At the end of the proof, it leaves behind a file describing final result. This file will typically be one of: FAIL, PASS, UNKNOWN (BMC passed but induction failed), or ERROR. The important thing here is that only one of these status results is a PASS. If the design passes, and only if, there will be an (empty) file named PASS in the proof directory. If we make this file properly dependent upon the files each proof depends upon, then make will handle this quite nicely.

The other neat thing about this small little make script is that it will now formally verify all three of these configurations. Even better, it can do so in a highly threaded fashion.

As an aside, a similar approach could be made to apply to simulation scripts as well. A simulation script should either exist for each configuration, or at least be able to be configured for each configuration. For more details about simulating a design against multiple configurations, check out this article.