使用 Synopsys Formality 验证 AIG 的 miter 电路等价性

前言

遇到等价性检查工具和商业工具对比的需求，这里记录一下，完整脚本流程可以参考 Git 仓库：

YuhangQ/formality\_cec: 使用商业工具测试 AIG 格式的 miter 电路等价性 - formality\_cec - Gitea: Git with a cup of tea

数据准备

由于 Formality 并不支持 AIG 格式，并且也不支持 miter 电路，因此需要将 miter 电路拆分成两个电路，并且都需要转换成 verilog 格式。

电路拆分这里使用 abc，里面存在 &demiter 命令，可以将电路拆分成两部分：

usage: &demiter [-ftdvh]
                 decomposes a miter (by default, tries to extract an OR gate)
        -f     : write files with two sides of a dual-output miter [default = no]
        -t     : write files with two sides of a two-word miter [default = no]
        -d     : take single-output and decompose into dual-output [default = no]
        -v     : toggles printing verbose information [default = no]
        -h     : print the command usage

直接调用即可，会在数据同目录自动生成两个文件，然后读进来调用 write_verilog 输出就行了：

abc -c "&r xxx.aig; &demiter -d -v; &demiter -f"

完整脚本如下：

formality\_cec/convert.py 位于 main - formality\_cec - Gitea: Git with a cup of tea

Formality 脚本

Formality 采用 tcl 格式的脚本，具体的命令很冷门，不过还好组合电路比较简单，按照下面的写就可以了。

# 设置搜索路径
set_app_var search_path "."

# 读取两个 verilog 文件 (添加设计名称)
read_verilog -r demiter_verilog/easy1_1.v
set_top -auto

read_verilog -i demiter_verilog/easy1_2.v
set_top -auto

# 建立匹配点
match

# 设置比较点并验证
verify

quit

写完脚本，调用 fm_shell -f xxx.tcl 就可以运行了。