diff options
author | Clifford Wolf <clifford@clifford.at> | 2015-07-18 13:10:40 +0200 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2015-07-18 13:10:40 +0200 |
commit | 48154cb6f452d3bdb4da36cc267b4b6c45588dc9 (patch) | |
tree | 3ec3be9ef7e8db1fb7c764ed8202e0215a8eb7c7 /icefuzz/check.sh | |
parent | 13e63e6b65e044e348356731b55610d02cb308b9 (diff) | |
download | icestorm-48154cb6f452d3bdb4da36cc267b4b6c45588dc9.tar.gz icestorm-48154cb6f452d3bdb4da36cc267b4b6c45588dc9.tar.bz2 icestorm-48154cb6f452d3bdb4da36cc267b4b6c45588dc9.zip |
Imported full dev sources
Diffstat (limited to 'icefuzz/check.sh')
-rw-r--r-- | icefuzz/check.sh | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/icefuzz/check.sh b/icefuzz/check.sh new file mode 100644 index 0000000..bb23cea --- /dev/null +++ b/icefuzz/check.sh @@ -0,0 +1,50 @@ +#!/bin/bash + +set -ex + +for id; do + id=${id%.bin} + icebox_vlog_opts="-Sa" + if test -f $id.pcf; then icebox_vlog_opts="$icebox_vlog_opts -p $id.pcf"; fi + if test -f $id.psb; then icebox_vlog_opts="$icebox_vlog_opts -P $id.psb"; fi + + ../icepack/iceunpack $id.bin $id.txt + ../icebox/icebox_vlog.py $icebox_vlog_opts $id.txt > $id.ve + + yosys -p " + read_verilog $id.v + read_verilog $id.ve + read_verilog -lib +/ice40/cells_sim.v + rename top gold + rename chip gate + + proc + splitnets -ports + clean -purge + + ## Variant 1 ## + + # miter -equiv -flatten gold gate equiv + # tee -q synth -top equiv + # sat -verify -prove trigger 0 -show-ports equiv + + ## Variant 2 ## + + # miter -equiv -flatten -ignore_gold_x -make_outcmp -make_outputs gold gate equiv + # hierarchy -top equiv + # sat -max_undef -prove trigger 0 -show-ports equiv + + ## Variant 3 ## + + equiv_make gold gate equiv + hierarchy -top equiv + opt -share_all + + equiv_simple + equiv_induct + equiv_status -assert + " + + touch $id.ok +done + |