Dismiss
InnovationQ will be updated on Sunday, Oct. 22, from 10am ET - noon. You may experience brief service interruptions during that time.
Browse Prior Art Database

Method for automatic synchronization of finite state machines for sequential verification of chip designs

IP.com Disclosure Number: IPCOM000146262D
Publication Date: 2007-Feb-08
Document File: 4 page(s) / 132K

Publishing Venue

The IP.com Prior Art Database

Abstract

Disclosed is a method for automatic synchronization of finite state machines for sequential verification of chip designs. Benefits include improved functionality, improved reliability, and an improved development environment.

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

Method for automatic synchronization of finite state machines for sequential verification of chip designs

Disclosed is a method for automatic synchronization of finite state machines for sequential verification of chip designs. Benefits include improved functionality, improved reliability, and an improved development environment.

Background

      Formal equivalence verification (FEV) is an essential computer aided design (CAD) capability that verifies the equivalence between the implementation (Schematics) and the resistor transistor logic (RTL) in the Specification. However, conventional FEV tools have a major limitation. They require the RTL to be state matching with the schematics. A one-to-one correspondence must exist between the state elements of the two compared circuits.

      With the increased complexity of chip designs, the RTL validation process has become one of the severe bottlenecks. Recent studies indicate that the number of the bugs in a given design is relatively consistent with the number of lines of code.

      One conventional FEV solution verifies sequential logic. The system includes engines for verifying the equivalence of two designs with the same or with different state encoding. Additionally, the system verifies the validity of properties specified for the designs. This backbone design verification tool is free of the state matching limitation and supports more abstract RTL code. The synchronization of synchronous circuits is one of the fundamental and tasks. The solution verifies whether a specific property holds for every binary input sequence.

General description

      The disclosed method is automatic synchronization of finite state machines for sequential verification of chip designs. The method provides algorithms that enable the automatic initialization or synchronization of synchronous circuits.

Advantages

      The disclosed method provides advantages, including:
•     Improved functionality due to providing automatic synchronization of finite state machines for sequential verification of chip design

•     Improved functionality due to providing a synchronization sequence whether or not an initialization sequence exists

•     Improved reliability due to not generating false-positive results

•     Improved development environment due to enabling the detection of designs that cannot be initialized

•     Improved development environment due to detecting the areas in the design that are not initialized

Detailed description

      The disclosed method is automatic synchronization of finite state machines for sequential verification of chip designs. The method is a satisfiability solver (SAT) based algorithm for synchronizing sequential circuits. The algorithm finds a binary sequence that brings the circuit to a state in...