data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv
1: b'%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:7: Cannot find include file: prim_assert.sv\n`include "prim_assert.sv" \n         ^~~~~~~~~~~~~~~~\n        ... Looked in:\n             data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing,data/full_repos/permissive/509468557/prim_assert.sv\n             data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing,data/full_repos/permissive/509468557/prim_assert.sv.v\n             data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing,data/full_repos/permissive/509468557/prim_assert.sv.sv\n             prim_assert.sv\n             prim_assert.sv.v\n             prim_assert.sv.sv\n             obj_dir/prim_assert.sv\n             obj_dir/prim_assert.sv.v\n             obj_dir/prim_assert.sv.sv\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:49: Cannot find include file: multdiv_operation.svh\n  `include "multdiv_operation.svh" \n           ^~~~~~~~~~~~~~~~~~~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:51: Cannot find include file: multdiv_check.svh\n  `include "multdiv_check.svh" \n           ^~~~~~~~~~~~~~~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:17: syntax error, unexpected ::, expecting \')\' or \',\'\n    input  ibex_pkg::md_op_e operator_i,\n                   ^~\n                                                                                                                                : ... Perhaps \'ibex_pkg\' is a package which needs to be predeclared? (IEEE 1800-2017 26.3)\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:19: syntax error, unexpected input, expecting IDENTIFIER or \'=\' or do or final\n    input  logic      [31:0] op_a_i,\n    ^~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:20: syntax error, unexpected input, expecting IDENTIFIER or \'=\' or do or final\n    input  logic      [31:0] op_b_i,\n    ^~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:21: syntax error, unexpected input, expecting IDENTIFIER or \'=\' or do or final\n    input  logic      [33:0] alu_adder_ext_i,\n    ^~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:22: syntax error, unexpected input, expecting IDENTIFIER or \'=\' or do or final\n    input  logic      [31:0] alu_adder_i,\n    ^~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:23: syntax error, unexpected input, expecting IDENTIFIER or \'=\' or do or final\n    input  logic             equal_to_zero_i,\n    ^~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:24: syntax error, unexpected input, expecting IDENTIFIER or \'=\' or do or final\n    input  logic             data_ind_timing_i,\n    ^~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:26: syntax error, unexpected input, expecting IDENTIFIER or \'=\' or do or final\n    input logic      [32:0]  alu_operand_a_o,\n    ^~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:27: syntax error, unexpected input, expecting IDENTIFIER or \'=\' or do or final\n    input logic      [32:0]  alu_operand_b_o,\n    ^~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:29: syntax error, unexpected input, expecting IDENTIFIER or \'=\' or do or final\n    input logic      [33:0]  imd_val_q_i[1:0],\n    ^~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:30: syntax error, unexpected input, expecting IDENTIFIER or \'=\' or do or final\n    input logic      [33:0]  imd_val_d_o[1:0],\n    ^~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:31: syntax error, unexpected input, expecting IDENTIFIER or \'=\' or do or final\n    input logic       [1:0]  imd_val_we_o,\n    ^~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:33: syntax error, unexpected input, expecting IDENTIFIER or \'=\' or do or final\n    input  logic             multdiv_ready_id_i,\n    ^~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:35: syntax error, unexpected input, expecting IDENTIFIER or \'=\' or do or final\n    input logic      [31:0]  multdiv_result_o,\n    ^~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:37: syntax error, unexpected input, expecting IDENTIFIER or \'=\' or do or final\n    input logic              valid_o\n    ^~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:43: syntax error, unexpected always_ff\n  always_ff @(posedge clk_i) begin : reset_assertion\n  ^~~~~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/formal/data_ind_timing/formal_tb.sv:57: syntax error, unexpected always_ff\n  always_ff @(posedge clk_i) begin : count_assertion\n  ^~~~~~~~~\n%Error: Exiting due to 20 error(s)\n'
module formal_tb (

    input  logic             clk_i,
    input  logic             rst_ni,
    input  logic             mult_en_i,
    input  logic             div_en_i,
    input  logic             mult_sel_i,
    input  logic             div_sel_i,
    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 (~((f_startup_count == 3'd0) ^ ~rst_ni));
  end

  `include "multdiv_operation.svh"

  `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
module formal_tb (

    input  logic             clk_i,
    input  logic             rst_ni,
    input  logic             mult_en_i,
    input  logic             div_en_i,
    input  logic             mult_sel_i,
    input  logic             div_sel_i,
    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 (~((f_startup_count == 3'd0) ^ ~rst_ni));
  end

  `include "multdiv_operation.svh"

  `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