fmcombine - combine two instances of a cell into one
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.