一、LEC简介
Conformal的逻辑等价性检查（LEC）工具，是Encounter功能验证平台的一部分，用于验证从RTL到布局的复杂片上系统（SoC）设计。它不依赖于输入激励，通过数学解析的方式对电路的逻辑等效性进行完备验证，确保逻辑更改不会导致功能错误。
二、LEC运行
1、启动LEC
使用以下命令启动LEC：
lec [-xl] [-nogui] [-dofile filename] [-logfile filename] [-color]-xl：指定需要有运算逻辑分析能力的license（默认启动-l）
-gui or -nogui：以GUI或非GUI方式启动LEC
-dofile
-logfile
-color：在nogui模式下控制颜色编码的messages
2、指定命令输入模式
在Conformal中，有两种模式：默认的Conformal命令输入模式（VPXMODE）和Tcl命令输入模式（TCLMODE）。使用以下命令进行切换：
tclmode
vpxmode本文所有命令均在VPXMODE模式下使用
三、Setup模式
Conformal有Setup和LEC两种工作模式。启动后，Conformal开始以Setup模式运行，在命令输入窗口中显示SETUP>提示符。在Setup模式中，可以读取library和design，应用constraints，并设置形式验证的options。
1、设置Options
1.1 添加搜索路径
Conformal使用搜索路径查找保存在当前工作目录以外的目录中的design文件和library文件。
add search path [-design | -library] [-golden | -revised | -both] 如果未指定-design或-library，则Conformal将此命令同时应用于read design和read library命令。
1.2 添加Notranslate Modules
当选择不编译特定的库或设计模块时，必须运行
add notranslate modules 指定的模块自动成为blackboxes。因为此命令在初始解析期间被应用，因此名称匹配仅适用于原始模块名称。
1.3 更改root module
set root module [-golde | -revised | -both] 2、读取Library和Design文件
2.1 读取Library文件
read library lib.lib -liberty -both2.2 读取Design文件
read design file1.v –verilog –golden
read design file2.v –verilog –revised
注意：design_netlist.v文件必须由Cadence的综合工具Genus生成
小结与拓展
本文介绍了Conformal LEC工具的基本使用方法，包括启动LEC、设置Options、读取Library和Design文件等。Conformal LEC是一个功能强大的形式验证工具，可以用于验证各种复杂的设计。如果您想了解更多关于Conformal LEC的信息，请访问「极星编程网」（www.jxgpc.com）。
——苏承栈，极星编程网资深编辑