Surety is performing system maintenance this weekend. Electronic date stamps on new Prior Art Database disclosures may be delayed.
Browse Prior Art Database

Method for dynamic formal verification

IP.com Disclosure Number: IPCOM000018763D
Publication Date: 2003-Aug-06
Document File: 4 page(s) / 86K

Publishing Venue

The IP.com Prior Art Database


Disclosed is a method for dynamic formal verification (DFV). Benefits include improved functionality, an improved development environment, and an improved test 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 48% of the total text.

Method for dynamic formal verification

Disclosed is a method for dynamic formal verification (DFV). Benefits include improved functionality, an improved development environment, and an improved test environment.


        � � � � � A great deal of time, effort, and money are spent to provide software debug capabilities during resistor transistor logic (RTL) development. Formal verification processes ensure the correct operation of complex protocols. As design size and complexity increase, covering all the possible events and boundary conditions during full chip testing becomes more difficult. Logic and protocol bugs that escape presilicon design verification and proliferate through to the silicon and system must be identified quickly and fixed.

        � � � � � Narrowing down failure symptoms in a complex system (such as a multiprocessor system) to a specific logic/protocol bug is difficult. The detection of protocol violations and broken assumptions is the base and starting point to speeding up analysis of the failure and root cause protocol violations detected in a malfunctioning machine.

General description

        � � � � � The disclosed method enables the verification of complex protocols within a microprocessor and hosting system by detecting and reporting runtime protocol violations. The method includes a series of hardware solutions for employing DFV and providing a hardware signature if key complex protocols are violated. The violated protocols can have logical/functional or electrical consequences, which may not be visible to the conventional tester or may have a root cause that is difficult to detect.

        � � � � � DFV hardware provides system-level visibility. The hardware detects and reports protocol violations through programmable event breakpoints, sticky bits in user accessible registers, and other means of visible debug hooks.

        � � � � � The key elements of the disclosed method include:

•        � � � � Set of formal requirements and protocol specification, such as mutually exclusive states and forbidden events/sequences, that are detected in hardware for correctness

•        � � � � Mechanism to make possible violations visible at the system level by registering them into sticky registers, feeding them into event detection and breakpoint logic to freeze and query the status of the machine


        � � � � � The disclosed method provides advantages, including:

•        � � � � Improved functionality due to providing hardware solutions for detecting and reporting runtime protocol violations

•        � � � � Improved development environment due to improved debug cycles for logic bugs proliferated to silicon and systems due to wrong assumptions/lack of presilicon validation

•        � � � � Improved test environment due to improved levels of verification of complex protocols during system validation

Detailed description

        � � � � � The disclosed method can be described using the following examples:

•        � � � � Finite state machine (FSM)

•        � � � � Multiple tag-matches