From 48154cb6f452d3bdb4da36cc267b4b6c45588dc9 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 18 Jul 2015 13:10:40 +0200
Subject: Imported full dev sources

---
 icefuzz/check.sh | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 icefuzz/check.sh

(limited to 'icefuzz/check.sh')

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
+
-- 
cgit v1.2.3