Latch mapper

Details Latch mapper Latch mapper

2000-06-16

2002-12-17

Siek, Vuthe (Department: 2825)

Computer-aided design and analysis of circuits and semiconductor

Nanotechnology related integrated circuit design

C703S027000, C716S030000, C716S030000, C716S030000

Reexamination Certificate

active

06496955

ABSTRACT:

BACKGROUND OF THE INVENTION
1. Field of the Invention
The invention relates generally to design of digital systems, e.g., a computer or a component of a computer. More specifically, the invention relates to a method and apparatus for constructing a latch mapping.
2. Background Art
Modern computer and electrical engineers use hardware description languages such as Verilog HDL and VHDL to describe a digital system from a functional specification of the digital system. The engineers may describe the digital system at different levels of abstraction. One of the higher-level descriptions of the digital system is the register transfer level (RTL). In the RTL, variables and data operators are used to describe registers and transfer of vectors of information between registers. For example, in the RTL, a very simple digital circuit performing an AND operation may be described as “OUT=a&b,” where “&” represents the AND operation between the variables a and b and OUT represents the output of the digital circuit. The next lower-level description of the digital system is the gate level. At the gate level, the digital system may be described as a set of interconnected logic gates, e.g., AND and OR, and memory components, e.g., flip-flops and latches.
FIG. 1
shows a gate level description
2
of the RTL description: “OUT=a&b.” The lowest-level description of the digital system is the transistor level. At the transistor level, the digital system may be described as a set of interconnected wires, resistors, and transistors on an integrated circuit (IC) chip. The transistor-level schematic is used to create the physical model of the IC chip.
FIG. 2
shows the digital circuit of
FIG. 1
at the transistor level. The digital circuit includes two transistors
4
,
6
which are coupled to perform an AND operation on input signals a and b.
In practice, a digital system would consist of hundreds of thousands to millions of transistors. Thus, formal verification is important in designing functionally correct digital systems. Formal verification is checking to see whether the system performs its intended function. One form of formal verification called equivalence checking involves proving equivalence between two designs, which may be at the same level or different levels of abstraction. Equivalence checking is often used to prove equivalence between the RTL model and the transistor-level schematic of the digital system. Equivalence checking in sequential circuits, i.e., digital circuits containing latches and flip-flops, typically consists of two steps. The first step involves constructing a latch mapping, also known as a register mapping. The latch mapping identifies corresponding latches in the two designs to be compared. Once the corresponding latches are identified, it is then possible to decompose the designs into corresponding combinational blocks. The second step is to verify whether the corresponding combinational blocks are equivalent. If the combinational blocks are equivalent, then the two designs are functionally equivalent.
There are various techniques for checking equivalence of combinational blocks. See, for example, Jerry R. Burch and Vigyan Singhal, “Robust Latch Mapping for Combinational Equivalence Checking,” Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, 1998, pages 563-569, Pranav Ashar et al., “Using Complete-1-Distinguishability for FSM Equivalence Checking,” Proceedings of the 1996 IEEE/ACM International Conference on Computer-aided design, 1996, pages 346-353, and Andreas Kuehlmann and Florian Krohm, “Equivalence Checking Using Cuts and Heaps,” Proceedings of the 34th annual conference on Design automation conference, 1997, pages 263-268.
Various methods are known for constructing latch mapping between two designs. In general, these methods can be divided into three categories: structure mapping, function mapping, and name-matching mapping. Structure mapping involves matching structurally similar latches. For example, the latches
8
,
10
shown in
FIGS. 3A and 3B
are structurally similar because they have their ports “d” connected to the same data block “b
1
k.d[
0
],” their ports “q” connected to the same net “
1063
,” and their ports “clk” connected to the same net “
2176
.” Thus, the latches
8
,
10
will be correlated in the latch mapping. Function mapping involves analyzing and using the functional properties of the latches to correlate the designs. In function mapping, for example, two latches may be correlated because they have one set of ports connected to a net whose function is “a&b&c” and another set of ports connected to a net whose function is “clk.” Name-matching mapping depends on the latches in the two design models having similar labels. For example, the labels “X
1
” and “SX
1
” of the latches
12
,
14
shown in
FIGS. 4A and 4B
are similar because they both contain “X
1
.” Thus, the latches
12
,
14
will be correlated in the latch mapping. Typically, there will be mapping rules that indicate which portions of the labels are relevant to latch mapping.
In the practical implementation of formal equivalence, label correspondence can become a weak link. This is because the circuit designer often uses different labels than the logic designer. Also, tools that perform design transformation, such as synthesis or clock tree insertion, often do not preserve labels, especially when the design is being flattened as part of the transformation. Thus, there is a possibility that some latches will be unmapped because they cannot be correlated to other latches. Thus, if two combinational blocks are found to not be equivalent, it may be because of an incorrect label matching rather than a bug in the circuit. This, of course, complicates the debugging process. However, in an environment with a naming convention, it is worthwhile to have a tool that can perform name matching mapping because the function/structure mapping techniques use complex algorithms that can sometimes fail. Also, function/structure mapping techniques are more suited to an environment where equivalence checking is being performed between two designs at the same level (e.g., gate-gate).
SUMMARY OF THE INVENTION
In one aspect, the invention is a method for constructing a latch mapping between a first level description and a second level description of a digital system, wherein the first level description and the second level descriptions identify components in the digital system using a predefined naming convention. The method comprises identifying first latch components in the first level description and, for each identified latch component, storing a first string comprising a selected property of the first latch component in a first storage. The method further includes identifying second latch components in the second level description and, for each identified second latch component, storing a second string comprising a selected property of the second latch component in a second storage. The method further includes generating a latch mapping by matching the first strings in the first storage with the second strings in the second storage.
Other aspects and advantages of the invention will be apparent from the following description and the appended claims.


REFERENCES:
patent: 5491639 (1996-02-01), Filkorn
patent: 5493508 (1996-02-01), Dangelo et al.
patent: 5638381 (1997-06-01), Cho et al.
patent: 5727187 (1998-03-01), Lemche et al.
patent: 5841663 (1998-11-01), Sharma et al.
patent: 5867395 (1999-02-01), Watkins et al.
patent: 6059837 (2000-05-01), Kukula et al.
patent: 6247163 (2001-06-01), Burch et al.
A. Kuehlmann and F. Krohm, “Equivalence Checking Using Cuts and Heaps,” Proceedings of the 34th annual conference on Design automation conference, 1997, pp. 263-268.
“CSCI 320 Computer Architecture Handbook on Verilog HDL,” Daniel C. Hyde, Computer Science Department, Bucknell University, Lewisburg, Pennsylvania, Aug. 25, 1995, pp. 1-32.
J. Burch and V. Singhal, “Robust Latch Mapping for Combinational Equivalence Checking,” Proceeding

Affiliated with

Also associated with

Rating

Latch mapper does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Latch mapper, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Latch mapper will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-2988028