SAT-based Automatic Rectification and Debugging of Combinational Circuits with LUT Insertions

DOI DOI PDF Web Site 被引用文献1件 参考文献3件 オープンアクセス
  • Jo Satoshi
    Department of Electrical Engineering and Information Systems, The University of Tokyo
  • Matsumoto Takeshi
    VLSI Design and Education Center, The University of Tokyo
  • Fujita Masahiro
    VLSI Design and Education Center, The University of Tokyo CREST, JST

説明

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. The proposed method first finds a candidate of LUT configurations that can correct a given circuit by SAT solvers. Then, it checks the correctness of the candidate by checking equivalence between the circuit with LUTs and its specification. Although this can be solved as SAT problem, we introduce to use commercial equivalence checker to improve the efficiency. If the result of the check is “not equivalent”, an input pattern showing the non-equivalence will be added, and the method repeats with the pattern added. Through the experimental results on ISCAS '85 benchmark circuits and Open RISC 1200 microprocessor design, we show our proposed method can quickly find LUT configurations for large circuits with many LUTs, which cannot be solved by a QBF solver.

収録刊行物

被引用文献 (1)*注記

もっと見る

参考文献 (3)*注記

もっと見る

関連プロジェクト

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