Skip to content

Instantly share code, notes, and snippets.

@ZipCPU

ZipCPU/wb2axi_v0.v

Created August 29, 2019 23:41
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save ZipCPU/18f337eb4d29f2eebd44561a5b9f1f47 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save ZipCPU/18f337eb4d29f2eebd44561a5b9f1f47 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
wb2axi_v0.v
// This is the core as it was originally given to me, and without any modifications
//
//
module wb2axi
(
input wire i_clk,
input wire i_rst,
input wire [31:0] i_wb_adr,
input wire [31:0] i_wb_dat,
input wire [3:0] i_wb_sel,
input wire i_wb_we,
input wire i_wb_cyc,
input wire i_wb_stb,
output wire [31:0] o_wb_rdt,
output wire o_wb_ack,
output wire [31:0] o_awaddr,
output wire o_awvalid,
input wire i_awready,
output wire [31:0] o_araddr,
output wire o_arvalid,
input wire i_arready,
output wire [63:0] o_wdata,
output wire [7:0] o_wstrb,
output wire o_wvalid,
input wire i_wready,
input wire i_bvalid,
output reg o_bready = 1'b1,
input wire [63:0] i_rdata,
input wire i_rvalid,
output reg o_rready = 1'b1);
reg awdone = 1'b0;
reg ardone = 1'b0;
reg wdone = 1'b0;
reg bdone = 1'b0;
reg rdone = 1'b0;
localparam [1:0]
IDLE = 2'd0,
WRITE = 2'd1,
READ = 2'd2;
reg [1:0] state = IDLE;
assign o_awaddr = {i_wb_adr[31:3], 3'b000};
assign o_awvalid = (state == WRITE) & !awdone;
assign o_araddr = {i_wb_adr[31:3], 3'b000};
assign o_arvalid = (state == READ) & !ardone;
assign o_wdata = {i_wb_dat, i_wb_dat};
assign o_wstrb = i_wb_adr[2] ? {i_wb_sel,4'd0} : {4'd0, i_wb_sel};
assign o_wvalid = (state == WRITE) & !wdone;
assign o_wb_rdt = i_wb_adr[2] ? i_rdata[63:32] : i_rdata[31:0];
assign o_wb_ack = (state != IDLE) && ((awdone & wdone & bdone) | (ardone & rdone));
always @(posedge i_clk) begin
if (state == IDLE) begin
awdone <= 1'b0;
ardone <= 1'b0;
wdone <= 1'b0;
bdone <= 1'b0;
rdone <= 1'b0;
end
if (o_awvalid & i_awready)
awdone <= 1'b1;
if (o_arvalid & i_arready)
ardone <= 1'b1;
if (o_wvalid & i_wready)
wdone <= 1'b1;
if (i_bvalid & o_bready)
bdone <= 1'b1;
if (i_rvalid & o_rready)
rdone <= 1'b1;
case(state)
IDLE: begin
if (i_wb_cyc & i_wb_stb)
state <= i_wb_we ? WRITE : READ;
end
WRITE:
if (awdone & wdone & bdone)
state <= IDLE;
READ:
if (ardone & rdone)
state <= IDLE;
endcase
if (i_rst) begin
state <= IDLE;
awdone <= 1'b0;
ardone <= 1'b0;
wdone <= 1'b0;
bdone <= 1'b0;
rdone <= 1'b0;
end
end // always @ (posedge i_clk)
`ifdef FORMAL
faxil_master
#(
.C_AXI_DATA_WIDTH (64),
.C_AXI_ADDR_WIDTH (28),
.F_OPT_ASSUME_RESET (1),
.F_OPT_BRESP (1'b0),
.F_OPT_RRESP (1'b0),
.F_AXI_MAXWAIT (4),
.F_AXI_MAXDELAY (4),
.F_AXI_MAXRSTALL (1),
.F_LGDEPTH (2))
faxil_master
(
.i_clk (i_clk),
.i_axi_reset_n (~i_rst),
.i_axi_awready (i_awready),
.i_axi_awaddr (o_awaddr),
.i_axi_awcache (4'h0),
.i_axi_awprot (3'd0),
.i_axi_awvalid (o_awvalid),
.i_axi_wready (i_wready),
.i_axi_wdata (o_wdata),
.i_axi_wstrb (o_wstrb),
.i_axi_wvalid (o_wvalid),
.i_axi_bresp (2'd0),
.i_axi_bvalid (i_bvalid),
.i_axi_bready (o_bready),
.i_axi_arready (i_arready),
.i_axi_araddr (o_araddr),
.i_axi_arcache (4'h0),
.i_axi_arprot (3'd0),
.i_axi_arvalid (o_arvalid),
.i_axi_rresp (2'd0),
.i_axi_rvalid (i_rvalid),
.i_axi_rdata (i_rdata),
.i_axi_rready (o_rready),
.f_axi_rd_outstanding (),
.f_axi_wr_outstanding (),
.f_axi_awr_outstanding ());
fwbc_slave
#(.AW (32),
.F_MAX_DELAY (10),
.OPT_BUS_ABORT (0))
fwbc_slave
(.i_clk (i_clk),
.i_reset (i_rst),
.i_wb_addr (i_wb_adr),
.i_wb_data (i_wb_dat),
.i_wb_sel (i_wb_sel),
.i_wb_we (i_wb_we),
.i_wb_cyc (i_wb_cyc),
.i_wb_stb (i_wb_stb),
.i_wb_cti (3'd0),
.i_wb_bte (2'd0),
.i_wb_idata (o_wb_rdt),
.i_wb_ack (o_wb_ack),
.i_wb_err (1'b0),
.i_wb_rty (1'b0));
`endif
endmodule
Raw
wb2axi_v1.v
// This is the original logic, but properties adjusted until the proof passes, and passes induction
//
// This one still as the o_wb_rdt bug, where return values may have garbage in them
//
`default_nettype none
module wb2axi
(
input wire i_clk,
input wire i_rst,
input wire [31:0] i_wb_adr,
input wire [31:0] i_wb_dat,
input wire [3:0] i_wb_sel,
input wire i_wb_we,
input wire i_wb_cyc,
input wire i_wb_stb,
output wire [31:0] o_wb_rdt,
output wire o_wb_ack,
output wire [31:0] o_awaddr,
output wire o_awvalid,
input wire i_awready,
output wire [31:0] o_araddr,
output wire o_arvalid,
input wire i_arready,
output wire [63:0] o_wdata,
output wire [7:0] o_wstrb,
output wire o_wvalid,
input wire i_wready,
input wire i_bvalid,
output reg o_bready = 1'b1,
input wire [63:0] i_rdata,
input wire i_rvalid,
output reg o_rready = 1'b1);
reg awdone = 1'b0;
reg ardone = 1'b0;
reg wdone = 1'b0;
reg bdone = 1'b0;
reg rdone = 1'b0;
localparam [1:0]
IDLE = 2'd0,
WRITE = 2'd1,
READ = 2'd2;
reg [1:0] state = IDLE;
assign o_awaddr = {i_wb_adr[31:3], 3'b000};
assign o_awvalid = (state == WRITE) & !awdone;
assign o_araddr = {i_wb_adr[31:3], 3'b000};
assign o_arvalid = (state == READ) & !ardone;
assign o_wdata = {i_wb_dat, i_wb_dat};
assign o_wstrb = i_wb_adr[2] ? {i_wb_sel,4'd0} : {4'd0, i_wb_sel};
assign o_wvalid = (state == WRITE) & !wdone;
assign o_wb_rdt = i_wb_adr[2] ? i_rdata[63:32] : i_rdata[31:0];
assign o_wb_ack = (state != IDLE) && ((awdone & wdone & bdone) | (ardone & rdone));
always @(posedge i_clk) begin
if (state == IDLE) begin
awdone <= 1'b0;
ardone <= 1'b0;
wdone <= 1'b0;
bdone <= 1'b0;
rdone <= 1'b0;
end
if (o_awvalid & i_awready)
awdone <= 1'b1;
if (o_arvalid & i_arready)
ardone <= 1'b1;
if (o_wvalid & i_wready)
wdone <= 1'b1;
if (i_bvalid & o_bready)
bdone <= 1'b1;
if (i_rvalid & o_rready)
rdone <= 1'b1;
case(state)
IDLE: begin
if (i_wb_cyc & i_wb_stb)
state <= i_wb_we ? WRITE : READ;
end
WRITE:
if (awdone & wdone & bdone)
state <= IDLE;
READ:
if (ardone & rdone)
state <= IDLE;
endcase
if (i_rst) begin
state <= IDLE;
awdone <= 1'b0;
ardone <= 1'b0;
wdone <= 1'b0;
bdone <= 1'b0;
rdone <= 1'b0;
end
end // always @ (posedge i_clk)
`ifdef FORMAL
localparam F_LGDEPTH = 5;
wire [F_LGDEPTH-1:0] faxi_awr_outstanding, faxi_wr_outstanding, faxi_rd_outstanding;
faxil_master
#(
.C_AXI_DATA_WIDTH (64),
.C_AXI_ADDR_WIDTH (28),
.F_OPT_ASSUME_RESET (1),
.F_OPT_BRESP (1'b0),
.F_OPT_RRESP (1'b0),
.F_AXI_MAXWAIT (4),
.F_AXI_MAXDELAY (4),
.F_AXI_MAXRSTALL (1),
.F_LGDEPTH (5))
faxil_master
(
.i_clk (i_clk),
.i_axi_reset_n (~i_rst),
.i_axi_awready (i_awready),
.i_axi_awaddr (o_awaddr),
.i_axi_awcache (4'h0),
.i_axi_awprot (3'd0),
.i_axi_awvalid (o_awvalid),
.i_axi_wready (i_wready),
.i_axi_wdata (o_wdata),
.i_axi_wstrb (o_wstrb),
.i_axi_wvalid (o_wvalid),
.i_axi_bresp (2'd0),
.i_axi_bvalid (i_bvalid),
.i_axi_bready (o_bready),
.i_axi_arready (i_arready),
.i_axi_araddr (o_araddr),
.i_axi_arcache (4'h0),
.i_axi_arprot (3'd0),
.i_axi_arvalid (o_arvalid),
.i_axi_rresp (2'd0),
.i_axi_rvalid (i_rvalid),
.i_axi_rdata (i_rdata),
.i_axi_rready (o_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(o_rready);
assert(o_bready);
assert(faxi_awr_outstanding <= 1);
assert(faxi_wr_outstanding <= 1);
assert(faxi_rd_outstanding <= 1);
case(state)
IDLE: begin
assert(!o_wb_ack);
assert(faxi_awr_outstanding == 0);
assert(faxi_wr_outstanding == 0);
assert(faxi_rd_outstanding == 0);
end
READ: begin
assert(i_wb_stb);
assert(!i_wb_we);
assert(!awdone);
assert(!wdone);
assert(!bdone);
assert(faxi_awr_outstanding == 0);
assert(faxi_wr_outstanding == 0);
assert(faxi_rd_outstanding == ((ardone && !rdone) ? 1:0));
end
WRITE: begin
assert(i_wb_stb);
assert(i_wb_we);
assert(!ardone);
assert(!rdone);
assert(faxi_awr_outstanding == ((awdone && !bdone) ? 1:0));
assert(faxi_wr_outstanding == (( wdone && !bdone) ? 1:0));
assert(faxi_rd_outstanding == 0);
end
default:
assert(0);
endcase
end
fwbc_slave
#(.AW (32),
.F_MAX_DELAY (10),
.OPT_BUS_ABORT (0))
fwbc_slave
(.i_clk (i_clk),
.i_reset (i_rst),
.i_wb_addr (i_wb_adr),
.i_wb_data (i_wb_dat),
.i_wb_sel (i_wb_sel),
.i_wb_we (i_wb_we),
.i_wb_cyc (i_wb_cyc),
.i_wb_stb (i_wb_stb),
.i_wb_cti (3'd0),
.i_wb_bte (2'd0),
.i_wb_idata (o_wb_rdt),
.i_wb_ack (o_wb_ack),
.i_wb_err (1'b0),
.i_wb_rty (1'b0));
reg f_past_valid;
initial f_past_valid = 0;
always @(posedge i_clk)
f_past_valid <= 1;
// This *should* be part of the fwbc_* properties ...
always @(posedge i_clk)
if (f_past_valid && $past(!i_rst && i_wb_stb && !o_wb_ack))
begin
assume($stable(i_wb_stb));
assume($stable(i_wb_we));
assume($stable(i_wb_adr));
assume($stable(i_wb_dat));
assume($stable(i_wb_sel));
end
reg [2:0] count_writes, count_reads;
initial count_writes = 0;
always @(posedge i_clk)
if (i_rst)
count_writes <= 0;
else if (o_wb_ack && bdone && !(&count_writes))
count_writes <= count_writes + 1;
initial count_reads = 0;
always @(posedge i_clk)
if (i_rst)
count_reads <= 0;
else if (o_wb_ack && rdone && !(&count_writes))
count_reads <= count_reads + 1;
always @(*)
cover(count_writes == 3'h3);
always @(*)
cover(count_reads == 3'h3);
`endif
endmodule
Raw
wb2axi_v2.v
`default_nettype none
module wb2axi
(
input wire i_clk,
input wire i_rst,
input wire [31:0] i_wb_adr,
input wire [31:0] i_wb_dat,
input wire [3:0] i_wb_sel,
input wire i_wb_we,
input wire i_wb_cyc,
input wire i_wb_stb,
output wire [31:0] o_wb_rdt,
output wire o_wb_ack,
output wire [31:0] o_awaddr,
output wire o_awvalid,
input wire i_awready,
output wire [31:0] o_araddr,
output wire o_arvalid,
input wire i_arready,
output wire [63:0] o_wdata,
output wire [7:0] o_wstrb,
output wire o_wvalid,
input wire i_wready,
input wire i_bvalid,
output reg o_bready = 1'b1,
input wire [63:0] i_rdata,
input wire i_rvalid,
output reg o_rready = 1'b1);
reg awdone = 1'b0;
reg ardone = 1'b0;
reg wdone = 1'b0;
localparam [1:0]
IDLE = 2'd0,
WRITE = 2'd1,
READ = 2'd2;
reg [1:0] state = IDLE;
assign o_awaddr = {i_wb_adr[31:3], 3'b000};
assign o_awvalid = (state == WRITE) & !awdone;
assign o_araddr = {i_wb_adr[31:3], 3'b000};
assign o_arvalid = (state == READ) & !ardone;
assign o_wdata = {i_wb_dat, i_wb_dat};
assign o_wstrb = i_wb_adr[2] ? {i_wb_sel,4'd0} : {4'd0, i_wb_sel};
assign o_wvalid = (state == WRITE) & !wdone;
assign o_wb_rdt = i_wb_adr[2] ? i_rdata[63:32] : i_rdata[31:0];
assign o_wb_ack = i_bvalid | i_rvalid;
always @(posedge i_clk) begin
if (state == IDLE) begin
awdone <= 1'b0;
ardone <= 1'b0;
wdone <= 1'b0;
end
if (o_awvalid & i_awready)
awdone <= 1'b1;
if (o_arvalid & i_arready)
ardone <= 1'b1;
if (o_wvalid & i_wready)
wdone <= 1'b1;
case(state)
IDLE: begin
if (i_wb_cyc & i_wb_stb)
state <= i_wb_we ? WRITE : READ;
end
WRITE:
if (i_bvalid)
state <= IDLE;
READ:
if (i_rvalid)
state <= IDLE;
endcase
if (i_rst) begin
state <= IDLE;
awdone <= 1'b0;
ardone <= 1'b0;
wdone <= 1'b0;
end
end // always @ (posedge i_clk)
`ifdef FORMAL
localparam F_LGDEPTH = 5;
wire [F_LGDEPTH-1:0] faxi_awr_outstanding, faxi_wr_outstanding, faxi_rd_outstanding;
faxil_master
#(
.C_AXI_DATA_WIDTH (64),
.C_AXI_ADDR_WIDTH (28),
.F_OPT_ASSUME_RESET (1),
.F_OPT_BRESP (1'b0),
.F_OPT_RRESP (1'b0),
.F_AXI_MAXWAIT (4),
.F_AXI_MAXDELAY (4),
.F_AXI_MAXRSTALL (1),
.F_LGDEPTH (5))
faxil_master
(
.i_clk (i_clk),
.i_axi_reset_n (~i_rst),
.i_axi_awready (i_awready),
.i_axi_awaddr (o_awaddr),
.i_axi_awcache (4'h0),
.i_axi_awprot (3'd0),
.i_axi_awvalid (o_awvalid),
.i_axi_wready (i_wready),
.i_axi_wdata (o_wdata),
.i_axi_wstrb (o_wstrb),
.i_axi_wvalid (o_wvalid),
.i_axi_bresp (2'd0),
.i_axi_bvalid (i_bvalid),
.i_axi_bready (o_bready),
.i_axi_arready (i_arready),
.i_axi_araddr (o_araddr),
.i_axi_arcache (4'h0),
.i_axi_arprot (3'd0),
.i_axi_arvalid (o_arvalid),
.i_axi_rresp (2'd0),
.i_axi_rvalid (i_rvalid),
.i_axi_rdata (i_rdata),
.i_axi_rready (o_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(o_rready);
assert(o_bready);
assert(faxi_awr_outstanding <= 1);
assert(faxi_wr_outstanding <= 1);
assert(faxi_rd_outstanding <= 1);
case(state)
IDLE: begin
assert(!o_wb_ack);
assert(faxi_awr_outstanding == 0);
assert(faxi_wr_outstanding == 0);
assert(faxi_rd_outstanding == 0);
end
READ: begin
assert(i_wb_stb);
assert(!i_wb_we);
assert(!awdone);
assert(!wdone);
assert(faxi_awr_outstanding == 0);
assert(faxi_wr_outstanding == 0);
assert(faxi_rd_outstanding == (ardone ? 1:0));
end
WRITE: begin
assert(i_wb_stb);
assert(i_wb_we);
assert(!ardone);
assert(faxi_awr_outstanding == (awdone ? 1:0));
assert(faxi_wr_outstanding == ( wdone ? 1:0));
assert(faxi_rd_outstanding == 0);
end
default:
assert(0);
endcase
end
fwbc_slave
#(.AW (32),
.F_MAX_DELAY (10),
.OPT_BUS_ABORT (0))
fwbc_slave
(.i_clk (i_clk),
.i_reset (i_rst),
.i_wb_addr (i_wb_adr),
.i_wb_data (i_wb_dat),
.i_wb_sel (i_wb_sel),
.i_wb_we (i_wb_we),
.i_wb_cyc (i_wb_cyc),
.i_wb_stb (i_wb_stb),
.i_wb_cti (3'd0),
.i_wb_bte (2'd0),
.i_wb_idata (o_wb_rdt),
.i_wb_ack (o_wb_ack),
.i_wb_err (1'b0),
.i_wb_rty (1'b0));
reg f_past_valid;
initial f_past_valid = 0;
always @(posedge i_clk)
f_past_valid <= 1;
// This *should* be part of the fwbc_* properties ...
always @(posedge i_clk)
if (f_past_valid && $past(!i_rst && i_wb_stb && !o_wb_ack))
begin
assume($stable(i_wb_stb));
assume($stable(i_wb_we));
assume($stable(i_wb_adr));
assume($stable(i_wb_dat));
assume($stable(i_wb_sel));
end
reg [2:0] count_writes, count_reads;
initial count_writes = 0;
always @(posedge i_clk)
if (i_rst)
count_writes <= 0;
else if (o_wb_ack && i_bvalid && !(&count_writes))
count_writes <= count_writes + 1;
initial count_reads = 0;
always @(posedge i_clk)
if (i_rst)
count_reads <= 0;
else if (o_wb_ack && !(&count_writes))
count_reads <= count_reads + 1;
always @(*)
cover(count_writes == 3'h3);
always @(*)
cover(count_reads == 3'h3);
`endif
endmodule
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment