////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
// Filename: pipemem.v
|
// Filename: pipemem.v
|
//
|
//
|
// Project: Zip CPU -- a small, lightweight, RISC CPU soft core
|
// Project: Zip CPU -- a small, lightweight, RISC CPU soft core
|
//
|
//
|
// Purpose: A memory unit to support a CPU, this time one supporting
|
// Purpose: A memory unit to support a CPU, this time one supporting
|
// pipelined wishbone memory accesses. The goal is to be able
|
// pipelined wishbone memory accesses. The goal is to be able
|
// to issue one pipelined wishbone access per clock, and (given the memory
|
// to issue one pipelined wishbone access per clock, and (given the memory
|
// is fast enough) to be able to read the results back at one access per
|
// is fast enough) to be able to read the results back at one access per
|
// clock. This renders on-chip memory fast enough to handle single cycle
|
// clock. This renders on-chip memory fast enough to handle single cycle
|
// (pipelined) access.
|
// (pipelined) access.
|
//
|
//
|
//
|
//
|
// 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.
|
//
|
//
|
// This program is distributed in the hope that it will be useful, but WITHOUT
|
// This program is distributed in the hope that it will be useful, but WITHOUT
|
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
|
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
|
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
|
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
|
// for more details.
|
// for more details.
|
//
|
//
|
// You should have received a copy of the GNU General Public License along
|
// 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
|
// 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
|
// target there if the PDF file isn't present.) If not, see
|
// <http://www.gnu.org/licenses/> for a copy.
|
// <http://www.gnu.org/licenses/> for a copy.
|
//
|
//
|
// License: GPL, v3, as defined and found on www.gnu.org,
|
// License: GPL, v3, as defined and found on www.gnu.org,
|
// http://www.gnu.org/licenses/gpl.html
|
// http://www.gnu.org/licenses/gpl.html
|
//
|
//
|
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
//
|
//
|
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;
|
output reg [4:0] o_wreg;
|
output reg [4:0] o_wreg;
|
output reg [31:0] o_result;
|
output reg [31:0] o_result;
|
// Wishbone outputs
|
// Wishbone outputs
|
output wire o_wb_cyc_gbl;
|
output wire o_wb_cyc_gbl;
|
output reg o_wb_stb_gbl;
|
output reg o_wb_stb_gbl;
|
output wire o_wb_cyc_lcl;
|
output wire o_wb_cyc_lcl;
|
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
|
