Please use this identifier to cite or link to this item: http://hdl.handle.net/10553/49685
Title: A one-step algorithm for finding the optimum solution of the state justification problem in RTL designs using MILP
Authors: Navarro Botello,Héctor 
Montiel-Nelson, Juan A. 
Sosa, Javier 
García, José C. 
UNESCO Clasification: 3307 Tecnología electrónica
Keywords: Logic
Clocks
Multiplexers
Binary data
Digital electronics, et al
Issue Date: 2005
Journal: Proceedings of SPIE - The International Society for Optical Engineering 
Conference: Conference on VLSI Circuits and Systems II 
Abstract: The state justification problem is the decision problem of finding a sequence of states and input values that satisfy an output condition for a given state machine or RTL description. In such problems, there always exist optimal state sequences that require a minimum number of clock cycles to reach the desired state.As Boolean decision problems, state justification problems can be expressed as satisfiability problems (SAT) by using the time-frame expansion algorithm. Boolean SAT or BDD-based techniques are bit-level decision procedures commonly used by industrial hardware verification tools. Unfortunately, these approaches are not efficient enough, because they do not inherit the word-level information from the RTL design. Recent approaches to the SAT problem are addressed to RTL designs containing instances of both, word-level arithmetic blocks for data flow, and bit-level Boolean logic for control flow. These approaches transform the whole SAT problem for an RTL description into a mixed integer linear program (MILP).This paper presents a new approach that finds in a single step, the optimum input sequence for a given RTL description to reach a desired state. This is accomplished by applying a novel time-frame expansion method that guarantees an optimal solution and avoids performing time-frame expansions iteratively.Experimental results will demonstrate that the proposed methodology can solve any state justification problem in one step for complex FSMs. The main application of this procedure is the test pattern generation, where the main problem is to reduce the length of test sequences that verifies a microcircuit.
URI: http://hdl.handle.net/10553/49685
ISBN: 0-8194-5832-5
ISSN: 0277-786X
DOI: 10.1117/12.608526
Source: Proceedings of SPIE - The International Society for Optical Engineering[ISSN 0277-786X],v. 5837 PART II (83), p. 754-763
Appears in Collections:Actas de congresos
Show full item record

Page view(s)

57
checked on Oct 5, 2024

Google ScholarTM

Check

Altmetric


Share



Export metadata



Items in accedaCRIS are protected by copyright, with all rights reserved, unless otherwise indicated.