Identificador persistente para citar o vincular este elemento: http://hdl.handle.net/10553/49685
Título: A one-step algorithm for finding the optimum solution of the state justification problem in RTL designs using MILP
Autores/as: Navarro Botello,Héctor 
Montiel-Nelson, Juan A. 
Sosa, Javier 
García, José C. 
Clasificación UNESCO: 3307 Tecnología electrónica
Palabras clave: Logic
Clocks
Multiplexers
Binary data
Digital electronics, et al.
Fecha de publicación: 2005
Publicación seriada: Proceedings of SPIE - The International Society for Optical Engineering 
Conferencia: Conference on VLSI Circuits and Systems II 
Resumen: 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
Fuente: Proceedings of SPIE - The International Society for Optical Engineering[ISSN 0277-786X],v. 5837 PART II (83), p. 754-763
Colección:Actas de congresos
Vista completa

Visitas

57
actualizado el 05-oct-2024

Google ScholarTM

Verifica

Altmetric


Comparte



Exporta metadatos



Los elementos en ULPGC accedaCRIS están protegidos por derechos de autor con todos los derechos reservados, a menos que se indique lo contrario.