data/full_repos/permissive/499787978/projects/arty_s7_atrover/rtl/boxcar.v
data/verilator_xmls/46ba7bf7-7eee-40ed-ab6f-b1f56b442754.xml
module  boxcar #(

    parameter  IW=16,
    parameter  LGMEM=6,
    parameter  OW=(IW+LGMEM),
    parameter [0:0]  FIXED_NAVG=1'b0,



    parameter  [(LGMEM-1):0]  INITIAL_NAVG= -1

    ) (


        input  wire      i_clk,
        input  wire      i_reset,
        input  wire  [(LGMEM-1):0]  i_navg,

        input  wire      i_ce,
        input  wire  [(IW-1):0]  i_sample,
        output  reg  [(OW-1):0]  o_result

  );
  
  localparam [0:0] OPT_SIGNED=1'b1;


  reg      full;
  reg  [(LGMEM-1):0]  rdaddr, wraddr;
  reg  [(IW-1):0]  mem [0:((1<<LGMEM)-1)];
  reg  [(IW-1):0]  preval, memval;
  reg  [IW:0]  sub;
  reg  [(IW+LGMEM-1):0] acc;

  wire  [(LGMEM-1):0]  w_requested_navg;
  wire  [(IW+LGMEM-1):0]  rounded;






  initial  wraddr = 0;
  always @(posedge i_clk)
  if (i_reset)
    wraddr <= 0;
  else if (i_ce)
    wraddr <= wraddr + 1'b1;








  assign w_requested_navg = (FIXED_NAVG) ? INITIAL_NAVG : i_navg;













  initial  rdaddr = -INITIAL_NAVG;
  always @(posedge i_clk)
  if (i_reset)
    rdaddr <= -w_requested_navg;
  else if (i_ce)

    rdaddr <= rdaddr + 1'b1;













  initial  preval = 0;
  always @(posedge i_clk)
  if (i_reset)
    preval <= 0;
  else if (i_ce)
    preval <= i_sample;




  always @(posedge i_clk)
  if (i_ce)
    mem[wraddr] <= i_sample;




  initial  memval = 0;
  always @(posedge i_clk)
  if (i_ce)
    memval <= mem[rdaddr];





  initial  full   = 1'b0;
  always @(posedge i_clk)
  if (i_reset)
    full <= 0;
  else if (i_ce)
    full <= (full)||(rdaddr==0);

















  initial  sub = 0;
  always @(posedge i_clk)
  if (i_reset)
    sub <= 0;
  else if (i_ce)
  begin
    if (full)
      sub <= { OPT_SIGNED&preval[(IW-1)], preval }
          - { OPT_SIGNED&memval[(IW-1)], memval };
    else
      sub <= { OPT_SIGNED&preval[(IW-1)], preval };
  end

















  initial  acc = 0;
  always @(posedge i_clk)
  if (i_reset)
    acc <= 0;
  else if (i_ce)
    acc <= acc + { {(LGMEM-1){OPT_SIGNED&sub[IW]}}, sub };















  generate




  if (IW+LGMEM == OW)

    assign  rounded = acc;
  else if (IW+LGMEM == OW + 1)

    assign  rounded = acc + { {(OW){1'b0}}, acc[1] };
  else

    assign  rounded = acc + {
        {(OW){1'b0}},
        acc[(IW+LGMEM-OW)],
        {(IW+LGMEM-OW-1){!acc[(IW+LGMEM-OW)]}}
        };
  endgenerate









  initial  o_result = 0;
  always @(posedge i_clk)
  if (i_reset)
    o_result <= 0;
  else if (i_ce)
    o_result <= rounded[(IW+LGMEM-1):(IW+LGMEM-OW)];











`ifdef  FORMAL


  reg      f_past_valid;
  wire  [LGMEM-1:0]  f_rdaddr;
  reg  [LGMEM+IW-1:0]  f_sum;
  wire  [LGMEM-1:0]  f_full_addr;
  reg  [3:0]    f_test;
  reg  [(LGMEM-1):0]  f_navg;
  integer      k;

  initial  f_past_valid = 1'b0;
  always @(posedge i_clk)
    f_past_valid <= 1'b1;

  always @(*)
  if ((!FIXED_NAVG)&&(!f_past_valid))
    assume(i_reset);


  always @(posedge i_clk)
  if ((f_past_valid)&&(!$past(i_ce)))
    assume(i_ce);

  always @(*)
  if ((!FIXED_NAVG)&&(i_reset))
    assume(i_navg > 3);

  always @(posedge i_clk)
  if ((f_test[3])&&(f_navg < (1<<LGMEM)-3))
    assert(f_sum == acc);

  always @(*)
    assert(f_navg > 3);

  always @(posedge i_clk)
    cover($rose(full));

  initial  f_navg = INITIAL_NAVG;
  always @(posedge i_clk)
  if (FIXED_NAVG)
    f_navg <= INITIAL_NAVG;
  else if (i_reset)
    f_navg <= i_navg;


  assign  f_rdaddr = wraddr - f_navg;
  always @(posedge i_clk)
  if (!i_reset)
    assert(f_rdaddr == rdaddr);

  always @(*)
  begin
    f_sum = 0;
    for(k=0; k<(1<<LGMEM); k=k+1)
    begin
      if (((full)&&(k<f_navg)) || ((!full)&&(wraddr>=3)&&(k < wraddr-2)))
        f_sum = f_sum
        + {{(LGMEM){OPT_SIGNED&mem[wraddr-k-3][IW-1]}},
            mem[wraddr-k-3] };
    end
  end

  assign  f_full_addr = - f_navg;

  always @(*)
  if ((rdaddr < f_full_addr)&&(rdaddr != 0))
    assert(full);

  initial  f_test = 0;
  always @(posedge i_clk)
  if (i_reset)
    f_test <= 0;
  else if ((full)&&(i_ce))
    f_test <= { f_test[2:0], 1'b1 };

  always @(posedge i_clk)
  if ((f_test[3])&&(f_navg < (1<<LGMEM)-4))
  begin
    assert(f_sum == acc);
  end else if ((wraddr > 1)&&(!full))
    assert(f_sum == acc);
`endif

endmodule
module  boxcar #(

    parameter  IW=16,
    parameter  LGMEM=6,
    parameter  OW=(IW+LGMEM),
    parameter [0:0]  FIXED_NAVG=1'b0,



    parameter  [(LGMEM-1):0]  INITIAL_NAVG= -1

    ) (


        input  wire      i_clk,
        input  wire      i_reset,
        input  wire  [(LGMEM-1):0]  i_navg,

        input  wire      i_ce,
        input  wire  [(IW-1):0]  i_sample,
        output  reg  [(OW-1):0]  o_result

  );

  
  localparam [0:0] OPT_SIGNED=1'b1;


  reg      full;
  reg  [(LGMEM-1):0]  rdaddr, wraddr;
  reg  [(IW-1):0]  mem [0:((1<<LGMEM)-1)];
  reg  [(IW-1):0]  preval, memval;
  reg  [IW:0]  sub;
  reg  [(IW+LGMEM-1):0] acc;

  wire  [(LGMEM-1):0]  w_requested_navg;
  wire  [(IW+LGMEM-1):0]  rounded;






  initial  wraddr = 0;
  always @(posedge i_clk)
  if (i_reset)
    wraddr <= 0;
  else if (i_ce)
    wraddr <= wraddr + 1'b1;








  assign w_requested_navg = (FIXED_NAVG) ? INITIAL_NAVG : i_navg;













  initial  rdaddr = -INITIAL_NAVG;
  always @(posedge i_clk)
  if (i_reset)
    rdaddr <= -w_requested_navg;
  else if (i_ce)

    rdaddr <= rdaddr + 1'b1;













  initial  preval = 0;
  always @(posedge i_clk)
  if (i_reset)
    preval <= 0;
  else if (i_ce)
    preval <= i_sample;




  always @(posedge i_clk)
  if (i_ce)
    mem[wraddr] <= i_sample;




  initial  memval = 0;
  always @(posedge i_clk)
  if (i_ce)
    memval <= mem[rdaddr];





  initial  full   = 1'b0;
  always @(posedge i_clk)
  if (i_reset)
    full <= 0;
  else if (i_ce)
    full <= (full)||(rdaddr==0);

















  initial  sub = 0;
  always @(posedge i_clk)
  if (i_reset)
    sub <= 0;
  else if (i_ce)
  begin
    if (full)
      sub <= { OPT_SIGNED&preval[(IW-1)], preval }
          - { OPT_SIGNED&memval[(IW-1)], memval };
    else
      sub <= { OPT_SIGNED&preval[(IW-1)], preval };
  end

















  initial  acc = 0;
  always @(posedge i_clk)
  if (i_reset)
    acc <= 0;
  else if (i_ce)
    acc <= acc + { {(LGMEM-1){OPT_SIGNED&sub[IW]}}, sub };















  generate




  if (IW+LGMEM == OW)

    assign  rounded = acc;
  else if (IW+LGMEM == OW + 1)

    assign  rounded = acc + { {(OW){1'b0}}, acc[1] };
  else

    assign  rounded = acc + {
        {(OW){1'b0}},
        acc[(IW+LGMEM-OW)],
        {(IW+LGMEM-OW-1){!acc[(IW+LGMEM-OW)]}}
        };
  endgenerate









  initial  o_result = 0;
  always @(posedge i_clk)
  if (i_reset)
    o_result <= 0;
  else if (i_ce)
    o_result <= rounded[(IW+LGMEM-1):(IW+LGMEM-OW)];











`ifdef  FORMAL


  reg      f_past_valid;
  wire  [LGMEM-1:0]  f_rdaddr;
  reg  [LGMEM+IW-1:0]  f_sum;
  wire  [LGMEM-1:0]  f_full_addr;
  reg  [3:0]    f_test;
  reg  [(LGMEM-1):0]  f_navg;
  integer      k;

  initial  f_past_valid = 1'b0;
  always @(posedge i_clk)
    f_past_valid <= 1'b1;

  always @(*)
  if ((!FIXED_NAVG)&&(!f_past_valid))
    assume(i_reset);


  always @(posedge i_clk)
  if ((f_past_valid)&&(!$past(i_ce)))
    assume(i_ce);

  always @(*)
  if ((!FIXED_NAVG)&&(i_reset))
    assume(i_navg > 3);

  always @(posedge i_clk)
  if ((f_test[3])&&(f_navg < (1<<LGMEM)-3))
    assert(f_sum == acc);

  always @(*)
    assert(f_navg > 3);

  always @(posedge i_clk)
    cover($rose(full));

  initial  f_navg = INITIAL_NAVG;
  always @(posedge i_clk)
  if (FIXED_NAVG)
    f_navg <= INITIAL_NAVG;
  else if (i_reset)
    f_navg <= i_navg;


  assign  f_rdaddr = wraddr - f_navg;
  always @(posedge i_clk)
  if (!i_reset)
    assert(f_rdaddr == rdaddr);

  always @(*)
  begin
    f_sum = 0;
    for(k=0; k<(1<<LGMEM); k=k+1)
    begin
      if (((full)&&(k<f_navg)) || ((!full)&&(wraddr>=3)&&(k < wraddr-2)))
        f_sum = f_sum
        + {{(LGMEM){OPT_SIGNED&mem[wraddr-k-3][IW-1]}},
            mem[wraddr-k-3] };
    end
  end

  assign  f_full_addr = - f_navg;

  always @(*)
  if ((rdaddr < f_full_addr)&&(rdaddr != 0))
    assert(full);

  initial  f_test = 0;
  always @(posedge i_clk)
  if (i_reset)
    f_test <= 0;
  else if ((full)&&(i_ce))
    f_test <= { f_test[2:0], 1'b1 };

  always @(posedge i_clk)
  if ((f_test[3])&&(f_navg < (1<<LGMEM)-4))
  begin
    assert(f_sum == acc);
  end else if ((wraddr > 1)&&(!full))
    assert(f_sum == acc);
`endif

endmodule