fx

Author: kroening

examples/Hazard3/Hazard3.sh

@@ -9,22 +9,52 @@ if [ ! -e Hazard3/.git ] ; then
   git checkout v1.0
 fi
 
-cd Hazard3/hdl
-
-ebmc -I . -D 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 . -D HAZARD3_ASSERTIONS --bound 0 arith/hazard3_multdiv_seq.v
-ebmc -I . -D HAZARD3_ASSERTIONS --bound 0 arith/hazard3_shift_barrel.v
-
-ebmc -I . -D HAZARD3_ASSERTIONS --bound 0 hazard3_core.v
-ebmc -I . -D HAZARD3_ASSERTIONS --bound 0 hazard3_cpu_2port.v
-ebmc -I . -D HAZARD3_ASSERTIONS --bound 0 hazard3_csr.v
-ebmc -I . -D HAZARD3_ASSERTIONS --bound 0 hazard3_decode.v
-ebmc -I . -D HAZARD3_ASSERTIONS --bound 0 hazard3_frontend.v
-ebmc -I . -D HAZARD3_ASSERTIONS --bound 0 hazard3_instr_decompress.v
-ebmc -I . -D HAZARD3_ASSERTIONS --bound 0 hazard3_power_ctrl.v
+cd Hazard3
+
+# unimplemented boolbv_widtht::get_entry()
+# ebmc -I hdl -D HAZARD3_ASSERTIONS --bound 0 \
+#  --top hazard3_alu \
+#  hdl/arith/hazard3_alu.v \
+#  hdl/arith/hazard3_priority_encode.v \
+#  hdl/arith/hazard3_onehot_encode.v \
+#  hdl/arith/hazard3_onehot_priority.v \
+#  hdl/arith/hazard3_shift_barrel.v
+
+# constant fold 0 || ~|1
+# ebmc -I hdl -D HAZARD3_ASSERTIONS --systemverilog --bound 0 hdl/arith/hazard3_muldiv_seq.v
+
+ebmc -I hdl -D HAZARD3_ASSERTIONS --bound 0 hdl/arith/hazard3_shift_barrel.v
+
+# ebmc -I hdl -I test/formal/riscv-formal/tb -I test/formal/instruction_fetch_match -D HAZARD3_ASSERTIONS --bound 0 \
+#  hdl/hazard3_core.v \
+#  hdl/arith/hazard3_alu.v
+
+# failed to convert part select index
+#ebmc -I hdl -I test/formal/riscv-formal/tb -I test/formal/instruction_fetch_match -D HAZARD3_ASSERTIONS --systemverilog --bound 0 \
+#  hdl/hazard3_cpu_2port.v \
+#  hdl/hazard3_core.v \
+#  hdl/arith/hazard3_alu.v \
+#  hdl/arith/hazard3_branchcmp.v \
+#  hdl/arith/hazard3_priority_encode.v \
+#  hdl/arith/hazard3_onehot_encode.v \
+#  hdl/arith/hazard3_onehot_priority.v \
+#  hdl/arith/hazard3_onehot_priority_dynamic.v \
+#  hdl/arith/hazard3_shift_barrel.v \
+#  hdl/hazard3_csr.v \
+#  hdl/hazard3_irq_ctrl.v
+
+# failed to convert part select index
+# ebmc -I hdl -D HAZARD3_ASSERTIONS --systemverilog --bound 0 hdl/hazard3_csr.v hdl/hazard3_irq_ctrl.v hdl/arith/hazard3_onehot_encode.v hdl/arith/hazard3_onehot_priority.v hdl/arith/hazard3_onehot_priority_dynamic.v
+
+# constant folding for ~|1
+# ebmc -I hdl -D HAZARD3_ASSERTIONS --bound 0 hdl/hazard3_decode.v hdl/hazard3_instr_decompress.v
+
+# conflicting assignment types
+# ebmc -I hdl -D HAZARD3_ASSERTIONS --systemverilog --bound 0 hdl/hazard3_frontend.v
+
+# constant folding for ~|1
+# ebmc -I hdl -D HAZARD3_ASSERTIONS --bound 0 hdl/hazard3_instr_decompress.v
+
+# property fails
+# ebmc -I hdl -D HAZARD3_ASSERTIONS --bound 0 hdl/hazard3_power_ctrl.v