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

Subversion Repositories zipcpu

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

Show entire file | Details | Blame | View Log

Rev 205 Rev 209
Line 17... Line 17...
// 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,2017-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 41... Line 41...
//
//
//
//
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
//
//
//
module  memops(i_clk, i_rst, i_stb, i_lock,
`default_nettype        none
 
//
 
module  memops(i_clk, i_reset, i_stb, i_lock,
                i_op, i_addr, i_data, i_oreg,
                i_op, i_addr, i_data, i_oreg,
                        o_busy, o_valid, o_err, o_wreg, o_result,
                        o_busy, 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, WITH_LOCAL_BUS=0;
`ifdef  FORMAL
 
                , f_nreqs, f_nacks, f_outstanding
 
`endif
 
                );
 
        parameter       ADDRESS_WIDTH=30;
 
        parameter [0:0]   IMPLEMENT_LOCK=1'b1,
 
                        WITH_LOCAL_BUS=1'b1,
 
                        OPT_ALIGNMENT_ERR=1'b1,
 
                        OPT_ZERO_ON_IDLE=1'b0;
        localparam      AW=ADDRESS_WIDTH;
        localparam      AW=ADDRESS_WIDTH;
        input                   i_clk, i_rst;
        input   wire            i_clk, i_reset;
        input                   i_stb, i_lock;
        input   wire            i_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  reg             o_valid;
        output  reg             o_valid;
        output  reg             o_err;
        output  reg             o_err;
        output  reg     [4:0]    o_wreg;
        output  reg     [4:0]    o_wreg;
Line 73... Line 83...
        output  reg             o_wb_we;
        output  reg             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 = 2;
 
`ifdef  FORMAL
 
        output  wire    [(F_LGDEPTH-1):0]        f_nreqs, f_nacks, f_outstanding;
 
`endif
 
 
 
        reg     misaligned;
 
 
 
        generate if (OPT_ALIGNMENT_ERR)
 
        begin : GENERATE_ALIGNMENT_ERR
 
                always @(*)
 
                casez({ i_op[2:1], i_addr[1:0] })
 
                4'b01?1: misaligned = i_stb; // Words must be halfword aligned
 
                4'b0110: misaligned = i_stb; // Words must be word aligned
 
                4'b10?1: misaligned = i_stb; // Halfwords must be aligned
 
                // 4'b11??: misaligned <= 1'b0; Byte access are never misaligned
 
                default: misaligned = 1'b0;
 
                endcase
 
        end else
 
                always @(*)     misaligned = 1'b0;
 
        endgenerate
 
 
        reg     r_wb_cyc_gbl, r_wb_cyc_lcl;
        reg     r_wb_cyc_gbl, r_wb_cyc_lcl;
        wire    gbl_stb, lcl_stb;
        wire    gbl_stb, lcl_stb;
        assign  lcl_stb = (i_stb)&&(WITH_LOCAL_BUS!=0)&&(i_addr[31:24]==8'hff);
        assign  lcl_stb = (i_stb)&&(WITH_LOCAL_BUS!=0)&&(i_addr[31:24]==8'hff)
        assign  gbl_stb = (i_stb)&&((WITH_LOCAL_BUS==0)||(i_addr[31:24]!=8'hff));
                                &&(!misaligned);
 
        assign  gbl_stb = (i_stb)&&((WITH_LOCAL_BUS==0)||(i_addr[31:24]!=8'hff))
 
                                &&(!misaligned);
 
 
        initial r_wb_cyc_gbl = 1'b0;
        initial r_wb_cyc_gbl = 1'b0;
        initial r_wb_cyc_lcl = 1'b0;
        initial r_wb_cyc_lcl = 1'b0;
        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;
                end else if ((r_wb_cyc_gbl)||(r_wb_cyc_lcl))
                end else if ((r_wb_cyc_gbl)||(r_wb_cyc_lcl))
                begin
                begin
                        if ((i_wb_ack)||(i_wb_err))
                        if ((i_wb_ack)||(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;
                        end
                        end
                end else if (i_stb) // New memory operation
        end else begin // New memory operation
                begin // Grab the wishbone
                // 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);
                end
                end
 
        initial o_wb_stb_gbl = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (o_wb_cyc_gbl)
        if (i_reset)
 
                o_wb_stb_gbl <= 1'b0;
 
        else if ((i_wb_err)&&(r_wb_cyc_gbl))
 
                o_wb_stb_gbl <= 1'b0;
 
        else if (o_wb_cyc_gbl)
                        o_wb_stb_gbl <= (o_wb_stb_gbl)&&(i_wb_stall);
                        o_wb_stb_gbl <= (o_wb_stb_gbl)&&(i_wb_stall);
                else
                else
                        o_wb_stb_gbl <= gbl_stb; // Grab wishbone on new operation
                // Grab wishbone on any new transaction to the gbl bus
 
                o_wb_stb_gbl <= (gbl_stb);
 
 
 
        initial o_wb_stb_lcl = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (o_wb_cyc_lcl)
        if (i_reset)
 
                o_wb_stb_lcl <= 1'b0;
 
        else if ((i_wb_err)&&(r_wb_cyc_lcl))
 
                o_wb_stb_lcl <= 1'b0;
 
        else if (o_wb_cyc_lcl)
                        o_wb_stb_lcl <= (o_wb_stb_lcl)&&(i_wb_stall);
                        o_wb_stb_lcl <= (o_wb_stb_lcl)&&(i_wb_stall);
                else
                else
                        o_wb_stb_lcl  <= lcl_stb; // Grab wishbone on new operation
                // Grab wishbone on any new transaction to the lcl bus
 
                o_wb_stb_lcl  <= (lcl_stb);
 
 
        reg     [3:0]    r_op;
        reg     [3:0]    r_op;
 
        initial o_wb_we   = 1'b0;
 
        initial o_wb_data = 0;
 
        initial o_wb_sel  = 0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (i_stb)
                if (i_stb)
                begin
                begin
                        o_wb_we   <= i_op[0];
                        o_wb_we   <= i_op[0];
 
                if (OPT_ZERO_ON_IDLE)
 
                begin
                        casez({ i_op[2:1], i_addr[1:0] })
                        casez({ i_op[2:1], i_addr[1:0] })
`ifdef  ZERO_ON_IDLE
 
                        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] };
