terapines
/
circt
mirror of https://github.com/llvm/circt.git
2
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
circt/utils/equiv-rtl.sh

79 lines
1.5 KiB
Bash
Raw Normal View History

utils/*.sh: Prefer /usr/bin/env bash for portability. (#3697) Fixes use on NixOS.
2022-08-11 02:09:55 +08:00
#!/usr/bin/env bash
[FIRRTL] yosys equiv checking infrastructure and FIRRTL primatives testcase (#291) Yosys formal equivalence checking infrastructure.
2020-12-03 04:18:23 +08:00
##===- utils/equiv-rtl.sh - Formal Equivalence via yosys------*- Script -*-===##
#
# Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
# See https://llvm.org/LICENSE.txt for license information.
# SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
#
##===----------------------------------------------------------------------===##
#
# This script checks two input verilog files for equivalence using yosys.
#
# Usage equiv-rtl.sh File1.v File2.v TopLevelModuleName
#
##===----------------------------------------------------------------------===##
Add SAT solver yosys fallback for failed simple solver attempts
2021-01-21 05:58:26 +08:00
if [ "$4" != "" ]; then
mdir=$4
else
mdir=.
fi
[FIRRTL] yosys equiv checking infrastructure and FIRRTL primatives testcase (#291) Yosys formal equivalence checking infrastructure.
2020-12-03 04:18:23 +08:00
Add SAT solver yosys fallback for failed simple solver attempts
2021-01-21 05:58:26 +08:00
echo "Comparing $1 and $2 with $3 Missing Dir $mdir"
[FIRRTL] yosys equiv checking infrastructure and FIRRTL primatives testcase (#291) Yosys formal equivalence checking infrastructure.
2020-12-03 04:18:23 +08:00
yosys -q -p "
read_verilog $1
Add SAT solver yosys fallback for failed simple solver attempts
2021-01-21 05:58:26 +08:00
hierarchy -libdir $mdir
[FIRRTL] yosys equiv checking infrastructure and FIRRTL primatives testcase (#291) Yosys formal equivalence checking infrastructure.
2020-12-03 04:18:23 +08:00
rename $3 top1
proc
memory
flatten top1
Add SAT solver yosys fallback for failed simple solver attempts
2021-01-21 05:58:26 +08:00
read_verilog $2
hierarchy -libdir $mdir
[FIRRTL] yosys equiv checking infrastructure and FIRRTL primatives testcase (#291) Yosys formal equivalence checking infrastructure.
2020-12-03 04:18:23 +08:00
rename $3 top2
proc
memory
flatten top2
Add SAT solver yosys fallback for failed simple solver attempts
2021-01-21 05:58:26 +08:00
clean -purge
opt -purge
[FIRRTL] yosys equiv checking infrastructure and FIRRTL primatives testcase (#291) Yosys formal equivalence checking infrastructure.
2020-12-03 04:18:23 +08:00
equiv_make top1 top2 equiv
hierarchy -top equiv
[VerilogQuality] Remove muxes feeding registers their old value (#965) When a mux feeds an assign to a register and one branch of the mux is the register's old value, we can turn that into a conditional assign. This results in much cleaner verilog output.
2021-04-27 23:43:52 +08:00
equiv_simple -undef
equiv_induct -undef
[FIRRTL] yosys equiv checking infrastructure and FIRRTL primatives testcase (#291) Yosys formal equivalence checking infrastructure.
2020-12-03 04:18:23 +08:00
equiv_status -assert
"
if [ $? -eq 0 ]
then
Add SAT solver yosys fallback for failed simple solver attempts
2021-01-21 05:58:26 +08:00
echo "PASS,INDUCT"
[FIRRTL] yosys equiv checking infrastructure and FIRRTL primatives testcase (#291) Yosys formal equivalence checking infrastructure.
2020-12-03 04:18:23 +08:00
exit 0
fi
Add SAT solver yosys fallback for failed simple solver attempts
2021-01-21 05:58:26 +08:00
#repeat with sat
echo "Trying SAT $1 and $2 with $3 Missing Dir $mdir"
yosys -q -p "
read_verilog $1
hierarchy -libdir $mdir
rename $3 top1
proc
memory
flatten top1
read_verilog $2
hierarchy -libdir $mdir
rename $3 top2
proc
memory
flatten top2
opt
miter -equiv -make_assert -flatten top1 top2 equiv
hierarchy -top equiv
opt
sat -prove-asserts -seq 4 -verify
"
if [ $? -eq 0 ]
then
echo "PASS,SAT"
exit 0
fi
echo "FAIL"
exit 1