Cadence® Encounter® Conformal® Equivalence Checker (EC),
makes it possible to verify and debug multi-million-gate designs
without using test vectors. It offers the only complete equivalence
checking solution available for verifying SoC designs—from RTL
to final LVS netlist (SPICE)—as well as FPGA designs. Encounter
Conformal EC enables designers to verify the widest variety of
circuits, including complex arithmetic logic, datapaths, memories,
and custom logic.
ENCOUNTER CONFORMAL
EQUIVALENCE CHECKER
Already proven in thousands of tapeouts,
Encounter Conformal EC is the industry’s
most widely supported equivalence
checking product. In addition, it is
production-proven on more physical
design closure products, advanced
synthesis software, ASIC libraries, and IP
cores than any other formal verification
technology.
Encounter Conformal EC is available in L,
XL, and GXL offerings.
BENEFITS
• Exhaustively verifies multimillion-gate
ASICs and FPGAs—several times faster
than traditional gate-level simulation
• Decreases the risk of missing critical
bugs with independent verification
technology
• Enables faster, more accurate bug
detection and correction throughout
the entire design flow
Figure 1: Encounter digital IC design platform
Page 2
RTL
Synthesis
Place and route
Physical synthesis
ECOs
Final layout
Datapath synthesis
Custom circuit design
Custom memory design
Encounter
Conformal EC L
Logic equivalence checking
Dual language support
Semantic checks
Structural checks
Clock domain crossing check
Extends equivalence checking
to digital custom logic and
memories
Encounter
Conformal EC XL
Encounter
Conformal EC GXL
Extends equivalence
checking to datapath
and layout vs. schematic
(LVS) reference SPICE netlist
Figure 2: Encounter Conformal EC offers a complete solution—from RTL to final layout
• Eliminates functional clock domain
crossing problems early in the design
cycle
• Extends equivalence checking capability
to complex datapaths, and closes the
RTL-to-layout verification gap (with
Encounter Conformal EC XL)
• Ensures RTL models perform the same
functions as the corresponding transistor
circuits implemented on silicon (with
Encounter Conformal EC GXL)
FEATURES
ENCOUNTER CONFORMAL
EQUIVALENCE CHECKER L
Encounter Conformal EC L combines
extended functional checks with core
equivalence checking technology.
2www.c a den c e.c om
ENC OU NTER CO NF ORMA L E QU IVA LEN CE CHE CKE R
Equivalence Checking
During the development of a design, it
undergoes numerous iterations prior to
final layout, and each step in this process
has the potential to introduce logical bugs.
Encounter Conformal EC L checks the
functional equivalence of different versions
of a design at these various stages and
enables designers to identify and correct
errors as soon as they are introduced.
Design Flow Independence
Encounter Conformal EC L provides
an independent audit of the design
process to eliminate the risks associated
with sharing technologies across design
implementation and design verification
products. The tool includes technologies
developed independently from the design
flow, including production-proven HDL
parsing, synthesis, mapping, optimization,
and datapath algorithms. Using Encounter
Conformal EC L ensures that the maximum
number of design bugs will be caught.
Integrated Environment
An intuitive graphical user interface (GUI)
provides for setup and debugging. It allows
users to work more productively and
quickly pinpoint the cause of mismatches.
The environment includes:
• Graphical debugging via an integrated
schematic viewer that shows logic values
for each error vector
• Full cross-highlighting between RTL
model and circuit
• Automatic error candidate identification
with assigned and weighted percentages
• Logic-cone pruning to focus debugging
on relevant information
FPGA Equivalence Checking
Support
As FPGA devices continue to grow in
size and complexity, FPGA designers are
facing design closure challenges similar
to those encountered by their ASIC
counterparts. Equivalence checking has
become a necessity in the FPGA design
implementation flow. Encounter Conformal
EC L supports Synplify Pro synthesis, as
well as the Xilinx ISE and Altera Quartus II
implementation flows.
Clock Domain Crossing (CDC) and
Extended Functional Checks
Encounter Conformal EC L enables designers
to perform verification of the asynchronous
clock domain crossings and other intrinsic
properties of their designs. These checks
complement equivalence checking by verifying
areas previously not validated by traditional
equivalence checkers and by finding difficult
implementation bugs early in the design cycle.
The end result is a safer verification solution.
• Clock domain crossing checks
– Recognize FIFO synchronizers
automatically
– Validate synchronization structure
– Verify data stability
• Semantic checks—Verify synthesis
assumptions and find conditions that
may create mismatches between RTL
and gate-level simulations
Page 3
compares circuitry that has gone through
RTL
design
IP Lib
Gate GDS
SPICE
reference
netlist
Encounter
Conformal EC
Equivalence
checking
Abstraction
Physical design
LVS
Encounter Conformal EC
expression optimization and automatically
verifies multipliers with standard
architectures and dynamic structures
• Advanced pipelining check—Verifies
proper implementation of pipelined
designs
• Carry-save verification capability—Allows
verification of circuits containing carrysave transformations introduced during
optimization for sequence of adders,
multipliers, and registers
Final Circuit Verification
Encounter Conformal EC XL is the only
verification product that enables a
complete verification solution from RTL
to final layout. It functionally compares a
SPICE netlist created for LVS or extracted
from GDS to the RTL or gate model. This
process ensures that the circuit on silicon
has the same logic function that was
designed and verified.
Figure 3: Encounter Conformal EC has an easy-to-use GUI with extensive diagnosis and debugging capabilities
• Structural checks—Include bus checks for
data conflicts, set-reset exclusivity checks,
and multiport latch contention checks
ENCOUNTER CONFORMAL
EQUIVALENCE CHECKER XL
In addition to all the features provided
by Encounter Conformal EC L, Encounter
using test vectors. It can handle a wide
variety of datapath structures required for
high-performance designs.
• Automatic flat datapath module
verification—Enables easy verification
without manually specifying boundaries
or architectures in the flattened netlist;
automatically verifies merged operators;
Conformal EC XL offers automated
checking of complex datapaths. It also
extends equivalence checking to final
place-and-route netlist.
Datapath Synthesis Verification
Datapath optimization can create designs
that are difficult to formally verify because
of complex arithmetic operations.
Designers have been relying on simulation
to verify datapath blocks, but simulation
runtimes are exceedingly long and the
results can be incomplete.
Smart Setup and Diagnosis
Encounter Conformal EC XL includes a set
of intelligent ‘analyze’ commands to ease
setup and diagnosis. For example, ‘analyze
setup’ investigates the current environment
and automatically remedies common setup
issues sometimes experienced by new
users. In tandem, ‘analyze nonequivalent’
can be invoked if non-equivalences are
encountered. The command then presents
a one-line answer as to what is wrong.
Encounter Conformal EC XL offers a firstof-its-kind formal solution that exhaustively
verifies complex datapath blocks without
www.c a den c e.c om3
Figure 4: Encounter Conformal EC XL provides complete verification from RTL to SPICE
ENC OU NTER CO NF ORMA L E QU IVA LEN CE CHE CKE R
Page 4
Parallel Processing
For larger designs, overall verification time
can be reduced with multiple licenses by
running Encounter Conformal EC XL on
many machines simultaneously. LSF is also
supported.
ENCOUNTER CONFORMAL
EQUIVALENCE CHECKER GXL
In addition to all the features in Encounter
Conformal EC XL, Encounter Conformal
EC GXL offers transistor circuit analysis for
custom designs and embedded memories.
Designers can use Encounter Conformal
EC GXL with custom embedded memories,
arithmetic blocks, datapaths, standard and
extended libraries, and all other custom
and semi-custom digital circuit functions.
Circuit styles supported include standard
and complex Boolean functions, latches
and registers, pass-gate, transmission-gate,
tri-state switch logic, pre-charged logic
cells, domino logic blocks, and dual-rail.
Custom Logic Abstraction
Encounter Conformal EC GXL analyzes
digital transistor circuits and derives an
equivalent logical Verilog® model. The
underlying abstraction algorithms are more
powerful than pattern-based solutions.
A Verilog gate logic model of the
abstracted circuit can be used for:
• Emulation—Provides accurate emulation
models for actual transistor-level circuits
• Simulation acceleration—Using the
abstracted Verilog model allows
simulation to run many times faster than
with SPICE circuit
Memory Verification
Traditional and symbolic simulation tools
do not scale for verifying today’s memory
functions and their ever increasing
complexity. Encounter Conformal EC
GXL provides exhaustive logic verification
and— since no testbench is needed—the
quality of results is not limited by
availability of time or resources to develop
comprehensive tests. Encounter Conformal
EC GXL generates memory primitive
models for Verilog system simulation and
complete logic function verification of the
transistor circuit design using equivalence
checking.
• Intuitive graphical interface to generate
specific primitives
• Generated primitives are address, word,
and column MUX configurable
• All read-write, read-only, and write-only
combinations can be generated
• Generated simulation models have
the highest performance and contain
built-in assertions for trapping illegal
memory use such as address collision and
simultaneous read-write
PLATFORMS
• Linux (32-bit, 64-bit)
• Sun Solaris (32-bit, 64-bit)
• IBM AIX (32-bit, 64-bit)
LANGUAGE SUPPORT
• Verilog (1995, 2001)
• SystemVerilog
• VHDL (87, 93)
• SPICE (traditional, LVS)
• EDIF
• Liberty
• Mixed languages
• Equivalence checking
• Fault grading—Preserves the circuit
hierarchy and structure for maximum
debugging efficiency