`else
                        default: o_wb_data <= i_data;
 
                        endcase
 
                end else
 
                        casez({ i_op[2:1], i_addr[1:0] })
                        4'b10??: o_wb_data <= { (2){ i_data[15:0] } };
                        4'b10??: o_wb_data <= { (2){ i_data[15:0] } };
                        4'b11??: o_wb_data <= { (4){ i_data[7:0] } };
                        4'b11??: o_wb_data <= { (4){ i_data[7:0] } };
`endif
 
                        default: o_wb_data <= i_data;
                        default: o_wb_data <= i_data;
                        endcase
                        endcase
 
 
                        o_wb_addr <= i_addr[(AW+1):2];
                        o_wb_addr <= i_addr[(AW+1):2];
`ifdef  SET_SEL_ON_READ
 
                        if (i_op[0] == 1'b0)
 
                                o_wb_sel <= 4'hf;
 
                        else
 
`endif
 
                        casez({ i_op[2:1], i_addr[1:0] })
                        casez({ i_op[2:1], i_addr[1:0] })
                        4'b01??: o_wb_sel <= 4'b1111;
                        4'b01??: o_wb_sel <= 4'b1111;
                        4'b100?: o_wb_sel <= 4'b1100;
                        4'b100?: o_wb_sel <= 4'b1100;
                        4'b101?: o_wb_sel <= 4'b0011;
                        4'b101?: o_wb_sel <= 4'b0011;
                        4'b1100: o_wb_sel <= 4'b1000;
                        4'b1100: o_wb_sel <= 4'b1000;
