From 1553636a7dabc38aab4841f80da8220dae7d459f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tobias=20W=C3=B6lfel?= Date: Mon, 24 Aug 2020 10:18:51 +0200 Subject: [PATCH] [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 | 37 ++++ formal/data_ind_timing/check_fast_div.svh | 5 + formal/data_ind_timing/check_fast_mulh.svh | 5 + formal/data_ind_timing/check_fast_mull.svh | 5 + formal/data_ind_timing/check_fast_rem.svh | 5 + formal/data_ind_timing/check_single_div.svh | 5 + formal/data_ind_timing/check_single_mulh.svh | 5 + formal/data_ind_timing/check_single_mull.svh | 5 + formal/data_ind_timing/check_single_rem.svh | 5 + formal/data_ind_timing/check_slow_div.svh | 5 + formal/data_ind_timing/check_slow_mulh.svh | 5 + formal/data_ind_timing/check_slow_mull.svh | 5 + formal/data_ind_timing/check_slow_rem.svh | 5 + formal/data_ind_timing/formal_tb.sv | 77 ++++++++ formal/data_ind_timing/formal_tb_frag.svh | 5 + .../data_ind_timing/ibex_data_ind_timing.core | 185 ++++++++++++++++++ formal/data_ind_timing/operation_div.svh | 21 ++ formal/data_ind_timing/operation_mulh.svh | 21 ++ formal/data_ind_timing/operation_mull.svh | 21 ++ formal/data_ind_timing/operation_rem.svh | 21 ++ formal/data_ind_timing/run.sby.j2 | 23 +++ ibex_multdiv.core | 28 +++ rtl/ibex_multdiv_fast.sv | 6 + rtl/ibex_multdiv_slow.sv | 6 + 24 files changed, 511 insertions(+) create mode 100644 formal/data_ind_timing/Makefile create mode 100644 formal/data_ind_timing/check_fast_div.svh create mode 100644 formal/data_ind_timing/check_fast_mulh.svh create mode 100644 formal/data_ind_timing/check_fast_mull.svh create mode 100644 formal/data_ind_timing/check_fast_rem.svh create mode 100644 formal/data_ind_timing/check_single_div.svh create mode 100644 formal/data_ind_timing/check_single_mulh.svh create mode 100644 formal/data_ind_timing/check_single_mull.svh create mode 100644 formal/data_ind_timing/check_single_rem.svh create mode 100644 formal/data_ind_timing/check_slow_div.svh create mode 100644 formal/data_ind_timing/check_slow_mulh.svh create mode 100644 formal/data_ind_timing/check_slow_mull.svh create mode 100644 formal/data_ind_timing/check_slow_rem.svh create mode 100644 formal/data_ind_timing/formal_tb.sv create mode 100644 formal/data_ind_timing/formal_tb_frag.svh create mode 100644 formal/data_ind_timing/ibex_data_ind_timing.core create mode 100644 formal/data_ind_timing/operation_div.svh create mode 100644 formal/data_ind_timing/operation_mulh.svh create mode 100644 formal/data_ind_timing/operation_mull.svh create mode 100644 formal/data_ind_timing/operation_rem.svh create mode 100644 formal/data_ind_timing/run.sby.j2 create mode 100644 ibex_multdiv.core 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