### Abstract

The results of a formal logic verification system implemented as part of the multilevel logic synthesis system MIS are discussed. Combinational logic verification involves checking two networks for functional equivalence. Techniques that flatten networks or use cube enumeration and simulation cannot be used with functions that have very large cube covers. Binary decision diagrams (BDDs) are canonical representations for Boolean functions and offer a technique for formal logic verification. However, the size of BDDs is sensitive to the variable ordering. Ordering strategies based on the network topology are considered. Using these strategies with BDDs, it has been possible to carry out formal verification for a larger set of networks than with existing verification systems. The present method proved significantly faster on the benchmark set of examples tested.

Original language | English (US) |
---|---|

Title of host publication | IEEE Int Conf on Comput Aided Des ICCAD 88 a Conf for the EE CAD Prof |

Publisher | Publ by IEEE |

Pages | 6-9 |

Number of pages | 4 |

ISBN (Print) | 0818608692 |

State | Published - Dec 1 1988 |

### Publication series

Name | IEEE Int Conf on Comput Aided Des ICCAD 88 a Conf for the EE CAD Prof |
---|

### All Science Journal Classification (ASJC) codes

- Engineering(all)

## Fingerprint Dive into the research topics of 'Logic verification using binary decision diagrams in a logic synthesis environment'. Together they form a unique fingerprint.

## Cite this

*IEEE Int Conf on Comput Aided Des ICCAD 88 a Conf for the EE CAD Prof*(pp. 6-9). (IEEE Int Conf on Comput Aided Des ICCAD 88 a Conf for the EE CAD Prof). Publ by IEEE.