411 lines
9.1 KiB
Coq
411 lines
9.1 KiB
Coq
|
// SPDX-License-Identifier: Apache-2.0
|
||
|
|
// Copyright 2019 Peter Gustavsson <peter.gustavsson@qamcom.se>
|
||
|
|
//
|
||
|
|
// Licensed under the Apache License, Version 2.0 (the "License");
|
||
|
|
// you may not use this file except in compliance with the License.
|
||
|
|
// You may obtain a copy of the License at
|
||
|
|
//
|
||
|
|
// http://www.apache.org/licenses/LICENSE-2.0
|
||
|
|
//
|
||
|
|
// Unless required by applicable law or agreed to in writing, software
|
||
|
|
// distributed under the License is distributed on an "AS IS" BASIS,
|
||
|
|
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||
|
|
// See the License for the specific language governing permissions and
|
||
|
|
// limitations under the License.
|
||
|
|
|
||
|
|
//********************************************************************************
|
||
|
|
// $Id$
|
||
|
|
//
|
||
|
|
// Function: AXI lite to Wishbone non pipelined bridge
|
||
|
|
// Comments: Assumes single accesses to a 32bit register on an 64bit aligned address
|
||
|
|
//
|
||
|
|
//********************************************************************************
|
||
|
|
|
||
|
|
`default_nettype none
|
||
|
|
module axi2wb
|
||
|
|
#(parameter AW = 12,
|
||
|
|
parameter IW = 0)
|
||
|
|
(
|
||
|
|
input wire i_clk,
|
||
|
|
input wire i_rst,
|
||
|
|
|
||
|
|
// Wishbone master
|
||
|
|
output reg [AW-1:2] o_wb_adr,
|
||
|
|
output reg [31:0] o_wb_dat,
|
||
|
|
output reg [3:0] o_wb_sel,
|
||
|
|
output reg o_wb_we,
|
||
|
|
output reg o_wb_cyc,
|
||
|
|
output reg o_wb_stb,
|
||
|
|
|
||
|
|
input wire [31:0] i_wb_rdt,
|
||
|
|
input wire i_wb_ack,
|
||
|
|
input wire i_wb_err,
|
||
|
|
|
||
|
|
// AXI slave
|
||
|
|
// AXI adress write channel
|
||
|
|
input wire [AW-1:0] i_awaddr,
|
||
|
|
input wire [IW-1:0] i_awid,
|
||
|
|
input wire i_awvalid,
|
||
|
|
output reg o_awready,
|
||
|
|
//AXI adress read channel
|
||
|
|
input wire [AW-1:0] i_araddr,
|
||
|
|
input wire [IW-1:0] i_arid,
|
||
|
|
input wire i_arvalid,
|
||
|
|
output reg o_arready,
|
||
|
|
//AXI write channel
|
||
|
|
input wire [63:0] i_wdata,
|
||
|
|
input wire [7:0] i_wstrb,
|
||
|
|
input wire i_wvalid,
|
||
|
|
output reg o_wready,
|
||
|
|
//AXI response channel
|
||
|
|
output reg [IW-1:0] o_bid,
|
||
|
|
output wire [1:0] o_bresp,
|
||
|
|
output reg o_bvalid,
|
||
|
|
input wire i_bready,
|
||
|
|
//AXI read channel
|
||
|
|
output reg [63:0] o_rdata,
|
||
|
|
output reg [IW-1:0] o_rid,
|
||
|
|
output wire [1:0] o_rresp,
|
||
|
|
output wire o_rlast,
|
||
|
|
output reg o_rvalid,
|
||
|
|
input wire i_rready
|
||
|
|
);
|
||
|
|
|
||
|
|
assign o_bresp = 2'b00;
|
||
|
|
assign o_rresp = 2'b00;
|
||
|
|
assign o_rlast = 1'b1;
|
||
|
|
|
||
|
|
reg hi_32b_w;
|
||
|
|
reg arbiter;
|
||
|
|
reg [31:0] wb_rdt_low;
|
||
|
|
|
||
|
|
|
||
|
|
parameter STATESIZE = 4;
|
||
|
|
|
||
|
|
parameter [STATESIZE-1:0]
|
||
|
|
IDLE = 4'd0,
|
||
|
|
AWACK = 4'd1,
|
||
|
|
WBWACK= 4'd2,
|
||
|
|
WBRACK1 = 4'd3,
|
||
|
|
WBR2 = 4'd4,
|
||
|
|
WBRACK2 = 4'd5,
|
||
|
|
BAXI = 4'd6,
|
||
|
|
RRAXI = 4'd7;
|
||
|
|
|
||
|
|
reg [STATESIZE-1:0] cs;
|
||
|
|
|
||
|
|
// formal helper registers
|
||
|
|
reg aw_req;
|
||
|
|
reg w_req;
|
||
|
|
reg ar_req;
|
||
|
|
|
||
|
|
|
||
|
|
initial o_rvalid = 1'b0;
|
||
|
|
initial o_bvalid = 1'b0;
|
||
|
|
initial o_wb_stb = 1'b0;
|
||
|
|
initial o_wb_cyc = 1'b0;
|
||
|
|
initial o_wb_we = 1'b0;
|
||
|
|
initial cs = 4'd0;
|
||
|
|
initial aw_req = 1'b0;
|
||
|
|
initial w_req = 1'b0;
|
||
|
|
initial ar_req = 1'b0;
|
||
|
|
|
||
|
|
|
||
|
|
always @(posedge i_clk) begin
|
||
|
|
if (i_rst) begin
|
||
|
|
o_awready <= 1'b0;
|
||
|
|
o_wready <= 1'b0;
|
||
|
|
o_arready <= 1'b0;
|
||
|
|
o_rvalid <= 1'b0;
|
||
|
|
o_bvalid <= 1'b0;
|
||
|
|
o_wb_adr <= {AW-2{1'b0}};
|
||
|
|
o_wb_cyc <= 1'b0;
|
||
|
|
o_wb_stb <= 1'b0;
|
||
|
|
o_wb_sel <= 4'd0;
|
||
|
|
o_wb_we <= 1'b0;
|
||
|
|
arbiter <= 1'b1;
|
||
|
|
wb_rdt_low <= 32'hDEADBEEF;
|
||
|
|
cs <= IDLE;
|
||
|
|
|
||
|
|
aw_req <= 1'b0;
|
||
|
|
w_req <= 1'b0;
|
||
|
|
ar_req <= 1'b0;
|
||
|
|
o_bid <= {IW{1'b0}};
|
||
|
|
o_rid <= {IW{1'b0}};
|
||
|
|
|
||
|
|
end
|
||
|
|
else begin
|
||
|
|
if (i_awvalid & o_awready)
|
||
|
|
o_bid <= i_awid;
|
||
|
|
|
||
|
|
if (i_arvalid & o_arready)
|
||
|
|
o_rid <= i_arid;
|
||
|
|
|
||
|
|
o_awready <= 1'b0;
|
||
|
|
o_wready <= 1'b0;
|
||
|
|
o_arready <= 1'b0;
|
||
|
|
|
||
|
|
if (i_awvalid && o_awready)
|
||
|
|
aw_req <= 1'b1;
|
||
|
|
else if (i_bready && o_bvalid)
|
||
|
|
aw_req <= 1'b0;
|
||
|
|
|
||
|
|
if (i_wvalid && o_wready)
|
||
|
|
w_req <= 1'b1;
|
||
|
|
else if (i_bready && o_bvalid)
|
||
|
|
w_req <= 1'b0;
|
||
|
|
|
||
|
|
if (i_arvalid && o_arready)
|
||
|
|
ar_req <= 1'b1;
|
||
|
|
else if (i_rready && o_rvalid)
|
||
|
|
ar_req <= 1'b0;
|
||
|
|
|
||
|
|
case (cs)
|
||
|
|
IDLE : begin
|
||
|
|
arbiter <= 1'b1;
|
||
|
|
if (i_awvalid && arbiter) begin
|
||
|
|
o_wb_adr[AW-1:3] <= i_awaddr[AW-1:3];
|
||
|
|
o_awready <= 1'b1;
|
||
|
|
arbiter <= 1'b0;
|
||
|
|
if (i_wvalid) begin
|
||
|
|
hi_32b_w = (i_wstrb[3:0] == 4'h0) ? 1'b1 : 1'b0;
|
||
|
|
o_wb_adr[2] <= hi_32b_w;
|
||
|
|
o_wb_cyc <= 1'b1;
|
||
|
|
o_wb_stb <= 1'b1;
|
||
|
|
o_wb_sel <= hi_32b_w ? i_wstrb[7:4] : i_wstrb[3:0];
|
||
|
|
o_wb_dat <= hi_32b_w ? i_wdata[63:32] : i_wdata[31:0];
|
||
|
|
o_wb_we <= 1'b1;
|
||
|
|
o_wready <= 1'b1;
|
||
|
|
cs <= WBWACK;
|
||
|
|
end
|
||
|
|
else begin
|
||
|
|
cs <= AWACK;
|
||
|
|
end
|
||
|
|
end
|
||
|
|
else if (i_arvalid) begin
|
||
|
|
o_wb_adr[AW-1:2] <= i_araddr[AW-1:2];
|
||
|
|
o_wb_sel <= 4'hF;
|
||
|
|
o_wb_cyc <= 1'b1;
|
||
|
|
o_wb_stb <= 1'b1;
|
||
|
|
o_arready <= 1'b1;
|
||
|
|
cs <= WBRACK1;
|
||
|
|
end
|
||
|
|
end
|
||
|
|
|
||
|
|
AWACK : begin
|
||
|
|
if (i_wvalid) begin
|
||
|
|
hi_32b_w = (i_wstrb[3:0] == 4'h0) ? 1'b1 : 1'b0;
|
||
|
|
o_wb_adr[2] <= hi_32b_w;
|
||
|
|
o_wb_cyc <= 1'b1;
|
||
|
|
o_wb_stb <= 1'b1;
|
||
|
|
o_wb_sel <= hi_32b_w ? i_wstrb[7:4] : i_wstrb[3:0];
|
||
|
|
o_wb_dat <= hi_32b_w ? i_wdata[63:32] : i_wdata[31:0];
|
||
|
|
o_wb_we <= 1'b1;
|
||
|
|
o_wready <= 1'b1;
|
||
|
|
cs <= WBWACK;
|
||
|
|
end
|
||
|
|
end
|
||
|
|
|
||
|
|
WBWACK : begin
|
||
|
|
if ( i_wb_err || i_wb_ack ) begin
|
||
|
|
o_wb_cyc <= 1'b0;
|
||
|
|
o_wb_stb <= 1'b0;
|
||
|
|
o_wb_sel <= 4'h0;
|
||
|
|
o_wb_we <= 1'b0;
|
||
|
|
o_bvalid <= 1'b1;
|
||
|
|
cs <= BAXI;
|
||
|
|
end
|
||
|
|
end
|
||
|
|
|
||
|
|
WBRACK1 : begin
|
||
|
|
if ( i_wb_err || i_wb_ack) begin
|
||
|
|
o_wb_cyc <= 1'b0;
|
||
|
|
o_wb_stb <= 1'b0;
|
||
|
|
o_wb_sel <= 4'h0;
|
||
|
|
wb_rdt_low <= i_wb_rdt;
|
||
|
|
cs <= WBR2;
|
||
|
|
end
|
||
|
|
end
|
||
|
|
|
||
|
|
WBR2 : begin
|
||
|
|
o_wb_adr[2] <= 1'b1;
|
||
|
|
o_wb_sel <= 4'hF;
|
||
|
|
o_wb_cyc <= 1'b1;
|
||
|
|
o_wb_stb <= 1'b1;
|
||
|
|
cs <= WBRACK2;
|
||
|
|
end
|
||
|
|
|
||
|
|
|
||
|
|
WBRACK2 : begin
|
||
|
|
if ( i_wb_err || i_wb_ack) begin
|
||
|
|
o_wb_cyc <= 1'b0;
|
||
|
|
o_wb_stb <= 1'b0;
|
||
|
|
o_wb_sel <= 4'h0;
|
||
|
|
o_rvalid <= 1'b1;
|
||
|
|
o_rdata <= {i_wb_rdt, wb_rdt_low};
|
||
|
|
cs <= RRAXI;
|
||
|
|
end
|
||
|
|
end
|
||
|
|
|
||
|
|
BAXI : begin
|
||
|
|
o_bvalid <= 1'b1;
|
||
|
|
if (i_bready) begin
|
||
|
|
o_bvalid <= 1'b0;
|
||
|
|
cs <= IDLE;
|
||
|
|
end
|
||
|
|
end
|
||
|
|
|
||
|
|
RRAXI : begin
|
||
|
|
o_rvalid <= 1'b1;
|
||
|
|
if (i_rready) begin
|
||
|
|
o_rvalid <= 1'b0;
|
||
|
|
cs <= IDLE;
|
||
|
|
end
|
||
|
|
end
|
||
|
|
|
||
|
|
default : begin
|
||
|
|
o_awready <= 1'b0;
|
||
|
|
o_wready <= 1'b0;
|
||
|
|
o_arready <= 1'b0;
|
||
|
|
o_rvalid <= 1'b0;
|
||
|
|
o_bvalid <= 1'b0;
|
||
|
|
o_wb_adr <= {AW-2{1'b0}};
|
||
|
|
o_wb_cyc <= 1'b0;
|
||
|
|
o_wb_stb <= 1'b0;
|
||
|
|
o_wb_sel <= 4'd0;
|
||
|
|
o_wb_we <= 1'b0;
|
||
|
|
arbiter <= 1'b1;
|
||
|
|
cs <= IDLE;
|
||
|
|
end
|
||
|
|
endcase
|
||
|
|
end
|
||
|
|
end
|
||
|
|
|
||
|
|
`ifdef FORMAL
|
||
|
|
localparam F_LGDEPTH = 4;
|
||
|
|
|
||
|
|
wire [(F_LGDEPTH-1):0] faxi_awr_outstanding,
|
||
|
|
faxi_wr_outstanding,
|
||
|
|
faxi_rd_outstanding;
|
||
|
|
|
||
|
|
|
||
|
|
faxil_slave
|
||
|
|
#(
|
||
|
|
.C_AXI_DATA_WIDTH(64),
|
||
|
|
.C_AXI_ADDR_WIDTH(AW),
|
||
|
|
.F_OPT_BRESP (1'b1),
|
||
|
|
.F_OPT_RRESP (1'b1),
|
||
|
|
.F_AXI_MAXWAIT (16),
|
||
|
|
.F_AXI_MAXDELAY (4),
|
||
|
|
.F_AXI_MAXRSTALL (1),
|
||
|
|
.F_LGDEPTH(F_LGDEPTH))
|
||
|
|
faxil_slave
|
||
|
|
(
|
||
|
|
.i_clk(i_clk),
|
||
|
|
.i_axi_reset_n(~i_rst),
|
||
|
|
//
|
||
|
|
.i_axi_awaddr(i_awaddr),
|
||
|
|
.i_axi_awcache(4'h0),
|
||
|
|
.i_axi_awprot(3'd0),
|
||
|
|
.i_axi_awvalid(i_awvalid),
|
||
|
|
.i_axi_awready(o_awready),
|
||
|
|
//
|
||
|
|
.i_axi_wdata(i_wdata),
|
||
|
|
.i_axi_wstrb(i_wstrb),
|
||
|
|
.i_axi_wvalid(i_wvalid),
|
||
|
|
.i_axi_wready(o_wready),
|
||
|
|
//
|
||
|
|
.i_axi_bresp(2'd0),
|
||
|
|
.i_axi_bvalid(o_bvalid),
|
||
|
|
.i_axi_bready(i_bready),
|
||
|
|
//
|
||
|
|
.i_axi_araddr(i_araddr),
|
||
|
|
.i_axi_arprot(3'd0),
|
||
|
|
.i_axi_arcache(4'h0),
|
||
|
|
.i_axi_arvalid(i_arvalid),
|
||
|
|
.i_axi_arready(o_arready),
|
||
|
|
//
|
||
|
|
.i_axi_rdata(o_rdata),
|
||
|
|
.i_axi_rresp(2'd0),
|
||
|
|
.i_axi_rvalid(o_rvalid),
|
||
|
|
.i_axi_rready(i_rready),
|
||
|
|
//
|
||
|
|
.f_axi_rd_outstanding(faxi_rd_outstanding),
|
||
|
|
.f_axi_wr_outstanding(faxi_wr_outstanding),
|
||
|
|
.f_axi_awr_outstanding(faxi_awr_outstanding));
|
||
|
|
|
||
|
|
|
||
|
|
always @(*) begin
|
||
|
|
|
||
|
|
assert(faxi_awr_outstanding <= 1);
|
||
|
|
assert(faxi_wr_outstanding <= 1);
|
||
|
|
assert(faxi_rd_outstanding <= 1);
|
||
|
|
|
||
|
|
case (cs)
|
||
|
|
IDLE : begin
|
||
|
|
assert(!o_wb_we);
|
||
|
|
assert(!o_wb_stb);
|
||
|
|
assert(!o_wb_cyc);
|
||
|
|
assert(!aw_req);
|
||
|
|
assert(!ar_req);
|
||
|
|
assert(!w_req);
|
||
|
|
assert(faxi_awr_outstanding == 0);
|
||
|
|
assert(faxi_wr_outstanding == 0);
|
||
|
|
assert(faxi_rd_outstanding == 0);
|
||
|
|
end
|
||
|
|
AWACK : begin
|
||
|
|
assert(!o_wb_we);
|
||
|
|
assert(!o_wb_stb);
|
||
|
|
assert(!o_wb_cyc);
|
||
|
|
assert(faxi_awr_outstanding == (aw_req ? 1:0));
|
||
|
|
assert(faxi_wr_outstanding == 0);
|
||
|
|
assert(faxi_rd_outstanding == 0);
|
||
|
|
end
|
||
|
|
WBWACK : begin
|
||
|
|
assert(faxi_awr_outstanding == (aw_req ? 1:0));
|
||
|
|
assert(faxi_wr_outstanding == (w_req ? 1:0));
|
||
|
|
assert(faxi_rd_outstanding == 0);
|
||
|
|
end
|
||
|
|
WBRACK : begin
|
||
|
|
assert(faxi_awr_outstanding == 0);
|
||
|
|
assert(faxi_wr_outstanding == 0);
|
||
|
|
assert(faxi_rd_outstanding == (ar_req ? 1:0));
|
||
|
|
end
|
||
|
|
BAXI : begin
|
||
|
|
assert(faxi_rd_outstanding == 0);
|
||
|
|
end
|
||
|
|
RRAXI : begin
|
||
|
|
assert(faxi_awr_outstanding == 0);
|
||
|
|
assert(faxi_wr_outstanding == 0);
|
||
|
|
end
|
||
|
|
|
||
|
|
default:
|
||
|
|
assert(0);
|
||
|
|
endcase // case (cs)
|
||
|
|
end
|
||
|
|
|
||
|
|
fwbc_master
|
||
|
|
#(.AW (AW-2),
|
||
|
|
.DW (32),
|
||
|
|
.F_MAX_DELAY (4),
|
||
|
|
.OPT_BUS_ABORT (0))
|
||
|
|
fwbc_master
|
||
|
|
(.i_clk (i_clk),
|
||
|
|
.i_reset (i_rst),
|
||
|
|
.i_wb_addr (o_wb_adr),
|
||
|
|
.i_wb_data (o_wb_dat),
|
||
|
|
.i_wb_sel (o_wb_sel),
|
||
|
|
.i_wb_we (o_wb_we),
|
||
|
|
.i_wb_cyc (o_wb_cyc),
|
||
|
|
.i_wb_stb (o_wb_stb),
|
||
|
|
.i_wb_cti (3'd0),
|
||
|
|
.i_wb_bte (2'd0),
|
||
|
|
.i_wb_idata (i_wb_rdt),
|
||
|
|
.i_wb_ack (i_wb_ack),
|
||
|
|
.i_wb_err (i_wb_err),
|
||
|
|
.i_wb_rty (1'b0));
|
||
|
|
|
||
|
|
`endif
|
||
|
|
endmodule
|
||
|
|
`default_nettype wire
|