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

Subversion Repositories zipcpu

[/] [zipcpu/] [trunk/] [rtl/] [core/] [div.v] - Diff between revs 205 and 209

Show entire file | Details | Blame | View Log

Rev 205 Rev 209
Line 6... Line 6...
//
//
// Purpose:     Provide an Integer divide capability to the Zip CPU.  Provides
// Purpose:     Provide an Integer divide capability to the Zip CPU.  Provides
//              for both signed and unsigned divide.
//              for both signed and unsigned divide.
//
//
// Steps:
// Steps:
//      i_rst   The DIVide unit starts in idle.  It can also be placed into an
//      i_reset The DIVide unit starts in idle.  It can also be placed into an
//      idle by asserting the reset input.
//      idle by asserting the reset input.
//
//
//      i_wr    When i_rst is asserted, a divide begins.  On the next clock:
//      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
//        o_busy is set high so everyone else knows we are at work and they can
//              wait for us to complete.
//              wait for us to complete.
//
//
//        pre_sign is set to true if we need to do a signed divide.  In this
//        pre_sign is set to true if we need to do a signed divide.  In this
Line 69... Line 69...
// Creator:     Dan Gisselquist, Ph.D.
// Creator:     Dan Gisselquist, Ph.D.
//              Gisselquist Technology, LLC
//              Gisselquist Technology, LLC
//
//
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
//
// Copyright (C) 2015-2017, Gisselquist Technology, LLC
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
//
//
// This program is free software (firmware): you can redistribute it and/or
// 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
// 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
// by the Free Software Foundation, either version 3 of the License, or (at
// your option) any later version.
// your option) any later version.
Line 93... Line 93...
//
//
//
//
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
//
//
//
 
`default_nettype        none
 
//
// `include "cpudefs.v"
// `include "cpudefs.v"
//
//
module  div(i_clk, i_rst, i_wr, i_signed, i_numerator, i_denominator,
module  div(i_clk, i_reset, i_wr, i_signed, i_numerator, i_denominator,
                o_busy, o_valid, o_err, o_quotient, o_flags);
                o_busy, o_valid, o_err, o_quotient, o_flags);
        parameter               BW=32, LGBW = 5;
        parameter               BW=32, LGBW = 5;
        input                   i_clk, i_rst;
        input   wire            i_clk, i_reset;
        // Input parameters
        // Input parameters
        input                   i_wr, i_signed;
        input   wire            i_wr, i_signed;
        input   [(BW-1):0]       i_numerator, i_denominator;
        input   wire [(BW-1):0]  i_numerator, i_denominator;
        // Output parameters
        // Output parameters
        output  reg             o_busy, o_valid, o_err;
        output  reg             o_busy, o_valid, o_err;
        output  reg [(BW-1):0]   o_quotient;
        output  reg [(BW-1):0]   o_quotient;
        output  wire    [3:0]    o_flags;
        output  wire    [3:0]    o_flags;
 
 
        // r_busy is an internal busy register.  It will clear one clock
        // r_busy is an internal busy register.  It will clear one clock
        // before we are valid, so it can't be o_busy ...
        // before we are valid, so it can't be o_busy ...
        //
        //
        reg                     r_busy;
        reg                     r_busy;
        reg     [(2*BW-2):0]     r_divisor;
        reg     [BW-1:0] r_divisor;
        reg     [(BW-1):0]       r_dividend;
        reg     [(2*BW-2):0]     r_dividend;
        wire    [(BW):0] diff; // , xdiff[(BW-1):0];
        wire    [(BW):0] diff; // , xdiff[(BW-1):0];
        assign  diff = r_dividend - r_divisor[(BW-1):0];
        assign  diff = r_dividend[2*BW-2:BW-1] - r_divisor;
        // assign       xdiff= r_dividend - { 1'b0, r_divisor[(BW-1):1] };
 
 
 
        reg             r_sign, pre_sign, r_z, r_c, last_bit;
        reg             r_sign, pre_sign, r_z, r_c, last_bit;
        reg     [(LGBW-1):0]     r_bit;
        reg     [(LGBW-1):0]     r_bit;
        reg     zero_divisor;
        reg     zero_divisor;
 
 
