Merge pull request #166 from liujed/verify-pfpu32_mul

Formal verification for pfpu32_muldiv: MULT (and some DIV)

Author: stffrdhrn

bench/formal/Makefile

@@ -28,7 +28,9 @@ TESTS := mor1kx_cache_lru \
 	mor1kx_rf_cappuccino \
 	mor1kx_bus_if_wb32 \
 	pfpu32_addsub \
-	pfpu32_cmp
+	pfpu32_cmp \
+	pfpu32_muldiv_check \
+	pfpu32_muldiv
 
 # tests that no longer work keep them here so we can easily
 # run them if we want to try and fix them.

bench/formal/f_multiclock_pfpu32_addsub.v renamed to bench/formal/f_multiclock_pfpu32_op.v

@@ -1,21 +1,21 @@
 /* ****************************************************************************
   SPDX-License-Identifier: CERN-OHL-W-2.0
 
-  Description: mor1kx formal multiclock pfpu32 addsub checker
+  Description: mor1kx formal multiclock pfpu32 operation checker
 
-  Checks that an pfpu32 addsub operation finishes within a number of clock
-  cycles. The completion of the operation is signaled by asserting add_rdy_i.
+  Checks that an pfpu32 operation finishes within a number of clock cycles.
+  The completion of the operation is signaled by asserting result_rdy_i.
 
 ***************************************************************************** */
 
-module f_multiclock_pfpu32_addsub
+module f_multiclock_pfpu32_op
 #(
   parameter OP_MAX_CLOCKS = 3
 ) (
   input clk,
   input flush_i,
   input adv_i,
-  input add_rdy_i,
+  input result_rdy_i,
   input start_i,
   input f_initialized,
 );
@@ -25,18 +25,18 @@ module f_multiclock_pfpu32_addsub
   initial f_op_count = 0;
   initial f_op = 0;
 
-  // Valid addsub output is seen after three clocks.
+  // Valid output is seen after OP_MAX_CLOCKS cycles.
   always @(posedge clk) begin
     if (f_initialized) begin
       if (flush_i)
         // The pipeline is being flushed. The results of any operations in
         // flight will not be reported. Stop counting.
         f_op <= 0;
-      else if ($rose(adv_i & start_i)) begin
+      else if (adv_i & start_i) begin
         // A new operation is starting. Start/reset the counter.
         f_op <= 1;
         f_op_count <= 1;
-      end else if (add_rdy_i)
+      end else if (result_rdy_i)
         // Result is ready. Stop counting.
         f_op <= 0;
       else if (f_op) begin

bench/formal/pfpu32_addsub.sby

@@ -6,14 +6,14 @@ depth 10
 smtbmc yices
 
 [script]
-read -formal f_multiclock_pfpu32_addsub.v
+read -formal f_multiclock_pfpu32_op.v
 read -formal -D PFPU32_ADDSUB pfpu32_addsub.v
 
 
 prep -top pfpu32_addsub
 
 [files]
-f_multiclock_pfpu32_addsub.v
+f_multiclock_pfpu32_op.v
 ../../rtl/verilog/pfpu32/pfpu32_addsub.v
 ../../rtl/verilog/mor1kx-defines.v
 ../../rtl/verilog/mor1kx-sprs.v

bench/formal/pfpu32_muldiv.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 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

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

rtl/verilog/pfpu32/pfpu32_addsub.v

@@ -573,14 +573,14 @@ module pfpu32_addsub
   // Verify that a result is produced after three clocks.
   generate
   begin : f_addsub_multiclock
-    f_multiclock_pfpu32_addsub #(
+    f_multiclock_pfpu32_op #(
       .OP_MAX_CLOCKS(3),
     ) u_f_multiclock (
       .clk(clk),
       .flush_i(flush_i),
       .adv_i(adv_i),
       .start_i(start_i),
-      .add_rdy_i(add_rdy_o),
+      .result_rdy_i(add_rdy_o),
       .f_initialized(f_initialized),
     );
   end