Line 148... Line 195...
                        4'b1110: o_wb_sel <= 4'b0010;
                        4'b1110: o_wb_sel <= 4'b0010;
                        4'b1111: o_wb_sel <= 4'b0001;
                        4'b1111: o_wb_sel <= 4'b0001;
                        default: o_wb_sel <= 4'b1111;
                        default: o_wb_sel <= 4'b1111;
                        endcase
                        endcase
                        r_op <= { i_op[2:1] , i_addr[1:0] };
                        r_op <= { i_op[2:1] , i_addr[1:0] };
                end
        end else if ((OPT_ZERO_ON_IDLE)&&(!o_wb_cyc_gbl)&&(!o_wb_cyc_lcl))
`ifdef  ZERO_ON_IDLE
 
                else if ((!o_wb_cyc_gbl)&&(!o_wb_cyc_lcl))
 
                begin
                begin
                        o_wb_we   <= 1'b0;
                        o_wb_we   <= 1'b0;
                        o_wb_addr <= 0;
                        o_wb_addr <= 0;
                        o_wb_data <= 32'h0;
                        o_wb_data <= 32'h0;
                        o_wb_sel  <= 4'h0;
                        o_wb_sel  <= 4'h0;
                end
                end
`endif
 
 
 
        initial o_valid = 1'b0;
        initial o_valid = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                o_valid <= (!i_rst)&&((o_wb_cyc_gbl)||(o_wb_cyc_lcl))&&(i_wb_ack)&&(~o_wb_we);
        if (i_reset)
 
                o_valid <= 1'b0;
 
        else
 
                o_valid <= (((o_wb_cyc_gbl)||(o_wb_cyc_lcl))
 
                                &&(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 <= (!i_rst)&&((o_wb_cyc_gbl)||(o_wb_cyc_lcl))&&(i_wb_err);
        if (i_reset)
        assign  o_busy = (o_wb_cyc_gbl)||(o_wb_cyc_lcl);
                o_err <= 1'b0;
 
        else if ((r_wb_cyc_gbl)||(r_wb_cyc_lcl))
 
                o_err <= i_wb_err;
 
        else if ((i_stb)&&(!o_busy))
 
                o_err <= misaligned;
 
        else
 
                o_err <= 1'b0;
 
 
 
        assign  o_busy = (r_wb_cyc_gbl)||(r_wb_cyc_lcl);
 
 
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (i_stb)
                if (i_stb)
                        o_wreg    <= i_oreg;
                        o_wreg    <= i_oreg;
        always @(posedge i_clk)
        always @(posedge i_clk)
`ifdef  ZERO_ON_IDLE
        if ((OPT_ZERO_ON_IDLE)&&(!i_wb_ack))
                if (!i_wb_ack)
 
                        o_result <= 32'h0;
                        o_result <= 32'h0;
                else
        else begin
`endif
 
                casez(r_op)
                casez(r_op)
                4'b01??: o_result <= i_wb_data;
                4'b01??: o_result <= i_wb_data;
                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] };
                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] };
                default: o_result <= i_wb_data;
                default: o_result <= i_wb_data;
                endcase
                endcase
 
        end
 
 
 
        reg     lock_gbl, lock_lcl;
 
 
        generate
        generate
        if (IMPLEMENT_LOCK != 0)
        if (IMPLEMENT_LOCK != 0)
        begin
        begin
                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)
                begin
                begin
                        lock_gbl <= (i_lock)&&((r_wb_cyc_gbl)||(lock_gbl));
                        lock_gbl <= 1'b0;
                        lock_lcl <= (i_lock)&&((r_wb_cyc_lcl)||(lock_lcl));
                        lock_lcl <= 1'b0;
 
                end else if (((i_wb_err)&&((r_wb_cyc_gbl)||(r_wb_cyc_lcl)))
 
                                ||(misaligned))
 
                begin
 
                        // Kill the lock if
 
                        //      there's a bus error, or
 
                        //      User requests a misaligned memory op
 
                        lock_gbl <= 1'b0;
 
                        lock_lcl <= 1'b0;
 
                end else begin
 
                        // Kill the lock if
 
                        //      i_lock goes down
 
                        //      User starts on the global bus, then switches
 
                        //        to local or vice versa
 
                        lock_gbl <= (i_lock)&&((r_wb_cyc_gbl)||(lock_gbl))
 
                                        &&(!lcl_stb);
 
                        lock_lcl <= (i_lock)&&((r_wb_cyc_lcl)||(lock_lcl))
 
                                        &&(!gbl_stb);
                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);
 
 
 
                always @(*)
 
                        { lock_gbl, lock_lcl } = 2'b00;
 
 
 
                // Make verilator happy
 
                // verilator lint_off UNUSED
 
                wire    [2:0]    lock_unused;
 
                assign  lock_unused = { i_lock, lock_gbl, lock_lcl };
 
                // verilator lint_on  UNUSED
 
 
 
        end endgenerate
 
 
 
