OpenCores
URL https://opencores.org/ocsvn/wbuart32/wbuart32/trunk

Subversion Repositories wbuart32

[/] [wbuart32/] [trunk/] [rtl/] [ufifo.v] - Diff between revs 17 and 18

Go to most recent revision | Show entire file | Details | Blame | View Log

Rev 17 Rev 18
Line 2... Line 2...
//
//
// Filename:    ufifo.v
// Filename:    ufifo.v
//
//
// Project:     wbuart32, a full featured UART with simulator
// Project:     wbuart32, a full featured UART with simulator
//
//
// Purpose:     
// Purpose:     A synchronous data FIFO, designed for supporting the Wishbone
 
//              UART.  Particular features include the ability to read and
 
//      write on the same clock, while maintaining the correct output FIFO
 
//      parameters.  Two versions of the FIFO exist within this file, separated
 
//      by the RXFIFO parameter's value.  One, where RXFIFO = 1, produces status
 
//      values appropriate for reading and checking a read FIFO from logic,
 
//      whereas the RXFIFO = 0 applies to writing to the FIFO from bus logic
 
//      and reading it automatically any time the transmit UART is idle.
//
//
// Creator:     Dan Gisselquist, Ph.D.
// Creator:     Dan Gisselquist, Ph.D.
//              Gisselquist Technology, LLC
//              Gisselquist Technology, LLC
//
//
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
Line 109... Line 116...
        initial will_underflow = 1'b1;
        initial will_underflow = 1'b1;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (i_rst)
                if (i_rst)
                        will_underflow <= 1'b1;
                        will_underflow <= 1'b1;
                else if (i_wr)
                else if (i_wr)
                        will_underflow <= (will_underflow)&&(i_rd);
                        will_underflow <= 1'b0;
                else if (i_rd)
                else if (i_rd)
                        will_underflow <= (will_underflow)||(w_last_plus_one == r_first);
                        will_underflow <= (will_underflow)||(w_last_plus_one == r_first);
                else
                else
                        will_underflow <= (r_last == r_first);
                        will_underflow <= (r_last == r_first);
 
 
