fmcombine - combine two instances of a cell into one¶
yosys> help fmcombine¶
fmcombine [options] module_name gold_cell gate_cell
This pass takes two cells, which are instances of the same module, and replaces them with one instance of a special 'combined' module, that effectively contains two copies of the original module, plus some formal properties. This is useful for formal test benches that check what differences in behavior a slight difference in input causes in a module.
Insert assumptions that initially all FFs in both circuits have the same initial values.
Do not duplicate $anyseq/$anyconst cells.
Insert forward hint assumptions into the combined module.
Insert backward hint assumptions into the combined module. (Backward hints are logically equivalend to fordward hits, but some solvers are faster with bwd hints, or even both -bwd and -fwd.)
Don't insert hint assumptions into the combined module. (This should not provide any speedup over the original design, but strangely sometimes it does.)
If none of -fwd, -bwd, and -nop is given, then -fwd is used as default.