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

Subversion Repositories zipcpu

[/] [zipcpu/] [trunk/] [rtl/] [core/] [pipemem.v] - Diff between revs 201 and 209

Show entire file | Details | Blame | View Log

Rev 201 Rev 209
Line 15... Line 15... 
// 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 39... Line 39... 
//
 
//
 
//
 
//
 
////////////////////////////////////////////////////////////////////////////////
 
////////////////////////////////////////////////////////////////////////////////
 
//
 
//
 
//
 
//
 
module  pipemem(i_clk, i_rst, i_pipe_stb, i_lock,
 
`default_nettype        none
 
 
 
//
 
 
 
module  pipemem(i_clk, i_reset, i_pipe_stb, i_lock,
 
                i_op, i_addr, i_data, i_oreg,
 
                i_op, i_addr, i_data, i_oreg,
 
                        o_busy, o_pipe_stalled, o_valid, o_err, o_wreg, o_result,
 
                        o_busy, o_pipe_stalled, o_valid, o_err, o_wreg, o_result,
 
                o_wb_cyc_gbl, o_wb_cyc_lcl,
 
                o_wb_cyc_gbl, o_wb_cyc_lcl,
 
                        o_wb_stb_gbl, o_wb_stb_lcl,
 
                        o_wb_stb_gbl, o_wb_stb_lcl,
 
                        o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
 
                        o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
 
                i_wb_ack, i_wb_stall, i_wb_err, i_wb_data);
 
                i_wb_ack, i_wb_stall, i_wb_err, i_wb_data
 
        parameter       ADDRESS_WIDTH=30, IMPLEMENT_LOCK=0;
 
`ifdef  FORMAL
 
        localparam      AW=ADDRESS_WIDTH;
 
                , f_nreqs, f_nacks, f_outstanding, f_pc
 
        input                   i_clk, i_rst;
 
`endif
 
        input                   i_pipe_stb, i_lock;
 
                );
 
 
 
        parameter       ADDRESS_WIDTH=30;
 
 
 
        parameter [0:0]   IMPLEMENT_LOCK=1'b1,
 
 
 
                        WITH_LOCAL_BUS=1'b1,
 
 
 
                        OPT_ZERO_ON_IDLE=1'b0,
 
 
 
                        // OPT_ALIGNMENT_ERR
 
 
 
                        OPT_ALIGNMENT_ERR=1'b0;
 
 
 
        localparam      AW=ADDRESS_WIDTH,
 
 
 
                        FLN=4;
 
 
 
        parameter [(FLN-1):0]    OPT_MAXDEPTH=4'hd;
 
 
 
        input   wire            i_clk, i_reset;
 
 
 
        input   wire            i_pipe_stb, i_lock;
 
        // CPU interface
 
        // CPU interface
 
        input   [2:0]            i_op;
 
        input   wire    [2:0]    i_op;
 
        input           [31:0]   i_addr;
 
        input   wire    [31:0]   i_addr;
 
        input           [31:0]   i_data;
 
        input   wire    [31:0]   i_data;
 
        input           [4:0]    i_oreg;
 
        input   wire    [4:0]    i_oreg;
 
        // CPU outputs
 
        // CPU outputs
 
        output  wire            o_busy;
 
        output  wire            o_busy;
 
        output  wire            o_pipe_stalled;
 
        output  wire            o_pipe_stalled;
 
        output  reg             o_valid;
 
        output  reg             o_valid;
 
        output  reg             o_err;
 
        output  reg             o_err;
Line 71... Line 84... 
        output  reg             o_wb_stb_lcl, o_wb_we;
 
        output  reg             o_wb_stb_lcl, o_wb_we;
 
        output  reg     [(AW-1):0]       o_wb_addr;
 
        output  reg     [(AW-1):0]       o_wb_addr;
 
        output  reg     [31:0]   o_wb_data;
 
        output  reg     [31:0]   o_wb_data;
 
        output  reg     [3:0]    o_wb_sel;
 
        output  reg     [3:0]    o_wb_sel;
 
        // Wishbone inputs
 
        // Wishbone inputs
 
        input                   i_wb_ack, i_wb_stall, i_wb_err;
 
        input   wire            i_wb_ack, i_wb_stall, i_wb_err;
 
        input           [31:0]   i_wb_data;
 
        input   wire    [31:0]   i_wb_data;
 
 
 
// Formal
 
 
 
        parameter       F_LGDEPTH=5;
 
 
 
`ifdef  FORMAL
 
 
 
        output  wire    [(F_LGDEPTH-1):0]        f_nreqs, f_nacks, f_outstanding;
 
 
 
        output  reg     f_pc;
 
 
 
`endif
 
 
 
 
 
 
 
 
 
        reg     cyc;
 
        reg     cyc;
 
        reg                     r_wb_cyc_gbl, r_wb_cyc_lcl;
 
        reg                     r_wb_cyc_gbl, r_wb_cyc_lcl, fifo_full;
 
        reg     [3:0]            rdaddr, wraddr;
 
        reg     [(FLN-1):0]              rdaddr, wraddr;
 
        wire    [3:0]            nxt_rdaddr;
 
        wire    [(FLN-1):0]              nxt_rdaddr, fifo_fill;
 
        reg     [(4+5-1):0]      fifo_oreg [0:15];
 
        reg     [(3+5-1):0]      fifo_oreg [0:15];
 
 
 
        reg                     fifo_gie;
 
        initial rdaddr = 0;
 
        initial rdaddr = 0;
 
        initial wraddr = 0;
 
        initial wraddr = 0;
 
 
 
 
 
 
 
        reg     misaligned;
 
 
 
 
 
 
 
        always  @(*)
 
 
 
        if (OPT_ALIGNMENT_ERR)
 
 
 
        begin
 
 
 
                casez({ i_op[2:1], i_addr[1:0] })
 
 
 
                4'b01?1: misaligned = i_pipe_stb;
 
 
 
                4'b0110: misaligned = i_pipe_stb;
 
 
 
                4'b10?1: misaligned = i_pipe_stb;
 
 
 
                default: misaligned = i_pipe_stb;
 
 
 
                endcase
 
 
 
        end else
 
 
 
                misaligned = 1'b0;
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
                fifo_oreg[wraddr] <= { i_oreg[3:0], i_op[2:1], i_addr[1:0] };
 
 
 
 
 
        always @(posedge i_clk)
 
        always @(posedge i_clk)
 
                fifo_oreg[wraddr] <= { i_oreg, i_op[2:1], i_addr[1:0] };
 
        if (i_pipe_stb)
 
 
 
                fifo_gie <= i_oreg[4];
 
 
 
 
 
 
 
        initial wraddr = 0;
 
        always @(posedge i_clk)
 
        always @(posedge i_clk)
 
                if ((i_rst)||(i_wb_err))
 
        if (i_reset)
 
 
 
                wraddr <= 0;
 
 
 
        else if (((i_wb_err)&&(cyc))||((i_pipe_stb)&&(misaligned)))
 
                        wraddr <= 0;
 
                        wraddr <= 0;
 
                else if (i_pipe_stb)
 
                else if (i_pipe_stb)
 
                        wraddr <= wraddr + 1'b1;
 
                        wraddr <= wraddr + 1'b1;
 
 
 
 
 
 
 
        initial rdaddr = 0;
 
        always @(posedge i_clk)
 
        always @(posedge i_clk)
 
                if ((i_rst)||(i_wb_err))
 
        if (i_reset)
 
 
 
                rdaddr <= 0;
 
 
 
        else if (((i_wb_err)&&(cyc))||((i_pipe_stb)&&(misaligned)))
 
                        rdaddr <= 0;
 
                        rdaddr <= 0;
 
                else if ((i_wb_ack)&&(cyc))
 
                else if ((i_wb_ack)&&(cyc))
 
                        rdaddr <= rdaddr + 1'b1;
 
                        rdaddr <= rdaddr + 1'b1;
 
 
 
 
 
 
 
        assign  fifo_fill = wraddr - rdaddr;
 
 
 
 
 
 
 
        initial fifo_full = 0;
 
 
 
        always @(posedge i_clk)
 
 
 
        if (i_reset)
 
 
 
                fifo_full <= 0;
 
 
 
        else if (((i_wb_err)&&(cyc))||((i_pipe_stb)&&(misaligned)))
 
 
 
                fifo_full <= 0;
 
 
 
        else if (i_pipe_stb)
 
 
 
                fifo_full <= (fifo_fill >= OPT_MAXDEPTH-1);
 
 
 
        else
 
 
 
                fifo_full <= (fifo_fill >= OPT_MAXDEPTH);
 
 
 
 
 
        assign  nxt_rdaddr = rdaddr + 1'b1;
 
        assign  nxt_rdaddr = rdaddr + 1'b1;
 
 
 
 
 
        wire    gbl_stb, lcl_stb;
 
        wire    gbl_stb, lcl_stb, lcl_bus;
 
        assign  lcl_stb = (i_addr[31:24]==8'hff);
 
        assign  lcl_bus = (i_addr[31:24]==8'hff)&&(WITH_LOCAL_BUS);
 
        assign  gbl_stb = (~lcl_stb);
 
        assign  lcl_stb = (lcl_bus)&&(!misaligned);
 
 
 
        assign  gbl_stb = ((!lcl_bus)||(!WITH_LOCAL_BUS))&&(!misaligned);
 
                        //= ((i_addr[31:8]!=24'hc00000)||(i_addr[7:5]!=3'h0));
 
                        //= ((i_addr[31:8]!=24'hc00000)||(i_addr[7:5]!=3'h0));
 
 
 
 
 
        initial cyc = 0;
 
        initial cyc = 0;
 
        initial r_wb_cyc_lcl = 0;
 
        initial r_wb_cyc_lcl = 0;
 
        initial r_wb_cyc_gbl = 0;
 
        initial r_wb_cyc_gbl = 0;
 
 
 
        initial o_wb_stb_lcl = 0;
 
 
 
        initial o_wb_stb_gbl = 0;
 
        always @(posedge i_clk)
 
        always @(posedge i_clk)
 
                if (i_rst)
 
        if (i_reset)
 
                begin
 
                begin
 
                        r_wb_cyc_gbl <= 1'b0;
 
                        r_wb_cyc_gbl <= 1'b0;
 
                        r_wb_cyc_lcl <= 1'b0;
 
                        r_wb_cyc_lcl <= 1'b0;
 
                        o_wb_stb_gbl <= 1'b0;
 
                        o_wb_stb_gbl <= 1'b0;
 
                        o_wb_stb_lcl <= 1'b0;
 
                        o_wb_stb_lcl <= 1'b0;
 
                        cyc <= 1'b0;
 
                        cyc <= 1'b0;
 
                end else if (cyc)
 
                end else if (cyc)
 
                begin
 
                begin
 
                        if ((~i_wb_stall)&&(~i_pipe_stb))
 
                if (((!i_wb_stall)&&(!i_pipe_stb)&&(!misaligned))
 
 
 
                        ||(i_wb_err))
 
                        begin
 
                        begin
 
                                o_wb_stb_gbl <= 1'b0;
 
                                o_wb_stb_gbl <= 1'b0;
 
                                o_wb_stb_lcl <= 1'b0;
 
                                o_wb_stb_lcl <= 1'b0;
 
                        // end else if ((i_pipe_stb)&&(~i_wb_stall))
 
 
 
                        // begin
 
 
 
                                // o_wb_addr <= i_addr[(AW-1):0];
 
 
 
                                // o_wb_data <= i_data;
 
 
 
                        end
 
                        end
 
 
 
 
 
                        if (((i_wb_ack)&&(nxt_rdaddr == wraddr))||(i_wb_err))
 
                if (((i_wb_ack)&&(nxt_rdaddr == wraddr)
 
 
 
                                &&((!i_pipe_stb)||(misaligned)))
 
 
 
                        ||(i_wb_err))
 
                        begin
 
                        begin
 
                                r_wb_cyc_gbl <= 1'b0;
 
                                r_wb_cyc_gbl <= 1'b0;
 
                                r_wb_cyc_lcl <= 1'b0;
 
                                r_wb_cyc_lcl <= 1'b0;
 
 
 
                        o_wb_stb_gbl <= 1'b0;
 
 
 
                        o_wb_stb_lcl <= 1'b0;
 
                                cyc <= 1'b0;
 
                                cyc <= 1'b0;
 
                        end
 
                        end
 
                end else if (i_pipe_stb) // New memory operation
 
                end else if (i_pipe_stb) // New memory operation
 
                begin // Grab the wishbone
 
                begin // Grab the wishbone
 
                        r_wb_cyc_lcl <= lcl_stb;
 
                        r_wb_cyc_lcl <= lcl_stb;
 
                        r_wb_cyc_gbl <= gbl_stb;
 
                        r_wb_cyc_gbl <= gbl_stb;
 
                        o_wb_stb_lcl <= lcl_stb;
 
                        o_wb_stb_lcl <= lcl_stb;
 
                        o_wb_stb_gbl <= gbl_stb;
 
                        o_wb_stb_gbl <= gbl_stb;
 
                        cyc <= 1'b1;
 
                cyc <= (!misaligned);
 
                        // o_wb_addr <= i_addr[(AW-1):0];
 
 
 
                        // o_wb_data <= i_data;
 
 
 
                        // o_wb_we <= i_op
 
 
 
                end
 
                end
 
 
 
 
 
        always @(posedge i_clk)
 
        always @(posedge i_clk)
 
                if ((!cyc)||(!i_wb_stall))
 
                if ((!cyc)||(!i_wb_stall))
 
                begin
 
                begin
 
 
 
                if ((OPT_ZERO_ON_IDLE)&&(!i_pipe_stb))
 
 
 
                        o_wb_addr <= 0;
 
 
 
                else
 
                        o_wb_addr <= i_addr[(AW+1):2];
 
                        o_wb_addr <= i_addr[(AW+1):2];
 
                        if (!i_op[0]) // Always select everything on reads
 
 
 
                                o_wb_sel <= 4'b1111;    // Op is even
 
                if ((OPT_ZERO_ON_IDLE)&&(!i_pipe_stb))
 
 
 
                        o_wb_sel <= 4'b0000;
 
                        else casez({ i_op[2:1], i_addr[1:0] })
 
                        else casez({ i_op[2:1], i_addr[1:0] })
 
                                4'b100?: o_wb_sel <= 4'b1100;   // Op = 5
 
                                4'b100?: o_wb_sel <= 4'b1100;   // Op = 5
 
                                4'b101?: o_wb_sel <= 4'b0011;   // Op = 5
 
                                4'b101?: o_wb_sel <= 4'b0011;   // Op = 5
 
                                4'b1100: o_wb_sel <= 4'b1000;   // Op = 5
 
                                4'b1100: o_wb_sel <= 4'b1000;   // Op = 5
 
                                4'b1101: o_wb_sel <= 4'b0100;   // Op = 7
 
                                4'b1101: o_wb_sel <= 4'b0100;   // Op = 7
 
                                4'b1110: o_wb_sel <= 4'b0010;   // Op = 7
 
                                4'b1110: o_wb_sel <= 4'b0010;   // Op = 7
 
                                4'b1111: o_wb_sel <= 4'b0001;   // Op = 7
 
                                4'b1111: o_wb_sel <= 4'b0001;   // Op = 7
 
                                default: o_wb_sel <= 4'b1111;   // Op = 7
 
                                default: o_wb_sel <= 4'b1111;   // Op = 7
 
                        endcase
 
                        endcase
 
 
 
 
 
                        casez({ i_op[2:1], i_addr[1:0] })
 
                if ((OPT_ZERO_ON_IDLE)&&(!i_pipe_stb))
 
 
 
                        o_wb_data <= 0;
 
 
 
                else casez({ i_op[2:1], i_addr[1:0] })
 
                        4'b100?: o_wb_data <= { i_data[15:0], 16'h00 };
 
                        4'b100?: o_wb_data <= { i_data[15:0], 16'h00 };
 
                        4'b101?: o_wb_data <= { 16'h00, i_data[15:0] };
 
                        4'b101?: o_wb_data <= { 16'h00, i_data[15:0] };
 
                        4'b1100: o_wb_data <= {         i_data[7:0], 24'h00 };
 
                        4'b1100: o_wb_data <= {         i_data[7:0], 24'h00 };
 
                        4'b1101: o_wb_data <= {  8'h00, i_data[7:0], 16'h00 };
 
                        4'b1101: o_wb_data <= {  8'h00, i_data[7:0], 16'h00 };
 
                        4'b1110: o_wb_data <= { 16'h00, i_data[7:0],  8'h00 };
 
                        4'b1110: o_wb_data <= { 16'h00, i_data[7:0],  8'h00 };
 
                        4'b1111: o_wb_data <= { 24'h00, i_data[7:0] };
 
                        4'b1111: o_wb_data <= { 24'h00, i_data[7:0] };
 
                        default: o_wb_data <= i_data;
 
                        default: o_wb_data <= i_data;
 
                        endcase
 
                        endcase
 
 
 
 
 
                end
 
                end
 
 
 
 
 
        always @(posedge i_clk)
 
        always @(posedge i_clk)
 
                if ((i_pipe_stb)&&(~cyc))
 
        if ((i_pipe_stb)&&(!cyc))
 
                        o_wb_we   <= i_op[0];
 
                        o_wb_we   <= i_op[0];
 
 
 
        else if ((OPT_ZERO_ON_IDLE)&&(!cyc))
 
 
 
                o_wb_we   <= 1'b0;
 
 
 
 
 
        initial o_valid = 1'b0;
 
        initial o_valid = 1'b0;
 
        always @(posedge i_clk)
 
        always @(posedge i_clk)
 
                o_valid <= (cyc)&&(i_wb_ack)&&(~o_wb_we);
 
        if (i_reset)
 
 
 
                o_valid <= 1'b0;
 
 
 
        else
 
 
 
                o_valid <= (cyc)&&(i_wb_ack)&&(!o_wb_we);
 
 
 
 
 
        initial o_err = 1'b0;
 
        initial o_err = 1'b0;
 
        always @(posedge i_clk)
 
        always @(posedge i_clk)
 
                o_err <= (cyc)&&(i_wb_err);
 
        if (i_reset)
 
 
 
                o_err <= 1'b0;
 
 
 
        else
 
 
 
                o_err <= ((cyc)&&(i_wb_err))||((i_pipe_stb)&&(misaligned));
 
        assign  o_busy = cyc;
 
        assign  o_busy = cyc;
 
 
 
 
 
        wire    [8:0]    w_wreg;
 
        wire    [7:0]    w_wreg;
 
        assign  w_wreg = fifo_oreg[rdaddr];
 
        assign  w_wreg = fifo_oreg[rdaddr];
 
        always @(posedge i_clk)
 
        always @(posedge i_clk)
 
                o_wreg <= w_wreg[8:4];
 
                o_wreg <= { fifo_gie, w_wreg[7:4] };
 
        always @(posedge i_clk)
 
        always @(posedge i_clk)
 
 
 
        if ((OPT_ZERO_ON_IDLE)&&((!cyc)||((!i_wb_ack)&&(!i_wb_err))))
 
 
 
                o_result <= 0;
 
 
 
        else begin
 
                casez(w_wreg[3:0])
 
                casez(w_wreg[3:0])
 
                4'b1100: o_result = { 24'h00, i_wb_data[31:24] };
 
                4'b1100: o_result <= { 24'h00, i_wb_data[31:24] };
 
                4'b1101: o_result = { 24'h00, i_wb_data[23:16] };
 
                4'b1101: o_result <= { 24'h00, i_wb_data[23:16] };
 
                4'b1110: o_result = { 24'h00, i_wb_data[15: 8] };
 
                4'b1110: o_result <= { 24'h00, i_wb_data[15: 8] };
 
                4'b1111: o_result = { 24'h00, i_wb_data[ 7: 0] };
 
                4'b1111: o_result <= { 24'h00, i_wb_data[ 7: 0] };
 
                4'b100?: o_result = { 16'h00, i_wb_data[31:16] };
 
                4'b100?: o_result <= { 16'h00, i_wb_data[31:16] };
 
                4'b101?: o_result = { 16'h00, i_wb_data[15: 0] };
 
                4'b101?: o_result <= { 16'h00, i_wb_data[15: 0] };
 
                default: o_result = i_wb_data[31:0];
 
                default: o_result <= i_wb_data[31:0];
 
                endcase
 
                endcase
 
 
 
        end
 
 
 
 
 
        assign  o_pipe_stalled = (cyc)
 
        assign  o_pipe_stalled = ((cyc)&&(fifo_full))||((cyc)
 
                        &&((i_wb_stall)||((~o_wb_stb_lcl)&&(~o_wb_stb_gbl)));
 
                        &&((i_wb_stall)||((!o_wb_stb_lcl)&&(!o_wb_stb_gbl))));
 
 
 
 
 
        generate
 
        generate
 
        if (IMPLEMENT_LOCK != 0)
 
        if (IMPLEMENT_LOCK != 0)
 
        begin
 
        begin
 
                reg     lock_gbl, lock_lcl;
 
                reg     lock_gbl, lock_lcl;
 
 
 
 
 
                initial lock_gbl = 1'b0;
 
                initial lock_gbl = 1'b0;
 
                initial lock_lcl = 1'b0;
 
                initial lock_lcl = 1'b0;
 
                always @(posedge i_clk)
 
                always @(posedge i_clk)
 
 
 
                if ((i_reset)||((i_wb_err)&&(cyc))
 
 
 
                        ||((i_pipe_stb)&&(misaligned)))
 
                begin
 
                begin
 
 
 
                        lock_gbl <= 1'b0;
 
 
 
                        lock_lcl <= 1'b0;
 
 
 
                end else begin
 
                        lock_gbl <= (i_lock)&&((r_wb_cyc_gbl)||(lock_gbl));
 
                        lock_gbl <= (i_lock)&&((r_wb_cyc_gbl)||(lock_gbl));
 
                        lock_lcl <= (i_lock)&&((r_wb_cyc_lcl)||(lock_lcl));
 
                        lock_lcl <= (i_lock)&&((r_wb_cyc_lcl)||(lock_lcl));
 
                end
 
                end
 
 
 
 
 
                assign  o_wb_cyc_gbl = (r_wb_cyc_gbl)||(lock_gbl);
 
                assign  o_wb_cyc_gbl = (r_wb_cyc_gbl)||(lock_gbl);
 
                assign  o_wb_cyc_lcl = (r_wb_cyc_lcl)||(lock_lcl);
 
                assign  o_wb_cyc_lcl = (r_wb_cyc_lcl)||(lock_lcl);
 
 
 
 
 
        end else begin
 
        end else begin
 
                assign  o_wb_cyc_gbl = (r_wb_cyc_gbl);
 
                assign  o_wb_cyc_gbl = (r_wb_cyc_gbl);
 
                assign  o_wb_cyc_lcl = (r_wb_cyc_lcl);
 
                assign  o_wb_cyc_lcl = (r_wb_cyc_lcl);
 
        end endgenerate
 
        end endgenerate
 
 
 
 
 
 
 
        // Make verilator happy
 
 
 
        // verilator lint_off UNUSED
 
 
 
        wire    unused;
 
 
 
        assign  unused = i_lock;
 
 
 
        // verilator lint_on  UNUSED
 
 
 
 
 
 
 
`ifdef  FORMAL
 
 
 
`define ASSERT  assert
 
 
 
`ifdef  PIPEMEM
 
 
 
`define ASSUME  assume
 
 
 
`else
 
 
 
`define ASSUME  assert
 
 
 
`endif
 
 
 
 
 
 
 
        reg     f_past_valid;
 
 
 
        initial f_past_valid = 0;
 
 
 
        always @(posedge i_clk)
 
 
 
                f_past_valid = 1'b1;
 
 
 
        always @(*)
 
 
 
                if (!f_past_valid)
 
 
 
                        `ASSUME(i_reset);
 
 
 
 
 
 
 
        initial `ASSUME( i_reset);
 
 
 
        initial `ASSUME(!i_pipe_stb);
 
 
 
 
 
 
 
        wire    f_cyc, f_stb;
 
 
 
        assign  f_cyc = cyc;
 
 
 
        assign  f_stb = (o_wb_stb_gbl)||(o_wb_stb_lcl);
 
 
 
 
 
 
 
`ifdef  PIPEMEM
 
 
 
`define MASTER  fwb_master
 
 
 
`else
 
 
 
`define MASTER  fwb_counter
 
 
 
`endif
 
 
 
        `MASTER #(.AW(AW), .F_LGDEPTH(F_LGDEPTH),
 
 
 
                        // .F_MAX_REQUESTS(14), // Not quite true, can do more
 
 
 
                        .F_OPT_RMW_BUS_OPTION(IMPLEMENT_LOCK),
 
 
 
                        .F_OPT_DISCONTINUOUS(IMPLEMENT_LOCK))
 
 
 
                fwb(i_clk, i_reset,
 
 
 
                        cyc, f_stb, o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
 
 
 
                                i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,
 
 
 
                        f_nreqs, f_nacks, f_outstanding);
 
 
 
 
 
 
 
 
 
 
 
        //
 
 
 
        // Assumptions about inputs
 
 
 
        //
 
 
 
        always @(posedge i_clk)
 
 
 
        if ((!f_past_valid)||($past(i_reset)))
 
 
 
        begin
 
 
 
                `ASSERT(!o_err);
 
 
 
                `ASSERT(!o_busy);
 
 
 
                `ASSERT(!o_pipe_stalled);
 
 
 
                `ASSERT(!o_valid);
 
 
 
        end
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
                if (o_pipe_stalled)
 
 
 
                        `ASSUME(!i_pipe_stb);
 
 
 
 
 
 
 
        // On any pipe request, the new address is the same or plus one
 
 
 
        always @(posedge i_clk)
 
 
 
                if ((f_past_valid)&&(f_cyc)&&(!i_wb_stall)&&(i_pipe_stb))
 
 
 
                begin
 
 
 
                        `ASSUME( (i_addr[(AW+1):2] == o_wb_addr)
 
 
 
                                ||(i_addr[(AW+1):2] == o_wb_addr+1));
 
 
 
                        `ASSUME(i_op[0] == o_wb_we);
 
 
 
                end
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
                if ((r_wb_cyc_gbl)&&(i_pipe_stb))
 
 
 
                        `ASSUME(gbl_stb);
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
                if ((r_wb_cyc_lcl)&&(i_pipe_stb))
 
 
 
                        `ASSUME(lcl_stb);
 
 
 
 
 
 
 
        // If stb is false, then either lock is on or there are no more STB's
 
 
 
        always @(posedge i_clk)
 
 
 
                if ((f_cyc)&&(!f_stb))
 
 
 
                        `ASSUME((i_lock)||(!i_pipe_stb));
 
 
 
 
 
 
 
//always @(posedge i_clk)
 
 
 
//      if ((f_past_valid)&&($past(f_cyc))&&(!$past(i_lock)))
 
 
 
//              `ASSUME(!i_lock);
 
 
 
 
 
 
 
        wire    [3:0]    f_pipe_used;
 
 
 
        assign  f_pipe_used = wraddr - rdaddr;
 
 
 
        always @(*)
 
 
 
                `ASSERT(f_pipe_used == fifo_fill);
 
 
 
        always @(posedge i_clk)
 
 
 
        if (f_pipe_used == OPT_MAXDEPTH)
 
 
 
 
 
 
 
        begin
 
 
 
                `ASSUME(!i_pipe_stb);
 
 
 
                `ASSERT((o_busy)&&(o_pipe_stalled));
 
 
 
        end
 
 
 
 
 
 
 
        always @(*)
 
 
 
                `ASSERT(fifo_fill <= OPT_MAXDEPTH);
 
 
 
 
 
 
 
        always @(*)
 
 
 
                if (!IMPLEMENT_LOCK)
 
 
 
                        `ASSUME(!i_lock);
 
 
 
 
 
 
 
`ifndef VERILATOR
 
 
 
        always @(*)
 
 
 
                if ((WITH_LOCAL_BUS)&&(o_wb_cyc_gbl|o_wb_cyc_lcl)
 
 
 
                        &&(i_pipe_stb))
 
 
 
                begin
 
 
 
                        if (o_wb_cyc_lcl)
 
 
 
                                // `ASSUME(i_addr[31:24] == 8'hff);
 
 
 
                                assume(i_addr[31:24] == 8'hff);
 
 
 
                        else
 
 
 
                                assume(i_addr[31:24] != 8'hff);
 
 
 
                end
 
 
 
`endif
 
 
 
 
 
 
 
        always @(*)
 
 
 
                if (!WITH_LOCAL_BUS)
 
 
 
                begin
 
 
 
                        assert(!r_wb_cyc_lcl);
 
 
 
                        assert(!o_wb_cyc_lcl);
 
 
 
                        assert(!o_wb_stb_lcl);
 
 
 
                end
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
                if ((f_past_valid)&&(!$past(f_cyc))&&(!$past(i_pipe_stb)))
 
 
 
                        `ASSERT(f_pipe_used == 0);
 
 
 
 
 
 
 
        always @(*)
 
 
 
        if (!f_cyc)
 
 
 
                `ASSERT(f_pipe_used == 0);
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
        if (f_pipe_used >= 13)
 
 
 
                `ASSUME(!i_pipe_stb);
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
        if ((f_cyc)&&(f_pipe_used >= 13))
 
 
 
                `ASSERT((o_busy)&&(o_pipe_stalled));
 
 
 
 
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
                `ASSERT((!r_wb_cyc_gbl)||(!r_wb_cyc_lcl));
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
                `ASSERT((!o_wb_cyc_gbl)||(!o_wb_cyc_lcl));
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
                `ASSERT((!o_wb_stb_gbl)||(!o_wb_stb_lcl));
 
 
 
 
 
 
 
        always @(*)
 
 
 
                if (!WITH_LOCAL_BUS)
 
 
 
                begin
 
 
 
                        assert(!o_wb_cyc_lcl);
 
 
 
                        assert(!o_wb_stb_lcl);
 
 
 
                        if (o_wb_stb_lcl)
 
 
 
                                assert(o_wb_addr[(AW-1):22] == {(8-(30-AW)){1'b1}});
 
 
 
                end
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
                if (o_wb_stb_gbl)
 
 
 
                        `ASSERT(o_wb_cyc_gbl);
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
                if (o_wb_stb_lcl)
 
 
 
                        `ASSERT(o_wb_cyc_lcl);
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
                `ASSERT(cyc == (r_wb_cyc_gbl|r_wb_cyc_lcl));
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
                `ASSERT(cyc == (r_wb_cyc_lcl)|(r_wb_cyc_gbl));
 
 
 
        always @(posedge i_clk)
 
 
 
        if ((f_past_valid)&&(!i_reset)&&(!$past(misaligned)))
 
 
 
        begin
 
 
 
                if (f_stb)
 
 
 
                        `ASSERT(f_pipe_used == f_outstanding + 4'h1);
 
 
 
                else
 
 
 
                        `ASSERT(f_pipe_used == f_outstanding);
 
 
 
        end
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
                if ((f_past_valid)&&($past(r_wb_cyc_gbl||r_wb_cyc_lcl))
 
 
 
                                &&(!$past(f_stb)))
 
 
 
                        `ASSERT(!f_stb);
 
 
 
 
 
 
 
        always @(*)
 
 
 
                `ASSERT((!lcl_stb)||(!gbl_stb));
 
 
 
 
 
 
 
        reg     [(1<<FLN)-1:0]   f_mem_used;
 
 
 
        wire    [(1<<FLN)-1:0]   f_zero;
 
 
 
        //
 
 
 
        // insist that we only ever accept memory requests for the same GIE
 
 
 
        // (i.e. 4th bit of register)
 
 
 
        //
 
 
 
        always @(*)
 
 
 
        if ((i_pipe_stb)&&(wraddr != rdaddr))
 
 
 
                `ASSUME(i_oreg[4] == fifo_gie);
 
 
 
 
 
 
 
        initial f_pc = 1'b0;
 
 
 
        always @(posedge i_clk)
 
 
 
        if(i_reset)
 
 
 
                f_pc <= 1'b0;
 
 
 
        else if (i_pipe_stb)
 
 
 
                f_pc <= (((f_pc)&&(f_cyc))
 
 
 
                                ||((!i_op[0])&&(i_oreg[3:1] == 3'h7)));
 
 
 
        else if (!f_cyc)
 
 
 
                f_pc <= 1'b0;
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
        if ((f_cyc)&&(o_wb_we))
 
 
 
                `ASSERT(!f_pc);
 
 
 
 
 
 
 
        always @(*)
 
 
 
        if ((f_pc)&&(f_cyc))
 
 
 
                `ASSUME(!i_pipe_stb);
 
 
 
 
 
 
 
        always @(*)
 
 
 
        if (wraddr == rdaddr)
 
 
 
        begin
 
 
 
                `ASSERT(!r_wb_cyc_gbl);
 
 
 
                `ASSERT(!r_wb_cyc_lcl);
 
 
 
        end else if (f_cyc)
 
 
 
        begin
 
 
 
                `ASSERT(fifo_fill == f_outstanding + ((f_stb)?1:0));
 
 
 
        end
 
 
 
 
 
 
 
 
 
 
 
`define FIFOCHECK
 
 
 
`ifdef  FIFOCHECK
 
 
 
        wire    [3:0]    lastaddr = wraddr - 1'b1;
 
 
 
 
 
 
 
        integer k;
 
 
 
        always @(*)
 
 
 
        begin
 
 
 
                f_mem_used = 0;
 
 
 
                for(k = 0 ; k < (1<<FLN); k=k+1)
 
 
 
                begin
 
 
 
                        if (wraddr == rdaddr)
 
 
 
                                f_mem_used[k] = 1'b0;
 
 
 
                        else if (wraddr > rdaddr)
 
 
 
                        begin
 
 
 
                                if ((k < wraddr)&&(k >= rdaddr))
 
 
 
                                        f_mem_used[k] = 1'b1;
 
 
 
                        end else if (k < wraddr)
 
 
 
                                f_mem_used[k] = 1'b1;
 
 
 
                        else if (k >= rdaddr)
 
 
 
                                f_mem_used[k] = 1'b1;
 
 
 
                end
 
 
 
        end
 
 
 
 
 
 
 
 
 
 
 
        always @(*)
 
 
 
        begin
 
 
 
                for(k=0; k<(1<<FLN); k=k+1)
 
 
 
                if ((f_mem_used[k])&&(!o_wb_we)&&((!f_pc)||(k!=lastaddr)))
 
 
 
                        `ASSERT(fifo_oreg[k][7:5] != 3'h7);
 
 
 
        end
 
 
 
 
 
 
 
        initial assert(!fifo_full);
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
                cover(cyc && !fifo_full);
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
                cover((f_cyc)&&(f_stb)&&(!i_wb_stall)&&(!i_wb_ack)
 
 
 
                        &&(!o_pipe_stalled));
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
        if ((f_past_valid)&&(!$past(f_stb))&&($past(f_cyc)))
 
 
 
                cover((f_cyc)&&(i_wb_ack));
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
        if ((f_past_valid)&&(!$past(f_stb))&&($past(f_cyc)))
 
 
 
                cover($past(i_wb_ack)&&(i_wb_ack));
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
        if ((f_past_valid)&&($past(o_valid)))
 
 
 
                cover(o_valid);
 
 
 
 
 
 
 
`endif // FIFOCHECK
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
 
 
        if ((f_past_valid)&&($past(f_past_valid))&&($past(f_cyc))&&($past(f_cyc,2)))
 
 
 
                `ASSERT($stable(o_wreg[4]));
 
 
 
 
 
 
 
        always @(*)
 
 
 
                `ASSERT((!f_cyc)||(!o_valid)||(o_wreg[3:1]!=3'h7));
 
 
 
 
 
 
 
`endif // FORMAL
 
endmodule
 
endmodule
 
 
 
//
 
 
 
//
 
 
 
// Usage (from yosys): (Before) (A,!OPTZ)       (A,OPTZ)
 
 
 
//      Cells:          302     314             391
 
 
 
//        FDRE          138     140             140
 
 
 
//        LUT1            2       2               2
 
 
 
//        LUT2           38      41              61
 
 
 
//        LUT3           13      16              33
 
 
 
//        LUT4            3       8              12
 
 
 
//        LUT5           22      10               8
 
 
 
//        LUT6           52      59              81
 
 
 
//        MUXCY           6       6               6
 
 
 
//        MUXF7          10      13              21
 
 
 
//        MUXF8           1       2              10
 
 
 
//        RAM64X1D        9       9               9
 
 
 
//        XORCY           8       8               8
 
 
 
//
 
 
 
//
 
 
 
 
 
 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.