[i=s] 本帖最后由 走来走去 于 2020-7-22 23:28 编辑 [/i]

Formality breaks the reference and implementation designs
into compare points, each with its own logic cone
Formaility将参考设计和应用设计打断成比较点，每个比较点有自己的逻辑锥

READ: Partitions reference and
implementation designs into logic cones
and compare points
把参考设计和应用设计切分成逻辑锥和比较点
->
MATCH : Aligns (map) corresponding
compare points between the two designs
匹配：对齐两个设计相应的比较点
->
VERIFY : Checks functionality of each
compare point pair
验证：检查每对比较点的功能性
->
DEBUG : GUI and Reports
诊断：图形化界面诊断，查看报告




最简单的formal流程：
#Step 0: Guidance
set_svf default.svf
#Step 1: Read Reference Design
read_verilog -r alu.v
set_top alu
load_upf –r alu.upf
#Step 2: Read Implementation Design
read_db –i lsi_10k.db
read_verilog -i alu.fast.vg
set_top -auto
load_upf –I alu.fast.upf
#Step 3: Setup
#No setup required here
#Steps 4 & 5: Match and Verify
verify