Large-scale Gatelevel Optimization Leveraging Property Checking

Conference: DVCon Europe 2023 - Design and Verification Conference and Exhibition Europe
11/14/2023 - 11/15/2023 at Munich, Germany

Proceedings: DVCon Europe 2023

Pages: 8Language: englishTyp: PDF

Authors:
Klemmer, Lucas; Bonora, Dominik; Grosse, Daniel (Institute for Complex Systems, Johannes Kepler University Linz, Austria)

Abstract:
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 within 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. In this paper, we present PSYN, an approach to detect and eliminate inactive gates using Property Checking (PC). Our approach can be viewed as a technology-independent logic optimization to be used before technology mapping. PSYN uses only free and open-source tools for each step from synthesis to formal. We split the underlying large problem into many small sub-problems, which can be effectively distributed over multiple machines. This enables PC-based gate optimization on a large scale, eventually producing an optimized netlist. In the experiments, we show that our approach can lead to significant logic reductions in moderate runtimes, even for large netlists.