[formal] Add check for multdiv cycle consumption

Check that the number of cycles are always as specified for the current
configuration for data independent operations.

The required input signals for each arithmetic operation are split into
different files which are included into the testbench.
For each combination of operation and configured configuration
(slow/fast/single) a define stores the number of cycles in a separate
file. A target exists for each combination.
For a convenient execution the targets are grouped together in a
makefile.

The implementation is based on the formal/icache checks.

For the selection of the single cycle multiplication with the fast
multiplication the parameter is set directly to the enum integer value.

formal/data_ind_timing/Makefile

@@ -0,0 +1,37 @@
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
+# A simple wrapper around fusesoc to make it a bit easier to run the formal flow
+
+core-name   := lowrisc:fpv:ibex_data_ind_timing
+vlnv        := $(subst :,_,$(core-name))
+build-root  := $(abspath ../../build/$(vlnv))
+
+# Since we have a hacky hook that runs sv2v in place on fusesoc's
+# copied source files, we have to generate different build roots for
+# the two flavours (otherwise bad things will happen if you run make
+# -j2)
+mk-build-root = $(abspath ../../build/$(vlnv)/$(1))
+
+mk-fusesoc-cmd = \
+  fusesoc --cores-root=../.. \
+  run --build-root=$(call mk-build-root,$(1)) \
+  --target=$(1) \
+  $(core-name) $(fusesoc-params)
+
+.PHONY: all slow fast single
+all: slow fast single
+
+operations  := mull mulh div rem
+slow_tgts   := $(addprefix slow_, $(operations))
+fast_tgts   := $(addprefix fast_, $(operations))
+single_tgts := $(addprefix single_, $(operations))
+all_tgts    := $(slow_tgts) $(fast_tgts) $(single_tgts)
+
+slow: $(slow_tgts)
+fast: $(fast_tgts)
+single: $(single_tgts)
+
+$(all_tgts):
+	$(call mk-fusesoc-cmd,$@)

formal/data_ind_timing/check_fast_div.svh

@@ -0,0 +1,5 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+localparam int unsigned DATA_IND_OP_COUNT = 'd37;

formal/data_ind_timing/check_fast_mulh.svh

@@ -0,0 +1,5 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+localparam int unsigned DATA_IND_OP_COUNT = 'd4;

formal/data_ind_timing/check_fast_mull.svh

@@ -0,0 +1,5 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+localparam int unsigned DATA_IND_OP_COUNT = 'd3;

formal/data_ind_timing/check_fast_rem.svh

@@ -0,0 +1,5 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+localparam int unsigned DATA_IND_OP_COUNT = 'd37;

formal/data_ind_timing/check_single_div.svh

@@ -0,0 +1,5 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+localparam int unsigned DATA_IND_OP_COUNT = 'd37;

formal/data_ind_timing/check_single_mulh.svh

@@ -0,0 +1,5 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+localparam int unsigned DATA_IND_OP_COUNT = 'd2;

formal/data_ind_timing/check_single_mull.svh

@@ -0,0 +1,5 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+localparam int unsigned DATA_IND_OP_COUNT = 'd1;

formal/data_ind_timing/check_single_rem.svh

@@ -0,0 +1,5 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+localparam int unsigned DATA_IND_OP_COUNT = 'd37;

formal/data_ind_timing/check_slow_div.svh

@@ -0,0 +1,5 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+localparam int unsigned DATA_IND_OP_COUNT = 'd37;

formal/data_ind_timing/check_slow_mulh.svh

@@ -0,0 +1,5 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+localparam int unsigned DATA_IND_OP_COUNT = 'd33;

formal/data_ind_timing/check_slow_mull.svh

@@ -0,0 +1,5 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+localparam int unsigned DATA_IND_OP_COUNT = 'd33;

formal/data_ind_timing/check_slow_rem.svh

@@ -0,0 +1,5 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+localparam int unsigned DATA_IND_OP_COUNT = 'd37;

formal/data_ind_timing/formal_tb.sv

