Browse Prior Art Database

Method for Optimal Sequence Recognition in Formal Verification

IP.com Disclosure Number: IPCOM000033981D
Original Publication Date: 2005-Jan-10
Included in the Prior Art Database: 2005-Jan-10
Document File: 6 page(s) / 230K

Publishing Venue

IBM

Abstract

A novel method is disclosed that optimally synthesizes regular-expression recognition logic by creating "fuzzy state machines" in a hardware description language. This approach enables significant performance improvements to various verification frameworks.

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 26% of the total text.

Page 1 of 6

Method for Optimal Sequence Recognition in Formal Verification

Disclosed is a method for creating optimal regular-expression recognition logic in a hardware description language using "fuzzy state machines." We additionally describe a modular approach to synthesize nested regular expressions, which creates a set of interacting state machines - one per regular expression - instead of using one large state machine for the entire nested regular expression. We provide algorithms for synthesizing these state machines in VHDL.

Regular expressions are commonly used to reason about many sequential processes; for example, if some sequence "A" of conditions is witnessed, then some sequence "B" of conditions must hold. Sequences "A" and "B" may include nested sequences, possibly qualified by the regular matching operators + and * (formally known as Kleene star) to denote repetition. Traditionally, regular expressions are represented by non-deterministic finite state machines (NFSMs) - where each "present state, input" pair may have multiple possible "next states". Because evaluation of NFSMs using an explicit-state algorithm like simulation involves decision making (as to which "next state" to choose for a given "present state, input" pair), and backtracking in case an incorrect decision was made, NFSMs traditionally must be converted into deterministic finite state machines (DFSMs) which have a unique "next state" for each "present state, input" pair to enable them to be used as specifications. The DFSM may then be coded using hardware description languages (VHDL, Verilog, etc.) enabling its synthesis with the design, and evaluation using a variety of verification platforms such as simulation, emulation, and formal and semi-formal verification. The primary drawback of using traditional NFSM synthesis (via a DFSM translation) in verification is that they result in exponentially more logic than necessary. Because formal verification requires exponential resources with respect to design size, this traditional approach for NFSM synthesis results in a significant suboptimality to formal verification. Even semi-formal verification, emulation, and simulation frameworks suffer performance penalties due to this suboptimality.

Described is a method for representing sequences efficiently as fuzzy finite state machines (FFSMs). Demonstrated is how the number of states necessary to implement the FFSM is equivalent to that necessary for a NFSM-based representation (without the exponential penalty of DFSM expansion noted above), and how the logic that captures transitions between the states required for an FFSM implementation is much simpler. A fuzzy state machine allows a system to be in a given state probabilistically. A transition takes place with a specified probability that is attached to the transition. Besides the state space reduction, there are two other important advantages of using FFSMs:

Sub-sequences in equivalent expressions share the same i...