Line 123... Line 130...
        // We'll still report FIFO overflow, however.
        // We'll still report FIFO overflow, however.
        //
        //
        // reg          r_unfl;
        // reg          r_unfl;
        // initial      r_unfl = 1'b0;
        // initial      r_unfl = 1'b0;
        initial r_last = 0;
        initial r_last = 0;
 
        initial r_next = { {(LGFLEN-1){1'b0}}, 1'b1 };
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (i_rst)
                if (i_rst)
                begin
                begin
                        r_last <= 0;
                        r_last <= 0;
                        r_next <= { {(LGFLEN-1){1'b0}}, 1'b1 };
                        r_next <= { {(LGFLEN-1){1'b0}}, 1'b1 };
                        // r_unfl <= 1'b0;
                        // r_unfl <= 1'b0;
                end else if (i_rd)
                end else if (i_rd)
                begin
                begin
                        if ((i_wr)||(!will_underflow)) // (r_first != r_last)
                        if (!will_underflow) // (r_first != r_last)
                        begin
                        begin
                                r_last <= r_next;
                                r_last <= r_next;
                                r_next <= r_last +{{(LGFLEN-2){1'b0}},2'b10};
                                r_next <= r_last +{{(LGFLEN-2){1'b0}},2'b10};
                                // Last chases first
                                // Last chases first
                                // Need to be prepared for a possible two
                                // Need to be prepared for a possible two
Line 174... Line 182...
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (i_rst)
                if (i_rst)
                        r_empty_n <= 1'b0;
                        r_empty_n <= 1'b0;
                else casez({i_wr, i_rd, will_underflow})
                else casez({i_wr, i_rd, will_underflow})
                        3'b00?: r_empty_n <= (r_first != r_last);
                        3'b00?: r_empty_n <= (r_first != r_last);
                        3'b11?: r_empty_n <= (r_first != r_last);
 
                        3'b10?: r_empty_n <= 1'b1;
 
                        3'b010: r_empty_n <= (r_first != w_last_plus_one);
                        3'b010: r_empty_n <= (r_first != w_last_plus_one);
                        // 3'b001: r_empty_n <= 1'b0;
                        3'b10?: r_empty_n <= 1'b1;
 
                        3'b110: r_empty_n <= (r_first != r_last);
 
                        3'b111: r_empty_n <= 1'b1;
                        default: begin end
                        default: begin end
                endcase
                endcase
 
 
        wire    w_full_n;
        wire    w_full_n;
        assign  w_full_n = will_overflow;
        assign  w_full_n = will_overflow;
Line 192... Line 200...
        // the FIFO count that matters is the number of empty positions that
        // the FIFO count that matters is the number of empty positions that
        // can still be filled before the FIFO is full.
        // can still be filled before the FIFO is full.
        //
        //
        // Adjust for these differences here.
        // Adjust for these differences here.
        reg     [(LGFLEN-1):0]   r_fill;
        reg     [(LGFLEN-1):0]   r_fill;
 
        generate
 
        if (RXFIFO != 0)
        initial r_fill = 0;
        initial r_fill = 0;
 
        else
 
                initial r_fill = -1;
 
        endgenerate
 
 
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (RXFIFO!=0) begin
                if (RXFIFO!=0) begin
                        // Calculate the number of elements in our FIFO
                        // Calculate the number of elements in our FIFO
                        //
                        //
                        // Although used for receive, this is actually the more
                        // Although used for receive, this is actually the more
                        // generic answer--should you wish to use the FIFO in
                        // generic answer--should you wish to use the FIFO in
                        // another context.
                        // another context.
                        if (i_rst)
                        if (i_rst)
                                r_fill <= 0;
                                r_fill <= 0;
                        else case({(i_wr)&&(!will_overflow), (i_rd)&&(!will_underflow)})
                        else casez({(i_wr), (!will_overflow), (i_rd)&&(!will_underflow)})
                        2'b01:   r_fill <= r_first - r_next;
                        3'b0?1:   r_fill <= r_first - r_next;
                        2'b10:   r_fill <= r_first - r_last + 1'b1;
                        3'b110:   r_fill <= r_first - r_last + 1'b1;
 
                        3'b1?1:   r_fill <= r_first - r_last;
                        default: r_fill <= r_first - r_last;
                        default: r_fill <= r_first - r_last;
                        endcase
                        endcase
                end else begin
                end else begin
                        // Calculate the number of elements that are empty and
                        // Calculate the number of elements that are empty and
                        // can be filled within our FIFO.  Hence, this is really
                        // can be filled within our FIFO.  Hence, this is really
                        // not the fill, but (SIZE-1)-fill.
                        // not the fill, but (SIZE-1)-fill.
                        if (i_rst)
                        if (i_rst)
                                r_fill <= { (LGFLEN){1'b1} };
                                r_fill <= { (LGFLEN){1'b1} };
                        else case({i_wr, i_rd})
                        else casez({i_wr, (!will_overflow), (i_rd)&&(!will_underflow)})
                        2'b01:   r_fill <= r_last - r_first;
                        3'b0?1:   r_fill <= r_fill + 1'b1;
                        2'b10:   r_fill <= r_last - w_first_plus_two;
                        3'b110:   r_fill <= r_fill - 1'b1;
                        default: r_fill <= r_last - w_first_plus_one;
                        default: r_fill  <= r_fill;
                        endcase
                        endcase
                end
                end
 
 
        // We don't report underflow errors.  These
        // We don't report underflow errors.  These
        assign o_err = (r_ovfl); //  || (r_unfl);
        assign o_err = (r_ovfl); //  || (r_unfl);
 
 
        wire    [3:0]    lglen;
        wire    [3:0]    lglen;
        assign lglen = LGFLEN;
        assign lglen = LGFLEN;
 
 
 
        wire    w_half_full;
        wire    [9:0]    w_fill;
        wire    [9:0]    w_fill;
        assign  w_fill[(LGFLEN-1):0] = r_fill;
        assign  w_fill[(LGFLEN-1):0] = r_fill;
        generate if (LGFLEN < 10)
        generate if (LGFLEN < 10)
                assign w_fill[9:(LGFLEN)] = 0;
                assign w_fill[9:(LGFLEN)] = 0;
        endgenerate
        endgenerate
 
 
        wire    w_half_full;
 
        assign  w_half_full = r_fill[(LGFLEN-1)];
        assign  w_half_full = r_fill[(LGFLEN-1)];
 
 
        assign  o_status = {
        assign  o_status = {
                // Our status includes a 4'bit nibble telling anyone reading
                // Our status includes a 4'bit nibble telling anyone reading
                // this the size of our FIFO.  The size is then given by
                // this the size of our FIFO.  The size is then given by
Line 256... Line 271...
                (RXFIFO!=0)?r_empty_n:w_full_n
                (RXFIFO!=0)?r_empty_n:w_full_n
        };
        };
 
 
        assign  o_empty_n = r_empty_n;
        assign  o_empty_n = r_empty_n;
 
 
 
//
 
//
 
//
 
// FORMAL METHODS
 
//
 
//
 
//
 
`ifdef  FORMAL
 
 
 
`ifdef  UFIFO
 
`define ASSUME  assume
 
`else
 
`define ASSUME  assert
 
`endif
 
 
 
//
 
// Assumptions about our input(s)
 
//
 
//
 
        reg     f_past_valid, f_last_clk;
 
 
 
        initial restrict(i_rst);
 
 
 
        always @($global_clock)
 
        begin
 
                restrict(i_clk == !f_last_clk);
 
                f_last_clk <= i_clk;
 
                if (!$rose(i_clk))
 
                begin
 
                        `ASSUME($stable(i_rst));
 
                        `ASSUME($stable(i_wr));
 
                        `ASSUME($stable(i_data));
 
                        `ASSUME($stable(i_rd));
 
                end
 
        end
 
 
 
        //
 
        // Underflows are a very real possibility, should the user wish to
 
        // read from this FIFO while it is empty.  Our parent module will need
 
        // to deal with this.
 
        //
 
        // always @(posedge i_clk)
 
        //      `ASSUME((!will_underflow)||(!i_rd)||(i_rst));
 
//
 
// Assertions about our outputs
 
//
 
//
 
 
 
        initial f_past_valid = 1'b0;
 
        always @(posedge i_clk)
 
                f_past_valid <= 1'b1;
 
 
 
        wire    [(LGFLEN-1):0]   f_fill, f_next, f_empty;
 
        assign  f_fill = r_first - r_last;
 
        assign  f_empty = {(LGFLEN){1'b1}} -f_fill;
 
        assign  f_next = r_last + 1'b1;
 
        always @(posedge i_clk)
 
        begin
 
                if (RXFIFO)
 
                        assert(f_fill == r_fill);
 
                else
 
                        assert(f_empty== r_fill);
 
                if (f_fill == 0)
 
                begin
 
                        assert(will_underflow);
 
                        assert(!o_empty_n);
 
                end else begin
 
                        assert(!will_underflow);
 
                        assert(o_empty_n);
 
                end
 
 
 
                if (f_fill == {(LGFLEN){1'b1}})
 
                        assert(will_overflow);
 
                else
 
                        assert(!will_overflow);
 
 
 
                assert(r_next == f_next);
 
        end
 
 
 
        always @(posedge i_clk)
 
        if (f_past_valid)
 
        begin
 
                if ($past(i_rst))
 
                        assert(!o_err);
 
                else begin
 
                        // No underflow detection in this core
 
                        //
 
                        // if (($past(i_rd))&&($past(r_fill == 0)))
 
                        //      assert(o_err);
 
                        //
 
                        // We do, though, have overflow detection
 
                        if (($past(i_wr))&&(!$past(i_rd))
 
                                        &&($past(will_overflow)))
 
                                assert(o_err);
 
                end
 
        end
 
 
 
`endif
endmodule
endmodule
 
 
 No newline at end of file
 No newline at end of file

powered by: WebSVN 2.1.0

© copyright 1999-2024 OpenCores.org, equivalent to Oliscience, all rights reserved. OpenCores®, registered trademark.