example: Hazard3 CPU

The Hazard3 RISC-V CPU comes with SVA assertions.  This script downloads the
RTL, and runs ebmc to check them.

Author: kroening

examples/Hazard3/Hazard3.sh

@@ -0,0 +1,30 @@
+#!/bin/sh
+
+# abort on error
+set -e
+
+# clone Hazard3 repo if not done yet
+if [ ! -e Hazard3/.git ] ; then
+  git clone https://github.com/Wren6991/Hazard3
+  git checkout v1.0
+fi
+
+cd Hazard3/hdl
+
+ebmc -I . -I HAZARD3_ASSERTIONS --bound 0 \
+  arith/hazard3_alu.v \
+  arith/hazard3_priority_encode.v \
+  arith/hazard3_onehot_encode.v \
+  arith/hazard3_onehot_priority.v \
+  arith/hazard3_shift_barrel.v
+ebmc -I . -I HAZARD3_ASSERTIONS --bound 0 arith/hazard3_multdiv_seq.v
+ebmc -I . -I HAZARD3_ASSERTIONS --bound 0 arith/hazard3_shift_barrel.v
+
+ebmc -I . -I HAZARD3_ASSERTIONS --bound 0 hazard3_core.v
+ebmc -I . -I HAZARD3_ASSERTIONS --bound 0 hazard3_cpu_2port.v
+ebmc -I . -I HAZARD3_ASSERTIONS --bound 0 hazard3_csr.v
+ebmc -I . -I HAZARD3_ASSERTIONS --bound 0 hazard3_decode.v
+ebmc -I . -I HAZARD3_ASSERTIONS --bound 0 hazard3_frontend.v
+ebmc -I . -I HAZARD3_ASSERTIONS --bound 0 hazard3_instr_decompress.v
+ebmc -I . -I HAZARD3_ASSERTIONS --bound 0 hazard3_power_ctrl.v
+