基於內插法與滿足性之邏輯修正

Abstract

In modern VLSI designs, late design changes are nearly inevitable to fix the design bugs or to cope with the specification changes. Due to the cost and time-to-market pressure, it is unlikely that designers would like to modify the register-transfer level (RTL) design and re-run the whole design flow from the beginning. Instead, they identify a patch circuit to rectify the gate-level design for the differences. This process is called logic rectification. This dissertation focuses on two closely related rectification problems: rectification for application-specific integrated circuits (ASICs) and field-programmable gate arrays (FPGAs). Rectification for ASICs For a design with multiple functional errors, multiple patches are usually needed to correct the design. Previous works on logic rectification are limited to single-output patch. In other words, only one erroneous behaviors can be fixed in one iteration. As a result, it may lead to unnecessarily large patches or even failure in rectification. We generalize the existing rectification techniques to a great extent and propose direct and incremental logic rectifications. For direct logic rectification, we derive multiple-output patch by interpolation with cofactor reduction. The multiple-output patch considers multiple design errors simultaneously. For incremental logic rectification, single- and multiple-output partial patches are identified in an iterative manner. Our experiments incorporate both direct and incremental methods, and the algorithms perform well on large designs. Rectification for FPGAs We present rectification methods for look-up table (LUT) type FPGAs to correct an erroneous circuit implementation by in-place logic reconfiguration; that is, we only reconfigure the functions of the LUTs and do not change the routing of the erroneous circuit. Therefore, the rectification can be very efficient since the relatively much more expensive re-routing can be avoided. Our proposed algorithm is based on the Boolean satisfiability (SAT) solver and use dynamic learning techniques to accelerate the computation. To enhance the reconfiguration power, both direct and incremental methods are investigated. Experimental results demonstrate that the learning techniques are effective in pruning infeasible solutions for both academic and industrial benchmarks.