Currently the assertFormal method in FHDLTestCase seems a bit rigid as it doesn't seem to allow for customization options other than the mode of proving (bmc, prove, cover) and depth. Perhaps it would be better to allow assertFormal to accept a few extra optional parameters for customizing the behavior of running SymbiYosys? E.g. SymbiYosys allows the --nopresat option to be specified (at least with particular solvers) which may be required in some cases such as my port of riscv-formal to prevent PREUNSAT errors.
Currently the
assertFormalmethod inFHDLTestCaseseems a bit rigid as it doesn't seem to allow for customization options other than the mode of proving (bmc,prove,cover) and depth. Perhaps it would be better to allowassertFormalto accept a few extra optional parameters for customizing the behavior of running SymbiYosys? E.g. SymbiYosys allows the--nopresatoption to be specified (at least with particular solvers) which may be required in some cases such as my port of riscv-formal to preventPREUNSATerrors.