data/full_repos/permissive/500345502/verilog/rtl/wrapped_wavelet_transform/properties/src/fir.v
data/verilator_xmls/921458a7-6ecb-4f59-abb8-c7c4849d6a51.xml
module fir #(
    parameter BITS_PER_ELEM = 8,
    parameter SUM_TRUNCATION = 8,
    parameter NUM_ELEM = 7,
    parameter FILTER_VAL = 0,
    parameter MAX_BITS = $clog2({BITS_PER_ELEM{1'b1}}*{BITS_PER_ELEM{1'b1}}*NUM_ELEM)
) (

    input wire clk,


    input wire rst,


    input wire i_start_calc,


    input wire [NUM_ELEM * BITS_PER_ELEM - 1:0] taps,


    output wire signed [SUM_TRUNCATION - 1:0] o_wavelet

);

  reg [NUM_ELEM * BITS_PER_ELEM - 1:0] filter;
  reg signed [MAX_BITS - 1:0] sum;
  reg signed [MAX_BITS - 1:0] working_sum;

  initial begin


    filter = FILTER_VAL;
    sum = 0;
    working_sum = 0;
  end

  assign o_wavelet = sum[(MAX_BITS - 1): (MAX_BITS) - SUM_TRUNCATION];


  reg [$clog2(NUM_ELEM) + 1:0] i;








  always @(posedge clk) begin
    if (rst) begin

      filter <= FILTER_VAL;
      sum <= 0;
      working_sum <= 0;
    end else begin
      working_sum = 0;
      if (i_start_calc) begin
        for (i = 0; i < NUM_ELEM; i = i + 1) begin
          working_sum = working_sum + $signed(filter[BITS_PER_ELEM*i+:BITS_PER_ELEM]) * $signed(taps[BITS_PER_ELEM*i+:BITS_PER_ELEM]);
        end
        sum <= working_sum;
      end
      else begin
        sum <= sum;
      end
    end
  end

  `ifdef FORMAL
    reg f_past_valid = 0;
    reg signed [31:0] overflow_test_sum = 0;
    reg signed [MAX_BITS - 1:0] truncated_overflow_test_sum = 0;

    initial assume(rst);

    always @(posedge clk) begin
      f_past_valid <= 1;
      if(f_past_valid) begin
        if (rst) begin
          overflow_test_sum <= 0;
          truncated_overflow_test_sum <= 0;
        end else begin
          if (i_start_calc) begin
            overflow_test_sum = 0;
            for (i = 0; i < NUM_ELEM; i = i + 1) begin
              overflow_test_sum = overflow_test_sum + $signed(filter[BITS_PER_ELEM*i+:BITS_PER_ELEM]) * $signed(taps[BITS_PER_ELEM*i+:BITS_PER_ELEM]);
            end
            truncated_overflow_test_sum <= overflow_test_sum[MAX_BITS - 1: 0];
          end
        end

        if(f_past_valid) begin
          if ($signed(overflow_test_sum) > 0) begin
            _overflow_test_pos: assert($signed(overflow_test_sum) <= {{(32 - MAX_BITS + 1){1'b0}},{(MAX_BITS - 1){1'b1}}});
          end
          if ($signed(overflow_test_sum) < 0) begin
            _overflow_test_neg: assert($signed(overflow_test_sum) >= {{(32 - MAX_BITS + 1){1'b1}},{(MAX_BITS - 1){1'b0}}});
          end
        end
      end
    end

  `endif
endmodule
module fir #(
    parameter BITS_PER_ELEM = 8,
    parameter SUM_TRUNCATION = 8,
    parameter NUM_ELEM = 7,
    parameter FILTER_VAL = 0,
    parameter MAX_BITS = $clog2({BITS_PER_ELEM{1'b1}}*{BITS_PER_ELEM{1'b1}}*NUM_ELEM)
) (

    input wire clk,


    input wire rst,


    input wire i_start_calc,


    input wire [NUM_ELEM * BITS_PER_ELEM - 1:0] taps,


    output wire signed [SUM_TRUNCATION - 1:0] o_wavelet

);


  reg [NUM_ELEM * BITS_PER_ELEM - 1:0] filter;
  reg signed [MAX_BITS - 1:0] sum;
  reg signed [MAX_BITS - 1:0] working_sum;

  initial begin


    filter = FILTER_VAL;
    sum = 0;
    working_sum = 0;
  end

  assign o_wavelet = sum[(MAX_BITS - 1): (MAX_BITS) - SUM_TRUNCATION];


  reg [$clog2(NUM_ELEM) + 1:0] i;








  always @(posedge clk) begin
    if (rst) begin

      filter <= FILTER_VAL;
      sum <= 0;
      working_sum <= 0;
    end else begin
      working_sum = 0;
      if (i_start_calc) begin
        for (i = 0; i < NUM_ELEM; i = i + 1) begin
          working_sum = working_sum + $signed(filter[BITS_PER_ELEM*i+:BITS_PER_ELEM]) * $signed(taps[BITS_PER_ELEM*i+:BITS_PER_ELEM]);
        end
        sum <= working_sum;
      end
      else begin
        sum <= sum;
      end
    end
  end

  `ifdef FORMAL
    reg f_past_valid = 0;
    reg signed [31:0] overflow_test_sum = 0;
    reg signed [MAX_BITS - 1:0] truncated_overflow_test_sum = 0;

    initial assume(rst);

    always @(posedge clk) begin
      f_past_valid <= 1;
      if(f_past_valid) begin
        if (rst) begin
          overflow_test_sum <= 0;
          truncated_overflow_test_sum <= 0;
        end else begin
          if (i_start_calc) begin
            overflow_test_sum = 0;
            for (i = 0; i < NUM_ELEM; i = i + 1) begin
              overflow_test_sum = overflow_test_sum + $signed(filter[BITS_PER_ELEM*i+:BITS_PER_ELEM]) * $signed(taps[BITS_PER_ELEM*i+:BITS_PER_ELEM]);
            end
            truncated_overflow_test_sum <= overflow_test_sum[MAX_BITS - 1: 0];
          end
        end

        if(f_past_valid) begin
          if ($signed(overflow_test_sum) > 0) begin
            _overflow_test_pos: assert($signed(overflow_test_sum) <= {{(32 - MAX_BITS + 1){1'b0}},{(MAX_BITS - 1){1'b1}}});
          end
          if ($signed(overflow_test_sum) < 0) begin
            _overflow_test_neg: assert($signed(overflow_test_sum) >= {{(32 - MAX_BITS + 1){1'b1}},{(MAX_BITS - 1){1'b0}}});
          end
        end
      end
    end

  `endif
endmodule