Browse Prior Art Database

Fax to Email automatic routing in PBX Centerx enviroment Disclosure Number: IPCOM000021235D
Original Publication Date: 2004-Jan-07
Included in the Prior Art Database: 2004-Jan-07
Document File: 5 page(s) / 86K

Publishing Venue



A computer-implemented method for systematically eliminating redundant circuit elements in a state machine of a model having sequential circuit elements possessing one of a fixed number of possible states, typically "0" and "1". Initially, the sequential circuit elements are sorted into groups whose state is determinate i.e. equal t"0" or "1". The state of each circuit element whose state is determinate is stored in memory and its next state is calculated and compared with its preceding state. Each circuit element whose successive states are different is moved to the group of indeterminate circuit elements, and the cycle is repeated in respect of all remaining determinate circuit elements until no further circuit elements are moved. Each of the remaining determinate circuit elements is then replaced by a constant equal to its corresponding state i.e. "0" or "1". Finally, any circuit elements whose output is connected to one or more of the replaced circuit elements and to no other circuit elements is eliminated from the model.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 20% of the total text.

Page 1 of 5

Fax to Email automatic routing in PBX Centerx enviroment

This invention relates in general to model checking and, in particular, to model reduction techniques prior to computer-implemented model checking.

  When designing integrated circuits including combinatorial and sequential gates and circuit elements, tools are used to check the integrity of the final design before proceeding to mass-production. The tools are computer programs which require as input a mathematical model of the integrated circuit design and a specification of desired design criteria. Thus, for example, a Flip-Flop circuit element may generate an acknowledge signal (ACK) responsive to a request signal (REQ) and the design specification may require that the REQ signal produces the ACK signal within three clock cycles.

  From knowledge of the design specification and the mathematical model of the integrated circuit, the computer determines whether the model meets the specified design criteria. Such a program solves a state machine having a large number of variables dependent, of course, on the model complexity. Thus, the more gates and memory elements in the integrated circuit, the more complex is the model and the greater the number of variables in the state machine to be solved. In practice, the more complex the design the greater is the size of memory which the computer requires to solve the state machine; and the longer the calculation time. There exists, therefore, a need to reduce the model complexity without compromising on the integrity of the model checking.

  Prior art techniques relate principally to manual reduction of the number of state variables by eliminating obviously redundant circuit elements. For example, Fig. 1 shows part of a logic circuit depicted generally as 10 comprising an AND-gate 11 whose output is fed to the REQ input of a Flip-Flop 12 having an ACK output 13 and a CLK input 14. A first input 15 of the AND-gate 11 is driven by the output of a sub-circuit designated 16 which may itself include a large number of logic elements. A second input 17 of the AND-gate 11 is tied to logic "0".

  In such an arrangement, the output of the AND-gate 11 will always be logic "0" regardless of any changes that occur in the logic state of the first input 15 of the AND-gate 11 consequent to operation of the sub-circuit 16. In this trivial example, the AND-gate 11 as well as the Flip-Flop 12 may be replaced by a line of constant logic level "0" thereby reducing the number of state space variables in the mathematical model representative of the logic circuit 10.

  Another example of useful reduction is the elimination of signals that are not in the so-called "cone of influence" of the circuit being verified. Thus, if only part of the circuit is being verified, then any other parts whose behavior does not alter the part under verification can be eliminated. Thus, in the example shown in Fig. 1, suppose that only that part of the logic circuit 10 which is connected...