Line 128... Line 129...
        // Here, we clear r_busy on any reset and set it on i_wr (the request
        // Here, we clear r_busy on any reset and set it on i_wr (the request
        // do to a divide).  The divide ends when we are on the last bit,
        // do to a divide).  The divide ends when we are on the last bit,
        // or equivalently when we discover we are dividing by zero.
        // or equivalently when we discover we are dividing by zero.
        initial r_busy = 1'b0;
        initial r_busy = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (i_rst)
        if (i_reset)
                        r_busy <= 1'b0;
                        r_busy <= 1'b0;
                else if (i_wr)
                else if (i_wr)
                        r_busy <= 1'b1;
                        r_busy <= 1'b1;
                else if ((last_bit)||(zero_divisor))
                else if ((last_bit)||(zero_divisor))
                        r_busy <= 1'b0;
                        r_busy <= 1'b0;
Line 143... Line 144...
        // clock where we negate the result (assuming a signed divide, and that
        // clock where we negate the result (assuming a signed divide, and that
        // the result is supposed to be negative.)  Otherwise, the two are
        // the result is supposed to be negative.)  Otherwise, the two are
        // identical.
        // identical.
        initial o_busy = 1'b0;
        initial o_busy = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (i_rst)
        if (i_reset)
                        o_busy <= 1'b0;
                        o_busy <= 1'b0;
                else if (i_wr)
                else if (i_wr)
                        o_busy <= 1'b1;
                        o_busy <= 1'b1;
                else if (((last_bit)&&(~r_sign))||(zero_divisor))
        else if (((last_bit)&&(!r_sign))||(zero_divisor))
                        o_busy <= 1'b0;
                        o_busy <= 1'b0;
                else if (~r_busy)
        else if (!r_busy)
                        o_busy <= 1'b0;
                        o_busy <= 1'b0;
 
 
        // If we are asked to divide by zero, we need to halt.  The sooner
        always @(posedge i_clk)
        // we halt and report the error, the better.  Hence, here we look
        if (i_wr)
        // for a zero divisor while being busy.  The always above us will then
 
        // look at this and halt a divide in the middle if we are trying to
 
        // divide by zero.
 
        //
 
        // Note that this works off of the 2BW-1 length vector.  If we can
 
        // simplify that, it should simplify our logic as well.
 
        initial zero_divisor = 1'b0;
 
        always @(posedge i_clk)
 
                // zero_divisor <= (r_divisor == 0)&&(r_busy);
 
                if (i_rst)
 
                        zero_divisor <= 1'b0;
 
                else if (i_wr)
 
                        zero_divisor <= (i_denominator == 0);
                        zero_divisor <= (i_denominator == 0);
                else if (!r_busy)
 
                        zero_divisor <= 1'b0;
 
 
 
        // o_valid is part of the ZipCPU protocol.  It will be set to true
        // o_valid is part of the ZipCPU protocol.  It will be set to true
        // anytime our answer is valid and may be used by the calling module.
        // anytime our answer is valid and may be used by the calling module.
        // Indeed, the ZipCPU will halt (and ignore us) once the i_wr has been
        // Indeed, the ZipCPU will halt (and ignore us) once the i_wr has been
        // set until o_valid gets set.
        // set until o_valid gets set.
