Functional Rectification on Sequential Circuits by Liveness Model Checking Techniques

• Main Authors: Wei-Hsun Lin, 林暐勛
• Other Authors: Chung-Yang Huang
• Format: Others
• Language: en_US
• Published: 2012
• Online Access: http://ndltd.ncl.edu.tw/handle/94831661329443282757

碩士 === 國立臺灣大學 === 電子工程學研究所 === 100 === Functional rectification has been an indispensable process in late VLSI design stages. Traditionally, functional rectification is achieved by various techniques on combinational circuits. It does not explore the flexibility of functional changes across the register boundary. As a result, these combinational rectification techniques cannot be applied directly to sequential circuits with unmatched registers. In this thesis, we propose a sequential rectification approach, which utilizes the liveness model checking techniques to facilitate checking of the sequential rectifiability between old implementation and golden specification. In addition, we apply the interpolation technique to construct the rectification function (i.e. the patch). By identifying better supports for the patch generation, we demonstrate that the whole procedure can be accelerated. Experimental results show that our method can efficiently determine whether a given signal is a rectification signal and find the patch circuits effectively. In the end, our method can provide an alternative way to the combinational rectification and it generates smaller in most of cases.