Subversion Repositories wb2axip

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

//

// Filename:    fav_slave.v

//

// Project:     Pipelined Wishbone to AXI converter

//

// Purpose:     Formal properties of an Avalon slave.  These are the properties

//              the module owning the slave should use: they assume inputs from

//      the bus master, and assert that the outputs from the slave are valid.

//

// Creator:     Dan Gisselquist, Ph.D.

//              Gisselquist Technology, LLC

//

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

//

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

//

// This file is part of the pipelined Wishbone to AXI converter project, a

// project that contains multiple bus bridging designs and formal bus property

// sets.

//

// The bus bridge designs and property sets are free RTL designs: you can

// redistribute them and/or modify any of them under the terms of the GNU

// Lesser General Public License as published by the Free Software Foundation,

// either version 3 of the License, or (at your option) any later version.

//

// The bus bridge designs and property sets are distributed in the hope that

// they will be useful, but WITHOUT ANY WARRANTY; without even the implied

// warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the

// GNU Lesser General Public License for more details.

//

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

// along with these designs.  (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:     LGPL, v3, as defined and found on www.gnu.org,

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

//

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

//

//

`default_nettype        none

//

module  fav_slave(i_clk, i_reset,

                i_av_read,

                i_av_write,

                i_av_address,

                i_av_writedata,

                        i_av_byteenable,

                i_av_lock,

                i_av_waitrequest,       // = wb_stall

                //

                i_av_writeresponsevalid,

                //

                i_av_readdatavalid,

                i_av_readdata,

                i_av_response,  // Error response = 2'b11

                f_rd_nreqs, f_rd_nacks, f_rd_outstanding,

                f_wr_nreqs, f_wr_nacks, f_wr_outstanding);

        parameter       DW=32, AW=14;

        parameter       F_LGDEPTH=6;

        parameter       [(F_LGDEPTH-1):0]        F_MAX_REQUESTS = 62;

        input   wire                    i_clk, i_reset;

        input   wire                    i_av_read;

        input   wire                    i_av_write;

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

        input   wire    [(DW-1):0]       i_av_writedata;

        input   wire    [(DW/8-1):0]     i_av_byteenable;

        input   wire                    i_av_lock;

        //

        input   wire                    i_av_waitrequest;

        input   wire                    i_av_writeresponsevalid;

        input   wire                    i_av_readdatavalid;

        input   wire    [(DW-1):0]       i_av_readdata;

        input   wire    [1:0]            i_av_response;

        //

        output  reg     [(F_LGDEPTH-1):0] f_rd_nreqs, f_rd_nacks;

        output  wire    [(F_LGDEPTH-1):0] f_rd_outstanding;

        output  reg     [(F_LGDEPTH-1):0] f_wr_nreqs, f_wr_nacks;

        output  wire    [(F_LGDEPTH-1):0] f_wr_outstanding;

        assert  property(F_MAX_REQUESTS < {(F_LGDEPTH){1'b1}});

        reg     f_past_valid;

        initial f_past_valid = 1'b0;

        always @(posedge i_clk)

                f_past_valid <= 1'b1;

        always @(*)

                assert((f_past_valid) || (i_reset));

        wire    [AW+(DW/8):0]    f_rd_request;

        assign  f_rd_request = { i_av_read,  i_av_byteenable, i_av_address };

        wire    [(AW+DW+(DW/8)):0]       f_wr_request;

        assign  f_wr_request = { i_av_write, i_av_address, i_av_writedata,

                                        i_av_byteenable };

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

        //

        // Require that nothing changes, save on a clock tick.

        //

        // This is only required if yosys is using the clk2fflogic

        // command, a command only required if multiple clocks are

        // in use.  Since this can greatly slow down formal proofs,

        // we limit any code associated with this option to only

        // those times the option is in play.

        //

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

        generate if (F_OPT_CLK2FFLOGIC)

        begin

                always @($global_clock)

                if ((f_past_valid)&&(!$rose(i_clk)))

                begin

                        assume($stable(f_rd_request));

                        assume($stable(f_wr_request));

                        assume($stable(i_av_lock));

                        assert($stable(i_av_readdatavalid));

                        assert($stable(i_av_writeresponsevalid));

                        assert($stable(i_av_readdata));

                        assert($stable(i_av_response));

                end

        end endgenerate

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

        //

        // Assumptions about a slave's inputs

        //

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

        initial assume(!i_av_read);

        initial assume(!i_av_write);

        initial assume(!i_av_lock);

        //

        initial assert(!i_av_readdatavalid);

        initial assert(!i_av_writeresponsevalid);

        //

        always @(posedge i_clk)

                if (i_reset)

                begin

                        assume(!i_av_read);

                        assume(!i_av_write);

                        assume(!i_av_lock);

                end

        always @(*)

                if (i_av_write)

                        assume(|i_av_byteenable);

        // It is a protocol violation to issue both read and write requests

        // on the same clock

        always @(*)

                assume((!i_av_read)||(!i_av_write));

        // Once a read request has been placed upon the bus, it will remain

        // there until wait request goes low

        always @(posedge i_clk)

        if ((f_past_valid)&&($past(i_av_waitrequest))&&($past(i_av_read)))

                assume((i_reset)||(f_rd_request == $past(f_rd_request)));

        // Same thing for a write request

        always @(posedge i_clk)

        if ((f_past_valid)&&($past(i_av_waitrequest))&&($past(i_av_write)))

                assume((i_reset)||(f_wr_request == $past(f_wr_request)));

        // A lock request can only be asserted at the same time a read or

        // write request is being made.

        always @(posedge i_clk)

                if ((f_past_valid)&&(!$past(i_av_lock)))

                        assume((!i_av_lock)||(i_av_read)||(i_av_write));

        // A lock request can only be de-asserted following the last read

        // or write request made with it asserted

        always @(posedge i_clk)

                if ((f_past_valid)&&($past(i_av_lock)

                                &&(!i_av_read)&&(!i_av_write)))

                        assume((i_reset)||(i_av_lock)

                                ||(i_av_read)||(i_av_write));

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

        //

        // Internal state variables

        //

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

        // Count the number of read requests

        initial f_rd_nreqs = 0;

        always @(posedge i_clk)

                if (i_reset)

                        f_rd_nreqs <= 0;

                else if ((i_av_read)&&(!i_av_waitrequest))

                        f_rd_nreqs <= f_rd_nreqs + 1'b1;

        // Count the number of read acknowledgements

        initial f_rd_nacks = 0;

        always @(posedge i_clk)

                if (i_reset)

                        f_rd_nacks <= 0;

                else if (i_av_readdatavalid)

                        f_rd_nacks <= f_rd_nacks + 1'b1;

        // The difference between read requests and acknowledgements is

        // the number of outstanding read requests

        assign  f_rd_outstanding = (i_reset) ? 0 : (f_rd_nreqs - f_rd_nacks);

        // Count the number of write requests

        initial f_wr_nreqs = 0;

        always @(posedge i_clk)

                if (i_reset)

                        f_wr_nreqs <= 0;

                else if ((i_av_write)&&(!i_av_waitrequest))

                        f_wr_nreqs <= f_wr_nreqs + 1'b1;

        // Count the number of write acknowledgements/responses

        initial f_wr_nacks = 0;

        always @(posedge i_clk)

                if (i_reset)

                        f_wr_nacks <= 0;

                else if (i_av_writeresponsevalid)

                        f_wr_nacks <= f_wr_nacks + 1'b1;

        assign  f_wr_outstanding = f_wr_nreqs - f_wr_nacks;

        initial assume(!i_av_read);

        initial assume(!i_av_write);

        initial assume(!i_av_lock);

        //

        initial assert(!i_av_readdatavalid);

        initial assert(!i_av_writeresponsevalid);

        //

        always @(posedge i_clk)

                if (i_reset)

                begin

                        assume(!i_av_read);

                        assume(!i_av_write);

                end

        always @(posedge i_clk)

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

                begin

                        assert(!i_av_readdatavalid);

                        assert(!i_av_writeresponsevalid);

                        assert(f_rd_nreqs == 0);

                        assert(f_rd_nacks == 0);

                        assert(f_wr_nreqs == 0);

                        assert(f_wr_nacks == 0);

                end

        // Just like a read and write request cannot both be made at the same

        // time, neither can both responses come back at the same time

        always @(*)

                assert((!i_av_writeresponsevalid)||(!i_av_readdatavalid));

        // If nothing is outstanding, then there should be no responses.

        // If i_reset is asserted, a response may have been registered, and

        // so may still return on this clock.

        always @(posedge i_clk)

                if ((f_rd_outstanding == 0)&&(!i_reset)

                                &&((!i_av_read)||(i_av_waitrequest)))

                        assert(!i_av_readdatavalid);

        always @(posedge i_clk)

                if ((f_wr_outstanding == 0)&&(!i_reset)

                                &&((!i_av_write)||(i_av_waitrequest)))

                        assert(!i_av_writeresponsevalid);

        always @(*)

                assert({1'b0, f_wr_outstanding} + { 1'b0, f_rd_outstanding }

                        < F_MAX_REQUESTS);

        generate if (F_OPT_MAX_STALL > 0)

        begin

                reg     [(LGWAIT-1):0]   stall_count;

                initial stall_count = 0;

                always @(posedge i_clk)

                        if (i_reset)

                                stall_count <= 0;

                        else if (((i_av_read)||(i_av_write))&&(i_av_waitrequest))

                                stall_count <= stall_count + 1'b1;

                        else

                                stall_count <= 0;

                always @(*)

                        assert((i_reset)||(stall_count < F_OPT_MAX_STALL));

        end endgenerate

        generate if (F_OPT_MAX_WAIT > 0)

        begin

                reg     [(LGWAIT-1):0]   read_wait, write_wait;

                //

                // Insist on a minimum amount of time to wait for a *read*

                // response.

                //

                always @(posedge i_clk)

                        if (i_reset)

                                read_wait <= 0;

                        else if ((i_av_readdatavalid)

                                        ||((i_av_read)&&(!i_av_waitrequest)))

                                read_wait <= 0;

                        else if (f_rd_outstanding > 0)

                                read_wait <= read_wait + 1'b1;

                always @(*)

                        assert((i_av_readdatavalid)

                                ||(f_rd_outstanding == 0)

                                ||(read_wait < F_OPT_MAX_WAIT));

                //

                // Insist on a minimum amount of time to wait for a *write*

                // response.

                //

                always @(posedge i_clk)

                        if (i_reset)

                                write_wait <= 0;

                        else if ((i_av_writeresponsevalid)

                                        ||((i_av_write)&&(!i_av_waitrequest)))

                                write_wait <= 0;

                        else if (f_wr_outstanding > 0)

                                write_wait <= write_wait + 1'b1;

                always @(*)

                        assert((i_av_writeresponsevalid)

                                ||(f_wr_outstanding == 0)

                                ||(write_wait < F_OPT_MAX_WAIT));

        end endgenerate

endmodule