Large-scale gatelevel optimization leveraging property checking

Often the full range of all possible input combinations of circuits is not needed for a specific use case. For example, an embedded processor might only use a small subset of all available instructions, or the operands to a multiplier are guaranteed to be with in certain bounds. These external don’t cares result in the interesting case of gates in the netlist that are completely inactive (or redundant), since they are never activated by the inputs to the design. Those gates can be safely eliminated, reducing the size of the netlist without loss of functionality.