Verification for pfpu32_muldiv: MULT (and some DIV)

This adds formal verification for the multiplication outputs in
pfpu32_muldiv, and some division outputs too.

To achieve this, I assumed (but not yet verified) that the muldiv module
will not receive further requests for the 12 cycles following a division
request, since the module will be busy with the Goldschmidt algorithm.

To make verification of the multiplication output tractable, I've split
it into two pieces. The `pfpu_muldiv_check` target in the Makefile
checks a series of assertions that together imply an assumption in the
`pfpu_muldiv` target. Unfortunately, making the first set of assertions
isn't enough to guide the solver towards proving the assumption within a
reasonable amount of time.

Author: liujed

bench/formal/Makefile

@@ -29,6 +29,7 @@ TESTS := mor1kx_cache_lru \
 	mor1kx_bus_if_wb32 \
 	pfpu32_addsub \
 	pfpu32_cmp \
+	pfpu32_muldiv_check \
 	pfpu32_muldiv
 
 # tests that no longer work keep them here so we can easily

bench/formal/pfpu32_muldiv_check.sby

@@ -0,0 +1,19 @@
+[options]
+mode prove
+depth 20
+
+[engines]
+smtbmc yices
+
+[script]
+read -formal f_multiclock_pfpu32_op.v
+read -formal -D PFPU32_MULDIV -D PFPU32_CHECK_MUL_ASSUMPTIONS pfpu32_muldiv.v
+
+
+prep -top pfpu32_muldiv
+
+[files]
+f_multiclock_pfpu32_op.v
+../../rtl/verilog/pfpu32/pfpu32_muldiv.v
+../../rtl/verilog/mor1kx-defines.v
+../../rtl/verilog/mor1kx-sprs.v