Line 181... Line 168...
        // bit while busy (provided the sign is zero, or we are dividing by
        // bit while busy (provided the sign is zero, or we are dividing by
        // zero).  Since o_valid is self-clearing, we don't need to clear
        // zero).  Since o_valid is self-clearing, we don't need to clear
        // it on an i_wr signal.
        // it on an i_wr signal.
        initial o_valid = 1'b0;
        initial o_valid = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (i_rst)
        if ((i_reset)||(o_valid))
                        o_valid <= 1'b0;
                        o_valid <= 1'b0;
 
        else if ((r_busy)&&(zero_divisor))
 
                o_valid <= 1'b1;
                else if (r_busy)
                else if (r_busy)
                begin
                begin
                        if ((last_bit)||(zero_divisor))
                if (last_bit)
                                o_valid <= (zero_divisor)||(!r_sign);
                        o_valid <= (!r_sign);
                end else if (r_sign)
                end else if (r_sign)
                begin
                begin
                        o_valid <= (!zero_divisor); // 1'b1;
                o_valid <= 1'b1;
                end else
                end else
                        o_valid <= 1'b0;
                        o_valid <= 1'b0;
 
 
        // Division by zero error reporting.  Anytime we detect a zero divisor,
        // Division by zero error reporting.  Anytime we detect a zero divisor,
        // we set our output error, and then hold it until we are valid and
        // we set our output error, and then hold it until we are valid and
        // everything clears.
        // everything clears.
        initial o_err = 1'b0;
        initial o_err = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if((i_rst)||(o_valid))
        if (i_reset)
                        o_err <= 1'b0;
                        o_err <= 1'b0;
                else if (((r_busy)||(r_sign))&&(zero_divisor))
        else if ((r_busy)&&(zero_divisor))
                        o_err <= 1'b1;
                        o_err <= 1'b1;
                else
                else
                        o_err <= 1'b0;
                        o_err <= 1'b0;
 
 
        // r_bit
        // r_bit
        //
        //
        // Keep track of which "bit" of our divide we are on.  This number
        // Keep track of which "bit" of our divide we are on.  This number
        // ranges from 31 down to zero.  On any write, we set ourselves to
        // ranges from 31 down to zero.  On any write, we set ourselves to
        // 5'h1f.  Otherwise, while we are busy (but not within the pre-sign
        // 5'h1f.  Otherwise, while we are busy (but not within the pre-sign
        // adjustment stage), we subtract one from our value on every clock.
        // adjustment stage), we subtract one from our value on every clock.
 
        initial r_bit = 0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if ((r_busy)&&(!pre_sign))
        if (i_reset)
                        r_bit <= r_bit + {(LGBW){1'b1}};
                r_bit <= 0;
 
        else if ((r_busy)&&(!pre_sign))
 
                r_bit <= r_bit + 1'b1;
                else
                else
                        r_bit <= {(LGBW){1'b1}};
                r_bit <= 0;
 
 
        // last_bit
        // last_bit
        //
        //
        // This logic replaces a lot of logic that was inside our giant state
        // This logic replaces a lot of logic that was inside our giant state
        // machine with ... something simpler.  In particular, we'll use this
        // machine with ... something simpler.  In particular, we'll use this
        // logic to determine we are processing our last bit.  The only trick
        // logic to determine if we are processing our last bit.  The only trick
        // is, this bit needs to be set whenever (r_busy) and (r_bit == 0),
        // is, this bit needs to be set whenever (r_busy) and (r_bit == -1),
        // hence we need to set on (r_busy) and (r_bit == 1) so as to be set
        // hence we need to set on (r_busy) and (r_bit == -2) so as to be set
        // when (r_bit == 0).
        // when (r_bit == 0).
        initial last_bit = 1'b0;
        initial last_bit = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (r_busy)
        if (i_reset)
                        last_bit <= (r_bit == {{(LGBW-1){1'b0}},1'b1});
                last_bit <= 1'b0;
 
        else if (r_busy)
 
                last_bit <= (r_bit == {(LGBW){1'b1}}-1'b1);
                else
                else
                        last_bit <= 1'b0;
                        last_bit <= 1'b0;
 
 
        // pre_sign
        // pre_sign
        //
        //
        // This is part of the state machine.  pre_sign indicates that we need
        // This is part of the state machine.  pre_sign indicates that we need
        // a extra clock to take the absolute value of our inputs.  It need only
        // a extra clock to take the absolute value of our inputs.  It need only
        // be true for the one clock, and then it must clear itself.
        // be true for the one clock, and then it must clear itself.
        initial pre_sign = 1'b0;
        initial pre_sign = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (i_wr)
        if (i_reset)
                        pre_sign <= i_signed;
 
                else
 
                        pre_sign <= 1'b0;
                        pre_sign <= 1'b0;
 
        else
 
                pre_sign <= (i_wr)&&(i_signed)&&((i_numerator[BW-1])||(i_denominator[BW-1]));
 
 
        // As a result of our operation, we need to set the flags.  The most
        // As a result of our operation, we need to set the flags.  The most
        // difficult of these is the "Z" flag indicating that the result is
        // difficult of these is the "Z" flag indicating that the result is
        // zero.  Here, we'll use the same logic that sets the low-order
        // zero.  Here, we'll use the same logic that sets the low-order
        // bit to clear our zero flag, and leave the zero flag set in all
        // bit to clear our zero flag, and leave the zero flag set in all
        // other cases.  Well ... not quite.  If we need to flip the sign of
        // other cases.
        // our value, then we can't quite clear the zero flag ... yet.
 
        always @(posedge i_clk)
        always @(posedge i_clk)
                if((r_busy)&&(r_divisor[(2*BW-2):(BW)] == 0)&&(!diff[BW]))
        if (i_wr)
                        // If we are busy, the upper bits of our divisor are
 
                        // zero (i.e., we got the shift right), and the top
 
                        // (carry) bit of the difference is zero (no overflow),
 
                        // then we could subtract our divisor from our dividend
 
                        // and hence we add a '1' to the quotient, while setting
 
                        // the zero flag to false.
 
                        r_z <= 1'b0;
 
                else if ((!r_busy)&&(!r_sign))
 
                        r_z <= 1'b1;
                        r_z <= 1'b1;
 
        else if ((r_busy)&&(!pre_sign)&&(!diff[BW]))
 
                r_z <= 1'b0;
 
 
        // r_dividend
        // r_dividend
        // This is initially the numerator.  On a signed divide, it then becomes
        // This is initially the numerator.  On a signed divide, it then becomes
        // the absolute value of the numerator.  We'll subtract from this value
        // the absolute value of the numerator.  We'll subtract from this value
        // the divisor shifted as appropriate for every output bit we are
        // the divisor for every output bit we are looking for--just as with
        // looking for--just as with traditional long division.
        // traditional long division.
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (pre_sign)
                if (pre_sign)
                begin
                begin
                        // If we are doing a signed divide, then take the
                        // If we are doing a signed divide, then take the
                        // absolute value of the dividend
                        // absolute value of the dividend
                        if (r_dividend[BW-1])
                        if (r_dividend[BW-1])
                                r_dividend <= -r_dividend;
                begin
                        // The begin/end block is important so we don't lose
                        r_dividend[2*BW-2:0] <= {(2*BW-1){1'b1}};
                        // the fact that on an else we don't do anything.
                        r_dividend[BW-1:0] <= -r_dividend[BW-1:0];
                end else if((r_busy)&&(r_divisor[(2*BW-2):(BW)]==0)&&(!diff[BW]))
                end
                        // This is the condition whereby we set a '1' in our
        end else if (r_busy)
                        // output quotient, and we subtract the (current)
        begin
                        // divisor from our dividend.  (The difference is
                r_dividend <= { r_dividend[2*BW-3:0], 1'b0 };
                        // already kept in the diff vector above.)
                if (!diff[BW])
                        r_dividend <= diff[(BW-1):0];
                        r_dividend[2*BW-2:BW] <= diff[(BW-2):0];
                else if (!r_busy)
        end else if (!r_busy)
                        // Once we are done, and r_busy is no longer high, we'll
                        // Once we are done, and r_busy is no longer high, we'll
                        // always accept new values into our dividend.  This
                        // always accept new values into our dividend.  This
                        // guarantees that, when i_wr is set, the new value
                        // guarantees that, when i_wr is set, the new value
                        // is already set as desired.
                        // is already set as desired.
                        r_dividend <=  i_numerator;
                r_dividend <=  { 31'h0, i_numerator };
 
 
        initial r_divisor = 0;
        initial r_divisor = 0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (pre_sign)
        if (i_reset)
 
                r_divisor <= 0;
 
        else if ((pre_sign)&&(r_busy))
                begin
                begin
                        if (r_divisor[(2*BW-2)])
                if (r_divisor[BW-1])
                                r_divisor[(2*BW-2):(BW-1)]
                        r_divisor <= -r_divisor;
                                        <= -r_divisor[(2*BW-2):(BW-1)];
        end else if (!r_busy)
                end else if (r_busy)
                r_divisor <= i_denominator;
                        r_divisor <= { 1'b0, r_divisor[(2*BW-2):1] };
 
                else
 
                        r_divisor <= {  i_denominator, {(BW-1){1'b0}} };
 
 
 
        // r_sign
        // r_sign
        // is a flag for our state machine control(s).  r_sign will be set to
        // is a flag for our state machine control(s).  r_sign will be set to
        // true any time we are doing a signed divide and the result must be
        // true any time we are doing a signed divide and the result must be
        // negative.  In that case, we take a final logic stage at the end of
        // negative.  In that case, we take a final logic stage at the end of
Line 312... Line 298...
        // goes low, r_sign will be checked, then the idle/reset stage will have
        // goes low, r_sign will be checked, then the idle/reset stage will have
        // been reached.  For this reason, we cannot set r_sign unless we are
        // been reached.  For this reason, we cannot set r_sign unless we are
        // up to something.
        // up to something.
        initial r_sign = 1'b0;
        initial r_sign = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (pre_sign)
        if (i_reset)
                        r_sign <= ((r_divisor[(2*BW-2)])^(r_dividend[(BW-1)]));
                r_sign <= 1'b0;
 
        else if (pre_sign)
 
                r_sign <= ((r_divisor[(BW-1)])^(r_dividend[(BW-1)]));
                else if (r_busy)
                else if (r_busy)
                        r_sign <= (r_sign)&&(!zero_divisor);
                        r_sign <= (r_sign)&&(!zero_divisor);
                else
                else
                        r_sign <= 1'b0;
                        r_sign <= 1'b0;
 
 
 
        initial o_quotient = 0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (r_busy)
        if (i_reset)
 
                o_quotient <= 0;
 
        else if (r_busy)
                begin
                begin
                        o_quotient <= { o_quotient[(BW-2):0], 1'b0 };
                        o_quotient <= { o_quotient[(BW-2):0], 1'b0 };
                        if ((r_divisor[(2*BW-2):(BW)] == 0)&&(!diff[BW]))
                if (!diff[BW])
                        begin
 
                                o_quotient[0] <= 1'b1;
                                o_quotient[0] <= 1'b1;
                        end
 
                end else if (r_sign)
                end else if (r_sign)
                        o_quotient <= -o_quotient;
                        o_quotient <= -o_quotient;
                else
                else
                        o_quotient <= 0;
                        o_quotient <= 0;
 
 
        // Set Carry on an exact divide
        // Set Carry on an exact divide
        // Perhaps nothing uses this, but ... well, I suppose we could remove
        // Perhaps nothing uses this, but ... well, I suppose we could remove
        // this logic eventually, just ... not yet.
        // this logic eventually, just ... not yet.
 
        initial r_c = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                r_c <= (r_busy)&&((diff == 0)||(r_dividend == 0));
        if (i_reset)
 
                r_c <= 1'b0;
 
        else
 
                r_c <= (r_busy)&&(diff == 0);
 
 
        // The last flag: Negative.  This flag is set assuming that the result
        // The last flag: Negative.  This flag is set assuming that the result
        // of the divide was negative (i.e., the high order bit is set).  This
        // of the divide was negative (i.e., the high order bit is set).  This
        // will also be true of an unsigned divide--if the high order bit is
        // will also be true of an unsigned divide--if the high order bit is
        // ever set upon completion.  Indeed, you might argue that there's no
        // ever set upon completion.  Indeed, you might argue that there's no
        // logic involved.
        // logic involved.
        wire    w_n;
        wire    w_n;
        assign w_n = o_quotient[(BW-1)];
        assign w_n = o_quotient[(BW-1)];
 
 
        assign o_flags = { 1'b0, w_n, r_c, r_z };
        assign o_flags = { 1'b0, w_n, r_c, r_z };
 
 
 
`ifdef  FORMAL
 
        reg     f_past_valid;
 
        initial f_past_valid = 0;
 
        always @(posedge i_clk)
 
                f_past_valid <= 1'b1;
 
 
 
`ifdef  DIV
 
`define ASSUME  assume
 
`else
 
`define ASSUME  assert
 
`endif
 
 
 
        initial `ASSUME(i_reset);
 
        always @(*)
 
        if (!f_past_valid)
 
                `ASSUME(i_reset);
 
 
 
        always @(posedge i_clk)
 
        if ((!f_past_valid)||($past(i_reset)))
 
        begin
 
                assert(!o_busy);
 
                assert(!o_valid);
 
                assert(!o_err);
 
                //
 
                assert(!r_busy);
 
                // assert(!zero_divisor);
 
                assert(r_bit==0);
 
                assert(!last_bit);
 
                assert(!pre_sign);
 
                // assert(!r_z);
 
                // assert(r_dividend==0);
 
                assert(o_quotient==0);
 
                assert(!r_c);
 
                assert(r_divisor==0);
 
 
 
                `ASSUME(!i_wr);
 
        end
 
 
 
        always @(*)
 
        if (o_busy)
 
                `ASSUME(!i_wr);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))&&($past(o_busy))&&(!o_busy))
 
        begin
 
                assert(o_valid);
 
        end
 
 
 
        // A formal methods section
 
        //
 
        // This section isn't yet complete.  For now, it is just
 
        // a description of things I think should be in here ... not
 
        // yet a description of what it would take to prove
 
        // this divide (yet).
 
        always @(*)
 
        if (o_err)
 
                assert(o_valid);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_wr)))
 
                assert(!pre_sign);
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wr))&&($past(i_signed))
 
                        &&(|$past({i_numerator[BW-1],i_denominator[BW-1]})))
 
                assert(pre_sign);
 
 
 
        // always @(posedge i_clk)
 
        // if ((f_past_valid)&&(!$past(pre_sign)))
 
                // assert(!r_sign);
 
        reg     [BW:0]   f_bits_set;
 
 
 
        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)))
 
                assert(!o_valid);
 
 
 
        always @(*)
 
        if ((o_valid)&&(!o_err))
 
                assert(r_z == ((o_quotient == 0)? 1'b1:1'b0));
 
        else if (o_busy)
 
                assert(r_z == (((o_quotient&f_bits_set[BW-1:0]) == 0)? 1'b1: 1'b0));
 
 
 
        always @(*)
 
        if ((o_valid)&&(!o_err))
 
                assert(w_n == o_quotient[BW-1]);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(r_busy))&&(!$past(i_wr)))
 
                assert(!o_busy);
 
        always @(posedge i_clk)
 
                assert((!o_busy)||(!o_valid));
 
 
 
        always @(*)
 
        if(r_busy)
 
                assert(o_busy);
 
 
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                f_bits_set <= 0;
 
        else if (i_wr)
 
                f_bits_set <= 0;
 
        else if ((r_busy)&&(!pre_sign))
 
                f_bits_set <= { f_bits_set[BW-1:0], 1'b1 };
 
 
 
        always @(posedge i_clk)
 
        if (r_busy)
 
                assert(((1<<r_bit)-1) == f_bits_set);
 
 
 
        always @(*)
 
        if ((o_valid)&&(!o_err))
 
                assert((!f_bits_set[BW])&&(&f_bits_set[BW-1:0]));
 
 
 
 
 
        /*
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))&&($past(r_busy))
 
                &&($past(r_divisor[2*BW-2:BW])==0))
 
        begin
 
                if ($past(r_divisor) == 0)
 
                        assert(o_err);
 
                else if ($past(pre_sign))
 
                begin
 
                        if ($past(r_dividend[BW-1]))
 
                                assert(r_dividend == -$past(r_dividend));
 
                        if ($past(r_divisor[(2*BW-2)]))
 
                        begin
 
                                assert(r_divisor[(2*BW-2):(BW-1)]
 
                                        == -$past(r_divisor[(2*BW-2):(BW-1)]));
 
                                assert(r_divisor[BW-2:0] == 0);
 
                        end
 
                end else begin
 
                        if (o_quotient[0])
 
                                assert(r_dividend == $past(diff));
 
                        else
 
                                assert(r_dividend == $past(r_dividend));
 
 
 
                        // r_divisor should shift down on every step
 
                        assert(r_divisor[2*BW-2]==0);
 
                        assert(r_divisor[2*BW-3:0]==$past(r_divisor[2*BW-2:1]));
 
                end
 
                if ($past(r_dividend) >= $past(r_divisor[BW-1:0]))
 
                        assert(o_quotient[0]);
 
                else
 
                        assert(!o_quotient[0]);
 
        end
 
        */
 
 
 
        always @(*)
 
        if (r_busy)
 
                assert((f_bits_set & r_dividend[BW-1:0])==0);
 
 
 
        always @(*)
 
        if (r_busy)
 
                assert((r_divisor == 0) == zero_divisor);
 
 
 
`ifdef  VERIFIC
 
        // Verify unsigned division
 
        assert property (@(posedge i_clk)
 
                disable iff (i_reset)
 
                (i_wr)&&(i_denominator != 0)&&(!i_signed)
 
                |=> ((!o_err)&&(!o_valid)&&(o_busy)&&(!r_sign)&&(!pre_sign)
 
                                throughout (r_bit == 0)
 
                        ##1 ((r_bit == $past(r_bit)+1)&&({1'b0,r_bit}< BW-1))
 
                                        [*0:$]
 
                        ##1 ({ 1'b0, r_bit } == BW-1))
 
                        ##1 (!o_err)&&(o_valid));
 
 
 
        // Verify division by zero
 
        assert property (@(posedge i_clk)
 
                disable iff (i_reset)
 
                (i_wr)&&(i_denominator == 0)
 
                |=> (zero_divisor throughout
 
                        (!o_err)&&(!o_valid)&&(pre_sign) [*0:1]
 
                        ##1 ((r_busy)&&(!o_err)&&(!o_valid))
 
                        ##1 ((o_err)&&(o_valid))));
 
 
 
 
 
`endif  // VERIFIC
 
`endif
endmodule
endmodule
 
//
 
// How much logic will this divide use, now that it's been updated to
 
// a different (long division) algorithm?
 
//
 
// iCE40 stats                  (Updated)       (Original)
 
//   Number of cells:                700        820
 
//     SB_CARRY                      125        125
 
//     SB_DFF                          1          
 
//     SB_DFFE                        33          1
 
//     SB_DFFESR                      37
 
//     SB_DFFESS                      31
 
//     SB_DFFSR                       40         40
 
//     SB_LUT4                       433        553
 
// 
 
// Xilinx stats                 (Updated)       (Original)
 
//   Number of cells:                758        831
 
//     FDRE                          142        142
 
//     LUT1                           97         97
 
//     LUT2                           69        174
 
//     LUT3                            6          5
 
//     LUT4                            1          6
 
//     LUT5                           68         35
 
//     LUT6                           94         98
 
//     MUXCY                         129        129
 
//     MUXF7                          12          8
 
//     MUXF8                           6          3
 
//     XORCY                         134        134
 
 
 
 
 No newline at end of file
 No newline at end of file

powered by: WebSVN 2.1.0

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