SAT-based automatic rectification and debugging of combinational circuits with LUT insertions

Relatore:  Masahiro Fujita - VLSI Design & Education Center, University of Tokyo
  venerdì 12 ottobre 2012 alle ore 16.00 3:45 pm rinfresco; 4:00 pm inizio seminario.
Introducing partial programmability in circuits by replacing some gates with look up tables (LUTs) can be an effective way to improve post-silicon or in-field rectification and debugging. Although finding configurations of LUTs that can correct the circuits can be formulated as a QBF problem, solving it by state-of-the-art QBF solvers is still a hard problem for large circuits and many LUTs. In this paper, we present a rectification and debugging method for combinational circuits with LUTs by repeatedly applying Boolean SAT solvers. Through the experimental results, we show our proposed method can quickly find LUT configurations for large circuits with many LUTs, which cannot be solved by a QBF solver.

Ca' Vignal 3 - Piramide, Piano 0, Sala Verde

Giuseppe Di Guglielmo

Data pubblicazione
1 ottobre 2012

Offerta formativa