mirror of
https://github.com/YosysHQ/yosys
synced 2026-05-31 22:27:50 +00:00
Use generic testing on few more places
This commit is contained in:
parent
f96fa5ff00
commit
8953007483
7 changed files with 82 additions and 150 deletions
|
|
@ -1,18 +1,13 @@
|
|||
#!/usr/bin/env python3
|
||||
|
||||
import sys
|
||||
sys.path.append("..")
|
||||
|
||||
import gen_tests_makefile
|
||||
|
||||
import glob
|
||||
import os
|
||||
|
||||
yosys = "../../yosys"
|
||||
default_abc = "../../yosys-abc"
|
||||
|
||||
aags = sorted(glob.glob("*.aag"))
|
||||
yss = sorted(glob.glob("*.ys"))
|
||||
|
||||
print("ABC ?= " + default_abc)
|
||||
print("YOSYS ?= " + yosys)
|
||||
print()
|
||||
|
||||
def base(fn):
|
||||
return os.path.splitext(fn)[0]
|
||||
|
||||
|
|
@ -23,46 +18,41 @@ def base(fn):
|
|||
# Since ABC cannot read *.aag, read the *.aig instead
|
||||
# (which would have been created by the reference aig2aig utility,
|
||||
# available from http://fmv.jku.at/aiger/)
|
||||
def create_tests():
|
||||
aags = sorted(glob.glob("*.aag"))
|
||||
yss = sorted(glob.glob("*.ys"))
|
||||
for aag in aags:
|
||||
b = base(aag)
|
||||
|
||||
for aag in aags:
|
||||
b = base(aag)
|
||||
cmd = [
|
||||
f"$(ABC) -q \"read -c {b}.aig; write {b}_ref.v\" >/dev/null 2>&1;",
|
||||
"$(YOSYS) -qp \"",
|
||||
f"read_verilog {b}_ref.v;",
|
||||
"prep;",
|
||||
"design -stash gold;",
|
||||
f"read_aiger -clk_name clock {aag};",
|
||||
"prep;",
|
||||
"design -stash gate;",
|
||||
"design -import gold -as gold;",
|
||||
"design -import gate -as gate;",
|
||||
"miter -equiv -flatten -make_assert -make_outputs gold gate miter;",
|
||||
"sat -verify -prove-asserts -show-ports -seq 16 miter;",
|
||||
f"\" -l {aag}.log >/dev/null 2>&1"
|
||||
]
|
||||
|
||||
print(f"all: {aag}")
|
||||
print(f".PHONY: {aag}")
|
||||
print(f"{aag}:")
|
||||
print(f"\t@echo Checking {aag}.")
|
||||
print(f"\t@$(ABC) -q \"read -c {b}.aig; write {b}_ref.v\" >/dev/null 2>&1")
|
||||
print("\t@$(YOSYS) -qp \"\\")
|
||||
print(f"\tread_verilog {b}_ref.v; \\")
|
||||
print("\tprep; \\")
|
||||
print("\tdesign -stash gold; \\")
|
||||
print(f"\tread_aiger -clk_name clock {aag}; \\")
|
||||
print("\tprep; \\")
|
||||
print("\tdesign -stash gate; \\")
|
||||
print("\tdesign -import gold -as gold; \\")
|
||||
print("\tdesign -import gate -as gate; \\")
|
||||
print("\tmiter -equiv -flatten -make_assert -make_outputs gold gate miter; \\")
|
||||
print("\tsat -verify -prove-asserts -show-ports -seq 16 miter; \\")
|
||||
print(f"\t\" -l {aag}.log >/dev/null 2>&1")
|
||||
print()
|
||||
gen_tests_makefile.generate_cmd_test(aag, cmd)
|
||||
|
||||
# ---- Yosys script tests ----
|
||||
for ys in yss:
|
||||
b = base(ys)
|
||||
print(f"all: {ys}")
|
||||
print(f".PHONY: {ys}")
|
||||
print(f"{ys}: ")
|
||||
print(f"\t@echo Running {ys}.")
|
||||
print(f"\t@$(YOSYS) -ql {b}.log {ys} >/dev/null 2>&1")
|
||||
print()
|
||||
# ---- Yosys script tests ----
|
||||
for ys in yss:
|
||||
gen_tests_makefile.generate_ys_test(ys)
|
||||
|
||||
# ---- aigmap test ----
|
||||
print(f"all: aigmap")
|
||||
print(f".PHONY: aigmap")
|
||||
print("aigmap:")
|
||||
print("\t@echo Running aigmap.")
|
||||
print("\t@rm -rf gate; mkdir gate")
|
||||
print('\t@$(YOSYS) --no-version -p "test_cell -aigmap -w gate/ -n 1 -s 1 all" >/dev/null 2>&1')
|
||||
print("\t@set -o pipefail; diff --brief gold gate | tee aigmap.err")
|
||||
print("\t@rm -f aigmap.err")
|
||||
print()
|
||||
cmd = [ "rm -rf gate; mkdir gate;",
|
||||
"$(YOSYS) --no-version -p \"test_cell -aigmap -w gate/ -n 1 -s 1 all\" >/dev/null 2>&1;",
|
||||
"set -o pipefail; diff --brief gold gate | tee aigmap.err;",
|
||||
"rm -f aigmap.err" ]
|
||||
|
||||
gen_tests_makefile.generate_cmd_test("aigmap", cmd)
|
||||
|
||||
extra = [ f"ABC ?= {gen_tests_makefile.yosys_basedir}/yosys-abc" ]
|
||||
|
||||
gen_tests_makefile.generate_custom(create_tests, extra)
|
||||
|
|
|
|||
|
|
@ -1,70 +0,0 @@
|
|||
#!/usr/bin/env bash
|
||||
source ../common-env.sh
|
||||
|
||||
set -e
|
||||
|
||||
OPTIND=1
|
||||
abcprog="../../yosys-abc" # default to built-in version of abc
|
||||
while getopts "A:" opt
|
||||
do
|
||||
case "$opt" in
|
||||
A) abcprog="$OPTARG" ;;
|
||||
esac
|
||||
done
|
||||
shift "$((OPTIND-1))"
|
||||
|
||||
# NB: *.aag and *.aig must contain a symbol table naming the primary
|
||||
# inputs and outputs, otherwise ABC and Yosys will name them
|
||||
# arbitrarily (and inconsistently with each other).
|
||||
|
||||
for aag in *.aag; do
|
||||
# Since ABC cannot read *.aag, read the *.aig instead
|
||||
# (which would have been created by the reference aig2aig utility,
|
||||
# available from http://fmv.jku.at/aiger/)
|
||||
echo "Checking $aag."
|
||||
$abcprog -q "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v" >/dev/null 2>&1
|
||||
../../yosys -qp "
|
||||
read_verilog ${aag%.*}_ref.v
|
||||
prep
|
||||
design -stash gold
|
||||
read_aiger -clk_name clock $aag
|
||||
prep
|
||||
design -stash gate
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -show-ports -seq 16 miter
|
||||
" -l ${aag}.log >/dev/null 2>&1
|
||||
done
|
||||
|
||||
for aig in *.aig; do
|
||||
echo "Checking $aig."
|
||||
$abcprog -q "read -c $aig; write ${aig%.*}_ref.v" >/dev/null 2>&1
|
||||
../../yosys -qp "
|
||||
read_verilog ${aig%.*}_ref.v
|
||||
prep
|
||||
design -stash gold
|
||||
read_aiger -clk_name clock $aig
|
||||
prep
|
||||
design -stash gate
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -show-ports -seq 16 miter
|
||||
" -l ${aig}.log >/dev/null 2>&1
|
||||
done
|
||||
|
||||
for y in *.ys; do
|
||||
echo "Running $y."
|
||||
../../yosys -ql ${y%.*}.log $y >/dev/null 2>&1
|
||||
done
|
||||
|
||||
# compare aigmap with reference
|
||||
# make gold with: rm gold/*; yosys --no-version -p "test_cell -aigmap -w gold/ -n 1 -s 1 all"
|
||||
rm -rf gate; mkdir gate
|
||||
../../yosys --no-version -p "test_cell -aigmap -w gate/ -n 1 -s 1 all" >/dev/null 2>&1
|
||||
(
|
||||
set -o pipefail
|
||||
diff --brief gold gate | tee aigmap.err
|
||||
)
|
||||
rm aigmap.err
|
||||
Loading…
Add table
Add a link
Reference in a new issue