diff --git a/formal/data_ind_timing/Makefile b/formal/data_ind_timing/Makefile new file mode 100644 index 00000000..4037ca05 --- /dev/null +++ b/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,$@) diff --git a/formal/data_ind_timing/check_fast_div.svh b/formal/data_ind_timing/check_fast_div.svh new file mode 100644 index 00000000..9933fbc8 --- /dev/null +++ b/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; diff --git a/formal/data_ind_timing/check_fast_mulh.svh b/formal/data_ind_timing/check_fast_mulh.svh new file mode 100644 index 00000000..b196719d --- /dev/null +++ b/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; diff --git a/formal/data_ind_timing/check_fast_mull.svh b/formal/data_ind_timing/check_fast_mull.svh new file mode 100644 index 00000000..ebf29dce --- /dev/null +++ b/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; diff --git a/formal/data_ind_timing/check_fast_rem.svh b/formal/data_ind_timing/check_fast_rem.svh new file mode 100644 index 00000000..9933fbc8 --- /dev/null +++ b/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; diff --git a/formal/data_ind_timing/check_single_div.svh b/formal/data_ind_timing/check_single_div.svh new file mode 100644 index 00000000..9933fbc8 --- /dev/null +++ b/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; diff --git a/formal/data_ind_timing/check_single_mulh.svh b/formal/data_ind_timing/check_single_mulh.svh new file mode 100644 index 00000000..8feaba54 --- /dev/null +++ b/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; diff --git a/formal/data_ind_timing/check_single_mull.svh b/formal/data_ind_timing/check_single_mull.svh new file mode 100644 index 00000000..aee61437 --- /dev/null +++ b/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; diff --git a/formal/data_ind_timing/check_single_rem.svh b/formal/data_ind_timing/check_single_rem.svh new file mode 100644 index 00000000..9933fbc8 --- /dev/null +++ b/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; diff --git a/formal/data_ind_timing/check_slow_div.svh b/formal/data_ind_timing/check_slow_div.svh new file mode 100644 index 00000000..9933fbc8 --- /dev/null +++ b/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; diff --git a/formal/data_ind_timing/check_slow_mulh.svh b/formal/data_ind_timing/check_slow_mulh.svh new file mode 100644 index 00000000..bfb6e1dc --- /dev/null +++ b/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; diff --git a/formal/data_ind_timing/check_slow_mull.svh b/formal/data_ind_timing/check_slow_mull.svh new file mode 100644 index 00000000..bfb6e1dc --- /dev/null +++ b/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; diff --git a/formal/data_ind_timing/check_slow_rem.svh b/formal/data_ind_timing/check_slow_rem.svh new file mode 100644 index 00000000..9933fbc8 --- /dev/null +++ b/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; diff --git a/formal/data_ind_timing/formal_tb.sv b/formal/data_ind_timing/formal_tb.sv new file mode 100644 index 00000000..c4ae26ef --- /dev/null +++ b/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 diff --git a/formal/data_ind_timing/formal_tb_frag.svh b/formal/data_ind_timing/formal_tb_frag.svh new file mode 100644 index 00000000..301ba2e3 --- /dev/null +++ b/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 (.*); diff --git a/formal/data_ind_timing/ibex_data_ind_timing.core b/formal/data_ind_timing/ibex_data_ind_timing.core new file mode 100644 index 00000000..621dbaba --- /dev/null +++ b/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 diff --git a/formal/data_ind_timing/operation_div.svh b/formal/data_ind_timing/operation_div.svh new file mode 100644 index 00000000..7accae5f --- /dev/null +++ b/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 diff --git a/formal/data_ind_timing/operation_mulh.svh b/formal/data_ind_timing/operation_mulh.svh new file mode 100644 index 00000000..d8b65d4c --- /dev/null +++ b/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 diff --git a/formal/data_ind_timing/operation_mull.svh b/formal/data_ind_timing/operation_mull.svh new file mode 100644 index 00000000..86f78a41 --- /dev/null +++ b/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 diff --git a/formal/data_ind_timing/operation_rem.svh b/formal/data_ind_timing/operation_rem.svh new file mode 100644 index 00000000..ec9a821c --- /dev/null +++ b/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 diff --git a/formal/data_ind_timing/run.sby.j2 b/formal/data_ind_timing/run.sby.j2 new file mode 100644 index 00000000..60ed757d --- /dev/null +++ b/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}} diff --git a/ibex_multdiv.core b/ibex_multdiv.core new file mode 100644 index 00000000..2c6374a2 --- /dev/null +++ b/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 diff --git a/rtl/ibex_multdiv_fast.sv b/rtl/ibex_multdiv_fast.sv index 40b6fcbc..8baa7755 100644 --- a/rtl/ibex_multdiv_fast.sv +++ b/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 diff --git a/rtl/ibex_multdiv_slow.sv b/rtl/ibex_multdiv_slow.sv index bcd04b0f..a8d60b4e 100644 --- a/rtl/ibex_multdiv_slow.sv +++ b/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