为chisel-nix添加formal支持#

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

构建以及运行#

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

nix build .#gcd.formal-rtl

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

通过jg的formal验证

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

JasperGold FPV Flow script#

# 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