Subversion Repositories dblclockfft

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

//

// Filename:    abs_mpy.v

//

// Project:     A General Purpose Pipelined FFT Implementation

//

// Purpose:     This code has been modified from the mpyop.v file so as to

//              abstract the multiply that formal methods struggle so hard to

//      deal with.  It also simplifies the interface so that (if enabled)

//      the multiply will return in 1-6 clocks, rather than the specified

//      number for the given architecture.

//

//

// Creator:     Dan Gisselquist, Ph.D.

//              Gisselquist Technology, LLC

//

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

//

// Copyright (C) 2015-2018, 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_mpy(i_a, i_b, o_result);

        parameter       AW = 32, BW=32;

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

        input   wire    [(AW-1):0]       i_a;

        input   wire    [(BW-1):0]       i_b;

        output  wire    [(AW+BW-1):0]    o_result;

        wire    [(AW+BW-1):0]    any_result;

        assign  any_result = $anyseq;

        reg     [AW-1:0] u_a;

        reg     [BW-1:0] u_b;

        always @(*)

        begin

                u_a = ((i_a[AW-1])&&(OPT_SIGNED)) ? -i_a : i_a;

                u_b = ((i_b[BW-1])&&(OPT_SIGNED)) ? -i_b : i_b;

        end

        reg     [(AW+BW-1):0]    u_result;

        always @(*)

        if ((OPT_SIGNED)&&(any_result[AW+BW-1]))

                u_result = - { 1'b1, any_result };

        else

                u_result =  { 1'b0, any_result };

        always @(*)

        begin

                // Constrain our result among many possibilities

                if ((i_a == 0)||(i_b == 0))

                        assume(any_result == 0);

                else if (OPT_SIGNED)

                        assume(any_result[AW+BW-1]

                                == (i_a[AW-1] ^ i_b[BW-1]));

                assume(u_result[AW+BW-1:BW] <= u_a);

                assume(u_result[AW+BW-1:AW] <= u_b);

        end

        genvar  k;

        generate

        begin

                for(k=0; k<AW-1; k=k+1)

                begin

                        always @(*)

                        if (u_a == (1<<k))

                                assume(u_result == (u_b << k));

                end

                for(k=0; k<BW; k=k+1)

                begin

                        always @(*)

                        if (u_b == (1<<k))

                                assume(u_result== (u_a << k));

                end

        end endgenerate

        assign  o_result = any_result;

        /*

        always @(*)

        if (i_a == 1)

                assert(o_result == {{(AW){i_b[BW-1]}}, i_b });

        always @(*)

        if (i_b == 1)

                assert(o_result == {{(BW){i_a[AW-1]}}, i_a });

        */

endmodule