Subversion Repositories zipcpu

////////////////////////////////////////////////////////////////////////////////

//

// Filename:    abs_div.v

//

// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core

//

// Purpose:     The original divide module provides an Integer divide

//              capability to the Zip CPU.  This module is an abstract

//      divide module.  It *might* produce a valid integer divide, either signed

//      or unsigned, result.  It might instead do somethin else.  It is designed

//      to be easier for the formal tools to work with.

//

// Steps:

//      i_reset The DIVide unit starts in idle.  It can also be placed into an

//      idle by asserting the reset input.

//

//      i_wr    When i_reset is asserted, a divide begins.  On the next clock:

//

//        o_busy is set high so everyone else knows we are at work and they can

//              wait for us to complete.

//

//        pre_sign is set to true if we need to do a signed divide.  In this

//              case, we take a clock cycle to turn the divide into an unsigned

//              divide.

//

//        o_quotient, a place to store our result, is initialized to all zeros.

//

//        r_dividend is set to the numerator

//

//        r_divisor is set to 2^31 * the denominator (shift left by 31, or add

//              31 zeros to the right of the number.

//

//      pre_sign When true (clock cycle after i_wr), a clock cycle is used

//              to take the absolute value of the various arguments (r_dividend

//              and r_divisor), and to calculate what sign the output result

//              should be.

//

//

//      At this point, the divide is has started.  The divide works by walking

//      through every shift of the

//

//                  DIVIDEND    over the

//              DIVISOR

//

//      If the DIVISOR is bigger than the dividend, the divisor is shifted

//      right, and nothing is done to the output quotient.

//

//                  DIVIDEND

//               DIVISOR

//

//      This repeats, until DIVISOR is less than or equal to the divident, as in

//

//              DIVIDEND

//              DIVISOR

//

//      At this point, if the DIVISOR is less than the dividend, the

//      divisor is subtracted from the dividend, and the DIVISOR is again

//      shifted to the right.  Further, a '1' bit gets set in the output

//      quotient.

//

//      Once we've done this for 32 clocks, we've accumulated our answer into

//      the output quotient, and we can proceed to the next step.  If the

//      result will be signed, the next step negates the quotient, otherwise

//      it returns the result.

//

//      On the clock when we are done, o_busy is set to false, and o_valid set

//      to true.  (It is a violation of the ZipCPU internal protocol for both

//      busy and valid to ever be true on the same clock.  It is also a

//      violation for busy to be false with valid true thereafter.)

//

//

// Creator:     Dan Gisselquist, Ph.D.

//              Gisselquist Technology, LLC

//

////////////////////////////////////////////////////////////////////////////////

//

// Copyright (C) 2015-2019, Gisselquist Technology, LLC

//

// This program is free software (firmware): you can redistribute it and/or

// modify it under the terms of  the GNU General Public License as published

// by the Free Software Foundation, either version 3 of the License, or (at

// your option) any later version.

//

// This program is distributed in the hope that it will be useful, but WITHOUT

// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or

// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License

// for more details.

//

// You should have received a copy of the GNU General Public License along

// with this program.  (It's in the $(ROOT)/doc directory.  Run make with no

// target there if the PDF file isn't present.)  If not, see

// <http://www.gnu.org/licenses/> for a copy.

//

// License:     GPL, v3, as defined and found on www.gnu.org,

//              http://www.gnu.org/licenses/gpl.html

//

//

////////////////////////////////////////////////////////////////////////////////

//

//

`default_nettype        none

//

module  abs_div(i_clk, i_reset, i_wr, i_signed, i_numerator, i_denominator,

                o_busy, o_valid, o_err, o_quotient, o_flags);

        parameter               BW=32, LGBW = 5;

        parameter       [4:0]    MAXDELAY = 3;

        input   wire            i_clk, i_reset;

        // Input parameters

        input   wire            i_wr, i_signed;

        input   wire [(BW-1):0]  i_numerator, i_denominator;

        // Output parameters

        output  wire            o_busy;

        output  reg             o_valid, o_err;

        output  reg [(BW-1):0]   o_quotient;

        output  wire    [3:0]    o_flags;

        (* anyseq *)    reg                     any_err;

        (* anyseq *)    reg     [(BW-1):0]       any_quotient;

        (* anyseq *)    reg     [5:0]            wait_time;

        always @(*)

                o_err      = any_err;

        always @(*)

                o_quotient = any_quotient;

        reg     [5:0]    r_busy_counter;

        always @(*)

                assume(wait_time > 5'h1);

        always @(*)

                assume((MAXDELAY == 0)||(wait_time < MAXDELAY));

        initial r_busy_counter = 0;

        always @(posedge i_clk)

        if (i_reset)

                r_busy_counter <= 0;

        else if ((i_wr)&&(!o_busy))

                r_busy_counter <= wait_time;

        else if (r_busy_counter > 0)

                r_busy_counter <= r_busy_counter - 1'b1;

        always @(*)

        assert((MAXDELAY == 0)||(r_busy_counter < MAXDELAY));

        assign  o_busy = (r_busy_counter != 0);

        initial o_valid = 1'b0;

        always @(posedge i_clk)

        if (i_reset)

                o_valid <= 1'b0;

        else

                o_valid <= (r_busy_counter == 1);

        (* anyseq *)    reg     [3:0]    any_flags;

        assign o_flags    = (o_valid) ?

                        { 1'b0, o_quotient[31], any_flags[1],

                                        (o_quotient == 0) } : any_flags;

`ifdef  FORMAL

        reg     f_past_valid;

        initial f_past_valid = 0;

        always @(posedge i_clk)

                f_past_valid <= 1'b1;

        always @(posedge i_clk)

        if (!f_past_valid)

                assert((!o_busy)&&(!o_valid));

`define ASSUME  assert

        initial `ASSUME(i_reset);

        always @(*)

        if (!f_past_valid)

                `ASSUME(i_reset);

        always @(posedge i_clk)

        if ((!f_past_valid)||($past(i_reset)))

                `ASSUME(!i_wr);

        always @(*)

        if (o_busy)

                `ASSUME(!i_wr);

        always @(posedge i_clk)

        if ((f_past_valid)&&(!$past(i_reset))&&($past(o_busy))&&(!o_busy))

                assume(o_valid);

        always @(*)

        if (o_err)

                assume(o_valid);

        always @(posedge i_clk)

        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wr)))

                assert(o_busy);

        always @(posedge i_clk)

        if ((f_past_valid)&&($past(o_valid)))

                assume(!o_valid);

        always @(*)

        if ((o_valid)&&(!o_err))

                assume(o_flags[3] == ((o_quotient == 0)? 1'b1:1'b0));

        always @(*)

        if ((o_valid)&&(!o_err))

                assume(o_flags[1] == o_quotient[BW-1]);

        always @(posedge i_clk)

        if ((f_past_valid)&&(!$past(o_busy))&&(!$past(i_wr)))

                assume(!o_busy);

        always @(posedge i_clk)

                assume((!o_busy)||(!o_valid));

`endif

endmodule