Conformal Equivalence
Checking Product Suite User
Manual
Version 3.5.1.a
January 2003
Verplex
TM
Systems, Inc.
Copyright © 1997 - 2003
All rights reserved
Copyright Notice and Proprietary Information
Copyright © 1997, 1998, 1999, 2000, 2001, 2002, 2003 Verplex Systems, Inc. All rights reserved. This
software and manual are owned by Verplex Systems, Inc. and may be used only as authorized in the license
agreement controlling such use. No part of this publication may be reproduced, transmitted, or translated, in
any form or by any means, electronic, mechanical, manual, optical, or otherwise, without prior written
permission of Verplex Systems, or as expressly provided by the license agreement.
This document is for information and instruction purposes. Verplex Systems reserves the right to make
changes in specifications and other information contained in this publication without prior notice, and the
reader should, in all cases, consult Verplex Systems to determine whether any changes have been made.
Disclaimer
VERPLEX SYSTEMS, INC. MAKES NO WARRANTY OF ANY KIND WITH REGARD TO
THIS MATERIAL, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.
VERPLEX SYSTEMS, INC. SHALL NOT BE LIABLE FOR ANY INCIDENTAL, INDIRECT,
SPECIAL, OR, CONSEQUENTIAL DAMAGES WHATSOEVER (INCLUDING BUT NOT
LIMITED TO LOST PROFITS) ARISING OUT OF OR RELATED TO THIS PUBLICATION
OR THE INFORMATION CONTAINED IN IT, EVEN IF VERPLEX SYSTEMS, INC. HAS
BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
Trademarks
Alliance, CORE Generator, and Virtex-II Pro are trademarks of Xilinx, Inc.
Conformal is a trademark of Verplex Systems, Inc.
Debussy is a trademark of Novas Software, Inc.
Liberty format is a trademark of Synopsys, Inc.
Synplify Pro is a trademark of Synplicity, Inc.
UNIX is a trademark of The Open Group.
Verilog is a trademark of Cadence Design Systems, Inc.
Windows is a trademark of the Microsoft Corporation.
Verplex Systems, Inc.
300 Montague Expressway
Suite 100
Milpitas, CA 95035
Tel: (408) 586-0300
Toll-Free: (800) 788-9337
Fax: (408) 586-0230
www.verplex.com
Table of Contents
Chapter 1:
Using This Manual . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1
Getting Started
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
What’s New in this Version?
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
Conventions Used in This Manual
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
How to Reach Verplex Systems
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
Chapter 2:
Conformal Installation . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5
Installing LEC
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
Installing the FLEXLM License Server
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
Executing LEC
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
LEC Demo
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
Troubleshooting
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
Feedback
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
Chapter 3:
Understanding Formal Verification . . . . . . . . . . . . . . . . . .
11
What is Formal Verification?
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
Why Use Formal Verification?
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
Design Complexity and Functional Uncertainty . . . . . . . . . . . . . . . . . . . . . . . 12
The Formal Alternative . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
How is Formal Verification Applied to the Design and Verification
Flow?
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
Chapter 4:
Conformal Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
15
Introduction
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
Conformal Features
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
LEC Methodology
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
Preparing the Designs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
Mapping and Comparing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
Diagnosing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
LEC Operation
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
System Modes. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Transition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Mapping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Comparison. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Diagnosis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
18
18
19
19
20
Conformal User Manual v 3.5.1.a
iii
Chapter 5:
LEC Commands and Process Flow . . . . . . . . . . . . . . . . . .
21
Phase I: Starting LEC
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
Initialization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
Phase II: Using the Setup Mode
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
Basic Operating Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Task Streamlining . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Parameters. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Designs and Libraries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Design Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Flattening Options. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Command Structure Complement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Mapping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Switching System Modes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Mapping Modification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Warning Messages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Compare Options . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Comparison . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
23
26
27
30
35
43
48
49
52
53
55
55
56
Using the LEC Mode
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
Debugging
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
Diagnosing Non-Equivalent Points . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
Proving Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
Gate Reporting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
Exiting. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
Chapter 6:
Conformal Graphical User Interface . . . . . . . . . . . . . . . . .
63
Menu Bar
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
File Pull-Down Menu Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
Setup Pull-Down Menu Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
Report Pull-Down Menu Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
Run Pull-Down Menu Command . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
Tools Pull-Down Menu Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
LTX Pull-Down Menu Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139
Preferences Pull-Down Menu Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . 146
Window Menu. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 148
Help Pull Down Menu Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 148
Icon Bar
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152
Source Code Manager. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153
Find . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 156
Hierarchical Browser
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157
Transcript Window
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 163
Command Entry Window
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 164
Status Bar
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 164
Chapter 7:
LEC Example Test Case . . . . . . . . . . . . . . . . . . . . . . . . . .
165
Step 1: Invoking the Tool
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
Step 2: Reading the Library
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 166
iv
Contents
Step 3: Reading the Designs
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
Step 4: Changing to the LEC System Mode
. . . . . . . . . . . . . . . . . . . . . . 168
Step 5: Viewing Unmapped and Mapped Points
. . . . . . . . . . . . . . . . . . 169
Step 6: Performing Comparison
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170
Step 7: Performing Diagnosis
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170
Step 8: Employing the Schematic Viewer
. . . . . . . . . . . . . . . . . . . . . . . . 172
Step 9: Adding Pin Constraints
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 174
Step 10: Reprocessing the Comparison
. . . . . . . . . . . . . . . . . . . . . . . . . . . 175
Step 11: Exiting
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175
Chapter 8:
Using the Verplex Schematic Viewer . . . . . . . . . . . . . . . .
Flatten Schematics Menu Bar. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Flatten Schematics Tool Bar. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Flatten Schematics Display . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Selected Object Field . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Module Schematics Menu Bar . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Module Schematics Tool Bar . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Module Schematics Display . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Selected Object Field . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Example Map File and Dofile . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Symmetric Input Symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Non-Symmetric Input Symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Transistor-Related Symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
177
Flatten Schematics
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 178
180
189
193
199
201
207
210
215
215
216
217
218
219
Module Schematics
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 200
Symbol Map File
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 215
Chapter 9:
Performing Hierarchical Comparison . . . . . . . . . . . . . . .
221
Overview
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 221
Command Flow
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 223
Reading the Libraries and Designs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Generating a Hierarchical Compare Dofile . . . . . . . . . . . . . . . . . . . . . . . . . .
Hierarchical Compare Dofile . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
No Black Boxing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Constraint Propagation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
223
224
225
227
227
Warning Messages
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 230
Renaming Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 230
Hierarchical Compare Dofile Execution
. . . . . . . . . . . . . . . . . . . . . . . . . . 230
Chapter 10:
LTX Commands and Process Flow . . . . . . . . . . . . . . . . .
233
Overview
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 233
LTX Licensing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 234
Conformal User Manual v 3.5.1.a
v
京公网安备 11010802033920号
Copyright © 2005-2024 EEWORLD.com.cn, Inc. All rights reserved
评论