Inferring assertion for complementary synthesis

Complementary synthesis can automatically synthesize the decoder circuit of an encoder. However, its user needs to manually specify an assertion on some configuration pins to prevent the encoder from reaching the non-working states. To avoid this tedious job, we propose an automatic approach to infer this assertion. First, we propose a halting algorithm that can decide the existence of the decoder for every particular assertion. Second, for every invalid value of configuration pins that leads to the non-existence of the decoder, we use cofactoring and Craig interpolation to infer a new formula, which covers a larger set of such invalid values. This second step is repeated until all invalid values are covered by these inferred formulas. Finally, we obtain the final assertion by anding the inverses of all these inferred formulas. The decoder exists if and only if this final assertion is still satisfiable. To illustrate its usefulness, we have run our algorithm on several complex encoder circuits, including PCI-E and Ethernet. Experimental results show that our algorithm can always infer assertions for them.