A one-step algorithm for finding the optimum solution of the state justification problem in RTL designs using MILP

Hector Navarro; Juan A. Montiel-Nelson; Javier Sosa; Jose C. Garcia

doi:10.1117/12.608526

30 June 2005 A one-step algorithm for finding the optimum solution of the state justification problem in RTL designs using MILP

Hector Navarro, Juan A. Montiel-Nelson, Javier Sosa, Jose C. Garcia

Author Affiliations +

Proceedings Volume 5837, VLSI Circuits and Systems II; (2005) https://doi.org/10.1117/12.608526
Event: Microtechnologies for the New Millennium 2005, 2005, Sevilla, Spain

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.

Citation Download Citation

Hector Navarro, Juan A. Montiel-Nelson, Javier Sosa, and Jose C. Garcia "A one-step algorithm for finding the optimum solution of the state justification problem in RTL designs using MILP", Proc. SPIE 5837, VLSI Circuits and Systems II, (30 June 2005); https://doi.org/10.1117/12.608526

ACCESS THE FULL ARTICLE

INSTITUTIONAL
Select your institution to access the SPIE Digital Library.

SELECT YOUR INSTITUTION

PERSONAL
Sign in with your SPIE account to access your personal subscriptions or to use specific features such as save to my library, sign up for alerts, save searches, etc.

PERSONAL SIGN IN

No SPIE Account? Create one

PURCHASE THIS CONTENT

SUBSCRIBE TO DIGITAL LIBRARY

50 downloads per 1-year subscription

Members: $195

Non-members: $335 ADD TO CART

25 downloads per 1 - year subscription

Members: $145

Non-members: $250 ADD TO CART

PURCHASE SINGLE ARTICLE

Includes PDF, HTML & Video, when available

Members: $17.00

Non-members: $21.00 ADD TO CART

PROCEEDINGS
10 PAGES

DOWNLOAD PAPER SAVE TO MY LIBRARY

GET CITATION

RIGHTS & PERMISSIONS

Get copyright permission Get copyright permission on Copyright Marketplace

KEYWORDS

Logic

Clocks

Multiplexers

Binary data

Digital electronics

Logic devices

Computer programming

Show All Keywords

Keywords/Phrases

Search In:

Publication Years