`ifdef  VERILATOR
 
        always @(posedge i_clk)
 
        if ((r_wb_cyc_gbl)||(r_wb_cyc_lcl))
 
                assert(!i_stb);
 
`endif
 
 
 
 
 
        // Make verilator happy
 
        // verilator lint_off UNUSED
 
        generate if (AW < 22)
 
        begin : TOO_MANY_ADDRESS_BITS
 
 
 
                wire    [(21-AW):0] unused_addr;
 
                assign  unused_addr = i_addr[23:(AW+2)];
 
 
 
        end endgenerate
 
        // verilator lint_on  UNUSED
 
 
 
`ifdef  FORMAL
 
`define ASSERT  assert
 
`ifdef  MEMOPS
 
`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_stb);
 
 
 
        wire    f_cyc, f_stb;
 
        assign  f_cyc = (o_wb_cyc_gbl)||(o_wb_cyc_lcl);
 
        assign  f_stb = (o_wb_stb_gbl)||(o_wb_stb_lcl);
 
 
 
`ifdef  MEMOPS
 
`define MASTER  fwb_master
 
`else
 
`define MASTER  fwb_counter
 
`endif
 
 
 
        fwb_master #(.AW(AW), .F_LGDEPTH(F_LGDEPTH),
 
                        .F_OPT_RMW_BUS_OPTION(IMPLEMENT_LOCK),
 
                        .F_OPT_DISCONTINUOUS(IMPLEMENT_LOCK))
 
                f_wb(i_clk, i_reset,
 
                        f_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);
 
 
 
 
 
        // Rule: Only one of the two CYC's may be valid, never both
 
        always @(posedge i_clk)
 
                `ASSERT((!o_wb_cyc_gbl)||(!o_wb_cyc_lcl));
 
 
 
        // Rule: Only one of the two STB's may be valid, never both
 
        always @(posedge i_clk)
 
                `ASSERT((!o_wb_stb_gbl)||(!o_wb_stb_lcl));
 
 
 
        // Rule: if WITH_LOCAL_BUS is ever false, neither the local STB nor CYC
 
        // may be valid
 
        always @(*)
 
                if (!WITH_LOCAL_BUS)
 
                begin
 
                        `ASSERT(!o_wb_cyc_lcl);
 
                        `ASSERT(!o_wb_stb_lcl);
 
                end
 
 
 
        // Rule: If the global CYC is ever true, the LCL one cannot be true
 
        // on the next clock without an intervening idle of both
 
        always @(posedge i_clk)
 
                if ((f_past_valid)&&($past(r_wb_cyc_gbl)))
 
                        `ASSERT(!r_wb_cyc_lcl);
 
 
 
        // Same for if the LCL CYC is true
 
        always @(posedge i_clk)
 
                if ((f_past_valid)&&($past(r_wb_cyc_lcl)))
 
                        `ASSERT(!r_wb_cyc_gbl);
 
 
 
        // STB can never be true unless CYC is also true
 
        always @(posedge i_clk)
 
                if (o_wb_stb_gbl)
 
                        `ASSERT(r_wb_cyc_gbl);
 
        always @(posedge i_clk)
 
                if (o_wb_stb_lcl)
 
                        `ASSERT(r_wb_cyc_lcl);
 
 
 
        // This core only ever has zero or one outstanding transaction(s)
 
        always @(posedge i_clk)
 
                if ((o_wb_stb_gbl)||(o_wb_stb_lcl))
 
                        `ASSERT(f_outstanding == 0);
 
                else
 
                        `ASSERT((f_outstanding == 0)||(f_outstanding == 1));
 
 
 
        // The LOCK function only allows up to two transactions (at most)
 
        // before CYC must be dropped.
 
        always @(posedge i_clk)
 
                if ((o_wb_stb_gbl)||(o_wb_stb_lcl))
 
                begin
 
                        if (IMPLEMENT_LOCK)
 
                                `ASSERT((f_outstanding == 0)||(f_outstanding == 1));
 
                        else
 
                                `ASSERT(f_nreqs <= 1);
 
                end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(o_busy))
 
        begin
 
 
 
                // If i_stb doesn't change, then neither do any of the other
 
                // inputs
 
                if (($past(i_stb))&&(i_stb))
 
                begin
 
                        `ASSUME($stable(i_op));
 
                        `ASSUME($stable(i_addr));
 
                        `ASSUME($stable(i_data));
 
                        `ASSUME($stable(i_oreg));
 
                        `ASSUME($stable(i_lock));
 
                end
 
 
 
 
 
                // No strobe's are allowed if a request is outstanding, either
 
                // having been accepted by the bus or waiting to be accepted
 
                // by the bus.
 
                if ((f_outstanding != 0)||(f_stb))
 
                        `ASSUME(!i_stb);
 
                /*
 
                if (o_busy)
 
                        assert( (!i_stb)
 
                                ||((!o_wb_stb_gbl)&&(!o_wb_stb_lcl)&&(i_lock)));
 
 
 
                if ((f_cyc)&&($past(f_cyc)))
 
                        assert($stable(r_op));
 
                */
 
        end
 
 
 
        always @(*)
 
                if (!IMPLEMENT_LOCK)
 
                        `ASSUME(!i_lock);
 
 
 
        always @(posedge i_clk)
 
                if ((f_past_valid)&&($past(f_cyc))&&($past(!i_lock)))
 
                        `ASSUME(!i_lock);
 
 
 
        // Following any i_stb request, assuming we are idle, immediately
 
        // begin a bus transaction
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(i_stb))
 
                &&(!$past(f_cyc))&&(!$past(i_reset)))
 
        begin
 
                if ($past(misaligned))
 
                begin
 
                        `ASSERT(!f_cyc);
 
                        `ASSERT(!o_busy);
 
                        `ASSERT(o_err);
 
                        `ASSERT(!o_valid);
 
                end else begin
 
                        `ASSERT(f_cyc);
 
                        `ASSERT(o_busy);
 
                end
 
        end
 
 
 
        always @(posedge i_clk)
 
        if (o_busy)
 
                `ASSUME(!i_stb);
 
 
 
        always @(posedge i_clk)
 
        if (o_wb_cyc_gbl)
 
                `ASSERT((o_busy)||(lock_gbl));
 
 
 
        always @(posedge i_clk)
 
        if (o_wb_cyc_lcl)
 
                `ASSERT((o_busy)||(lock_lcl));
 
 
 
        always @(posedge i_clk)
 
                if (f_outstanding > 0)
 
                        `ASSERT(o_busy);
 
 
 
        // If a transaction ends in an error, send o_err on the output port.
 
        always @(posedge i_clk)
 
                if (f_past_valid)
 
                begin
 
                        if ($past(i_reset))
 
                                `ASSERT(!o_err);
 
                        else if (($past(f_cyc))&&($past(i_wb_err)))
 
                                `ASSERT(o_err);
 
                        else if ($past(misaligned))
 
                                `ASSERT(o_err);
 
                end
 
 
 
        // Always following a successful ACK, return an O_VALID value.
 
        always @(posedge i_clk)
 
                if (f_past_valid)
 
                begin
 
                        if ($past(i_reset))
 
                                `ASSERT(!o_valid);
 
                        else if(($past(f_cyc))&&($past(i_wb_ack))
 
                                        &&(!$past(o_wb_we)))
 
                                `ASSERT(o_valid);
 
                        else if ($past(misaligned))
 
                                `ASSERT((!o_valid)&&(o_err));
 
                        else
 
                                `ASSERT(!o_valid);
 
                end
 
 
 
        //always @(posedge i_clk)
 
        //      if ((f_past_valid)&&($past(f_cyc))&&(!$past(o_wb_we))&&($past(i_wb_ack)))
 
 
 
        /*
 
        input   wire    [2:0]   i_op;
 
        input   wire    [31:0]  i_addr;
 
        input   wire    [31:0]  i_data;
 
        input   wire    [4:0]   i_oreg;
 
        // CPU outputs
 
        output  wire            o_busy;
 
        output  reg             o_valid;
 
        output  reg             o_err;
 
        output  reg     [4:0]   o_wreg;
 
        output  reg     [31:0]  o_result;
 
        */
 
 
 
        initial o_wb_we = 1'b0;
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_stb)))
 
        begin
 
                // On a write, assert o_wb_we should be true
 
                assert( $past(i_op[0]) == o_wb_we);
 
 
 
                // Word write
 
                if ($past(i_op[2:1]) == 2'b01)
 
                begin
 
                        `ASSERT(o_wb_sel == 4'hf);
 
                        `ASSERT(o_wb_data == $past(i_data));
 
                end
 
 
 
                // Halfword (short) write
 
                if ($past(i_op[2:1]) == 2'b10)
 
                begin
 
                        if (!$past(i_addr[1]))
 
                        begin
 
                                `ASSERT(o_wb_sel == 4'hc);
 
                                `ASSERT(o_wb_data[31:16] == $past(i_data[15:0]));
 
                        end else begin
 
                                `ASSERT(o_wb_sel == 4'h3);
 
                                `ASSERT(o_wb_data[15:0] == $past(i_data[15:0]));
 
                        end
 
                end
 
 
 
                if ($past(i_op[2:1]) == 2'b11)
 
                begin
 
                        if ($past(i_addr[1:0])==2'b00)
 
                        begin
 
                                `ASSERT(o_wb_sel == 4'h8);
 
                                `ASSERT(o_wb_data[31:24] == $past(i_data[7:0]));
 
                        end
 
 
 
                        if ($past(i_addr[1:0])==2'b01)
 
                        begin
 
                                `ASSERT(o_wb_sel == 4'h4);
 
                                `ASSERT(o_wb_data[23:16] == $past(i_data[7:0]));
 
                        end
 
                        if ($past(i_addr[1:0])==2'b10)
 
                        begin
 
                                `ASSERT(o_wb_sel == 4'h2);
 
                                `ASSERT(o_wb_data[15:8] == $past(i_data[7:0]));
 
                        end
 
                        if ($past(i_addr[1:0])==2'b11)
 
                        begin
 
                                `ASSERT(o_wb_sel == 4'h1);
 
                                `ASSERT(o_wb_data[7:0] == $past(i_data[7:0]));
 
                        end
 
                end
 
 
 
                `ASSUME($past(i_op[2:1] != 2'b00));
 
        end
 
 
 
        // This logic is fixed in the definitions of the lock(s) above
 
        // i.e., the user cna be stupid and this will still work
 
        /*
 
        always @(posedge i_clk)
 
                if ((i_lock)&&(i_stb)&&(WITH_LOCAL_BUS))
 
                begin
 
                        restrict((lock_gbl)||(i_addr[31:24] ==8'hff));
 
                        restrict((lock_lcl)||(i_addr[31:24]!==8'hff));
 
                end
 
        */
 
 
 
        always @(posedge i_clk)
 
                if (o_wb_stb_lcl)
 
                        `ASSERT(o_wb_addr[29:22] == 8'hff);
 
 
 
        always @(posedge i_clk)
 
                if ((f_past_valid)&&(!$past(i_reset))&&($past(misaligned)))
 
                begin
 
                        `ASSERT(!o_wb_cyc_gbl);
 
                        `ASSERT(!o_wb_cyc_lcl);
 
                        `ASSERT(!o_wb_stb_gbl);
 
                        `ASSERT(!o_wb_stb_lcl);
 
                        `ASSERT(o_err);
 
                        //OPT_ALIGNMENT_ERR=1'b0,
 
                        //OPT_ZERO_ON_IDLE=1'b0;
 
                end
 
 
 
        always @(posedge i_clk)
 
        if ((!f_past_valid)||($past(i_reset)))
 
                `ASSUME(!i_stb);
 
        always @(*)
 
        if (o_busy)
 
                `ASSUME(!i_stb);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(IMPLEMENT_LOCK)
 
                &&(!$past(i_reset))&&(!$past(i_wb_err))
 
                &&(!$past(misaligned))
 
                &&(!$past(lcl_stb))
 
                &&($past(i_lock))&&($past(lock_gbl)))
 
                assert(lock_gbl);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(IMPLEMENT_LOCK)
 
                        &&(!$past(i_reset))&&(!$past(i_wb_err))
 
                        &&(!$past(misaligned))
 
                        &&(!$past(lcl_stb))
 
                        &&($past(o_wb_cyc_gbl))&&($past(i_lock))
 
                        &&($past(lock_gbl)))
 
                assert(o_wb_cyc_gbl);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(IMPLEMENT_LOCK)
 
                        &&(!$past(i_reset))&&(!$past(i_wb_err))
 
                        &&(!$past(misaligned))
 
                        &&(!$past(gbl_stb))
 
                        &&($past(o_wb_cyc_lcl))&&($past(i_lock))
 
                        &&($past(lock_lcl)))
 
                assert(o_wb_cyc_lcl);
 
 
 
        //
 
        // Cover properties
 
        //
 
        always @(posedge i_clk)
 
                cover(i_wb_ack);
 
 
 
        // Cover a response on the same clock it is made
 
        always @(posedge i_clk)
 
                cover((o_wb_stb_gbl)&&(i_wb_ack));
 
 
 
        // Cover a response a clock later
 
        always @(posedge i_clk)
 
                cover((o_wb_stb_gbl)&&(i_wb_ack));
 
 
 
 
 
        generate if (WITH_LOCAL_BUS)
 
        begin
 
 
 
                // Same things on the local bus
 
                always @(posedge i_clk)
 
                        cover((o_wb_cyc_lcl)&&(!o_wb_stb_lcl)&&(i_wb_ack));
 
                always @(posedge i_clk)
 
                        cover((o_wb_stb_lcl)&&(i_wb_ack));
 
 
        end endgenerate
        end endgenerate
 
 
 
`endif
endmodule
endmodule
 
//
 
//
 
// Usage (from yosys):
 
//              (BFOR)  (!ZOI,ALIGN)    (ZOI,ALIGN)     (!ZOI,!ALIGN)
 
//      Cells    230            226             281             225
 
//        FDRE   114            116             116             116
 
//        LUT2    17             23              76              19
 
//        LUT3     9             23              17              20
 
//        LUT4    15              4              11              14
 
//        LUT5    18             18               7              15
 
//        LUT6    33             18              54              38
 
//        MUX7    16             12                               2
 
//        MUX8     8              1                               1
 
//
 
//
 
 
 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.