使用JasperGold进行形式化验证

为chisel-nix添加formal支持

源代码: https://github.com/chipsalliance/chisel-nix/tree/try_formal

构建以及运行

安装nix, 然后在项目目录下输入

1
nix build .#gcd.formal-rtl

获得result/GCD.sv以及result/GCDFormal.sv

通过jg的formal验证

1
jg -fpv ./script/formal/FPV.tcl

JasperGold FPV Flow script

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
# Make sure you have run the nix build command to build the formal results
# Now the result/ directory should contain the GCD.sv and GCDFormal.sv

# Analyze design under verification files
set RESULT_PATH ./result

# Analyze source files and property files
analyze -sv12 \
  ${RESULT_PATH}/GCD.sv \
  ${RESULT_PATH}/GCDFormal.sv

# Elaborate design and properties
elaborate -top GCDFormal

# Set up Clocks and Resets
clock clock
reset reset

# Get design information to check general complexity
get_design_info

# Prove properties
# 1st pass: Quick validation of properties with default engines
set_max_trace_length 10
prove -all

# Report proof results
report