@@ -0,0 +1,77 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+// A formal testbench for the ICache. This gets bound into the actual ICache DUT.
+
+`include "prim_assert.sv"
+
+module formal_tb (
+   // Top-level ports
+    input  logic             clk_i,
+    input  logic             rst_ni,
+    input  logic             mult_en_i,  // dynamic enable signal, for FSM control
+    input  logic             div_en_i,   // dynamic enable signal, for FSM control
+    input  logic             mult_sel_i, // static decoder input, for data muxes
+    input  logic             div_sel_i,  // static decoder input, for data muxes
+    input  ibex_pkg::md_op_e operator_i,
+    input  logic       [1:0] signed_mode_i,
+    input  logic      [31:0] op_a_i,
+    input  logic      [31:0] op_b_i,
+    input  logic      [33:0] alu_adder_ext_i,
+    input  logic      [31:0] alu_adder_i,
+    input  logic             equal_to_zero_i,
+    input  logic             data_ind_timing_i,
+
+    input logic      [32:0]  alu_operand_a_o,
+    input logic      [32:0]  alu_operand_b_o,
+
+    input logic      [33:0]  imd_val_q_i[1:0],
+    input logic      [33:0]  imd_val_d_o[1:0],
+    input logic       [1:0]  imd_val_we_o,
+
+    input  logic             multdiv_ready_id_i,
+
+    input logic      [31:0]  multdiv_result_o,
+
+    input logic              valid_o
+);
+
+  import ibex_pkg::*;
+
+  logic [2:0] f_startup_count = 3'd0;
+  always_ff @(posedge clk_i) begin : reset_assertion
+    f_startup_count <= f_startup_count + ((f_startup_count == 3'd5) ? 3'd0 : 3'd1);
+    // Assume that rst_ni is low for the first cycle and not true after that.
+    assume (~((f_startup_count == 3'd0) ^ ~rst_ni));
+  end
+
+  `include "multdiv_operation.svh"
+  // Defines with DATA_IND_OP_COUNT the number of cycles the current check must have.
+  `include "multdiv_check.svh"
+
+  logic [5:0] f_operation_count = 6'd0;
+
+  logic checked = 1'b0;
+
+  always_ff @(posedge clk_i) begin : count_assertion
+    if (f_startup_count >= 3'd1) begin
+      f_operation_count <= f_operation_count + 1;
+    end
+  end
+
+  always_ff @(posedge clk_i) begin : check
+    if (!checked && (valid_o || (f_operation_count == DATA_IND_OP_COUNT))) begin
+      checked <= 1'b1;
+      assert (valid_o && (f_operation_count == DATA_IND_OP_COUNT));
+      assume (multdiv_ready_id_i);
+    end
+  end
+
+  always_comb begin
+    if (f_operation_count > DATA_IND_OP_COUNT) begin
+      assert (checked);
+    end
+  end
+
+endmodule

formal/data_ind_timing/formal_tb_frag.svh

@@ -0,0 +1,5 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+formal_tb tb_i (.*);

formal/data_ind_timing/ibex_data_ind_timing.core

@@ -0,0 +1,185 @@
+CAPI=2:
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
+name: "lowrisc:fpv:ibex_data_ind_timing:0.1"
+description: "Formal test for data independent timing"
+
+filesets:
+  testbench:
+    depend:
+      - lowrisc:ibex:ibex_pkg
+      - lowrisc:ibex:ibex_multdiv
+      - lowrisc:util:sv2v
+    files:
+      - run.sby.j2 : {file_type: sbyConfigTemplate}
+      - formal_tb_frag.svh : {file_type: systemVerilogSource, is_include_file: true}
+      - formal_tb.sv : {file_type: systemVerilogSource}
+  op_mull:
+    files:
+      - operation_mull.svh : {file_type: systemVerilogSource, copyto: multdiv_operation.svh, is_include_file: true}
+  op_mulh:
+    files:
+      - operation_mulh.svh : {file_type: systemVerilogSource, copyto: multdiv_operation.svh, is_include_file: true}
+  op_div:
+    files:
+      - operation_div.svh : {file_type: systemVerilogSource, copyto: multdiv_operation.svh, is_include_file: true}
+  op_rem:
+    files:
+      - operation_rem.svh : {file_type: systemVerilogSource, copyto: multdiv_operation.svh, is_include_file: true}
+  slow_mull:
+    files:
+      - check_slow_mull.svh : {file_type: systemVerilogSource, copyto: multdiv_check.svh, is_include_file: true}
+  slow_mulh:
+    files:
+      - check_slow_mulh.svh : {file_type: systemVerilogSource, copyto: multdiv_check.svh, is_include_file: true}
+  slow_div:
+    files:
+      - check_slow_div.svh : {file_type: systemVerilogSource, copyto: multdiv_check.svh, is_include_file: true}
+  slow_rem:
+    files:
+      - check_slow_rem.svh : {file_type: systemVerilogSource, copyto: multdiv_check.svh, is_include_file: true}
+  fast_mull:
+    files:
+      - check_fast_mull.svh : {file_type: systemVerilogSource, copyto: multdiv_check.svh, is_include_file: true}
+  fast_mulh:
+    files:
+      - check_fast_mulh.svh : {file_type: systemVerilogSource, copyto: multdiv_check.svh, is_include_file: true}
+  fast_div:
+    files:
+      - check_fast_div.svh : {file_type: systemVerilogSource, copyto: multdiv_check.svh, is_include_file: true}
+  fast_rem:
+    files:
+      - check_fast_rem.svh : {file_type: systemVerilogSource, copyto: multdiv_check.svh, is_include_file: true}
+  single_mull:
+    files:
+      - check_single_mull.svh : {file_type: systemVerilogSource, copyto: multdiv_check.svh, is_include_file: true}
+  single_mulh:
+    files:
+      - check_single_mulh.svh : {file_type: systemVerilogSource, copyto: multdiv_check.svh, is_include_file: true}
+  single_div:
+    files:
+      - check_single_div.svh : {file_type: systemVerilogSource, copyto: multdiv_check.svh, is_include_file: true}
+  single_rem:
+    files:
+      - check_single_rem.svh : {file_type: systemVerilogSource, copyto: multdiv_check.svh, is_include_file: true}
+
+parameters:
+  RV32M:
+    datatype: int
+    default: 2
+    paramtype: vlogparam
+    description: "Selection of multiplication implementation. Switch to enable single cycle multiplications."
+
+targets:
+  slow: &slow
+    filesets:
+      - testbench
+    toplevel: ibex_multdiv_slow
+    default_tool: symbiyosys
+    tools:
+      symbiyosys:
+        tasknames:
+        - slow
+  slow_mull:
+    <<: *slow
+    filesets:
+      - testbench
+      - op_mull
+      - slow_mull
+
+  slow_mulh:
+    <<: *slow
+    filesets:
+      - testbench
+      - op_mulh
+      - slow_mulh
+
+  slow_div:
+    <<: *slow
+    filesets:
+      - testbench
+      - op_div
+      - slow_div
+
+  slow_rem:
+    <<: *slow
+    filesets:
+      - testbench
+      - op_rem
+      - slow_rem
+
+
+  fast: &fast
+    <<: *slow
+    toplevel: ibex_multdiv_fast
+    tools:
+      symbiyosys:
+        tasknames:
+        - fast
+
+  fast_mull:
+    <<: *fast
+    filesets:
+      - testbench
+      - op_mull
+      - fast_mull
+
+  fast_mulh:
+    <<: *fast
+    filesets:
+      - testbench
+      - op_mulh
+      - fast_mulh
+
+  fast_div:
+    <<: *fast
+    filesets:
+      - testbench
+      - op_div
+      - fast_div
+
+  fast_rem:
+    <<: *fast
+    filesets:
+      - testbench
+      - op_rem
+      - fast_rem
+
+  single: &single
+    <<: *fast
+    parameters:
+      - RV32M=3
+    tools:
+      symbiyosys:
+        tasknames:
+        - single
+
+  single_mull:
+    <<: *single
+    filesets:
+      - testbench
+      - op_mull
+      - single_mull
+
+  single_mulh:
+    <<: *single
+    filesets:
+      - testbench
+      - op_mulh
+      - single_mulh
+
+  single_div:
+    <<: *single
+    filesets:
+      - testbench
+      - op_div
+      - single_div
+
+  single_rem:
+    <<: *single
+    filesets:
+      - testbench
+      - op_rem
+      - single_rem

formal/data_ind_timing/operation_div.svh

@@ -0,0 +1,21 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+always_comb begin
+  // Formal prove only for data independent timing
+  assume (data_ind_timing_i);
+
+  assume(~mult_sel_i);
+  assume(~mult_en_i);
+
+  if (f_startup_count >= 3'd2) begin
+    // Enable signal must be asserted in order for the state machine to advance
+    assume (div_en_i);
+    assume (div_sel_i);
+    assume (operator_i == ibex_pkg::MD_OP_DIV);
+  end else begin
+    assume (~div_en_i);
+    assume (~div_sel_i);
+  end
+end

formal/data_ind_timing/operation_mulh.svh

@@ -0,0 +1,21 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+always_comb begin
+  // Formal prove only for data independent timing
+  assume (data_ind_timing_i);
+
+  assume(~div_sel_i);
+  assume(~div_en_i);
+
+  if (f_startup_count >= 3'd2) begin
+    // Enable signal must be asserted in order for the state machine to advance
+    assume (mult_en_i);
+    assume (mult_sel_i);
+    assume (operator_i == ibex_pkg::MD_OP_MULH);
+  end else begin
+    assume (~mult_en_i);
+    assume (~mult_sel_i);
+  end
+end

formal/data_ind_timing/operation_mull.svh

@@ -0,0 +1,21 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+always_comb begin
+  // Formal prove only for data independent timing
+  assume (data_ind_timing_i);
+
+  assume(~div_sel_i);
+  assume(~div_en_i);
+
+  if (f_startup_count >= 3'd2) begin
+    // Enable signal must be asserted in order for the state machine to advance
+    assume (mult_en_i);
+    assume (mult_sel_i);
+    assume (operator_i == ibex_pkg::MD_OP_MULL);
+  end else begin
+    assume (~mult_en_i);
+    assume (~mult_sel_i);
+  end
+end

formal/data_ind_timing/operation_rem.svh

@@ -0,0 +1,21 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+always_comb begin
+  // Formal prove only for data independent timing
+  assume (data_ind_timing_i);
+
+  assume(~mult_sel_i);
+  assume(~mult_en_i);
+
+  if (f_startup_count >= 3'd2) begin
+    // Enable signal must be asserted in order for the state machine to advance
+    assume (div_en_i);
+    assume (div_sel_i);
+    assume (operator_i == ibex_pkg::MD_OP_REM);
+  end else begin
+    assume (~div_en_i);
+    assume (~div_sel_i);
+  end
+end

formal/data_ind_timing/run.sby.j2

@@ -0,0 +1,23 @@
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
+[tasks]
+slow sl
+fast fs
+single si
+
+[options]
+mode bmc
+depth 50
+
+[engines]
+smtbmc boolector
+
+[script]
+{{"-sv"|gen_reads}}
+
+prep -top {{top_level}}
+
+[files]
+{{files}}

ibex_multdiv.core

@@ -0,0 +1,28 @@
+CAPI=2:
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+name: "lowrisc:ibex:ibex_multdiv:0.1"
+description: "Multiplier and divider"
+
+filesets:
+  files_rtl:
+    depend:
+      - lowrisc:prim:assert
+      - lowrisc:ibex:ibex_pkg
+    files:
+      - rtl/ibex_multdiv_fast.sv
+      - rtl/ibex_multdiv_slow.sv
+    file_type: systemVerilogSource
+
+parameters:
+  RV32M:
+    datatype: int
+    default: 2
+    paramtype: vlogparam
+    description: "Selection of multiplication implementation. Switch to enable single cycle multiplications."
+
+targets:
+  default: &default_target
+    filesets:
+      - files_rtl

rtl/ibex_multdiv_fast.sv

@@ -513,4 +513,10 @@ module ibex_multdiv_fast #(
   `ASSERT(IbexMultDivStateValid, md_state_q inside {
       MD_IDLE, MD_ABS_A, MD_ABS_B, MD_COMP, MD_LAST, MD_CHANGE_SIGN, MD_FINISH})
 
+`ifdef FORMAL
+  `ifdef YOSYS
+    `include "formal_tb_frag.svh"
+  `endif
+`endif
+
 endmodule // ibex_mult

rtl/ibex_multdiv_slow.sv

@@ -365,4 +365,10 @@ module ibex_multdiv_slow
       MD_IDLE, MD_ABS_A, MD_ABS_B, MD_COMP, MD_LAST, MD_CHANGE_SIGN, MD_FINISH
       }, clk_i, !rst_ni)
 
+`ifdef FORMAL
+  `ifdef YOSYS
+    `include "formal_tb_frag.svh"
+  `endif
+`endif
+
 endmodule