From b21c321a059e11edeece1c90d97776bb0716d7a0 Mon Sep 17 00:00:00 2001 From: Alejandro Soto Date: Thu, 16 May 2024 01:08:04 -0600 Subject: rtl: fix quartus errors: parser, synthesis, fitter --- platform/wavelet3d/w3d_host_vexriscv.v | 2 + rtl/gfx/gfx_ctz.sv | 8 +- rtl/gfx/gfx_front_back.sv | 5 +- rtl/gfx/gfx_isa.sv | 132 +- rtl/gfx/gfx_sched.sv | 22 +- rtl/gfx/gfx_shader.sv | 3 +- rtl/gfx/gfx_shader_back.sv | 8 +- rtl/gfx/gfx_shader_front.sv | 59 +- rtl/gfx/gfx_shader_group.sv | 2 + rtl/gfx/gfx_shader_mem.sv | 2 + rtl/gfx/gfx_shader_regs.sv | 13 +- rtl/gfx/gfx_shader_setup.sv | 5 +- rtl/gfx/gfx_shader_sfu.sv | 2 + rtl/if_common/if_rst_sync.sv | 5 +- rtl/if_common/mod.mk | 1 + rtl/wb2axip/Makefile | 344 ----- rtl/wb2axip/addrdecode.v | 4 +- rtl/wb2axip/afifo.v | 2 +- rtl/wb2axip/apbslave.v | 8 +- rtl/wb2axip/apbxclk.v | 6 +- rtl/wb2axip/axi2axi3.v | 26 +- rtl/wb2axip/axi2axilite.v | 2 +- rtl/wb2axip/axi2axilsub.v | 4 +- rtl/wb2axip/axi32axi.v | 2 +- rtl/wb2axip/axi3reorder.v | 6 +- rtl/wb2axip/axi_addr.v | 4 +- rtl/wb2axip/axidma.v | 18 +- rtl/wb2axip/axidouble.v | 1406 ------------------- rtl/wb2axip/axiempty.v | 2 +- rtl/wb2axip/axil2apb.v | 2 +- rtl/wb2axip/axil2axis.v | 883 ------------ rtl/wb2axip/axildouble.v | 4 +- rtl/wb2axip/axilempty.v | 4 +- rtl/wb2axip/axilfetch.v | 8 +- rtl/wb2axip/axilgpio.v | 4 +- rtl/wb2axip/axilite2axi.v | 4 +- rtl/wb2axip/axilrd2wbsp.v | 8 +- rtl/wb2axip/axilsafety.v | 1449 -------------------- rtl/wb2axip/axilsingle.v | 6 +- rtl/wb2axip/axilupsz.v | 8 +- rtl/wb2axip/axilwr2wbsp.v | 8 +- rtl/wb2axip/axilxbar.v | 8 +- rtl/wb2axip/axim2wbsp.v | 8 +- rtl/wb2axip/aximm2s.v | 10 +- rtl/wb2axip/aximrd2wbsp.v | 6 +- rtl/wb2axip/aximwr2wbsp.v | 6 +- rtl/wb2axip/axiperf.v | 4 +- rtl/wb2axip/axis2mm.v | 10 +- rtl/wb2axip/axisafety.v | 2339 -------------------------------- rtl/wb2axip/axisbroadcast.v | 2 +- rtl/wb2axip/axisgdma.v | 19 +- rtl/wb2axip/axisgfsm.v | 6 +- rtl/wb2axip/axispacker.v | 2 +- rtl/wb2axip/axisrandom.v | 4 +- rtl/wb2axip/axissafety.v | 2 +- rtl/wb2axip/axisswitch.v | 6 +- rtl/wb2axip/axivcamera.v | 12 +- rtl/wb2axip/axivdisplay.v | 10 +- rtl/wb2axip/axivfifo.v | 6 +- rtl/wb2axip/axixbar.v | 2 +- rtl/wb2axip/axixclk.v | 2 +- rtl/wb2axip/axlite2wbsp.v | 6 +- rtl/wb2axip/axlite_wrapper.vhd | 136 -- rtl/wb2axip/demoaxi.v | 4 +- rtl/wb2axip/demofull.v | 6 +- rtl/wb2axip/easyaxil.v | 4 +- rtl/wb2axip/migsdram.v | 4 +- rtl/wb2axip/sfifo.v | 4 +- rtl/wb2axip/sfifothresh.v | 2 +- rtl/wb2axip/skidbuffer.v | 2 +- rtl/wb2axip/wbarbiter.v | 4 +- rtl/wb2axip/wbc2pipeline.v | 4 +- rtl/wb2axip/wbm2axilite.v | 10 +- rtl/wb2axip/wbm2axisp.v | 2 +- rtl/wb2axip/wbp2classic.v | 4 +- rtl/wb2axip/wbsafety.v | 2 +- rtl/wb2axip/wbxbar.v | 4 +- rtl/wb2axip/wbxclk.v | 2 +- 78 files changed, 315 insertions(+), 6840 deletions(-) delete mode 100644 rtl/wb2axip/Makefile delete mode 100644 rtl/wb2axip/axidouble.v delete mode 100644 rtl/wb2axip/axil2axis.v delete mode 100644 rtl/wb2axip/axilsafety.v delete mode 100644 rtl/wb2axip/axisafety.v delete mode 100644 rtl/wb2axip/axlite_wrapper.vhd diff --git a/platform/wavelet3d/w3d_host_vexriscv.v b/platform/wavelet3d/w3d_host_vexriscv.v index 415a0ac..4ae9e2c 100644 --- a/platform/wavelet3d/w3d_host_vexriscv.v +++ b/platform/wavelet3d/w3d_host_vexriscv.v @@ -2,6 +2,8 @@ // Component : VexRiscv // Git hash : 457ae5c7e5c8183f0ba7c51f7f0301d05eb8ced1 +`define SYNTHESIS + module w3d_host_vexriscv ( input wire timerInterrupt, input wire externalInterrupt, diff --git a/rtl/gfx/gfx_ctz.sv b/rtl/gfx/gfx_ctz.sv index 2713f8a..f1075d7 100644 --- a/rtl/gfx/gfx_ctz.sv +++ b/rtl/gfx/gfx_ctz.sv @@ -8,11 +8,17 @@ module gfx_ctz output logic[$clog2(WIDTH):0] ctz ); + logic[WIDTH - 1:0] value_rev; + gfx_clz #(WIDTH) clz ( .clk, - .value({<<{value}}), + .value(value_rev), .clz(ctz) ); + always_comb + for (int i = 0; i < $bits(value); ++i) + value_rev[i] = value[$bits(value) - i - 1]; + endmodule diff --git a/rtl/gfx/gfx_front_back.sv b/rtl/gfx/gfx_front_back.sv index b768532..6618353 100644 --- a/rtl/gfx/gfx_front_back.sv +++ b/rtl/gfx/gfx_front_back.sv @@ -1,5 +1,6 @@ -interface gfx_front_back -import gfx::*;; +interface gfx_front_back; + + import gfx::*; struct { diff --git a/rtl/gfx/gfx_isa.sv b/rtl/gfx/gfx_isa.sv index 7239478..cc34156 100644 --- a/rtl/gfx/gfx_isa.sv +++ b/rtl/gfx/gfx_isa.sv @@ -5,80 +5,86 @@ package gfx_isa; typedef logic signed[7:0] pc_offset; - typedef union packed + typedef struct packed { sgpr_num sgpr; - - struct packed - { - logic[$bits(sgpr_num) - $bits(vgpr_num) - 1:0] reserved; - vgpr_num num; - } vgpr; - } xgpr_num; + } xgpr_sgpr; typedef struct packed { - enum logic[1:0] - { - REGS_SVS = 2'b00, - REGS_SSS = 2'b01, - REGS_VVS = 2'b10, - REGS_VVV = 2'b11 - } reg_mode; + logic[$bits(sgpr_num) - $bits(vgpr_num) - 1:0] reserved; + vgpr_num vgpr; + } xgpr_vgpr; - union packed - { - struct packed - { - logic b_is_imm; + typedef xgpr_vgpr xgpr_num; - union packed - { - logic[12:0] imm; + typedef enum logic[1:0] + { + REGS_SVS = 2'b00, + REGS_SSS = 2'b01, + REGS_VVS = 2'b10, + REGS_VVV = 2'b11 + } xgpr_mode; - struct packed - { - logic from_consts; - logic[7:0] reserved; - xgpr_num r; - } read; - } b; + typedef struct packed + { + logic[12:0] imm; + } dst_src_rr_b_imm; - xgpr_num ra, - rd; - } rr; - } dst_src; + typedef struct packed + { + logic from_consts; + logic[7:0] reserved; + xgpr_num r; + } dst_src_rr_b_read; - logic reg_rev; + typedef struct packed + { + logic b_is_imm; + dst_src_rr_b_read b; + xgpr_num ra, + rd; + } dst_src_rr; - union packed - { - struct packed - { - enum logic[4:0] - { - INSN_FPINT_MOV = 0, - INSN_FPINT_FMUL = 1, - INSN_FPINT_IMUL = 2, - INSN_FPINT_FADD = 3, - INSN_FPINT_RES4 = 4, - INSN_FPINT_FMAX = 5, - INSN_FPINT_RES6 = 6, - INSN_FPINT_FMIN = 7, - INSN_FPINT_RES8 = 8, - INSN_FPINT_FCVT = 9, - INSN_FPINT_RES[10:31] - } op; - } fpint; - } by_class; + typedef enum logic[1:0] + { + INSN_FPINT = 2'd0, + INSN_MEM = 2'd1, + INSN_SFU = 2'd2, + INSN_GROUP = 2'd3 + } insn_class; + + typedef enum logic[4:0] + { + INSN_FPINT_MOV = 5'd0, + INSN_FPINT_FMUL = 5'd1, + INSN_FPINT_IMUL = 5'd2, + INSN_FPINT_FADD = 5'd3, + INSN_FPINT_RES4 = 5'd4, + INSN_FPINT_FMAX = 5'd5, + INSN_FPINT_RES6 = 5'd6, + INSN_FPINT_FMIN = 5'd7, + INSN_FPINT_RES8 = 5'd8, + INSN_FPINT_FCVT = 5'd9, + INSN_FPINT_RES[10:31] + } insn_fpint_op; + + typedef struct packed + { + xgpr_mode reg_mode; + dst_src_rr dst_src; + logic reg_rev; + insn_fpint_op op; + insn_class op_class; + } insn_fpint; - enum logic[1:0] - { - INSN_FPINT = 0, - INSN_MEM = 1, - INSN_SFU = 2, - INSN_GROUP = 3 - } insn_class; - } insn_word; + typedef struct packed + { + xgpr_mode reg_mode; + dst_src_rr dst_src; + logic reg_rev; + logic[4:0] op_data; + insn_class op_class; + } insn_any; endpackage diff --git a/rtl/gfx/gfx_sched.sv b/rtl/gfx/gfx_sched.sv index 03498e4..dd6ca91 100644 --- a/rtl/gfx/gfx_sched.sv +++ b/rtl/gfx/gfx_sched.sv @@ -15,7 +15,6 @@ import gfx::*; logic axi_ready, axi_valid, bram_ready, bram_read, bram_write, bram_write_next, mem_instr, mem_la_read, mem_la_write, mem_ready, mem_valid, select_bram; - word bram[SCHED_BRAM_WORDS]; word axi_rdata, bram_rdata, mem_addr, mem_la_addr, mem_rdata, mem_wdata; logic[$bits(word) / $bits(byte) - 1:0] mem_wstrb; @@ -113,17 +112,18 @@ import gfx::*; .mem_rdata(axi_rdata) ); - always_ff @(posedge clk) begin - if (bram_write) begin - for (int i = 0; i < $bits(mem_wstrb); ++i) - if (mem_wstrb[i]) - bram[bram_addr][i] <= mem_wdata[i]; - - bram_rdata <= 'x; - end else - bram_rdata <= bram[bram_addr]; - end + genvar i; + generate + for (i = 0; i < BYTES_PER_WORD; ++i) begin: byte_lanes + logic[7:0] bram[SCHED_BRAM_WORDS]; + always_ff @(posedge clk) begin + bram_rdata[8 * i +: 8] <= bram[bram_addr]; + if (bram_write & mem_wstrb[i]) + bram[bram_addr] <= mem_wdata[8 * i +: 8]; + end + end + endgenerate always_ff @(posedge clk or negedge rst_n) if (~rst_n) begin diff --git a/rtl/gfx/gfx_shader.sv b/rtl/gfx/gfx_shader.sv index 6b81b41..8ff6edc 100644 --- a/rtl/gfx/gfx_shader.sv +++ b/rtl/gfx/gfx_shader.sv @@ -1,6 +1,5 @@ module gfx_shader -import gfx::*; -import gfx_shader_schedif_pkg::*; +import gfx::*, gfx_shader_schedif_pkg::*; ( input logic clk, rst_n, diff --git a/rtl/gfx/gfx_shader_back.sv b/rtl/gfx/gfx_shader_back.sv index 968a34b..f7c2349 100644 --- a/rtl/gfx/gfx_shader_back.sv +++ b/rtl/gfx/gfx_shader_back.sv @@ -159,7 +159,7 @@ module gfx_shader_writeback_arbiter4 .clk, .rst_n, .a(p0_p1.rx), - .b(p2_p3.tx), + .b(p2_p3.rx), .out ); @@ -267,12 +267,12 @@ import gfx::*; end regs.sgpr_write.data = setup.write.gpr_value; - regs.sgpr_write.sgpr = setup.write.gpr.sgpr; + regs.sgpr_write.sgpr = setup.write.gpr; regs.sgpr_write.group = setup.write.group; if (scalar_wb) begin regs.sgpr_write.data = wb.lanes[0]; - regs.sgpr_write.sgpr = wb.dest.sgpr; + regs.sgpr_write.sgpr = wb.dest; regs.sgpr_write.group = wb.group; end @@ -291,7 +291,7 @@ import gfx::*; loop_hold[i] = loop_hold[i - 1]; loop_hold[0].mask = wb.mask; - loop_hold[0].vgpr = wb.dest.vgpr.num; + loop_hold[0].vgpr = wb.dest.vgpr; loop_hold[0].group = wb.group; loop_hold[0].pc_add = wb.pc_add; loop_hold[0].pc_update = wb.pc_update; diff --git a/rtl/gfx/gfx_shader_front.sv b/rtl/gfx/gfx_shader_front.sv index 3398e52..acdde78 100644 --- a/rtl/gfx/gfx_shader_front.sv +++ b/rtl/gfx/gfx_shader_front.sv @@ -1,9 +1,9 @@ typedef struct { - logic valid, - retry; - gfx::group_id group; - gfx_isa::insn_word insn; + logic valid, + retry; + gfx::group_id group; + gfx_isa::insn_any insn; } front_wave; typedef struct @@ -124,7 +124,7 @@ import gfx::*; assign mem.arid = '0; assign mem.arlen = ($bits(mem.arlen))'($bits(oword) / $bits(word) - 1); - assign mem.arsize = 3'b101; // 32 bits/beat + assign mem.arsize = 3'b010; // 4 bytes/beat assign mem.araddr = {araddr, ($clog2($bits(oword)) - $clog2($bits(word)) + SUBWORD_BITS)'('0)}; assign mem.arburst = 2'b01; // Incremental mode @@ -424,17 +424,16 @@ import gfx::*; insn_valid <= valid_5; if (fetch_ready & fetch_valid) begin - fetch_shift[0] <= fetch_data; - for (int i = 1; i < $size(fetch_shift); ++i) - fetch_shift[i] <= fetch_shift[i - 1]; + fetch_shift[$size(fetch_shift) - 1] <= fetch_data; + for (int i = 0; i < $size(fetch_shift) - 1; ++i) + fetch_shift[i] <= fetch_shift[i + 1]; end end endmodule module gfx_shader_read_regs -import gfx::*; -import gfx_isa::*; +import gfx::*, gfx_isa::*; ( input logic clk, rst_n, @@ -470,7 +469,7 @@ import gfx_isa::*; for (int i = 1; i < $size(out_hold); ++i) out_hold[i] <= out_hold[i - 1]; - passthru_hold[0].dest <= in.insn.dst_src.rr.rd; + passthru_hold[0].dest <= in.insn.dst_src.rd; unique case (in.insn.reg_mode) REGS_SVS, REGS_SSS: passthru_hold[0].dest_scalar <= 1; @@ -484,13 +483,13 @@ import gfx_isa::*; read.op.group <= in.group; - read.op.b_imm <= in.insn.dst_src.rr.b.imm; - read.op.a_sgpr <= in.insn.dst_src.rr.ra.sgpr; - read.op.b_sgpr <= in.insn.dst_src.rr.b.read.r.sgpr; - read.op.a_vgpr <= in.insn.dst_src.rr.ra.vgpr.num; - read.op.b_vgpr <= in.insn.dst_src.rr.b.read.r.vgpr.num; - read.op.b_is_imm <= in.insn.dst_src.rr.b_is_imm; - read.op.b_is_const <= in.insn.dst_src.rr.b.read.from_consts; + read.op.b_imm <= in.insn.dst_src.b; + read.op.a_sgpr <= in.insn.dst_src.ra; + read.op.b_sgpr <= in.insn.dst_src.b.r; + read.op.a_vgpr <= in.insn.dst_src.ra.vgpr; + read.op.b_vgpr <= in.insn.dst_src.b.r.vgpr; + read.op.b_is_imm <= in.insn.dst_src.b_is_imm; + read.op.b_is_const <= in.insn.dst_src.b.from_consts; read.op.scalar_rev <= reg_rev; unique case (in.insn.reg_mode) @@ -525,8 +524,7 @@ import gfx_isa::*; endmodule module gfx_shader_decode_class -import gfx::*; -import gfx_isa::*; +import gfx::*, gfx_isa::*; ( input logic clk, rst_n, @@ -573,7 +571,7 @@ import gfx_isa::*; retry <= wave.retry; hold_valid <= wave.valid; - unique case (wave.insn.insn_class) + unique case (wave.insn.op_class) INSN_FPINT: ; // p0 no tiene ready INSN_MEM: is_mem <= 1; INSN_SFU: is_fsu <= 1; @@ -599,19 +597,22 @@ import gfx_isa::*; endmodule module gfx_shader_decode_fpint -import gfx::*; -import gfx_isa::*; +import gfx::*, gfx_isa::*; ( - input logic clk, + input logic clk, - input insn_word insn, - input logic writeback, + input insn_any insn, + input logic writeback, - output fpint_op op + output fpint_op op ); + insn_fpint as_fpint; + + assign as_fpint = insn; + always_ff @(posedge clk) begin - unique case (insn.by_class.fpint.op) + unique case (as_fpint.op) INSN_FPINT_MOV: begin op.setup_mul_float <= 0; op.setup_unit_b <= 1; @@ -709,7 +710,7 @@ import gfx_isa::*; op.mnorm_zero_flags <= 0; op.mnorm_zero_b <= 0; op.minmax_abs <= 0; - op.minmax_swap <= insn.by_class.fpint.op == INSN_FPINT_FMIN; + op.minmax_swap <= as_fpint.op == INSN_FPINT_FMIN; op.minmax_zero_min <= 1; op.minmax_copy_flags <= 1; op.shiftr_int_signed <= 0; diff --git a/rtl/gfx/gfx_shader_group.sv b/rtl/gfx/gfx_shader_group.sv index 4a602a8..c4a9894 100644 --- a/rtl/gfx/gfx_shader_group.sv +++ b/rtl/gfx/gfx_shader_group.sv @@ -14,4 +14,6 @@ import gfx::*; gfx_wb.tx wb ); + word foo; + endmodule diff --git a/rtl/gfx/gfx_shader_mem.sv b/rtl/gfx/gfx_shader_mem.sv index d9e4ff4..72ab0a4 100644 --- a/rtl/gfx/gfx_shader_mem.sv +++ b/rtl/gfx/gfx_shader_mem.sv @@ -14,4 +14,6 @@ import gfx::*; gfx_wb.tx wb ); + word foo; + endmodule diff --git a/rtl/gfx/gfx_shader_regs.sv b/rtl/gfx/gfx_shader_regs.sv index ef3a129..2b3451a 100644 --- a/rtl/gfx/gfx_shader_regs.sv +++ b/rtl/gfx/gfx_shader_regs.sv @@ -33,7 +33,7 @@ import gfx::*; assign pc_read_groups[1] = io.pc_front_group; assign io.mask_back = mask_read[0]; - assign pc_read_groups[0] = io.mask_back_group; + assign mask_read_groups[0] = io.mask_back_group; assign imm_out = hold_imm[$size(hold_imm) - 1]; assign a_scalar_out = hold_a_scalar[$bits(hold_a_scalar) - 1]; @@ -83,20 +83,21 @@ import gfx::*; .write_data(io.sgpr_write.data) ); + genvar gi; generate - for (genvar i = 0; i < SHADER_LANES; ++i) begin: vgprs + for (gi = 0; gi < SHADER_LANES; ++gi) begin: vgprs gfx_shader_regfile #($bits(group_id) + $bits(vgpr_num)) vgprs ( .clk, .read_a_num({hold_read_group_2, hold_read_a_vgpr_2}), .read_b_num({hold_read_group_2, hold_read_b_vgpr_2}), - .read_a_data(read_a_data_vgpr[i]), - .read_b_data(read_b_data_vgpr[i]), + .read_a_data(read_a_data_vgpr[gi]), + .read_b_data(read_b_data_vgpr[gi]), - .write(io.vgpr_write.mask[i]), + .write(io.vgpr_write.mask[gi]), .write_num({io.vgpr_write.group, io.vgpr_write.vgpr}), - .write_data(io.vgpr_write.data[i]) + .write_data(io.vgpr_write.data[gi]) ); end endgenerate diff --git a/rtl/gfx/gfx_shader_setup.sv b/rtl/gfx/gfx_shader_setup.sv index f46fb66..f437acb 100644 --- a/rtl/gfx/gfx_shader_setup.sv +++ b/rtl/gfx/gfx_shader_setup.sv @@ -1,5 +1,6 @@ -interface gfx_shader_setup -import gfx::*;; +interface gfx_shader_setup; + + import gfx::*; struct { diff --git a/rtl/gfx/gfx_shader_sfu.sv b/rtl/gfx/gfx_shader_sfu.sv index f15ff04..0886449 100644 --- a/rtl/gfx/gfx_shader_sfu.sv +++ b/rtl/gfx/gfx_shader_sfu.sv @@ -14,4 +14,6 @@ import gfx::*; gfx_wb.tx wb ); + word foo; + endmodule diff --git a/rtl/if_common/if_rst_sync.sv b/rtl/if_common/if_rst_sync.sv index 69f1b78..e6077b6 100644 --- a/rtl/if_common/if_rst_sync.sv +++ b/rtl/if_common/if_rst_sync.sv @@ -8,6 +8,9 @@ module if_rst_sync ); always_ff @(posedge clk or negedge rst_n) - srst_n <= ~rst_n ? 0 : 1; + if (~rst_n) + srst_n <= 0; + else + srst_n <= 1; endmodule diff --git a/rtl/if_common/mod.mk b/rtl/if_common/mod.mk index e60abc4..2f2a465 100644 --- a/rtl/if_common/mod.mk +++ b/rtl/if_common/mod.mk @@ -1,3 +1,4 @@ define core + $(this)/deps := peakrdl_intfs $(this)/rtl_dirs := . endef diff --git a/rtl/wb2axip/Makefile b/rtl/wb2axip/Makefile deleted file mode 100644 index db66615..0000000 --- a/rtl/wb2axip/Makefile +++ /dev/null @@ -1,344 +0,0 @@ -################################################################################ -## -## Filename: Makefile -## {{{ -## Project: WB2AXIPSP: bus bridges and other odds and ends -## -## Purpose: To describe how to build the Verilator libraries from the -## RTL, for the purposes of trying to discover if they work. -## Any actual testing will be done from the code within the bench/cpp -## directory. -## -## Targets: The default target, all, builds the target test, which includes -## the libraries necessary for Verilator testing. -## -## Creator: Dan Gisselquist, Ph.D. -## Gisselquist Technology, LLC -## -################################################################################ -## }}} -## Copyright (C) 2016-2023, Gisselquist Technology, LLC -## {{{ -## This file is part of the WB2AXIP project. -## -## The WB2AXIP project contains free software and gateware, licensed under the -## Apache License, Version 2.0 (the "License"). You may not use this project, -## or 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. -## -################################################################################ -## -## }}} -all: test -YYMMDD=`date +%Y%m%d` -CXX := g++ -IVCHECK := ivcheck -IVERILOG := iverilog -FBDIR := . -VDIRFB:= $(FBDIR)/obj_dir -VERILATOR := verilator -VFLAGS := -MMD -O3 -Wall -Wpedantic -cc -.DELETE_ON_ERROR: -.PHONY: test -test: testwb testaxi testaxil testapb testaxis - -.PHONY: testwb testaxi testaxil testapb testaxis - -.PHONY: axim2wbsp axim2wbsp wbm2axilite axilrd2wbsp axilwr2wbsp axlite2wbsp -.PHONY: axixbar axilxbar wbxbar axis2mm aximm2s axidma axim2wbsp aximrd2wbsp -.PHONY: aximwr2wbsp axixclk axiperf demoaxi demofull easyaxil sfifo skidbuffer -.PHONY: axilgpio -.PHONY: axilsafety axisafety wbsafety axivfifo axil2apb apbslave -.PHONY: axisrandom axisswitch axisbroadcast axispacker - -axim2wbsp: $(VDIRFB)/Vwbm2axisp__ALL.a $(IVCHECK)/axim2wbsp -axim2wbsp: $(VDIRFB)/Vaxim2wbsp__ALL.a -wbm2axilite: $(VDIRFB)/Vwbm2axilite__ALL.a $(IVCHECK)/wbm2axilite -axilrd2wbsp: $(VDIRFB)/Vaxilrd2wbsp__ALL.a $(IVCHECK)/axilrd2wbsp -axilwr2wbsp: $(VDIRFB)/Vaxilwr2wbsp__ALL.a $(IVCHECK)/axilwr2wbsp -axlite2wbsp: $(VDIRFB)/Vaxlite2wbsp__ALL.a $(IVCHECK)/axlite2wbsp -axiempty: $(VDIRFB)/Vaxiempty__ALL.a $(IVCHECK)/axiempty -axilempty: $(VDIRFB)/Vaxilempty__ALL.a $(IVCHECK)/axilempty -axilgpio: $(VDIRFB)/Vaxilgpio__ALL.a $(IVCHECK)/axilgpio -axivcamera: $(VDIRFB)/Vaxivcamera__ALL.a $(IVCHECK)/axivcamera -axivdisplay: $(VDIRFB)/Vaxivdisplay__ALL.a $(IVCHECK)/axivdisplay -axivfifo: $(VDIRFB)/Vaxivfifo__ALL.a $(IVCHECK)/axivfifo -axixbar: $(VDIRFB)/Vaxixbar__ALL.a $(IVCHECK)/axixbar -axilxbar: $(VDIRFB)/Vaxilxbar__ALL.a $(IVCHECK)/axilxbar -wbxbar: $(VDIRFB)/Vwbxbar__ALL.a $(IVCHECK)/wbxbar -axis2mm: $(VDIRFB)/Vaxis2mm__ALL.a $(IVCHECK)/axis2mm -aximm2s: $(VDIRFB)/Vaximm2s__ALL.a $(IVCHECK)/aximm2s -axidma: $(VDIRFB)/Vaxidma__ALL.a $(IVCHECK)/axidma -axim2wbsp: $(VDIRFB)/Vaxim2wbsp__ALL.a $(IVCHECK)/axim2wbsp -aximrd2wbsp: $(VDIRFB)/Vaximrd2wbsp__ALL.a $(IVCHECK)/aximrd2wbsp -aximwr2wbsp: $(VDIRFB)/Vaximwr2wbsp__ALL.a $(IVCHECK)/aximwr2wbsp -axiperf: $(VDIRFB)/Vaxiperf__ALL.a $(IVCHECK)/axiperf -axixclk: $(VDIRFB)/Vaxixclk__ALL.a $(IVCHECK)/axixclk -demoaxi: $(VDIRFB)/Vdemoaxi__ALL.a $(IVCHECK)/demoaxi -demofull: $(VDIRFB)/Vdemofull__ALL.a $(IVCHECK)/demofull -easyaxil: $(VDIRFB)/Veasyaxil__ALL.a $(IVCHECK)/easyaxil -sfifo: $(VDIRFB)/Vsfifo__ALL.a $(IVCHECK)/sfifo -skidbuffer: $(VDIRFB)/Vskidbuffer__ALL.a $(IVCHECK)/skidbuffer -axisafety: $(VDIRFB)/Vaxisafety__ALL.a $(IVCHECK)/axisafety -axilsafety: $(VDIRFB)/Vaxilsafety__ALL.a $(IVCHECK)/axilsafety -wbsafety: $(VDIRFB)/Vwbsafety__ALL.a $(IVCHECK)/wbsafety -axil2apb: $(VDIRFB)/Vaxil2apb__ALL.a $(IVCHECK)/axil2apb -apbslave: $(VDIRFB)/Vapbslave__ALL.a $(IVCHECK)/apbslave -axisbroadcast: $(VDIRFB)/Vaxisbroadcast__ALL.a $(IVCHECK)/axisbroadcast -axispacker: $(VDIRFB)/Vaxispacker__ALL.a $(IVCHECK)/axispacker -axisrandom: $(VDIRFB)/Vaxisrandom__ALL.a $(IVCHECK)/axisrandom -axisswitch: $(VDIRFB)/Vaxisswitch__ALL.a $(IVCHECK)/axisswitch - -testwb: wbsafety wbm2axilite wbxbar sfifo wbsafety wbxbar wbsafety -testaxi: axim2wbsp axixbar axixclk demofull axiempty -testaxi: aximrd2wbsp axim2wbsp aximwr2wbsp axisafety -testaxi: axis2mm aximm2s axidma axivfifo axivdisplay axivcamera -testaxil: axilrd2wbsp axilwr2wbsp axlite2wbsp axilxbar demoaxi easyaxil -testaxil: skidbuffer axiperf axilempty axilgpio -testapb: axil2apb apbslave -testaxis: axisbroadcast axisswitch axisrandom axispacker - -.PHONY: wbm2axisp -wbm2axisp: $(VDIRFB)/Vwbm2axisp__ALL.a -$(VDIRFB)/Vwbm2axisp__ALL.a: $(VDIRFB)/Vwbm2axisp.h $(VDIRFB)/Vwbm2axisp.cpp -$(VDIRFB)/Vwbm2axisp__ALL.a: $(VDIRFB)/Vwbm2axisp.mk -$(VDIRFB)/Vwbm2axisp.h $(VDIRFB)/Vwbm2axisp.cpp $(VDIRFB)/Vwbm2axisp.mk: wbm2axisp.v - -.PHONY: wbm2axilite -wbm2axilite: $(VDIRFB)/Vwbm2axilite__ALL.a -$(VDIRFB)/Vwbm2axilite__ALL.a: $(VDIRFB)/Vwbm2axilite.h $(VDIRFB)/Vwbm2axilite.cpp -$(VDIRFB)/Vwbm2axilite__ALL.a: $(VDIRFB)/Vwbm2axilite.mk -$(VDIRFB)/Vwbm2axilite.h $(VDIRFB)/Vwbm2axilite.cpp $(VDIRFB)/Vwbm2axilite.mk: wbm2axilite.v - -.PHONY: axilrd2wbsp -axilrd2wbsp: $(VDIRFB)/Vaxilrd2wbsp__ALL.a -$(VDIRFB)/Vaxilrd2wbsp__ALL.a: $(VDIRFB)/Vaxilrd2wbsp.h $(VDIRFB)/Vaxilrd2wbsp.cpp -$(VDIRFB)/Vaxilrd2wbsp__ALL.a: $(VDIRFB)/Vaxilrd2wbsp.mk -$(VDIRFB)/Vaxilrd2wbsp.h $(VDIRFB)/Vaxilrd2wbsp.cpp $(VDIRFB)/Vaxilrd2wbsp.mk: axilrd2wbsp.v - -.PHONY: axilwr2wbsp -axilwr2wbsp: $(VDIRFB)/Vaxilwr2wbsp__ALL.a -$(VDIRFB)/Vaxilwr2wbsp__ALL.a: $(VDIRFB)/Vaxilwr2wbsp.h $(VDIRFB)/Vaxilwr2wbsp.cpp -$(VDIRFB)/Vaxilwr2wbsp__ALL.a: $(VDIRFB)/Vaxilwr2wbsp.mk -$(VDIRFB)/Vaxilwr2wbsp.h $(VDIRFB)/Vaxilwr2wbsp.cpp $(VDIRFB)/Vaxilwr2wbsp.mk: axilwr2wbsp.v - -$(VDIRFB)/Vaxlite2wbsp__ALL.a: $(VDIRFB)/Vaxlite2wbsp.h $(VDIRFB)/Vaxlite2wbsp.cpp -$(VDIRFB)/Vaxlite2wbsp__ALL.a: $(VDIRFB)/Vaxlite2wbsp.mk -$(VDIRFB)/Vaxlite2wbsp.h $(VDIRFB)/Vaxlite2wbsp.cpp $(VDIRFB)/Vaxlite2wbsp.mk: axlite2wbsp.v - -$(VDIRFB)/Vaxiempty__ALL.a: $(VDIRFB)/Vaxiempty.h $(VDIRFB)/Vaxiempty.cpp -$(VDIRFB)/Vaxiempty__ALL.a: $(VDIRFB)/Vaxiempty.mk -$(VDIRFB)/Vaxiempty.h $(VDIRFB)/Vaxiempty.cpp $(VDIRFB)/Vaxiempty.mk: axiempty.v skidbuffer.v - -$(VDIRFB)/Vaxilempty__ALL.a: $(VDIRFB)/Vaxilempty.h $(VDIRFB)/Vaxilempty.cpp -$(VDIRFB)/Vaxilempty__ALL.a: $(VDIRFB)/Vaxilempty.mk -$(VDIRFB)/Vaxilempty.h $(VDIRFB)/Vaxilempty.cpp $(VDIRFB)/Vaxilempty.mk: axilempty.v skidbuffer.v - -$(VDIRFB)/Vaxilgpio__ALL.a: $(VDIRFB)/Vaxilgpio.h $(VDIRFB)/Vaxilgpio.cpp -$(VDIRFB)/Vaxilgpio__ALL.a: $(VDIRFB)/Vaxilgpio.mk -$(VDIRFB)/Vaxilgpio.h $(VDIRFB)/Vaxilgpio.cpp $(VDIRFB)/Vaxilgpio.mk: axilgpio.v skidbuffer.v - -$(VDIRFB)/Vaxim2wbsp__ALL.a: $(VDIRFB)/Vaxim2wbsp.h $(VDIRFB)/Vaxim2wbsp.cpp -$(VDIRFB)/Vaxim2wbsp__ALL.a: $(VDIRFB)/Vaxim2wbsp.mk -$(VDIRFB)/Vaxim2wbsp.h $(VDIRFB)/Vaxim2wbsp.cpp $(VDIRFB)/Vaxim2wbsp.mk: \ - axim2wbsp.v aximrd2wbsp.v aximwr2wbsp.v wbarbiter.v - -$(VDIRFB)/Vaxivfifo__ALL.a: $(VDIRFB)/Vaxivfifo.h $(VDIRFB)/Vaxivfifo.cpp -$(VDIRFB)/Vaxivfifo__ALL.a: $(VDIRFB)/Vaxivfifo.mk -$(VDIRFB)/Vaxivfifo.h $(VDIRFB)/Vaxivfifo.cpp $(VDIRFB)/Vaxivfifo.mk: \ - axivfifo.v skidbuffer.v sfifo.v - -$(VDIRFB)/Vaxivcamera__ALL.a: $(VDIRFB)/Vaxivcamera.h $(VDIRFB)/Vaxivcamera.cpp -$(VDIRFB)/Vaxivcamera__ALL.a: $(VDIRFB)/Vaxivcamera.mk -$(VDIRFB)/Vaxivcamera.h $(VDIRFB)/Vaxivcamera.cpp $(VDIRFB)/Vaxivcamera.mk: \ - axivcamera.v skidbuffer.v sfifo.v - -$(VDIRFB)/Vaxivdisplay__ALL.a: $(VDIRFB)/Vaxivdisplay.h $(VDIRFB)/Vaxivdisplay.cpp -$(VDIRFB)/Vaxivdisplay__ALL.a: $(VDIRFB)/Vaxivdisplay.mk -$(VDIRFB)/Vaxivdisplay.h $(VDIRFB)/Vaxivdisplay.cpp $(VDIRFB)/Vaxivdisplay.mk: \ - axivdisplay.v skidbuffer.v sfifo.v - -$(VDIRFB)/V%.cpp $(VDIRFB)/V%.h $(VDIRFB)/V%.mk: $(FBDIR)/%.v - $(VERILATOR) $(VFLAGS) $*.v - -$(VDIRFB)/V%__ALL.a: $(VDIRFB)/V%.mk - cd $(VDIRFB); make -f V$*.mk - -## -## Run Icarus Verilog (iverilog) on each of these cores for a lint check -## -$(IVCHECK)/axi2axilite: axi2axilite.v sfifo.v skidbuffer.v axi_addr.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axil2axis: axil2axis.v sfifo.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axildouble: axildouble.v sfifo.v skidbuffer.v addrdecode.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axilrd2wbsp: axilrd2wbsp.v sfifo.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axilsafety: axilsafety.v sfifo.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axilsingle: axilsingle.v sfifo.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axilwr2wbsp: axilwr2wbsp.v sfifo.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axilxbar: axilxbar.v skidbuffer.v addrdecode.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axidma: axidma.v sfifo.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/aximm2s: aximm2s.v sfifo.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axim2wbsp: axim2wbsp.v sfifo.v skidbuffer.v aximrd2wbsp.v aximwr2wbsp.v axi_addr.v wbarbiter.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/aximrd2wbsp: aximrd2wbsp.v sfifo.v skidbuffer.v axi_addr.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/aximwr2wbsp: aximwr2wbsp.v sfifo.v skidbuffer.v axi_addr.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axiperf: axiperf.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axisafety: axisafety.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axis2mm: axis2mm.v sfifo.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axivcamera: axivcamera.v sfifo.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axivdisplay: axivdisplay.v sfifo.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axivfifo: axivfifo.v sfifo.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axixbar: axixbar.v skidbuffer.v addrdecode.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axixclk: axixclk.v afifo.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axlite2wbsp: axlite2wbsp.v axilrd2wbsp.v axilwr2wbsp.v wbarbiter.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axiempty: axiempty.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axilempty: axilempty.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axilgpio: axilgpio.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/demoaxi: demoaxi.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/demofull: demofull.v axi_addr.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/easyaxil: easyaxil.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/sfifo: sfifo.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/skidbuffer: skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/wbm2axilite: wbm2axilite.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/wbsafety: wbsafety.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/wbxbar: wbxbar.v skidbuffer.v addrdecode.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axil2apb: axil2apb.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/apbslave: apbslave.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axisbroadcast: axisbroadcast.v sfifo.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axispacker: axispacker.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axisrandom: axisrandom.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -$(IVCHECK)/axisswitch: axisswitch.v skidbuffer.v - $(mk-ivcheck) - $(IVERILOG) -g2012 $^ -o $@ - -define mk-ivcheck - @bash -c "if [ ! -e $(IVCHECK) ]; then mkdir -p $(IVCHECK); fi" -endef - -.PHONY: clean -clean: - rm -rf $(VDIRFB)/*.mk - rm -rf $(VDIRFB)/*.cpp - rm -rf $(VDIRFB)/*.h - rm -rf $(VDIRFB)/ - rm -rf $(IVCHECK)/ diff --git a/rtl/wb2axip/addrdecode.v b/rtl/wb2axip/addrdecode.v index 2f3cac6..b6fc914 100644 --- a/rtl/wb2axip/addrdecode.v +++ b/rtl/wb2axip/addrdecode.v @@ -62,7 +62,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module addrdecode #( // {{{ @@ -457,5 +457,5 @@ module addrdecode #( // }}} endmodule `ifndef YOSYS -`default_nettype wire +//`default_nettype wire `endif diff --git a/rtl/wb2axip/afifo.v b/rtl/wb2axip/afifo.v index 99af9cc..6a4ca02 100644 --- a/rtl/wb2axip/afifo.v +++ b/rtl/wb2axip/afifo.v @@ -31,7 +31,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module afifo #( // {{{ diff --git a/rtl/wb2axip/apbslave.v b/rtl/wb2axip/apbslave.v index e3ba027..5a16d84 100644 --- a/rtl/wb2axip/apbslave.v +++ b/rtl/wb2axip/apbslave.v @@ -31,15 +31,15 @@ //////////////////////////////////////////////////////////////////////////////// // // }}} -`default_nettype none +//`default_nettype none // module apbslave #( // {{{ parameter C_APB_ADDR_WIDTH = 12, parameter C_APB_DATA_WIDTH = 32, - localparam AW = C_APB_ADDR_WIDTH, - localparam DW = C_APB_DATA_WIDTH, - localparam APBLSB = $clog2(C_APB_DATA_WIDTH)-3 + /*local*/parameter AW = C_APB_ADDR_WIDTH, + /*local*/parameter DW = C_APB_DATA_WIDTH, + /*local*/parameter APBLSB = $clog2(C_APB_DATA_WIDTH)-3 // }}} ) ( // {{{ diff --git a/rtl/wb2axip/apbxclk.v b/rtl/wb2axip/apbxclk.v index 831675b..c6a7acc 100644 --- a/rtl/wb2axip/apbxclk.v +++ b/rtl/wb2axip/apbxclk.v @@ -31,15 +31,15 @@ //////////////////////////////////////////////////////////////////////////////// // // }}} -`default_nettype none +//`default_nettype none // module apbxclk #( // {{{ parameter C_APB_ADDR_WIDTH = 12, parameter C_APB_DATA_WIDTH = 32, parameter [0:0] OPT_REGISTERED = 1'b0, - localparam AW = C_APB_ADDR_WIDTH, - localparam DW = C_APB_DATA_WIDTH + /*local*/parameter AW = C_APB_ADDR_WIDTH, + /*local*/parameter DW = C_APB_DATA_WIDTH // }}} ) ( // {{{ diff --git a/rtl/wb2axip/axi2axi3.v b/rtl/wb2axip/axi2axi3.v index 3682949..28059fa 100644 --- a/rtl/wb2axip/axi2axi3.v +++ b/rtl/wb2axip/axi2axi3.v @@ -48,7 +48,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} // module axi2axi3 #( @@ -63,17 +63,17 @@ module axi2axi3 #( input wire S_AXI_ARESETN, // // The AXI4 incoming/slave interface - input reg S_AXI_AWVALID, + input wire S_AXI_AWVALID, output wire S_AXI_AWREADY, - input reg [C_AXI_ID_WIDTH-1:0] S_AXI_AWID, - input reg [C_AXI_ADDR_WIDTH-1:0] S_AXI_AWADDR, - input reg [7:0] S_AXI_AWLEN, - input reg [2:0] S_AXI_AWSIZE, - input reg [1:0] S_AXI_AWBURST, - input reg S_AXI_AWLOCK, - input reg [3:0] S_AXI_AWCACHE, - input reg [2:0] S_AXI_AWPROT, - input reg [3:0] S_AXI_AWQOS, + input wire [C_AXI_ID_WIDTH-1:0] S_AXI_AWID, + input wire [C_AXI_ADDR_WIDTH-1:0] S_AXI_AWADDR, + input wire [7:0] S_AXI_AWLEN, + input wire [2:0] S_AXI_AWSIZE, + input wire [1:0] S_AXI_AWBURST, + input wire S_AXI_AWLOCK, + input wire [3:0] S_AXI_AWCACHE, + input wire [2:0] S_AXI_AWPROT, + input wire [3:0] S_AXI_AWQOS, // // input wire S_AXI_WVALID, @@ -297,7 +297,7 @@ module axi2axi3 #( end - initial M_AXI_AWSIZE = ADDRLSB[2:0]; + //initial M_AXI_AWSIZE = ADDRLSB[2:0]; always @(posedge S_AXI_ACLK) begin if (awskd_valid && awskd_ready) @@ -673,7 +673,7 @@ module axi2axi3 #( axi_arvalid <= 1'b0; initial r_arlen = 0; - initial M_AXI_ARLEN = 0; + //initial M_AXI_ARLEN = 0; always @(posedge S_AXI_ACLK) if (!S_AXI_ARESETN) begin diff --git a/rtl/wb2axip/axi2axilite.v b/rtl/wb2axip/axi2axilite.v index 8cb671d..d5662ee 100644 --- a/rtl/wb2axip/axi2axilite.v +++ b/rtl/wb2axip/axi2axilite.v @@ -48,7 +48,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module axi2axilite #( // {{{ diff --git a/rtl/wb2axip/axi2axilsub.v b/rtl/wb2axip/axi2axilsub.v index 694dc58..33dcc39 100644 --- a/rtl/wb2axip/axi2axilsub.v +++ b/rtl/wb2axip/axi2axilsub.v @@ -49,7 +49,7 @@ // //////////////////////////////////////////////////////////////////////////////// // -`default_nettype none +//`default_nettype none // `ifdef FORMAL `ifdef BMC @@ -645,7 +645,7 @@ module axi2axilsub #( // m_awvalid // {{{ - initial m_axi_awvalid = 0; + //initial m_axi_awvalid = 0; always @(posedge S_AXI_ACLK) if (!S_AXI_ARESETN) m_awvalid <= 0; diff --git a/rtl/wb2axip/axi32axi.v b/rtl/wb2axip/axi32axi.v index dfa2099..f4b17d5 100644 --- a/rtl/wb2axip/axi32axi.v +++ b/rtl/wb2axip/axi32axi.v @@ -54,7 +54,7 @@ // //////////////////////////////////////////////////////////////////////////////// // -`default_nettype none +//`default_nettype none // }}} module axi32axi #( // {{{ diff --git a/rtl/wb2axip/axi3reorder.v b/rtl/wb2axip/axi3reorder.v index 3c92c0d..a644749 100644 --- a/rtl/wb2axip/axi3reorder.v +++ b/rtl/wb2axip/axi3reorder.v @@ -80,7 +80,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module axi3reorder #( // {{{ @@ -293,7 +293,7 @@ module axi3reorder #( // for (gk = 0; gk 0) - write_len <= write_len - 1; - // }}} - end - // }}} - - // Slave address decoding - // {{{ - // Decode our incoming address in order to determine the next - // slave the address addresses - addrdecode #( - // {{{ - .AW(AW), .DW(3), .NS(NS), - .SLAVE_ADDR(SLAVE_ADDR), - .SLAVE_MASK(SLAVE_MASK), - .OPT_REGISTERED(1'b1) - // }}} - ) wraddr( - // {{{ - .i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN), - .i_valid(awskid_valid && write_awskidready), .o_stall(awskd_stall), - // .i_addr(awskid_valid && write_awskidready - // ? awskid_awaddr : next_waddr), - .i_addr(awskid_awaddr), - .i_data(awskid_prot), - .o_valid(dcd_awvalid), .i_stall(!S_AXI_WVALID), - .o_decode(raw_wdecode), .o_addr(m_awaddr), - .o_data(m_axi_awprot) - // }}} - ); - // }}} - - // last_wdecode - // {{{ - // We only do our decode on the address request. We need the decoded - // values long after the top of the burst. Therefore, let's use - // dcd_awvalid to know we have a valid output from the decoder and - // then we'll latch that (register it really) for the rest of the burst - always @(posedge S_AXI_ACLK) - if (dcd_awvalid) - last_wdecode <= raw_wdecode; - // }}} - - // wdecode - // {{{ - always @(*) - begin - if (dcd_awvalid) - wdecode = raw_wdecode; - else - wdecode = last_wdecode; - end - // }}} - - // Downstream slave (write) signals - // {{{ - // It's now time to create our write request for the slave. Slave - // writes take place on the clock after address valid is true as long - // as S_AXI_WVALID is true. This places combinatorial logic onto the - // outgoing AWVALID. The sign that we are in the middle of a burst - // will specifically be that WREADY is true. - // - - // - // If there were any part of this algorithm I disliked it would be the - // AWVALID logic here. It shouldn't nearly be this loaded. - assign S_AXI_WREADY = write_request; - assign M_AXI_AWVALID = (S_AXI_WVALID && write_request - && (!locked_burst || locked_write)) ? wdecode[NS-1:0] : 0; - assign M_AXI_AWADDR = write_addr; - assign M_AXI_AWPROT = m_axi_awprot; - assign M_AXI_AWSIZE = write_size; - assign M_AXI_WDATA = S_AXI_WDATA; - assign M_AXI_WSTRB = S_AXI_WSTRB; - // }}} - - // write_awskidready - // {{{ - // We can accept a new value from the skid buffer as soon as the last - // write value comes in, or equivalently if we are not in the middle - // of a write. This is all subject, of course, to our backpressure - // FIFO not being full. - assign write_awskidready = ((S_AXI_WVALID&&S_AXI_WLAST) - || !S_AXI_WREADY) && !bfull; - // }}} - - // write_windex - // {{{ - // Back out an index from our decoded slave value - generate if (NS <= 1) - begin : WR_ONE_SLAVE - - assign write_windex = 0; - - end else begin : WR_INDEX - reg [LGNS-1:0] r_write_windex; - integer k; - - always @(*) - begin - r_write_windex = 0; - for(k=0; k 0)) - rlen <= rlen - 1; - // }}} - - // arvalid - // {{{ - // Should the slave M_AXI_ARVALID be true in general? Based upon - // rlen above, but still needs to be gated across all slaves. - initial arvalid = 1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - arvalid <= 1'b0; - else if (S_AXI_ARVALID && S_AXI_ARREADY) - arvalid <= 1'b1; - else if (issue_read && (rlen == 0)) - arvalid <= 1'b0; - // }}} - - // next_araddr -- Get the next AXI address - // {{{ - axi_addr #( - // {{{ - .AW(C_AXI_ADDR_WIDTH), .DW(C_AXI_DATA_WIDTH) - // }}} - ) get_next_read_address( - // {{{ - araddr, - arsize, arburst, arlen, next_araddr - // }}} - ); - // }}} - - // raw_rdecode-- Decode which slave is being addressed by this read. - // {{{ - addrdecode #( - // {{{ - .AW(AW), .DW(1), .NS(NS), - .SLAVE_ADDR(SLAVE_ADDR), - .SLAVE_MASK(SLAVE_MASK), - .OPT_REGISTERED(1'b1) - // }}} - ) rdaddr( - // {{{ - .i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN), - .i_valid(S_AXI_ARVALID && S_AXI_ARREADY || rlen>0), - // Warning: there's no skid on this stall - .o_stall(arskd_stall), - .i_addr((S_AXI_ARVALID & S_AXI_ARREADY) - ? S_AXI_ARADDR : next_araddr), - .i_data(1'b0), - .o_valid(read_rwait), .i_stall(!issue_read), - .o_decode(raw_rdecode), .o_addr(m_araddr), - .o_data(unused_pin[0]) - // }}} - ); - // }}} - - // last_rdecode - // {{{ - // We want the value from the decoder on the first clock cycle. It - // may not be valid after that, so we'll hold on to it in last_rdecode - initial last_rdecode = 0; - always @(posedge S_AXI_ACLK) - if (read_rwait) - last_rdecode <= raw_rdecode; - // }}} - - // rdecode - // {{{ - always @(*) - if (read_rwait) - rdecode = raw_rdecode; - else - rdecode = last_rdecode; - // }}} - - // Finally, issue our read request any time the FIFO isn't full - // {{{ - assign issue_read = !read_full; - - assign M_AXI_ARVALID = issue_read ? rdecode[NS-1:0] : 0; - assign M_AXI_ARADDR = m_araddr; - assign M_AXI_ARPROT = arprot; - assign M_AXI_ARSIZE = arsize; - // }}} - - // read_rvalid, read_result - // {{{ - // read_rvalid would be the RVALID response from the slave that would - // be returned if we checked it. read_result is the same thing--one - // clock later. - initial { read_result, read_rvalid } = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - { read_result, read_rvalid } <= 2'b00; - else - { read_result, read_rvalid } <= { read_rvalid, - (arvalid&issue_read) }; - // }}} - - // read_rvid, read_rvlast, read_rvlock - // {{{ - // On the same clock when rvalid is true, we'll also want to know - // if RLAST should be true (decoded here, not in the slave), and - // whether or not the transaction is locked. These values are valid - // any time read_rvalid is true. - always @(posedge S_AXI_ACLK) - begin - if (arvalid && issue_read) - begin - read_rvid <= arid; - read_rvlast <= (rlen == 0); - read_rvlock <= (read_rvlock && !read_rvlast) || (OPT_EXCLUSIVE_ACCESS && arlock && lock_valid); - end else if (read_rvlast) - read_rvlock <= 1'b0; - - if (!S_AXI_ARESETN) - begin - read_rvlock <= 1'b0; - read_rvlast <= 1'b1; - end - end - // }}} - - // read_retid, read_retlast - // {{{ - // read_result is true one clock after read_rvalid is true. Copy - // the ID and LAST values into this pipeline clock cycle - always @(posedge S_AXI_ACLK) - begin - read_retid <= read_rvid; - read_retlast <= read_rvlast; - end - // }}} - - // - // Decode the read value. - // - - // read_index - First step is to calculate the index of the slave - // {{{ - generate if (NS <= 1) - begin : RD_ONE_SLAVE - - assign read_index = 0; - - end else begin : RD_INDEX - reg [LGNS-1:0] r_read_index = 0; - integer k; - - always @(*) - begin - r_read_index = 0; - - for(k=0; k= lock_addr) - &&(S_AXI_AWADDR <= lock_last)) - r_lock_valid <= 0; - end - - if (S_AXI_ARVALID && S_AXI_ARREADY && S_AXI_ARLOCK - && S_AXI_ARBURST == 2'b01) - begin - r_lock_valid <= !locked_write; - lock_addr <= S_AXI_ARADDR; - lock_id <= S_AXI_ARID; - lock_size <= S_AXI_ARSIZE; - lock_len <= S_AXI_ARLEN[3:0]; - lock_last <= S_AXI_ARADDR - + ({ {(AW-4){1'b0}}, lock_len } - << S_AXI_ARSIZE); - end - - if (awskid_valid && write_awskidready) - begin - r_locked_burst <= 1'b0; - locked_write <= awskid_awlock; - - if (awskid_awlock) - begin - r_locked_burst <= r_lock_valid; - if (lock_addr != awskid_awaddr) - r_locked_burst <= 1'b0; - if (lock_id != awskid_awid) - r_locked_burst <= 1'b0; - if (lock_size != awskid_awsize) - r_locked_burst <= 1'b0; - if (lock_len != awskid_awlen[3:0]) - r_locked_burst <= 1'b0; - if (2'b01 != awskid_awburst) - r_locked_burst <= 1'b0; - end - - // Write if !locked_write || write_burst - // EXOKAY on locked_write && write_burst - // OKAY on all other writes where the slave - // does not assert an error - end else if (S_AXI_WVALID && S_AXI_WREADY && S_AXI_WLAST) - r_locked_burst <= 1'b0; - - if (!S_AXI_ARESETN) - begin - r_lock_valid <= 1'b0; - r_locked_burst <= 1'b0; - end - end - - assign locked_burst = r_locked_burst; - assign lock_valid = r_lock_valid; - // }}} - end else begin : NO_EXCLUSIVE_ACCESS - // {{{ - // Keep track of whether or not the current burst requests - // exclusive access or not. locked_write is an important - // signal used to make certain that we do not write to our - // slave on any locked write requests. (Shouldn't happen, - // since we aren't returning any EXOKAY's from reads ...) - always @(posedge S_AXI_ACLK) - if (awskid_valid && write_awskidready) - locked_write <= awskid_awlock; - else if (S_AXI_WVALID && S_AXI_WREADY && S_AXI_WLAST) - locked_write <= 1'b0; - - assign locked_burst = 0; - assign lock_valid = 0; - // }}} - end endgenerate - // }}} - - // Make Verilator happy - // {{{ - // verilator lint_off UNUSED - wire unused; - assign unused = &{ 1'b0, - S_AXI_AWCACHE, S_AXI_ARCACHE, - S_AXI_AWQOS, S_AXI_ARQOS, - dcd_awvalid, m_awaddr, unused_pin, - bffull, rdfull, bfill, rfill, - awskd_stall, arskd_stall }; - // verilator lint_on UNUSED - // }}} -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -// -// Formal verification properties -// {{{ -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -`ifdef FORMAL - localparam F_LGDEPTH = LGFLEN+9; - - // - // ... - // - - faxi_slave #( .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH), - .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), - .C_AXI_ID_WIDTH(C_AXI_ID_WIDTH), - .F_AXI_MAXDELAY(5), - .F_LGDEPTH(F_LGDEPTH)) - properties ( - .i_clk(S_AXI_ACLK), - .i_axi_reset_n(S_AXI_ARESETN), - // - .i_axi_awvalid(S_AXI_AWVALID), - .i_axi_awready(S_AXI_AWREADY), - .i_axi_awid( S_AXI_AWID), - .i_axi_awaddr( S_AXI_AWADDR), - .i_axi_awlen( S_AXI_AWLEN), - .i_axi_awsize( S_AXI_AWSIZE), - .i_axi_awburst(S_AXI_AWBURST), - .i_axi_awlock( S_AXI_AWLOCK), - .i_axi_awcache(S_AXI_AWCACHE), - .i_axi_awprot( S_AXI_AWPROT), - .i_axi_awqos( S_AXI_AWQOS), - // - .i_axi_wvalid(S_AXI_WVALID), - .i_axi_wready(S_AXI_WREADY), - .i_axi_wdata( S_AXI_WDATA), - .i_axi_wstrb( S_AXI_WSTRB), - .i_axi_wlast( S_AXI_WLAST), - // - .i_axi_bvalid(S_AXI_BVALID), - .i_axi_bready(S_AXI_BREADY), - .i_axi_bid( S_AXI_BID), - .i_axi_bresp( S_AXI_BRESP), - // - .i_axi_arvalid(S_AXI_ARVALID), - .i_axi_arready(S_AXI_ARREADY), - .i_axi_arid( S_AXI_ARID), - .i_axi_araddr( S_AXI_ARADDR), - .i_axi_arlen( S_AXI_ARLEN), - .i_axi_arsize( S_AXI_ARSIZE), - .i_axi_arburst(S_AXI_ARBURST), - .i_axi_arlock( S_AXI_ARLOCK), - .i_axi_arcache(S_AXI_ARCACHE), - .i_axi_arprot( S_AXI_ARPROT), - .i_axi_arqos( S_AXI_ARQOS), - // - .i_axi_rvalid(S_AXI_RVALID), - .i_axi_rready(S_AXI_RREADY), - .i_axi_rid( S_AXI_RID), - .i_axi_rdata( S_AXI_RDATA), - .i_axi_rlast( S_AXI_RLAST), - .i_axi_rresp( S_AXI_RRESP) - // - // ... - // - ); - - // - // ... - // - - always @(*) - if (!OPT_EXCLUSIVE_ACCESS) - begin - assert(!S_AXI_BVALID || S_AXI_BRESP != EXOKAY); - assert(!S_AXI_RVALID || S_AXI_RRESP != EXOKAY); - end - - //////////////////////////////////////////////////////////////////////// - // - // Properties necessary to pass induction - // - //////////////////////////////////////////////////////////////////////// - // - // - always @(*) - assert($onehot0(M_AXI_AWVALID)); - - always @(*) - assert($onehot0(M_AXI_ARVALID)); - - // - // - // Write properties - // - // - - always @(*) - if (S_AXI_WVALID && S_AXI_WREADY) - begin - if (locked_burst && !locked_write) - assert(M_AXI_AWVALID == 0); - else if (wdecode[NS]) - assert(M_AXI_AWVALID == 0); - else begin - assert($onehot(M_AXI_AWVALID)); - assert(M_AXI_AWVALID == wdecode[NS-1:0]); - end - end else - assert(M_AXI_AWVALID == 0); - - // - // ... - // - - // - // - // Read properties - // - // - - // - // ... - // - - - //////////////////////////////////////////////////////////////////////// - // - // Simplifying (careless) assumptions - // - // Caution: these might void your proof - // - //////////////////////////////////////////////////////////////////////// - // - // - localparam [0:0] F_CHECK_WRITES = 1'b1; - localparam [0:0] F_CHECK_READS = 1'b1; - - generate if (!F_CHECK_WRITES) - begin - always @(*) - assume(!S_AXI_AWVALID); - always @(*) - assert(!S_AXI_BVALID); - always @(*) - assert(!M_AXI_AWVALID); - - // ... - end endgenerate - - generate if (!F_CHECK_READS) - begin - always @(*) - assume(!S_AXI_ARVALID); - always @(*) - assert(!S_AXI_RVALID); - always @(*) - assert(M_AXI_ARVALID == 0); - always @(*) - assert(rdecode == 0); - // ... - end endgenerate - - // - // ... - // - - //////////////////////////////////////////////////////////////////////// - // - // Cover properties - // - //////////////////////////////////////////////////////////////////////// - // - // - reg [3:0] cvr_arvalids, cvr_awvalids, cvr_reads, cvr_writes; - (* anyconst *) reg cvr_burst; - - always @(*) - if (cvr_burst && S_AXI_AWVALID) - assume(S_AXI_AWLEN > 2); - - always @(*) - if (cvr_burst && S_AXI_ARVALID) - assume(S_AXI_ARLEN > 2); - - initial cvr_awvalids = 0; - always @(posedge S_AXI_ACLK) - if (!cvr_burst || !S_AXI_ARESETN) - cvr_awvalids <= 0; - else if (S_AXI_AWVALID && S_AXI_AWREADY && !(&cvr_awvalids)) - cvr_awvalids <= cvr_awvalids + 1; - - initial cvr_arvalids = 0; - always @(posedge S_AXI_ACLK) - if (!cvr_burst || !S_AXI_ARESETN) - cvr_arvalids <= 0; - else if (S_AXI_ARVALID && S_AXI_ARREADY && !(&cvr_arvalids)) - cvr_arvalids <= cvr_arvalids + 1; - - initial cvr_writes = 0; - always @(posedge S_AXI_ACLK) - if (!cvr_burst || !S_AXI_ARESETN) - cvr_writes <= 0; - else if (S_AXI_BVALID && S_AXI_BREADY && !(&cvr_writes)) - cvr_writes <= cvr_writes + 1; - - initial cvr_reads = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - cvr_reads <= 0; - else if (S_AXI_RVALID && S_AXI_RREADY && S_AXI_RLAST - && !(&cvr_arvalids)) - cvr_reads <= cvr_reads + 1; - - generate if (F_CHECK_WRITES) - begin : COVER_WRITES - - always @(*) - cover(cvr_awvalids > 2); - - always @(*) - cover(cvr_writes > 2); - - always @(*) - cover(cvr_writes > 4); - end endgenerate - - generate if (F_CHECK_READS) - begin : COVER_READS - always @(*) - cover(cvr_arvalids > 2); - - always @(*) - cover(cvr_reads > 2); - - always @(*) - cover(cvr_reads > 4); - end endgenerate - - always @(*) - cover((cvr_writes > 2) && (cvr_reads > 2)); - - generate if (OPT_EXCLUSIVE_ACCESS) - begin : COVER_EXCLUSIVE_ACCESS - - always @(*) - cover(S_AXI_BVALID && S_AXI_BRESP == EXOKAY); - - end endgenerate -`endif -endmodule diff --git a/rtl/wb2axip/axiempty.v b/rtl/wb2axip/axiempty.v index d0ec896..a6f299d 100644 --- a/rtl/wb2axip/axiempty.v +++ b/rtl/wb2axip/axiempty.v @@ -33,7 +33,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module axiempty #( // {{{ diff --git a/rtl/wb2axip/axil2apb.v b/rtl/wb2axip/axil2apb.v index d8a73ae..3815d5b 100644 --- a/rtl/wb2axip/axil2apb.v +++ b/rtl/wb2axip/axil2apb.v @@ -33,7 +33,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module axil2apb #( // {{{ diff --git a/rtl/wb2axip/axil2axis.v b/rtl/wb2axip/axil2axis.v deleted file mode 100644 index 0e1d14f..0000000 --- a/rtl/wb2axip/axil2axis.v +++ /dev/null @@ -1,883 +0,0 @@ -//////////////////////////////////////////////////////////////////////////////// -// -// Filename: axil2axis -// {{{ -// Project: WB2AXIPSP: bus bridges and other odds and ends -// -// Purpose: Demonstrates a simple AXI-Lite interface to drive an AXI-Stream -// channel. This can then be used to debug DSP processing. -// -// Registers: This AXI-lite to AXI-Stream core supports four word-sized -// addresses. Byte enables are ignored. -// -// 2'b00, ADDR_SINK -// Writes to this register will send data to the stream master, -// with TLAST clear. Data goes first through a FIFO. If the -// FIFO is full, the write will stall. If it stalls OPT_TIMEOUT -// cycles, the write will fail and return a bus error. -// -// Reads from this register will return data from the stream slave, -// but without consuming it. Values read here may still be read -// from the ADDR_SOURCE register later. -// -// 2'b01, ADDR_SOURCE -// Writes to this register will send data downstream to the stream -// master as well, but this time with TLAST set. -// -// Reads from this register will accept a value from the stream -// slave interface. The read value contains TDATA. TLAST is -// ignored in this read. If you want access to TLAST, you can get -// it from the ADDR_FIFO register. -// -// If there is no data to be read, the read will not and does not -// stall. It will instead return a bus error. -// -// 2'b10, ADDR_STATS -// Since we can, we'll handle some statistics here. The top half -// word contains two counters: a 4-bit counter of TLAST's issued -// from the stream master, and a 12-bit counter of TDATA values -// issued. Neither counter includes data still contained in the -// FIFO. If the OPT_SOURCE option is clear, these values will -// always be zero. -// -// The second (bottom, or least-significant) halfword contains the -// same regarding the stream slave. If OPT_SINK is set, these -// counters count values read from the core. If OPT_SINK is clear, -// so that the stream sink is not truly implemented, then TREADY -// will be held high and the counter will just count values coming -// into the core never going into the FIFO. -// -// 2'b11, ADDR_FIFO -// Working with the core can be a challenge. You want to make -// certain that writing to the core doesn't hang the design, and -// that reading from the core doesn't cause a bus error. -// -// Bits 31:16 contain the number of items in the write FIFO, and -// bits 14:0 contain the number of items in the read FIFO. -// -// Bit 15 contains whether or not the next item to be read is -// the last item in a packet, i.e. with TLAST set. -// -// -// Creator: Dan Gisselquist, Ph.D. -// Gisselquist Technology, LLC -// -//////////////////////////////////////////////////////////////////////////////// -// }}} -// Copyright (C) 2020-2024, Gisselquist Technology, LLC -// {{{ -// -// This file is part of the WB2AXIP project. -// -// The WB2AXIP project contains free software and gateware, licensed under the -// Apache License, Version 2.0 (the "License"). You may not use this project, -// or 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. -// -//////////////////////////////////////////////////////////////////////////////// -// -`default_nettype none -// }}} -module axil2axis #( - // {{{ - // - // Size of the AXI-lite bus. These are fixed, since 1) AXI-lite - // is fixed at a width of 32-bits by Xilinx def'n, and 2) since - // we only ever have 4 configuration words. - parameter C_AXI_ADDR_WIDTH = 4, - localparam C_AXI_DATA_WIDTH = 32, - parameter C_AXIS_DATA_WIDTH = 16, - // - // OPT_SOURCE enables the AXI stream master logic. If not - // enabled, M_AXI_TVALID will be held at zero, and the stream - // master logic may be ignored. - parameter [0:0] OPT_SOURCE = 1'b1, - // - // OPT_SINK enables the AXI stream slave logic. If not enabled, - // reads will always return zero, and S_AXIS_TREADY will be - // held high. - parameter [0:0] OPT_SINK = 1'b1, - // - // If OPT_SIGN_EXTEND is set, values received will be sign - // extended to fill the full data width on read. Otherwise - // the most significant of any unused bits will remain clear. - parameter [0:0] OPT_SIGN_EXTEND = 1'b0, - // - // Data written to this core will be placed into a FIFO before - // entering the AXI stream master. LGFIFO is the log, based - // two, of the number of words in this FIFO. Similarly, data - // consumed by AXI stream slave contained in this core will go - // first into a read FIFO. Reads from the core will then return - // data from this FIFO, or a bus error if none is available. - parameter LGFIFO = 5, - // - // OPT_TIMEOUT, if non-zero, will allow writes to the stream - // master, or reads from the stream slave, to stall the core - // for OPT_TIMEOUT cycles for the stream to be ready. If the - // stream isn't ready at this time (i.e. if the write FIFO is - // still full, or the read FIFO still empty), the result will - // be returned as a bus error. Likewise, if OPT_TIMEOUT==0, - // the core will always return a bus error if ever the write - // FIFO is full or the read FIFO empty. - parameter OPT_TIMEOUT = 5, - // - // OPT_LOWPOWER sets outputs to zero if not valid. This applies - // to the AXI-lite bus, however, and not the AXI stream FIFOs, - // since those don't have LOWPOWER support (currently). - parameter [0:0] OPT_LOWPOWER = 0 - // - // This design currently ignores WSTRB, beyond checking that it - // is not zero. I see no easy way to add it. (I'll leave that - // to you to implement, if you wish.) - // parameter [0:0] OPT_WSTRB = 0, - // }}} - ) ( - // {{{ - input wire S_AXI_ACLK, - input wire S_AXI_ARESETN, - // AXI-lite signals - // {{{ - input wire S_AXI_AWVALID, - output wire S_AXI_AWREADY, - input wire [C_AXI_ADDR_WIDTH-1:0] S_AXI_AWADDR, - input wire [2:0] S_AXI_AWPROT, - // - input wire S_AXI_WVALID, - output wire S_AXI_WREADY, - input wire [C_AXI_DATA_WIDTH-1:0] S_AXI_WDATA, - input wire [C_AXI_DATA_WIDTH/8-1:0] S_AXI_WSTRB, - // - output wire S_AXI_BVALID, - input wire S_AXI_BREADY, - output wire [1:0] S_AXI_BRESP, - // - input wire S_AXI_ARVALID, - output wire S_AXI_ARREADY, - input wire [C_AXI_ADDR_WIDTH-1:0] S_AXI_ARADDR, - input wire [2:0] S_AXI_ARPROT, - // - output wire S_AXI_RVALID, - input wire S_AXI_RREADY, - output wire [C_AXI_DATA_WIDTH-1:0] S_AXI_RDATA, - output wire [1:0] S_AXI_RRESP, - // }}} - // AXI stream slave (sink) signals - // {{{ - input wire S_AXIS_TVALID, - output wire S_AXIS_TREADY, - input wire [C_AXIS_DATA_WIDTH-1:0] S_AXIS_TDATA, - input wire S_AXIS_TLAST, - // }}} - // AXI stream master (source) signals - // {{{ - output wire M_AXIS_TVALID, - input wire M_AXIS_TREADY, - output reg [C_AXIS_DATA_WIDTH-1:0] M_AXIS_TDATA, - output reg M_AXIS_TLAST - // }}} - // }}} - ); - - localparam ADDRLSB = $clog2(C_AXI_DATA_WIDTH)-3; - localparam [1:0] ADDR_SINK = 2'b00, // Read from stream - ADDR_SOURCE = 2'b01, // Write, also sets TLAST - ADDR_STATS = 2'b10, - ADDR_FIFO = 2'b11; - localparam SW = C_AXIS_DATA_WIDTH; - - //////////////////////////////////////////////////////////////////////// - // - // Register/wire signal declarations - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - wire i_reset = !S_AXI_ARESETN; - - wire axil_write_ready; - wire [C_AXI_ADDR_WIDTH-ADDRLSB-1:0] awskd_addr; - // - wire [C_AXI_DATA_WIDTH-1:0] wskd_data; - wire [C_AXI_DATA_WIDTH/8-1:0] wskd_strb; - reg axil_bvalid, axil_berr; - // - wire axil_read_ready; - wire [C_AXI_ADDR_WIDTH-ADDRLSB-1:0] arskd_addr; - reg [C_AXI_DATA_WIDTH-1:0] axil_read_data; - reg axil_read_valid; - - wire awskd_valid, wskd_valid; - wire wfifo_full, wfifo_write, wfifo_empty; - wire [LGFIFO:0] wfifo_fill; - reg write_timeout; - - wire read_timeout; - reg axil_rerr; - reg [3:0] read_bursts_completed; - reg [11:0] reads_completed; - - wire [3:0] write_bursts_completed; - wire [11:0] writes_completed; - - - // }}} - //////////////////////////////////////////////////////////////////////// - // - // AXI-lite signaling - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - - // - // Write signaling - // - // {{{ - skidbuffer #(.OPT_OUTREG(0), - .OPT_LOWPOWER(OPT_LOWPOWER), - .DW(C_AXI_ADDR_WIDTH-ADDRLSB)) - axilawskid(// - .i_clk(S_AXI_ACLK), .i_reset(i_reset), - .i_valid(S_AXI_AWVALID), .o_ready(S_AXI_AWREADY), - .i_data(S_AXI_AWADDR[C_AXI_ADDR_WIDTH-1:ADDRLSB]), - .o_valid(awskd_valid), .i_ready(axil_write_ready), - .o_data(awskd_addr)); - - skidbuffer #(.OPT_OUTREG(0), - .OPT_LOWPOWER(OPT_LOWPOWER), - .DW(C_AXI_DATA_WIDTH+C_AXI_DATA_WIDTH/8)) - axilwskid(// - .i_clk(S_AXI_ACLK), .i_reset(i_reset), - .i_valid(S_AXI_WVALID), .o_ready(S_AXI_WREADY), - .i_data({ S_AXI_WDATA, S_AXI_WSTRB }), - .o_valid(wskd_valid), .i_ready(axil_write_ready), - .o_data({ wskd_data, wskd_strb })); - - assign axil_write_ready = awskd_valid && wskd_valid - && (!S_AXI_BVALID || S_AXI_BREADY) - && ((awskd_addr[1] != ADDR_SOURCE[1]) - || (!wfifo_full || write_timeout)); - - // - // Write timeout generation - // - // {{{ - generate if ((OPT_TIMEOUT > 1) && OPT_SOURCE) - begin : GEN_WRITE_TIMEOUT - reg r_write_timeout; - reg [$clog2(OPT_TIMEOUT)-1:0] write_timer; - - initial write_timer = OPT_TIMEOUT-1; - initial r_write_timeout = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - begin - write_timer <= OPT_TIMEOUT-1; - r_write_timeout<= 1'b0; - end else if (!awskd_valid || !wfifo_full || !wskd_valid - || (awskd_addr[1] != ADDR_SOURCE[1]) - || (S_AXI_BVALID && !S_AXI_BREADY)) - begin - write_timer <= OPT_TIMEOUT-1; - r_write_timeout<= 1'b0; - end else begin - if (write_timer > 0) - write_timer <= write_timer - 1; - r_write_timeout <= (write_timer <= 1); - end - - assign write_timeout = r_write_timeout; -`ifdef FORMAL - always @(*) - assert(write_timer <= OPT_TIMEOUT-1); - always @(*) - assert(write_timeout == (write_timer == 0)); -`endif - end else begin : NO_WRITE_TIMEOUT - - assign write_timeout = 1'b1; - - end endgenerate - // }}} - - - initial axil_bvalid = 0; - always @(posedge S_AXI_ACLK) - if (i_reset) - axil_bvalid <= 0; - else if (axil_write_ready) - axil_bvalid <= 1; - else if (S_AXI_BREADY) - axil_bvalid <= 0; - - assign S_AXI_BVALID = axil_bvalid; - - initial axil_berr = 0; - always @(posedge S_AXI_ACLK) - if (OPT_LOWPOWER && i_reset) - axil_berr <= 0; - else if (axil_write_ready) - axil_berr <= (wfifo_full)&&(awskd_addr[1]==ADDR_SOURCE[1]); - else if (OPT_LOWPOWER && S_AXI_BREADY) - axil_berr <= 1'b0; - - assign S_AXI_BRESP = { axil_berr, 1'b0 }; - // }}} - - // - // AXI-stream source (Write) FIFO - // - // {{{ - assign wfifo_write = axil_write_ready && awskd_addr[1]==ADDR_SOURCE[1] - && wskd_strb != 0 && !wfifo_full; - - generate if (OPT_SOURCE) - begin : GEN_SOURCE_FIFO - - sfifo #(.BW(SW+1), .LGFLEN(LGFIFO)) - source(.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN), - .i_wr(wfifo_write), - .i_data({awskd_addr[0]==ADDR_SOURCE[0], - wskd_data[SW-1:0]}), - .o_full(wfifo_full), .o_fill(wfifo_fill), - .i_rd(M_AXIS_TREADY), - .o_data({ M_AXIS_TLAST, M_AXIS_TDATA }), - .o_empty(wfifo_empty)); - - assign M_AXIS_TVALID = !wfifo_empty; - - end else begin : NO_SOURCE_FIFO - - assign M_AXIS_TVALID = 1'b0; - assign M_AXIS_TDATA = 0; - assign M_AXIS_TLAST = 0; - - assign wfifo_full = 1'b0; - assign wfifo_fill = 0; - - end endgenerate - // }}} - - // - // AXI-stream consumer/sink (Read) FIFO - // - // {{{ - wire rfifo_empty, rfifo_full, rfifo_last, read_rfifo; - wire [LGFIFO:0] rfifo_fill; - wire [SW-1:0] rfifo_data; - - generate if (OPT_SINK) - begin : GEN_SINK_FIFO - - sfifo #(.BW(SW+1), .LGFLEN(LGFIFO)) - sink(.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN), - .i_wr(S_AXIS_TVALID && S_AXIS_TREADY), - .i_data({S_AXIS_TLAST, S_AXIS_TDATA}), - .o_full(rfifo_full), .o_fill(rfifo_fill), - .i_rd(read_rfifo), - .o_data({ rfifo_last, rfifo_data }), - .o_empty(rfifo_empty)); - - assign S_AXIS_TREADY = !rfifo_full; - assign read_rfifo =(axil_read_ready && arskd_addr== ADDR_SINK) - && !rfifo_empty; - - end else begin : NO_SINK - - assign S_AXIS_TREADY = 1'b1; - - assign rfifo_empty = 1'b1; - assign rfifo_data = 0; - assign rfifo_last = 1'b1; - assign rfifo_fill = 0; - - end endgenerate - // }}} - - // - // Read timeout generation - // - // {{{ - generate if (OPT_SINK && OPT_TIMEOUT > 1) - begin : GEN_READ_TIMEOUT - reg [$clog2(OPT_TIMEOUT)-1:0] read_timer; - reg r_read_timeout; - - initial read_timer = OPT_TIMEOUT-1; - initial r_read_timeout = 1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - begin - read_timer <= OPT_TIMEOUT-1; - r_read_timeout<= 1'b0; - end else if (!arskd_valid || (S_AXI_RVALID && !S_AXI_RREADY) - ||!rfifo_empty - ||(arskd_addr[1] != ADDR_SINK[1])) - begin - read_timer <= OPT_TIMEOUT-1; - r_read_timeout<= 1'b0; - end else begin - if (read_timer > 0) - read_timer <= read_timer - 1; - r_read_timeout <= (read_timer <= 1); - end - - assign read_timeout = r_read_timeout; - -`ifdef FORMAL - always @(*) - assert(read_timer <= OPT_TIMEOUT-1); - always @(*) - assert(read_timeout == (read_timer == 0)); -`endif - end else begin : NO_READ_TIMEOUT - - assign read_timeout = 1'b1; - - end endgenerate - // }}} - - // - // Read signaling - // - // {{{ - wire arskd_valid; - - skidbuffer #(.OPT_OUTREG(0), - .OPT_LOWPOWER(OPT_LOWPOWER), - .DW(C_AXI_ADDR_WIDTH-ADDRLSB)) - axilarskid(// - .i_clk(S_AXI_ACLK), .i_reset(i_reset), - .i_valid(S_AXI_ARVALID), .o_ready(S_AXI_ARREADY), - .i_data(S_AXI_ARADDR[C_AXI_ADDR_WIDTH-1:ADDRLSB]), - .o_valid(arskd_valid), .i_ready(axil_read_ready), - .o_data(arskd_addr)); - - assign axil_read_ready = arskd_valid - && (!S_AXI_RVALID || S_AXI_RREADY) - && ((arskd_addr[1] != ADDR_SINK[1]) - || (!rfifo_empty || read_timeout)); - - initial axil_read_valid = 1'b0; - always @(posedge S_AXI_ACLK) - if (i_reset) - axil_read_valid <= 1'b0; - else if (axil_read_ready) - axil_read_valid <= 1'b1; - else if (S_AXI_RREADY) - axil_read_valid <= 1'b0; - - assign S_AXI_RVALID = axil_read_valid; - - always @(posedge S_AXI_ACLK) - if (OPT_LOWPOWER && !S_AXI_ARESETN) - axil_rerr <= 1'b0; - else if (axil_read_ready) - axil_rerr <= rfifo_empty && (arskd_addr[1] == ADDR_SINK[1]); - else if (OPT_LOWPOWER && S_AXI_RREADY) - axil_rerr <= 1'b0; - - assign S_AXI_RRESP = { axil_rerr, 1'b0 }; - // }}} - - // }}} - //////////////////////////////////////////////////////////////////////// - // - // AXI-lite register logic - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - - // - // Read data counting : reads_completed and read_bursts_completed - // {{{ - initial reads_completed = 0; - initial read_bursts_completed = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - begin - // {{{ - reads_completed <= 0; - read_bursts_completed <= 0; - // }}} - end else if (!OPT_SINK) - begin - // {{{ - reads_completed <= reads_completed + (S_AXIS_TVALID ? 1:0); - read_bursts_completed <= read_bursts_completed - + ((S_AXIS_TVALID && S_AXIS_TLAST) ? 1:0); - // }}} - end else if (read_rfifo && !rfifo_empty) - begin - // {{{ - reads_completed <= reads_completed + 1; - read_bursts_completed <= read_bursts_completed + (rfifo_last ? 1:0); - // }}} - end - // }}} - - // - // Write data counting - // {{{ - generate if (OPT_SOURCE) - begin : GEN_WRITES_COMPLETED - // {{{ - reg [3:0] r_write_bursts_completed; - reg [11:0] r_writes_completed; - - initial r_writes_completed = 0; - initial r_write_bursts_completed = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - begin - r_writes_completed <= 0; - r_write_bursts_completed <= 0; - end else if (M_AXIS_TVALID && M_AXIS_TREADY) - begin - r_writes_completed <= writes_completed + 1; - r_write_bursts_completed <= write_bursts_completed - + (M_AXIS_TLAST ? 1:0); - end - - assign writes_completed = r_writes_completed; - assign write_bursts_completed = r_write_bursts_completed; - // }}} - end else begin : NO_COMPLETION_COUNTERS // No AXI-stream source logic - // {{{ - assign writes_completed = 0; - assign write_bursts_completed = 0; - // }}} - end endgenerate - // }}} - - // - // Read data register - // {{{ - initial axil_read_data = 0; - always @(posedge S_AXI_ACLK) - if (OPT_LOWPOWER && !S_AXI_ARESETN) - axil_read_data <= 0; - else if (!S_AXI_RVALID || S_AXI_RREADY) - begin - axil_read_data <= 0; - casez(arskd_addr) - { ADDR_SINK[1], 1'b? }: begin - if (OPT_SIGN_EXTEND && rfifo_data[SW-1]) - axil_read_data <= -1; - axil_read_data[SW-1:0] <= rfifo_data; - end - ADDR_STATS: begin - axil_read_data[31:28] <= write_bursts_completed; - axil_read_data[27:16] <= writes_completed; - axil_read_data[15:12] <= read_bursts_completed; - axil_read_data[11:0] <= reads_completed; - end - ADDR_FIFO: begin - // FIFO information - axil_read_data[16 +: LGFIFO+1] <= wfifo_fill; - axil_read_data[15] <= rfifo_last; - axil_read_data[LGFIFO:0] <= rfifo_fill; - end - endcase - - if (OPT_LOWPOWER && !axil_read_ready) - axil_read_data <= 0; - end - - assign S_AXI_RDATA = axil_read_data; - // }}} - - // Make Verilator happy - // {{{ - // Verilator lint_off UNUSED - wire unused; - assign unused = &{ 1'b0, S_AXI_AWPROT, S_AXI_ARPROT, - S_AXI_ARADDR[ADDRLSB-1:0], - S_AXI_AWADDR[ADDRLSB-1:0], - wskd_data[C_AXI_DATA_WIDTH-1:SW] }; - // Verilator lint_on UNUSED - // }}} - // }}} -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -// -// Formal properties used in verfiying this core -// {{{ -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -`ifdef FORMAL - // Register definitions - // {{{ - reg f_past_valid; - initial f_past_valid = 0; - always @(posedge S_AXI_ACLK) - f_past_valid <= 1; - - always @(*) - if (!f_past_valid) - assume(!S_AXI_ARESETN); - // }}} - //////////////////////////////////////////////////////////////////////// - // - // The AXI-lite control interface - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - localparam F_AXIL_LGDEPTH = 4; - wire [F_AXIL_LGDEPTH-1:0] faxil_rd_outstanding, - faxil_wr_outstanding, - faxil_awr_outstanding; - - faxil_slave #( - // {{{ - .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH), - .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), - .F_LGDEPTH(F_AXIL_LGDEPTH), - .F_AXI_MAXWAIT(OPT_TIMEOUT + 2), - .F_AXI_MAXDELAY(OPT_TIMEOUT + 2), - .F_AXI_MAXRSTALL(2), - .F_OPT_COVER_BURST(4) - // }}} - ) faxil( - // {{{ - .i_clk(S_AXI_ACLK), .i_axi_reset_n(S_AXI_ARESETN), - // - .i_axi_awvalid(S_AXI_AWVALID), - .i_axi_awready(S_AXI_AWREADY), - .i_axi_awaddr( S_AXI_AWADDR), - .i_axi_awprot( S_AXI_AWPROT), - // - .i_axi_wvalid(S_AXI_WVALID), - .i_axi_wready(S_AXI_WREADY), - .i_axi_wdata( S_AXI_WDATA), - .i_axi_wstrb( S_AXI_WSTRB), - // - .i_axi_bvalid(S_AXI_BVALID), - .i_axi_bready(S_AXI_BREADY), - .i_axi_bresp( S_AXI_BRESP), - // - .i_axi_arvalid(S_AXI_ARVALID), - .i_axi_arready(S_AXI_ARREADY), - .i_axi_araddr( S_AXI_ARADDR), - .i_axi_arprot( S_AXI_ARPROT), - // - .i_axi_rvalid(S_AXI_RVALID), - .i_axi_rready(S_AXI_RREADY), - .i_axi_rdata( S_AXI_RDATA), - .i_axi_rresp( S_AXI_RRESP), - // - .f_axi_rd_outstanding(faxil_rd_outstanding), - .f_axi_wr_outstanding(faxil_wr_outstanding), - .f_axi_awr_outstanding(faxil_awr_outstanding) - // }}} - ); - - always @(*) - begin - assert(faxil_awr_outstanding== (S_AXI_BVALID ? 1:0) - +(S_AXI_AWREADY ? 0:1)); - - assert(faxil_wr_outstanding == (S_AXI_BVALID ? 1:0) - +(S_AXI_WREADY ? 0:1)); - - assert(faxil_rd_outstanding == (S_AXI_RVALID ? 1:0) - +(S_AXI_ARREADY ? 0:1)); - end - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Verifying the packet counters - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - reg [11:0] f_reads, f_writes; - reg [3:0] f_read_pkts, f_write_pkts; - - // - // Mirror the read counter - // - initial f_reads = 0; - initial f_read_pkts = 0; - - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - begin - f_reads <= 0; - f_read_pkts <= 0; - end else if (OPT_SINK && (axil_read_ready - && arskd_addr == ADDR_SINK && !rfifo_empty)) - begin - f_reads <= f_reads + 1; - f_read_pkts <= f_read_pkts + (rfifo_last ? 1:0); - end else if (!OPT_SINK && S_AXIS_TVALID) - begin - f_reads <= f_reads + 1; - f_read_pkts <= f_read_pkts + (S_AXIS_TLAST ? 1:0); - end - - always @(*) - assert(f_reads == reads_completed); - always @(*) - assert(f_read_pkts == read_bursts_completed); - - always @(*) - if (!OPT_SINK) - assert(S_AXIS_TREADY); - - // - // Mirror the write counter - // - initial f_writes = 0; - initial f_write_pkts = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - begin - f_writes <= 0; - f_write_pkts <= 0; - end else if (OPT_SOURCE && M_AXIS_TVALID && M_AXIS_TREADY) - begin - f_writes <= f_writes + 1; - f_write_pkts <= f_write_pkts + (M_AXIS_TLAST ? 1:0); - end - - always @(*) - if (!OPT_SOURCE) - begin - assert(f_writes == 0); - assert(f_write_pkts == 0); - end - - always @(*) - begin - assert(f_writes == writes_completed); - assert(f_write_pkts == write_bursts_completed); - end - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Verify the read result - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - always @(posedge S_AXI_ACLK) - if (f_past_valid && $past(S_AXI_ARESETN && axil_read_ready)) - begin - assert(S_AXI_RVALID); - case($past(arskd_addr)) - ADDR_SINK: begin - assert(S_AXI_RDATA[SW-1:0] == $past(rfifo_data)); - if (SW < C_AXI_DATA_WIDTH) - begin - if (OPT_SIGN_EXTEND && $past(rfifo_data[SW-1])) - assert(&S_AXI_RDATA[C_AXI_DATA_WIDTH-1:SW]); - else - assert(S_AXI_RDATA[C_AXI_DATA_WIDTH-1:SW] == 0); - end end - // 1: assert(S_AXI_RDATA == $past(r1)); - ADDR_STATS: begin - assert(S_AXI_RRESP == 2'b00); - assert(S_AXI_RDATA[31:28] - == $past(write_bursts_completed)); - assert(S_AXI_RDATA[27:16] == $past(writes_completed)); - - assert(S_AXI_RDATA[15:12] - == $past(read_bursts_completed)); - assert(S_AXI_RDATA[11:0] == $past(reads_completed)); - end - ADDR_FIFO: begin - assert(S_AXI_RRESP == 2'b00); - if (LGFIFO < 16) - assert(S_AXI_RDATA[31:16+LGFIFO+1] == 0); - assert(S_AXI_RDATA[16+: LGFIFO+1]==$past(wfifo_fill)); - assert(S_AXI_RDATA[15] == $past(rfifo_last)); - if (LGFIFO < 15) - assert(S_AXI_RDATA[14:LGFIFO+1] == 0); - assert(S_AXI_RDATA[ 0+: LGFIFO+1]==$past(rfifo_fill)); - end - default: begin end - endcase - end - - // - // Check that our low-power only logic works by verifying that anytime - // S_AXI_RVALID is inactive, then the outgoing data is also zero. - // - always @(*) - if (OPT_LOWPOWER && !S_AXI_RVALID) - assert(S_AXI_RDATA == 0); - - // }}} - //////////////////////////////////////////////////////////////////////// - // - // The AXI-stream interfaces - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - - // Slave/consumer properties - always @(posedge S_AXI_ACLK) - if (!f_past_valid || !$past(S_AXI_ARESETN)) - begin - assume(!S_AXIS_TVALID); - end else if ($past(S_AXIS_TVALID && !S_AXIS_TREADY)) - begin - assume(S_AXIS_TVALID); - assume($stable(S_AXIS_TDATA)); - assume($stable(S_AXIS_TLAST)); - end - - // Master/producer/source properties - always @(posedge S_AXI_ACLK) - if (!f_past_valid || !$past(S_AXI_ARESETN)) - begin - assert(!M_AXIS_TVALID); - end else if ($past(M_AXIS_TVALID && !M_AXIS_TREADY)) - begin - assert(M_AXIS_TVALID); - assert($stable(M_AXIS_TDATA)); - assert($stable(M_AXIS_TLAST)); - end - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Cover checks - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - - always @(*) - cover(S_AXI_ARESETN && writes_completed == 16); - - always @(*) - cover(S_AXI_ARESETN && reads_completed == 16); - - always @(*) - cover(S_AXI_ARESETN && writes_completed == 16 - && reads_completed == 16); - - always @(*) - cover(S_AXI_BVALID && S_AXI_BRESP != 2'b00); - - always @(*) - cover(S_AXI_RVALID && S_AXI_RRESP != 2'b00); - - // }}} - // }}} -`endif -endmodule diff --git a/rtl/wb2axip/axildouble.v b/rtl/wb2axip/axildouble.v index ddaedb6..fcb4f49 100644 --- a/rtl/wb2axip/axildouble.v +++ b/rtl/wb2axip/axildouble.v @@ -97,7 +97,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // `ifdef VERILATOR // `define FORMAL // `endif @@ -730,5 +730,5 @@ module axildouble #( `endif endmodule // `ifndef YOSYS -// `default_nettype wire +// //`default_nettype wire // `endif diff --git a/rtl/wb2axip/axilempty.v b/rtl/wb2axip/axilempty.v index f429d69..656f1b7 100644 --- a/rtl/wb2axip/axilempty.v +++ b/rtl/wb2axip/axilempty.v @@ -36,7 +36,7 @@ // //////////////////////////////////////////////////////////////////////////////// // -`default_nettype none +//`default_nettype none // }}} module axilempty #( // {{{ @@ -47,7 +47,7 @@ module axilempty #( // Verilator lint_off UNUSED parameter C_AXI_ADDR_WIDTH = 4, // Verilator lint_on UNUSED - localparam C_AXI_DATA_WIDTH = 32, + /*local*/parameter C_AXI_DATA_WIDTH = 32, parameter [0:0] OPT_SKIDBUFFER = 1'b0, parameter [0:0] OPT_LOWPOWER = 0 // }}} diff --git a/rtl/wb2axip/axilfetch.v b/rtl/wb2axip/axilfetch.v index 7089b20..0b612ed 100644 --- a/rtl/wb2axip/axilfetch.v +++ b/rtl/wb2axip/axilfetch.v @@ -31,7 +31,7 @@ // //////////////////////////////////////////////////////////////////////////////// // -`default_nettype none +//`default_nettype none // }}} module axilfetch #( // {{{ @@ -40,7 +40,7 @@ module axilfetch #( parameter INSN_WIDTH=32, parameter FETCH_LIMIT=16, parameter [0:0] SWAP_ENDIANNESS = 1'b1, - localparam AW=C_AXI_ADDR_WIDTH + /*local*/parameter AW=C_AXI_ADDR_WIDTH // }}} ) ( // {{{ @@ -293,11 +293,15 @@ module axilfetch #( genvar gw, gb; // Word count, byte count for(gw=0; gw w_count); - w_aw_greater <= ( w_count > aw_count + 1); - end - 2'b01: begin - aw_w_greater <= (aw_count > w_count + 1); - w_aw_greater <= ( w_count + 1 > aw_count); - end - default: begin end - endcase - // }}} - // - // Read channel - // {{{ - - // r_count, r_zero, r_full - initial r_count = 0; - initial r_zero = 1; - initial r_full = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - begin - r_count <= 0; - r_zero <= 1; - r_full <= 0; - end else case({(arskd_valid&&arskd_ready), S_AXI_RVALID&&S_AXI_RREADY}) - 2'b10: begin - r_count <= r_count + 1; - r_zero <= 0; - r_full <= (r_count == { {(LGDEPTH-1){1'b1}}, 1'b0 }); - end - 2'b01: begin - r_count <= r_count - 1; - r_zero <= (r_count <= 1); - r_full <= 0; - end - default: begin end - endcase - // }}} - - // - // Downstream write address channel - // {{{ - - initial downstream_aw_count = 0; - initial downstream_aw_zero = 1; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault) - begin - downstream_aw_count <= 0; - downstream_aw_zero <= 1; - end else case({(M_AXI_AWVALID && M_AXI_AWREADY), M_AXI_BVALID && M_AXI_BREADY}) - 2'b10: begin - downstream_aw_count <= downstream_aw_count + 1; - downstream_aw_zero <= 0; - end - 2'b01: begin - downstream_aw_count <= downstream_aw_count - 1; - downstream_aw_zero <= (downstream_aw_count <= 1); - end - default: begin end - endcase - // }}} - - // - // Downstream write data channel - // {{{ - initial downstream_w_count = 0; - initial downstream_w_zero = 1; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault) - begin - downstream_w_count <= 0; - downstream_w_zero <= 1; - end else case({(M_AXI_WVALID && M_AXI_WREADY), M_AXI_BVALID && M_AXI_BREADY}) - 2'b10: begin - downstream_w_count <= downstream_w_count + 1; - downstream_w_zero <= 0; - end - 2'b01: begin - downstream_w_count <= downstream_w_count - 1; - downstream_w_zero <= (downstream_w_count <= 1); - end - default: begin end - endcase - // }}} - - // - // Downstream read channel - // {{{ - - initial downstream_r_count = 0; - initial downstream_r_zero = 1; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_read_fault) - begin - downstream_r_count <= 0; - downstream_r_zero <= 1; - end else case({M_AXI_ARVALID && M_AXI_ARREADY, M_AXI_RVALID && M_AXI_RREADY}) - 2'b10: begin - downstream_r_count <= downstream_r_count + 1; - downstream_r_zero <= 0; - end - 2'b01: begin - downstream_r_count <= downstream_r_count - 1; - downstream_r_zero <= (downstream_r_count <= 1); - end - default: begin end - endcase - // }}} - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Timeout checking - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - - // The key piece here is that we define the timeout depending upon - // what happens (or doesn't happen) *DOWNSTREAM*. These timeouts - // will need to propagate upstream before taking place. - - // - // Write address stall counter - // {{{ - initial aw_stall_counter = 0; - initial aw_stall_limit = 1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || o_write_fault || !M_AXI_ARESETN) - begin - aw_stall_counter <= 0; - aw_stall_limit <= 0; - end else if (!M_AXI_AWVALID || M_AXI_AWREADY || M_AXI_BVALID) - begin - aw_stall_counter <= 0; - aw_stall_limit <= 0; - end else if (aw_w_greater && !M_AXI_WVALID) - begin - aw_stall_counter <= 0; - aw_stall_limit <= 0; - end else // if (!S_AXI_BVALID || S_AXI_BREADY) - begin - aw_stall_counter <= aw_stall_counter + 1; - aw_stall_limit <= (aw_stall_counter+1 >= OPT_TIMEOUT); - end - // }}} - - // - // Write data stall counter - // {{{ - initial w_stall_counter = 0; - initial w_stall_limit = 1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault) - begin - w_stall_counter <= 0; - w_stall_limit <= 0; - end else if (!M_AXI_WVALID || M_AXI_WREADY || M_AXI_BVALID) - begin - w_stall_counter <= 0; - w_stall_limit <= 0; - end else if (w_aw_greater && !M_AXI_AWVALID) - begin - w_stall_counter <= 0; - w_stall_limit <= 0; - end else // if (!M_AXI_BVALID || M_AXI_BREADY) - begin - w_stall_counter <= w_stall_counter + 1; - w_stall_limit <= (w_stall_counter + 1 >= OPT_TIMEOUT); - end - // }}} - - // - // Write acknowledgment delay counter - // {{{ - initial w_ack_timer = 0; - initial w_ack_limit = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault) - begin - w_ack_timer <= 0; - w_ack_limit <= 0; - end else if (M_AXI_BVALID || downstream_aw_zero || downstream_w_zero) - begin - w_ack_timer <= 0; - w_ack_limit <= 0; - end else - begin - w_ack_timer <= w_ack_timer + 1; - w_ack_limit <= (w_ack_timer + 1 >= OPT_TIMEOUT); - end - // }}} - - // - // Read request stall counter - // {{{ - initial r_stall_counter = 0; - initial r_stall_limit = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_read_fault) - begin - r_stall_counter <= 0; - r_stall_limit <= 0; - end else if (!M_AXI_ARVALID || M_AXI_ARREADY || M_AXI_RVALID) - begin - r_stall_counter <= 0; - r_stall_limit <= 0; - end else begin - r_stall_counter <= r_stall_counter + 1; - r_stall_limit <= (r_stall_counter + 1 >= OPT_TIMEOUT); - end - // }}} - - // - // Read acknowledgement delay counter - // {{{ - initial r_ack_timer = 0; - initial r_ack_limit = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_read_fault) - begin - r_ack_timer <= 0; - r_ack_limit <= 0; - end else if (M_AXI_RVALID || downstream_r_zero) - begin - r_ack_timer <= 0; - r_ack_limit <= 0; - end else begin - r_ack_timer <= r_ack_timer + 1; - r_ack_limit <= (r_ack_timer + 1 >= OPT_TIMEOUT); - end - // }}} - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Fault detection - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - - // - // Determine if a write fault has taken place - // {{{ - initial o_write_fault =1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - o_write_fault <= 1'b0; - else if (OPT_SELF_RESET && o_write_fault) - begin - // - // Clear any fault on reset - if (!M_AXI_ARESETN) - o_write_fault <= 1'b0; - end else begin - // - // A write fault takes place if you respond without a prior - // bus request on both write address and write data channels. - if ((downstream_aw_zero || downstream_w_zero)&&(bskd_valid)) - o_write_fault <= 1'b1; - - // AXI-lite slaves are not allowed to return EXOKAY responses - // from the bus - if (bskd_valid && bskd_resp == EXOKAY) - o_write_fault <= 1'b1; - - // If the downstream core refuses to accept either a - // write address request, or a write data request, or for that - // matter if it doesn't return an acknowledgment in a timely - // fashion, then a fault has been detected. - if (aw_stall_limit || w_stall_limit || w_ack_limit) - o_write_fault <= 1'b1; - - // If the downstream core changes BRESP while VALID && !READY, - // then it isn't stalling the channel properly--that's a fault. - if (last_bchanged) - o_write_fault <= 1'b1; - end - // }}} - - // o_read_fault - // {{{ - initial o_read_fault =1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - o_read_fault <= 1'b0; - else if (OPT_SELF_RESET && o_read_fault) - begin - // - // Clear any fault on reset - if (!M_AXI_ARESETN) - o_read_fault <= 1'b0; - end else begin - // Responding without a prior request is a fault. Can only - // respond after a request has been made. - if (downstream_r_zero && rskd_valid) - o_read_fault <= 1'b1; - - // AXI-lite slaves are not allowed to return EXOKAY. This is - // an error. - if (rskd_valid && rskd_resp == EXOKAY) - o_read_fault <= 1'b1; - - // The slave cannot stall the bus forever, nor should the - // master wait forever for a response from the slave. - if (r_stall_limit || r_ack_limit) - o_read_fault <= 1'b1; - - // If the slave changes the data, or the RRESP on the wire, - // while the incoming bus is stalled, then that's also a fault. - if (last_rchanged) - o_read_fault <= 1'b1; - end - // }}} - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Self reset handling - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - - generate if (OPT_SELF_RESET) - begin : SELF_RESET_GENERATION - // {{{ - wire min_reset; - - if (OPT_MIN_RESET > 1) - begin : MIN_RESET - // {{{ - reg r_min_reset; - reg [$clog2(OPT_MIN_RESET+1):0] reset_counter; - - // - // Optionally insist that any downstream reset have a - // minimum duration. Many Xilinx components require - // a 16-clock reset. This ensures such reset - // requirements are achieved. - // - - initial reset_counter = OPT_MIN_RESET-1; - initial r_min_reset = 1'b0; - always @(posedge S_AXI_ARESETN) - if (M_AXI_ARESETN) - begin - reset_counter <= OPT_MIN_RESET-1; - r_min_reset <= 1'b0; - end else if (!M_AXI_ARESETN) - begin - if (reset_counter > 0) - reset_counter <= reset_counter-1; - min_reset <= (reset_counter <= 1); - end - - assign min_reset = r_min_reset; -`ifdef FORMAL - always @(*) - assert(reset_counter < OPT_MIN_RESET); - always @(*) - assert(min_reset == (reset_counter == 0)); -`endif - // }}} - end else begin : NO_MIN_RESET - // {{{ - assign min_reset = 1'b1; - // }}} - end - - // M_AXI_ARESETN - // {{{ - // Reset the downstream bus on either a write or a read fault. - // Once the bus returns to idle, and any minimum reset durations - // have been achieved, then release the downstream from reset. - // - initial M_AXI_ARESETN = 1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - M_AXI_ARESETN <= 1'b0; - else if (o_write_fault || o_read_fault) - M_AXI_ARESETN <= 1'b0; - else if (aw_zero && w_zero && r_zero && min_reset - && !awskd_valid && !wskd_valid && !arskd_valid) - M_AXI_ARESETN <= 1'b1; - // }}} - // }}} - end else begin : SAME_RESET - // {{{ - // - // The downstream reset equals the upstream reset - // - always @(*) - M_AXI_ARESETN = S_AXI_ARESETN; - // }}} - end endgenerate - // }}} -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -// -// Formal property section -// {{{ -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -`ifdef FORMAL - // {{{ - // - // The following proof comes in several parts. - // - // 1. PROVE that the upstream properties will hold independent of - // what the downstream slave ever does. - // - // 2. PROVE that if the downstream slave follows protocol, then - // neither o_write_fault nor o_read_fault will never get raised. - // - // We then repeat these proofs again with both OPT_SELF_RESET set and - // clear. Which of the four proofs is accomplished is dependent upon - // parameters set by the formal engine. - // - // - wire [LGDEPTH:0] faxils_awr_outstanding, faxils_wr_outstanding, - faxils_rd_outstanding; - - reg f_past_valid; - initial f_past_valid = 0; - always @(posedge S_AXI_ACLK) - f_past_valid <= 1; - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Upstream master Bus properties - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - always @(*) - if (!f_past_valid) - begin - assume(!S_AXI_ARESETN); - assert(!M_AXI_ARESETN); - end - - faxil_slave #( - // {{{ - .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH), - .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), - .F_OPT_ASSUME_RESET(1'b1), - .F_OPT_NO_RESET((OPT_MIN_RESET == 0) ? 1:0), -// .F_AXI_MAXWAIT((F_OPT_FAULTLESS) ? (2*OPT_TIMEOUT+2) : 0), - .F_AXI_MAXRSTALL(3), -// .F_AXI_MAXDELAY(OPT_TIMEOUT+OPT_TIMEOUT+5), - .F_LGDEPTH(LGDEPTH+1), - // - .F_AXI_MAXWAIT((F_OPT_FAULTLESS) ? (2*OPT_TIMEOUT+2) : 0), - .F_AXI_MAXDELAY(2*OPT_TIMEOUT+3) - // }}} - ) axils ( - // {{{ - .i_clk(S_AXI_ACLK), - .i_axi_reset_n(S_AXI_ARESETN), - // - .i_axi_awvalid(S_AXI_AWVALID), - .i_axi_awready(S_AXI_AWREADY), - .i_axi_awaddr( S_AXI_AWADDR), - .i_axi_awprot( S_AXI_AWPROT), - // - .i_axi_wvalid(S_AXI_WVALID), - .i_axi_wready(S_AXI_WREADY), - .i_axi_wdata( S_AXI_WDATA), - .i_axi_wstrb( S_AXI_WSTRB), - // - .i_axi_bvalid(S_AXI_BVALID), - .i_axi_bready(S_AXI_BREADY), - .i_axi_bresp( S_AXI_BRESP), - // - .i_axi_arvalid(S_AXI_ARVALID), - .i_axi_arready(S_AXI_ARREADY), - .i_axi_araddr( S_AXI_ARADDR), - .i_axi_arprot( S_AXI_ARPROT), - // - .i_axi_rvalid(S_AXI_RVALID), - .i_axi_rready(S_AXI_RREADY), - .i_axi_rdata( S_AXI_RDATA), - .i_axi_rresp( S_AXI_RRESP), - // - .f_axi_awr_outstanding(faxils_awr_outstanding), - .f_axi_wr_outstanding(faxils_wr_outstanding), - .f_axi_rd_outstanding(faxils_rd_outstanding) - // }}} - ); - - always @(*) - if (!F_OPT_WRITES) - begin - // {{{ - assume(!S_AXI_AWVALID); - assume(!S_AXI_WVALID); - assert(aw_count == 0); - assert(w_count == 0); - assert(!M_AXI_AWVALID); - assert(!M_AXI_WVALID); - // }}} - end - - always @(*) - if (!F_OPT_READS) - begin - // {{{ - assume(!S_AXI_ARVALID); - assert(r_count == 0); - assert(!S_AXI_RVALID); - assert(!M_AXI_ARVALID); - // }}} - end - // }}} - //////////////////////////////////////////////////////////////////////// - // - // General Induction properties - // {{{ - //////////////////////////////////////////////////////////////////////// - // - - always @(*) - begin - // {{{ - assert(aw_zero == (aw_count == 0)); - assert(w_zero == (w_count == 0)); - assert(r_zero == (r_count == 0)); - - // - assert(aw_full == (&aw_count)); - assert(w_full == (&w_count)); - assert(r_full == (&r_count)); - // - if (M_AXI_ARESETN && !o_write_fault) - begin - assert(downstream_aw_zero == (downstream_aw_count == 0)); - assert(downstream_w_zero == (downstream_w_count == 0)); - assert(downstream_aw_count + (M_AXI_AWVALID ? 1:0) - + (S_AXI_BVALID ? 1:0) == aw_count); - assert(downstream_w_count + (M_AXI_WVALID ? 1:0) - + (S_AXI_BVALID ? 1:0) == w_count); - end - - if (M_AXI_ARESETN && !o_read_fault) - begin - assert(downstream_r_zero == (downstream_r_count == 0)); - assert(downstream_r_count + (M_AXI_ARVALID ? 1:0) - + (S_AXI_RVALID ? 1:0) == r_count); - end - // - assert(aw_count == faxils_awr_outstanding); - assert(w_count == faxils_wr_outstanding); - assert(r_count == faxils_rd_outstanding); - - assert(aw_w_greater == (aw_count > w_count)); - assert(w_aw_greater == (w_count > aw_count)); - // }}} - end - // }}} - generate if (F_OPT_FAULTLESS) - begin : ASSUME_FAULTLESS - // {{{ - //////////////////////////////////////////////////////////////// - // - // Assume the downstream core is protocol compliant, and - // prove that o_fault stays low. - // {{{ - //////////////////////////////////////////////////////////////// - // - wire [LGDEPTH:0] faxilm_awr_outstanding, - faxilm_wr_outstanding, - faxilm_rd_outstanding; - - faxil_master #( - // {{{ - .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH), - .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), - .F_OPT_NO_RESET((OPT_MIN_RESET == 0) ? 1:0), - .F_AXI_MAXWAIT(OPT_TIMEOUT), - .F_AXI_MAXRSTALL(4), - .F_AXI_MAXDELAY(OPT_TIMEOUT), - .F_LGDEPTH(LGDEPTH+1) - // }}} - ) axilm ( - // {{{ - .i_clk(S_AXI_ACLK), - .i_axi_reset_n(M_AXI_ARESETN && S_AXI_ARESETN), - // - .i_axi_awvalid(M_AXI_AWVALID), - .i_axi_awready(M_AXI_AWREADY), - .i_axi_awaddr( M_AXI_AWADDR), - .i_axi_awprot( M_AXI_AWPROT), - // - .i_axi_wvalid(M_AXI_WVALID), - .i_axi_wready(M_AXI_WREADY), - .i_axi_wdata( M_AXI_WDATA), - .i_axi_wstrb( M_AXI_WSTRB), - // - .i_axi_bvalid(M_AXI_BVALID), - .i_axi_bready(M_AXI_BREADY), - .i_axi_bresp( M_AXI_BRESP), - // - .i_axi_arvalid(M_AXI_ARVALID), - .i_axi_arready(M_AXI_ARREADY), - .i_axi_araddr( M_AXI_ARADDR), - .i_axi_arprot( M_AXI_ARPROT), - // - .i_axi_rvalid(M_AXI_RVALID), - .i_axi_rready(M_AXI_RREADY), - .i_axi_rdata( M_AXI_RDATA), - .i_axi_rresp( M_AXI_RRESP), - // - .f_axi_awr_outstanding(faxilm_awr_outstanding), - .f_axi_wr_outstanding(faxilm_wr_outstanding), - .f_axi_rd_outstanding(faxilm_rd_outstanding) - // }}} - ); - - // - // Here's the big proof - // {{{ - always @(*) - assert(!o_write_fault); - always @(*) - assert(!o_read_fault); - // }}} - // }}} - //////////////////////////////////////////////////////////////// - // - // The following properties are necessary for passing induction - // {{{ - //////////////////////////////////////////////////////////////// - // - // - always @(*) - begin - assert(!aw_stall_limit); - assert(!w_stall_limit); - assert(!w_ack_limit); - - assert(!r_stall_limit); - assert(!r_ack_limit); - - if (M_AXI_ARESETN) - begin - assert(downstream_aw_count == faxilm_awr_outstanding); - assert(downstream_w_count == faxilm_wr_outstanding); - assert(downstream_r_count == faxilm_rd_outstanding); - end - end - - if (OPT_SELF_RESET) - begin - always @(posedge S_AXI_ACLK) - if (f_past_valid) - assert(M_AXI_ARESETN == $past(S_AXI_ARESETN)); - end - -`ifdef VERIFIC - wire [LGDEPTH:0] f_axi_arstall; - wire [LGDEPTH:0] f_axi_awstall; - wire [LGDEPTH:0] f_axi_wstall; - - assign f_axi_awstall = axilm.CHECK_STALL_COUNT.f_axi_awstall; - assign f_axi_wstall = axilm.CHECK_STALL_COUNT.f_axi_wstall; - assign f_axi_arstall = axilm.CHECK_STALL_COUNT.f_axi_arstall; - - always @(*) - if (M_AXI_ARESETN && S_AXI_ARESETN && !o_write_fault) - assert(f_axi_awstall == aw_stall_counter); - - always @(*) - if (M_AXI_ARESETN && S_AXI_ARESETN && !o_write_fault) - assert(f_axi_wstall == w_stall_counter); - - always @(*) - if (M_AXI_ARESETN && S_AXI_ARESETN && !o_read_fault) - assert(f_axi_arstall == r_stall_counter); -`endif - // }}} - // }}} - end else begin : WILD_DOWNSTREAM - // {{{ - //////////////////////////////////////////////////////////////// - // - // cover() checks, checks that only make sense if faults are - // possible - // - - reg write_faulted, read_faulted, faulted; - reg [3:0] cvr_writes, cvr_reads; - - - if (OPT_SELF_RESET) - begin - //////////////////////////////////////////////////////// - // - // Prove that we can actually reset the downstream - // bus/core as desired - // {{{ - //////////////////////////////////////////////////////// - // - // - initial write_faulted = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - write_faulted <= 0; - else if (o_write_fault) - write_faulted <= 1; - - - initial faulted = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - read_faulted <= 0; - else if (o_read_fault) - read_faulted <= 1; - - always @(*) - faulted = (write_faulted || read_faulted); - - always @(posedge S_AXI_ACLK) - cover(write_faulted && $rose(M_AXI_ARESETN)); - - always @(posedge S_AXI_ACLK) - cover(read_faulted && $rose(M_AXI_ARESETN)); - - always @(posedge S_AXI_ACLK) - cover(faulted && M_AXI_ARESETN && S_AXI_BVALID); - - always @(posedge S_AXI_ACLK) - cover(faulted && M_AXI_ARESETN && S_AXI_RVALID); - - - initial cvr_writes = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault) - cvr_writes <= 0; - else if (write_faulted && S_AXI_BVALID && S_AXI_BREADY - && S_AXI_BRESP == OKAY - &&(!(&cvr_writes))) - cvr_writes <= cvr_writes + 1; - - always @(*) - cover(cvr_writes > 5); - - initial cvr_reads = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_read_fault) - cvr_reads <= 0; - else if (read_faulted && S_AXI_RVALID && S_AXI_RREADY - && S_AXI_RRESP == OKAY - &&(!(&cvr_reads))) - cvr_reads <= cvr_reads + 1; - - always @(*) - cover(cvr_reads > 5); - // }}} - end - - // }}} - end endgenerate - //////////////////////////////////////////////////////////////////////// - // - // Never data properties - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - (* anyconst *) reg [C_AXI_DATA_WIDTH-1:0] fc_never_read_data; - (* anyconst *) reg [C_AXI_DATA_WIDTH+C_AXI_DATA_WIDTH/8-1:0] - fc_never_write_data; - - (* anyconst *) reg [C_AXI_ADDR_WIDTH-1:0] fc_never_read_addr, - fc_never_write_addr; - - // Write address checking - // {{{ - always @(*) - if (S_AXI_ARESETN && S_AXI_AWVALID) - assume(S_AXI_AWADDR != fc_never_write_addr); - - always @(*) - if (S_AXI_ARESETN && M_AXI_ARESETN && !o_write_fault && M_AXI_AWVALID) - assert(M_AXI_AWADDR != fc_never_write_addr); - // }}} - - // Write checking - // {{{ - always @(*) - if (S_AXI_ARESETN && S_AXI_WVALID) - assume({ S_AXI_WDATA, S_AXI_WSTRB } != fc_never_write_data); - - always @(*) - if (S_AXI_ARESETN && M_AXI_ARESETN && !o_write_fault && M_AXI_WVALID) - assert({ M_AXI_WDATA, M_AXI_WSTRB } != fc_never_write_data); - // }}} - - // Read address checking - // {{{ - always @(*) - if (S_AXI_ARESETN && S_AXI_ARVALID) - assume(S_AXI_ARADDR != fc_never_read_addr); - - always @(*) - if (S_AXI_ARESETN && M_AXI_ARESETN && !o_read_fault && M_AXI_ARVALID) - assert(M_AXI_ARADDR != fc_never_read_addr); - // }}} - - // Read checking - // {{{ - always @(*) - if (S_AXI_ARESETN && M_AXI_ARESETN && M_AXI_RVALID) - assume(M_AXI_RDATA != fc_never_read_data); - - always @(*) - if (S_AXI_ARESETN && S_AXI_RVALID && S_AXI_RRESP == 2'b00) - assert(S_AXI_RDATA != fc_never_read_data); - // }}} - - // }}} - -`endif -// }}} -endmodule diff --git a/rtl/wb2axip/axilsingle.v b/rtl/wb2axip/axilsingle.v index e92db40..8da2685 100644 --- a/rtl/wb2axip/axilsingle.v +++ b/rtl/wb2axip/axilsingle.v @@ -101,7 +101,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // `ifdef VERILATOR // `define FORMAL // `endif @@ -112,7 +112,7 @@ module axilsingle #( parameter NS = 16, // parameter integer C_AXI_DATA_WIDTH = 32, - localparam integer C_AXI_ADDR_WIDTH = $clog2(NS)+$clog2(C_AXI_DATA_WIDTH)-3, + /*local*/parameter integer C_AXI_ADDR_WIDTH = $clog2(NS)+$clog2(C_AXI_DATA_WIDTH)-3, // // LGFLEN specifies the log (based two) of the number of // transactions that may need to be held outstanding internally. @@ -710,5 +710,5 @@ module axilsingle #( `endif endmodule // `ifndef YOSYS -// `default_nettype wire +// //`default_nettype wire // `endif diff --git a/rtl/wb2axip/axilupsz.v b/rtl/wb2axip/axilupsz.v index 29dc41d..0d3c4ad 100644 --- a/rtl/wb2axip/axilupsz.v +++ b/rtl/wb2axip/axilupsz.v @@ -31,7 +31,7 @@ // //////////////////////////////////////////////////////////////////////////////// // -`default_nettype none +//`default_nettype none // }}} module axilupsz #( // {{{ @@ -40,9 +40,9 @@ module axilupsz #( parameter C_AXIL_ADDR_WIDTH = 32, parameter LGFIFO = 5, parameter [0:0] OPT_LOWPOWER = 1, - localparam SDW = C_S_AXIL_DATA_WIDTH, - localparam MDW = C_M_AXIL_DATA_WIDTH, - localparam AW = C_AXIL_ADDR_WIDTH + /*local*/parameter SDW = C_S_AXIL_DATA_WIDTH, + /*local*/parameter MDW = C_M_AXIL_DATA_WIDTH, + /*local*/parameter AW = C_AXIL_ADDR_WIDTH // }}} ) ( // {{{ diff --git a/rtl/wb2axip/axilwr2wbsp.v b/rtl/wb2axip/axilwr2wbsp.v index 9b75c0e..63f023c 100644 --- a/rtl/wb2axip/axilwr2wbsp.v +++ b/rtl/wb2axip/axilwr2wbsp.v @@ -33,16 +33,16 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module axilwr2wbsp #( // {{{ parameter C_AXI_DATA_WIDTH = 32, parameter C_AXI_ADDR_WIDTH = 28, - localparam AXI_LSBS = $clog2(C_AXI_DATA_WIDTH)-3, - localparam AW = C_AXI_ADDR_WIDTH-AXI_LSBS, + /*local*/parameter AXI_LSBS = $clog2(C_AXI_DATA_WIDTH)-3, + /*local*/parameter AW = C_AXI_ADDR_WIDTH-AXI_LSBS, parameter LGFIFO = 3, - localparam DW = C_AXI_DATA_WIDTH + /*local*/parameter DW = C_AXI_DATA_WIDTH // }}} ) ( // {{{ diff --git a/rtl/wb2axip/axilxbar.v b/rtl/wb2axip/axilxbar.v index 95c9172..44294b2 100644 --- a/rtl/wb2axip/axilxbar.v +++ b/rtl/wb2axip/axilxbar.v @@ -76,7 +76,7 @@ // //////////////////////////////////////////////////////////////////////////////// // -`default_nettype none +//`default_nettype none // }}} module axilxbar #( // {{{ @@ -90,8 +90,8 @@ module axilxbar #( parameter NS = 8, // // AW, and DW, are short-hand abbreviations used locally. - localparam AW = C_AXI_ADDR_WIDTH, - localparam DW = C_AXI_DATA_WIDTH, + /*local*/parameter AW = C_AXI_ADDR_WIDTH, + /*local*/parameter DW = C_AXI_DATA_WIDTH, // SLAVE_ADDR is a bit vector containing AW bits for each of the // slaves indicating the base address of the slave. This // goes with SLAVE_MASK below. @@ -2420,5 +2420,5 @@ module axilxbar #( // }}} endmodule `ifndef YOSYS -`default_nettype wire +//`default_nettype wire `endif diff --git a/rtl/wb2axip/axim2wbsp.v b/rtl/wb2axip/axim2wbsp.v index fb58458..729f5ac 100644 --- a/rtl/wb2axip/axim2wbsp.v +++ b/rtl/wb2axip/axim2wbsp.v @@ -39,7 +39,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module axim2wbsp #( // {{{ @@ -47,9 +47,9 @@ module axim2wbsp #( // This is an int between 1-16 parameter C_AXI_DATA_WIDTH = 32,// Width of the AXI R&W data parameter C_AXI_ADDR_WIDTH = 28, // AXI Address width - localparam AXI_LSBS = $clog2(C_AXI_DATA_WIDTH)-3, - localparam DW = C_AXI_DATA_WIDTH, - localparam AW = C_AXI_ADDR_WIDTH - AXI_LSBS, + /*local*/parameter AXI_LSBS = $clog2(C_AXI_DATA_WIDTH)-3, + /*local*/parameter DW = C_AXI_DATA_WIDTH, + /*local*/parameter AW = C_AXI_ADDR_WIDTH - AXI_LSBS, parameter LGFIFO = 5, parameter [0:0] OPT_SWAP_ENDIANNESS = 1'b0, parameter [0:0] OPT_READONLY = 1'b0, diff --git a/rtl/wb2axip/aximm2s.v b/rtl/wb2axip/aximm2s.v index b4c1056..eae16c8 100644 --- a/rtl/wb2axip/aximm2s.v +++ b/rtl/wb2axip/aximm2s.v @@ -135,7 +135,7 @@ // //////////////////////////////////////////////////////////////////////////////// // -`default_nettype none +//`default_nettype none // }}} module aximm2s #( // {{{ @@ -145,12 +145,12 @@ module aximm2s #( // // We support five 32-bit AXI-lite registers, requiring 5-bits // of AXI-lite addressing - localparam C_AXIL_ADDR_WIDTH = 5, - localparam C_AXIL_DATA_WIDTH = 32, + /*local*/parameter C_AXIL_ADDR_WIDTH = 5, + /*local*/parameter C_AXIL_DATA_WIDTH = 32, // // The bottom ADDRLSB bits of any AXI address are subword bits - localparam ADDRLSB = $clog2(C_AXI_DATA_WIDTH)-3, - localparam AXILLSB = $clog2(C_AXIL_DATA_WIDTH)-3, + /*local*/parameter ADDRLSB = $clog2(C_AXI_DATA_WIDTH)-3, + /*local*/parameter AXILLSB = $clog2(C_AXIL_DATA_WIDTH)-3, // // OPT_UNALIGNED: Allow unaligned accesses, address requests // and sizes which may or may not match the underlying data diff --git a/rtl/wb2axip/aximrd2wbsp.v b/rtl/wb2axip/aximrd2wbsp.v index 07dd7a7..bc7811d 100644 --- a/rtl/wb2axip/aximrd2wbsp.v +++ b/rtl/wb2axip/aximrd2wbsp.v @@ -44,7 +44,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module aximrd2wbsp #( // {{{ @@ -52,8 +52,8 @@ module aximrd2wbsp #( // This is an int between 1-16 parameter C_AXI_DATA_WIDTH = 32,// Width of the AXI R&W data parameter C_AXI_ADDR_WIDTH = 28, // AXI Address width - localparam AXI_LSBS = $clog2(C_AXI_DATA_WIDTH/8), - localparam AW = C_AXI_ADDR_WIDTH - AXI_LSBS, + /*local*/parameter AXI_LSBS = $clog2(C_AXI_DATA_WIDTH/8), + /*local*/parameter AW = C_AXI_ADDR_WIDTH - AXI_LSBS, parameter LGFIFO = 3, parameter [0:0] OPT_SWAP_ENDIANNESS = 1'b0, parameter [0:0] OPT_SIZESEL = 1 diff --git a/rtl/wb2axip/aximwr2wbsp.v b/rtl/wb2axip/aximwr2wbsp.v index 074467c..820f004 100644 --- a/rtl/wb2axip/aximwr2wbsp.v +++ b/rtl/wb2axip/aximwr2wbsp.v @@ -32,7 +32,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module aximwr2wbsp #( // {{{ @@ -40,8 +40,8 @@ module aximwr2wbsp #( parameter C_AXI_DATA_WIDTH = 32, parameter C_AXI_ADDR_WIDTH = 28, parameter [0:0] OPT_SWAP_ENDIANNESS = 1'b0, - localparam AXI_LSBS = $clog2(C_AXI_DATA_WIDTH)-3, - localparam AW = C_AXI_ADDR_WIDTH-AXI_LSBS, + /*local*/parameter AXI_LSBS = $clog2(C_AXI_DATA_WIDTH)-3, + /*local*/parameter AW = C_AXI_ADDR_WIDTH-AXI_LSBS, parameter LGFIFO = 5 // }}} diff --git a/rtl/wb2axip/axiperf.v b/rtl/wb2axip/axiperf.v index f2498e6..920599b 100644 --- a/rtl/wb2axip/axiperf.v +++ b/rtl/wb2axip/axiperf.v @@ -334,7 +334,7 @@ // //////////////////////////////////////////////////////////////////////////////// // -`default_nettype none +//`default_nettype none // }}} module axiperf #( // {{{ @@ -343,7 +343,7 @@ module axiperf #( // is fixed at a width of 32-bits by Xilinx def'n, and 2) since // we only ever have 4 configuration words. parameter C_AXIL_ADDR_WIDTH = 7, - localparam C_AXIL_DATA_WIDTH = 32, + /*local*/parameter C_AXIL_DATA_WIDTH = 32, parameter C_AXI_DATA_WIDTH = 32, parameter C_AXI_ADDR_WIDTH = 32, parameter C_AXI_ID_WIDTH = 4, diff --git a/rtl/wb2axip/axis2mm.v b/rtl/wb2axip/axis2mm.v index d578e41..90c6d7d 100644 --- a/rtl/wb2axip/axis2mm.v +++ b/rtl/wb2axip/axis2mm.v @@ -208,7 +208,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module axis2mm #( // {{{ @@ -272,7 +272,7 @@ module axis2mm #( // addresses. Only applies to non fixed addresses and // (possibly) non-continuous bursts. (THIS IS A PLACEHOLDER. // UNALIGNED ADDRESSING IS NOT CURRENTLY SUPPORTED.) - localparam [0:0] OPT_UNALIGNED = 0, + /*local*/parameter [0:0] OPT_UNALIGNED = 0, // parameter [0:0] OPT_LOWPOWER = 1'b0, parameter [0:0] OPT_CLKGATE = OPT_LOWPOWER, @@ -288,8 +288,8 @@ module axis2mm #( // Size of the AXI-lite bus. These are fixed, since 1) AXI-lite // is fixed at a width of 32-bits by Xilinx def'n, and 2) since // we only ever have 4 configuration words. - localparam C_AXIL_ADDR_WIDTH = 5, - localparam C_AXIL_DATA_WIDTH = 32 + /*local*/parameter C_AXIL_ADDR_WIDTH = 5, + /*local*/parameter C_AXIL_DATA_WIDTH = 32 // }}} ) ( // {{{ @@ -2230,5 +2230,5 @@ module axis2mm #( // }}} endmodule `ifndef YOSYS -`default_nettype wire +//`default_nettype wire `endif diff --git a/rtl/wb2axip/axisafety.v b/rtl/wb2axip/axisafety.v deleted file mode 100644 index ff7e351..0000000 --- a/rtl/wb2axip/axisafety.v +++ /dev/null @@ -1,2339 +0,0 @@ -//////////////////////////////////////////////////////////////////////////////// -// -// Filename: axisafety.v -// {{{ -// Project: WB2AXIPSP: bus bridges and other odds and ends -// -// Purpose: Given that 1) AXI interfaces can be difficult to write and to -// get right, 2) my experiences with the AXI infrastructure of an -// ARM+FPGA is that the device needs a power cycle following a bus fault, -// and given that I've now found multiple interfaces that had some bug -// or other within them, the following is a bus fault isolator. It acts -// as a bump in the log between the interconnect and the user core. As -// such, it has two interfaces: The first is the slave interface, -// coming from the interconnect. The second interface is the master -// interface, proceeding to a slave that might be faulty. -// -// INTERCONNECT --> (S) AXISAFETY (M) --> POTENTIALLY FAULTY CORE -// -// The slave interface has been formally verified to be a valid AXI -// slave, independent of whatever the potentially faulty core might do. -// If the user core (i.e. the potentially faulty one) responds validly -// to the requests of a master, then this core will turn into a simple -// delay on the bus. If, on the other hand, the user core suffers from -// a protocol error, then this core will set one of two output -// flags--either o_write_fault or o_read_fault indicating whether a write -// or a read fault was detected. Further attempts to access the user -// core will result in bus errors, generated by the AXISAFETY core. -// -// Assuming the bus master can properly detect and deal with a bus error, -// this should then make it possible to properly recover from a bus -// protocol error without later needing to cycle power. -// -// The core does have a couple of limitations. For example, it can only -// handle one burst transaction, and one ID at a time. This matches the -// performances of Xilinx's example AXI full core, from which many user -// cores have have been copied/modified from. Therefore, there will be -// no performance loss for such a core. -// -// Because of this, it is still possible that the user core might have an -// undetected fault when using this core. For example, if the interconnect -// issues more than one bus request before receiving the response from the -// first request, this safety core will stall the second request, -// preventing the downstream core from seeing this second request. If the -// downstream core would suffer from an error while handling the second -// request, by preventing the user core from seeing the second request this -// core eliminates that potential for error. -// -// Usage: The important part of using this core is to connect the slave -// side to the interconnect, and the master side to the user core. -// -// Some options are available: -// -// 1) C_S_AXI_ADDR_WIDTH The number of address bits in the AXI channel -// 1) C_S_AXI_DATA_WIDTH The number of data bits in the AXI channel -// 3) C_S_AXI_ID_WIDTH The number of bits in an AXI ID. As currently -// written, this number cannot be zero. You can, however, set it -// to '1' and connect all of the relevant ID inputs to zero. -// -// These three parameters have currently been abbreviated with AW, DW, and -// IW. I anticipate returning them to their original meanings, I just -// haven't done so (yet). -// -// 4) OPT_TIMEOUT This is the number of clock periods, from -// interconnect request to interconnect response, that the -// slave needs to respond within. (The actual timeout from the -// user slave's perspective will be shorter than this.) -// -// This timeout is part of the check that a slave core will -// always return a response. From the standpoint of this core, -// it can be set arbitrarily large. (From the standpoint of -// formal verification, it needs to be kept short ...) -// Feel free to set this even as large as 1ms if you would like. -// -// 5) OPT_SELF_RESET If set, will send a reset signal to the slave -// following any write or read fault. This will cause the other -// side of the link (write or read) to fault as well. Once the -// channel then becomes inactive, the slave will be released from -// reset and will be able to interact with the rest of the bus -// again. -// -// 5) OPT_EXCLUSIVE If clear, will prohibit the slave from ever -// receiving an exclusive access request. This saves the logic -// in the firewall necessary to check that an EXOKAY response -// to a write request was truly an allowed response. Since that -// logic can explode with the ID width, sparing it can be quite -// useful. If set, provides full exclusive access checking in -// addition to the normal bus fault checking. -// -// Performance: As mentioned above, this core can handle one read burst and one -// write burst at a time, no more. Further, the core will delay -// an input path by one clock and the output path by another clock, so that -// the latency involved with using this core is a minimum of two extra -// clocks beyond the latency user slave core. -// -// Maximum write latency: N+3 clocks for a burst of N values -// Maximum read latency: N+3 clocks for a burst of N values -// -// Faults detected: -// -// Write channel: -// 1. Raising BVALID prior to the last write value being sent -// to the user/slave core. -// 2. Raising BVALID prior to accepting the write address -// 3. A BID return ID that doesn't match the request AWID -// 4. Sending too many returns, such as not dropping BVALID -// or raising it when there is no outstanding write -// request -// -// While the following technically isn't a violation of the -// AXI protocol, it is treated as such by this fault isolator. -// -// 5. Accepting write data prior to the write address -// -// The fault isolator will guarantee that AWVALID is raised before -// WVALID, so this shouldn't be a problem. -// -// Read channel: -// -// 1. Raising RVALID before accepting the read address, ARVALID -// 2. A return ID that doesn't match the ID that was sent. -// 3. Raising RVALID after the last return value, and so returning -// too many response values -// 4. Setting the RLAST value on anything but the last value from -// the bus. -// -// -// Creator: Dan Gisselquist, Ph.D. -// Gisselquist Technology, LLC -// -//////////////////////////////////////////////////////////////////////////////// -// }}} -// Copyright (C) 2019-2024, Gisselquist Technology, LLC -// {{{ -// This file is part of the WB2AXIP project. -// -// The WB2AXIP project contains free software and gateware, licensed under the -// Apache License, Version 2.0 (the "License"). You may not use this project, -// or 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. -// -//////////////////////////////////////////////////////////////////////////////// -// -// -`default_nettype none -// }}} -module axisafety #( - // {{{ - parameter C_S_AXI_ID_WIDTH = 1, - parameter C_S_AXI_DATA_WIDTH = 32, - parameter C_S_AXI_ADDR_WIDTH = 16, - // OPT_SELF_RESET: Set to true if the downstream slave should be - // reset upon detecting an error and separate from the upstream reset - // domain - parameter [0:0] OPT_SELF_RESET = 1'b0, - // OPT_EXCLUSIVE: Set to true if the downstream slave might possibly - // offer an exclusive access capability - parameter [0:0] OPT_EXCLUSIVE = 1'b0, - // - // I use the following abbreviations, IW, DW, and AW, to simplify - // the code below (and to help it fit within an 80 col terminal) - localparam IW = C_S_AXI_ID_WIDTH, - localparam DW = C_S_AXI_DATA_WIDTH, - localparam AW = C_S_AXI_ADDR_WIDTH, - // - // OPT_TIMEOUT references the number of clock cycles to wait - // between raising the *VALID signal and when the respective - // *VALID return signal must be high. You might wish to set this - // to a very high number, to allow your core to work its magic. - parameter OPT_TIMEOUT = 20 - // }}} - ) ( - // {{{ - output reg o_read_fault, - output reg o_write_fault, - // User ports ends - // Do not modify the ports beyond this line - - // Global Clock Signal - input wire S_AXI_ACLK, - // Global Reset Signal. This Signal is Active LOW - input wire S_AXI_ARESETN, - output reg M_AXI_ARESETN, - // - // The input side. This is where slave requests come into - // the core. - // {{{ - // - // Write address - input wire [IW-1 : 0] S_AXI_AWID, - input wire [AW-1 : 0] S_AXI_AWADDR, - input wire [7 : 0] S_AXI_AWLEN, - input wire [2 : 0] S_AXI_AWSIZE, - input wire [1 : 0] S_AXI_AWBURST, - input wire S_AXI_AWLOCK, - input wire [3 : 0] S_AXI_AWCACHE, - input wire [2 : 0] S_AXI_AWPROT, - input wire [3 : 0] S_AXI_AWQOS, - input wire S_AXI_AWVALID, - output reg S_AXI_AWREADY, - // Write data - input wire [DW-1 : 0] S_AXI_WDATA, - input wire [(DW/8)-1 : 0] S_AXI_WSTRB, - input wire S_AXI_WLAST, - input wire S_AXI_WVALID, - output reg S_AXI_WREADY, - // Write return - output reg [IW-1 : 0] S_AXI_BID, - output reg [1 : 0] S_AXI_BRESP, - output reg S_AXI_BVALID, - input wire S_AXI_BREADY, - // Read address - input wire [IW-1 : 0] S_AXI_ARID, - input wire [AW-1 : 0] S_AXI_ARADDR, - input wire [7 : 0] S_AXI_ARLEN, - input wire [2 : 0] S_AXI_ARSIZE, - input wire [1 : 0] S_AXI_ARBURST, - input wire S_AXI_ARLOCK, - input wire [3 : 0] S_AXI_ARCACHE, - input wire [2 : 0] S_AXI_ARPROT, - input wire [3 : 0] S_AXI_ARQOS, - input wire S_AXI_ARVALID, - output reg S_AXI_ARREADY, - // Read data - output reg [IW-1 : 0] S_AXI_RID, - output reg [DW-1 : 0] S_AXI_RDATA, - output reg [1 : 0] S_AXI_RRESP, - output reg S_AXI_RLAST, - output reg S_AXI_RVALID, - input wire S_AXI_RREADY, - // }}} - // - // The output side, where slave requests are forwarded to the - // actual slave - // {{{ - // Write address - // {{{ - output reg [IW-1 : 0] M_AXI_AWID, - output reg [AW-1 : 0] M_AXI_AWADDR, - output reg [7 : 0] M_AXI_AWLEN, - output reg [2 : 0] M_AXI_AWSIZE, - output reg [1 : 0] M_AXI_AWBURST, - output reg M_AXI_AWLOCK, - output reg [3 : 0] M_AXI_AWCACHE, - output reg [2 : 0] M_AXI_AWPROT, - output reg [3 : 0] M_AXI_AWQOS, - output reg M_AXI_AWVALID, - input wire M_AXI_AWREADY, - // Write data - output reg [DW-1 : 0] M_AXI_WDATA, - output reg [(DW/8)-1 : 0] M_AXI_WSTRB, - output reg M_AXI_WLAST, - output reg M_AXI_WVALID, - input wire M_AXI_WREADY, - // Write return - input wire [IW-1 : 0] M_AXI_BID, - input wire [1 : 0] M_AXI_BRESP, - input wire M_AXI_BVALID, - output wire M_AXI_BREADY, - // }}} - // Read address - // {{{ - output reg [IW-1 : 0] M_AXI_ARID, - output reg [AW-1 : 0] M_AXI_ARADDR, - output reg [7 : 0] M_AXI_ARLEN, - output reg [2 : 0] M_AXI_ARSIZE, - output reg [1 : 0] M_AXI_ARBURST, - output reg M_AXI_ARLOCK, - output reg [3 : 0] M_AXI_ARCACHE, - output reg [2 : 0] M_AXI_ARPROT, - output reg [3 : 0] M_AXI_ARQOS, - output reg M_AXI_ARVALID, - input wire M_AXI_ARREADY, - // Read data - input wire [IW-1 : 0] M_AXI_RID, - input wire [DW-1 : 0] M_AXI_RDATA, - input wire [1 : 0] M_AXI_RRESP, - input wire M_AXI_RLAST, - input wire M_AXI_RVALID, - output wire M_AXI_RREADY - // }}} - // }}} - // }}} - ); - - localparam LGTIMEOUT = $clog2(OPT_TIMEOUT+1); - localparam [1:0] OKAY = 2'b00, EXOKAY = 2'b01; - localparam SLAVE_ERROR = 2'b10; - // - // - // Register declarations - // {{{ - reg faulty_write_return, faulty_read_return; - reg clear_fault; - // - // Timer/timeout variables - reg [LGTIMEOUT-1:0] write_timer, read_timer; - reg write_timeout, read_timeout; - - // - // Double buffer the write address channel - reg r_awvalid, m_awvalid; - reg [IW-1:0] r_awid, m_awid; - reg [AW-1:0] r_awaddr, m_awaddr; - reg [7:0] r_awlen, m_awlen; - reg [2:0] r_awsize, m_awsize; - reg [1:0] r_awburst, m_awburst; - reg r_awlock, m_awlock; - reg [3:0] r_awcache, m_awcache; - reg [2:0] r_awprot, m_awprot; - reg [3:0] r_awqos, m_awqos; - - // - // Double buffer for the write channel - reg r_wvalid,m_wvalid; - reg [DW-1:0] r_wdata, m_wdata; - reg [DW/8-1:0] r_wstrb, m_wstrb; - reg r_wlast, m_wlast; - - // - // Double buffer the write response channel - reg m_bvalid; // r_bvalid == 0 - reg [IW-1:0] m_bid; - reg [1:0] m_bresp; - - // - // Double buffer the read address channel - reg r_arvalid, m_arvalid; - reg [IW-1:0] r_arid, m_arid; - reg [AW-1:0] r_araddr, m_araddr; - reg [7:0] r_arlen, m_arlen; - reg [2:0] r_arsize, m_arsize; - reg [1:0] r_arburst, m_arburst; - reg r_arlock, m_arlock; - reg [3:0] r_arcache, m_arcache; - reg [2:0] r_arprot, m_arprot; - reg [3:0] r_arqos, m_arqos; - - // - // Double buffer the read data response channel - reg r_rvalid,m_rvalid; - reg [IW-1:0] m_rid; - reg [1:0] r_rresp, m_rresp; - reg m_rlast; - reg [DW-1:0] r_rdata, m_rdata; - - // - // Write FIFO data - wire [IW-1:0] wfifo_id; - wire wfifo_lock; - - // - // Read FIFO data - reg [IW-1:0] rfifo_id; - reg rfifo_lock; - reg [8:0] rfifo_counter; - reg rfifo_empty, rfifo_last, rfifo_penultimate; - - // - // - reg [0:0] s_wbursts; - reg [8:0] m_wpending; - reg m_wempty, m_wlastctr; - wire waddr_valid, raddr_valid; - - wire lock_enabled, lock_failed; - wire [(1<0), - // m_wempty is assigned to (m_wpending). Similarly, m_wlastctr is - // assigned to (m_wpending == 1). - // - initial m_wpending = 0; - initial m_wempty = 1; - initial m_wlastctr = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || o_write_fault) - begin - // {{{ - m_wpending <= 0; - m_wempty <= 1; - m_wlastctr <= 0; - // }}} - end else if (M_AXI_AWVALID && M_AXI_AWREADY) - begin - // {{{ - if (M_AXI_WVALID && M_AXI_WREADY) - begin - // {{{ - // Accepting AW* and W* packets on the same - // clock - if (m_wpending == 0) - begin - // The AW* and W* packets go together - m_wpending <= {1'b0, M_AXI_AWLEN}; - m_wempty <= (M_AXI_AWLEN == 0); - m_wlastctr <= (M_AXI_AWLEN == 1); - end else begin - // The W* packet goes with the last - // AW* command, the AW* packet with a - // new one - m_wpending <= M_AXI_AWLEN+1; - m_wempty <= 0; - m_wlastctr <= (M_AXI_AWLEN == 0); - end - // }}} - end else begin - // {{{ - m_wpending <= M_AXI_AWLEN+1; - m_wempty <= 0; - m_wlastctr <= (M_AXI_AWLEN == 0); - // }}} - end - // }}} - end else if (M_AXI_WVALID && M_AXI_WREADY && (!m_wempty)) - begin - // {{{ - // The AW* channel is idle, and we just accepted a value - // on the W* channel - m_wpending <= m_wpending - 1; - m_wempty <= (m_wpending <= 1); - m_wlastctr <= (m_wpending == 2); - // }}} - end - // }}} - - // Write data processing - // {{{ - // S_AXI_WREADY - // {{{ - // The S_AXI_WREADY or write channel stall signal - // - // For this core, we idle at zero (stalled) until an AW* packet - // comes through - // - initial S_AXI_WREADY = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - S_AXI_WREADY <= 0; - else if (S_AXI_WVALID && S_AXI_WREADY) - begin - // {{{ - if (S_AXI_WLAST) - S_AXI_WREADY <= 0; - else if (o_write_fault) - S_AXI_WREADY <= 1; - else if (!M_AXI_WVALID || M_AXI_WREADY) - S_AXI_WREADY <= 1; - else - S_AXI_WREADY <= 0; - // }}} - end else if ((s_wbursts == 0)&&(waddr_valid) - &&(o_write_fault || M_AXI_WREADY)) - S_AXI_WREADY <= 1; - else if (S_AXI_AWVALID && S_AXI_AWREADY) - S_AXI_WREADY <= 1; - // }}} - - // r_w* - // {{{ - // Double buffer for the write channel - // - // As before, the r_* values contain the values in the double - // buffer itself - // - initial r_wvalid = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - r_wvalid <= 0; - else if (!r_wvalid) - begin - // {{{ - r_wvalid <= (S_AXI_WVALID && S_AXI_WREADY - && M_AXI_WVALID && !M_AXI_WREADY); - r_wdata <= S_AXI_WDATA; - r_wstrb <= S_AXI_WSTRB; - r_wlast <= S_AXI_WLAST; - // }}} - end else if (o_write_fault || M_AXI_WREADY || !M_AXI_ARESETN) - r_wvalid <= 0; - // }}} - - // m_w* - // {{{ - // Here's the result of our double buffer - // - // m_* references the value within the double buffer in the case that - // something is in the double buffer. Otherwise, it is the values - // directly from the inputs. In the case of a fault, neither is true. - // Write faults override. - // - always @(*) - if (o_write_fault) - begin - // {{{ - m_wvalid = !m_wempty; - m_wlast = m_wlastctr; - m_wstrb = 0; - // }}} - end else if (r_wvalid) - begin - // {{{ - m_wvalid = 1; - m_wstrb = r_wstrb; - m_wlast = r_wlast; - // }}} - end else begin - // {{{ - m_wvalid = S_AXI_WVALID && S_AXI_WREADY; - m_wstrb = S_AXI_WSTRB; - m_wlast = S_AXI_WLAST; - // }}} - end - // }}} - - // m_wdata - // {{{ - // The logic for the DATA output of the double buffer doesn't - // matter so much in the case of o_write_fault - always @(*) - if (r_wvalid) - m_wdata = r_wdata; - else - m_wdata = S_AXI_WDATA; - // }}} - - // M_AXI_W* - // {{{ - // Set the downstream write channel values - // - // As per AXI spec, these values *must* be registered. Note that our - // source here is the m_* double buffer/incoming write data switch. - initial M_AXI_WVALID = 0; - always @(posedge S_AXI_ACLK) - begin - if (!M_AXI_WVALID || M_AXI_WREADY) - begin - M_AXI_WVALID <= m_wvalid; - M_AXI_WDATA <= m_wdata; - M_AXI_WSTRB <= m_wstrb; - if (OPT_EXCLUSIVE && lock_failed) - M_AXI_WSTRB <= 0; - M_AXI_WLAST <= m_wlast; - end - - // Override the WVALID signal (only) on reset, voiding any - // output we might otherwise send. - if (!M_AXI_ARESETN) - M_AXI_WVALID <= 0; - end - // }}} - // }}} - - // Write fault detection - // {{{ - // write_timer - // {{{ - // The write timer - // - // The counter counts up to saturation. It is reset any time - // the write channel is either clear, or a value is accepted - // at the *MASTER* (not slave) side. Why the master side? Simply - // because it makes the proof below easier. (At one time I checked - // both, but then couldn't prove that the faults wouldn't get hit - // if the slave responded in time.) - initial write_timer = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !waddr_valid) - write_timer <= 0; - else if (!o_write_fault && M_AXI_BVALID) - write_timer <= 0; - else if (S_AXI_WREADY) - write_timer <= 0; - else if (!(&write_timer)) - write_timer <= write_timer + 1; - // }}} - - // write_timeout - // {{{ - // Write timeout detector - // - // If the write_timer reaches the OPT_TIMEOUT, then the write_timeout - // will get set true. This will force a fault, taking the write - // channel off line. - initial write_timeout = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || clear_fault) - write_timeout <= 0; - else if (M_AXI_BVALID) - write_timeout <= write_timeout; - else if (S_AXI_WVALID && S_AXI_WREADY) - write_timeout <= write_timeout; - else if (write_timer >= OPT_TIMEOUT) - write_timeout <= 1; - // }}} - - // faulty_write_return - // {{{ - // fault_write_return - // - // This combinational logic is used to catch an invalid return, and - // so take the slave off-line before the return can corrupt the master - // channel. Reasons for taking the write return off line are listed - // below. - always @(*) - begin - faulty_write_return = 0; - if (M_AXI_WVALID && M_AXI_WREADY - && M_AXI_AWVALID && !M_AXI_AWREADY) - // Accepting the write *data* prior to the write - // *address* is a fault - faulty_write_return = 1; - if (M_AXI_BVALID) - begin - if (M_AXI_AWVALID || M_AXI_WVALID) - // Returning a B* acknowledgement while the - // request remains outstanding is also a fault - faulty_write_return = 1; - if (!m_wempty) - // Same as above, but this time the write - // channel is neither complete, nor is *WVALID - // active. Values remain to be written, - // and so a return is a fault. - faulty_write_return = 1; - if (s_wbursts <= (S_AXI_BVALID ? 1:0)) - // Too many acknowledgments - // - // Returning more than one BVALID&BREADY for - // every AWVALID & AWREADY is a fault. - faulty_write_return = 1; - if (M_AXI_BID != wfifo_id) - // An attempt to return the wrong ID - faulty_write_return = 1; - if (M_AXI_BRESP == EXOKAY && (!OPT_EXCLUSIVE - || !lock_enabled)) - // An attempt to return a valid lock, without - // a prior request - faulty_write_return = 1; - end - end - // }}} - - // o_write_fault - // {{{ - // On a write fault, we're going to disconnect the write port from - // the slave, and return errors on each write connect. o_write_fault - // is our signal determining if the write channel is disconnected. - // - // Most of this work is determined within faulty_write_return above. - // Here we do just a bit more: - initial o_write_fault = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || clear_fault) - o_write_fault <= 0; - else if ((!M_AXI_ARESETN&&o_read_fault) || write_timeout) - o_write_fault <= 1; - else if (M_AXI_BVALID && M_AXI_BREADY) - o_write_fault <= (o_write_fault) || faulty_write_return; - else if (M_AXI_WVALID && M_AXI_WREADY - && M_AXI_AWVALID && !M_AXI_AWREADY) - // Accepting the write data prior to the write address - // is a fault - o_write_fault <= 1; - // }}} - // }}} - - // Write return generation - // {{{ - // m_b* - // {{{ - // Since we only ever allow a single write burst at a time, we don't - // need to double buffer the return channel. Hence, we'll set our - // return channel based upon the incoming values alone. Note that - // we're overriding the M_AXI_BID below, in order to make certain that - // the return goes to the right source. - // - always @(*) - if (o_write_fault) - begin - m_bvalid = (s_wbursts > (S_AXI_BVALID ? 1:0)); - m_bid = wfifo_id; - m_bresp = SLAVE_ERROR; - end else begin - m_bvalid = M_AXI_BVALID; - if (faulty_write_return) - m_bvalid = 0; - m_bid = wfifo_id; - m_bresp = M_AXI_BRESP; - end - // }}} - - // S_AXI_B* - // {{{ - // We'll *never* stall the slaves BREADY channel - // - // If the slave returns the response we are expecting, then S_AXI_BVALID - // will be low and it can go directly into the S_AXI_BVALID slot. If - // on the other hand the slave returns M_AXI_BVALID at the wrong time, - // then we'll quietly accept it and send the write interface into - // fault detected mode, setting o_write_fault. - // - // Sadly, this will create a warning in Vivado. If/when you see it, - // see this note and then just ignore it. - assign M_AXI_BREADY = 1; - - // - // Return a write acknowlegement at the end of every write - // burst--regardless of whether or not the slave does so - // - initial S_AXI_BVALID = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - S_AXI_BVALID <= 0; - else if (!S_AXI_BVALID || S_AXI_BREADY) - S_AXI_BVALID <= m_bvalid; - - // - // Set the values associated with the response - // - always @(posedge S_AXI_ACLK) - if (!S_AXI_BVALID || S_AXI_BREADY) - begin - S_AXI_BID <= m_bid; - S_AXI_BRESP <= m_bresp; - end - // }}} - - // }}} - - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Read channel processing - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - - // - // Read address channel - // {{{ - - // S_AXI_ARREADY - // {{{ - initial S_AXI_ARREADY = (OPT_SELF_RESET) ? 0:1; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - S_AXI_ARREADY <= !OPT_SELF_RESET; - else if (S_AXI_ARVALID && S_AXI_ARREADY) - S_AXI_ARREADY <= 0; - // else if (clear_fault) - // S_AXI_ARREADY <= 1; - else if (!S_AXI_ARREADY) - S_AXI_ARREADY <= (S_AXI_RVALID && S_AXI_RLAST && S_AXI_RREADY); - // }}} - - // raddr_valid - // {{{ - generate if (OPT_SELF_RESET) - begin : GEN_READ_RESET - assign raddr_valid = !rfifo_empty; - end else begin : SIMPLE_RADDR_VALID - assign raddr_valid = !S_AXI_ARREADY; - end endgenerate - // }}} - - // r_ar* - // {{{ - // Double buffer the values associated with any read address request - // - initial r_arvalid = 0; - always @(posedge S_AXI_ACLK) - begin - if (S_AXI_ARVALID && S_AXI_ARREADY) - begin - r_arvalid <= 0; // (M_AXI_ARVALID && !M_AXI_ARREADY); - r_arid <= S_AXI_ARID; - r_araddr <= S_AXI_ARADDR; - r_arlen <= S_AXI_ARLEN; - r_arsize <= S_AXI_ARSIZE; - r_arburst <= S_AXI_ARBURST; - r_arlock <= S_AXI_ARLOCK; - r_arcache <= S_AXI_ARCACHE; - r_arprot <= S_AXI_ARPROT; - r_arqos <= S_AXI_ARQOS; - end else if (M_AXI_ARREADY) - r_arvalid <= 0; - - if (!M_AXI_ARESETN) - r_arvalid <= 0; - if (!OPT_EXCLUSIVE || !S_AXI_ARESETN) - r_arlock <= 1'b0; - end - // }}} - - // m_ar* - // {{{ - always @(*) - if (r_arvalid) - begin - m_arvalid = r_arvalid; - m_arid = r_arid; - m_araddr = r_araddr; - m_arlen = r_arlen; - m_arsize = r_arsize; - m_arburst = r_arburst; - m_arlock = r_arlock; - m_arcache = r_arcache; - m_arprot = r_arprot; - m_arqos = r_arqos; - end else begin - m_arvalid = S_AXI_ARVALID && S_AXI_ARREADY; - m_arid = S_AXI_ARID; - m_araddr = S_AXI_ARADDR; - m_arlen = S_AXI_ARLEN; - m_arsize = S_AXI_ARSIZE; - m_arburst = S_AXI_ARBURST; - m_arlock = S_AXI_ARLOCK && OPT_EXCLUSIVE; - m_arcache = S_AXI_ARCACHE; - m_arprot = S_AXI_ARPROT; - m_arqos = S_AXI_ARQOS; - end - // }}} - - // M_AXI_AR* - // {{{ - // Set the downstream values according to the transaction we've just - // received. - // - initial M_AXI_ARVALID = 0; - always @(posedge S_AXI_ACLK) - begin - if (!M_AXI_ARVALID || M_AXI_ARREADY) - begin - - if (o_read_fault) - M_AXI_ARVALID <= 0; - else - M_AXI_ARVALID <= m_arvalid; - - M_AXI_ARID <= m_arid; - M_AXI_ARADDR <= m_araddr; - M_AXI_ARLEN <= m_arlen; - M_AXI_ARSIZE <= m_arsize; - M_AXI_ARBURST <= m_arburst; - M_AXI_ARLOCK <= m_arlock && OPT_EXCLUSIVE; - M_AXI_ARCACHE <= m_arcache; - M_AXI_ARPROT <= m_arprot; - M_AXI_ARQOS <= m_arqos; - end - - if (!M_AXI_ARESETN) - M_AXI_ARVALID <= 0; - end - // }}} - - // }}} - - // - // Read fault detection - // {{{ - - // read_timer - // {{{ - // First step: a timer. The timer starts as soon as the S_AXI_ARVALID - // is accepted. Once that happens, rfifo_empty will no longer be true. - // The count is reset any time the slave produces a value for us to - // read. Once the count saturates, it stops counting. - initial read_timer = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || clear_fault) - read_timer <= 0; - else if (rfifo_empty||(S_AXI_RVALID)) - read_timer <= 0; - else if (M_AXI_RVALID) - read_timer <= 0; - else if (!(&read_timer)) - read_timer <= read_timer + 1; - // }}} - - // read_timeout - // {{{ - // Once the counter > OPT_TIMEOUT, we have a timeout condition. - // We'll detect this one clock earlier below. If we ever enter - // a read time out condition, we'll set the read fault. The read - // timeout condition can only be cleared by a reset. - initial read_timeout = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || clear_fault) - read_timeout <= 0; - else if (rfifo_empty||S_AXI_RVALID) - read_timeout <= read_timeout; - else if (M_AXI_RVALID) - read_timeout <= read_timeout; - else if (read_timer == OPT_TIMEOUT) - read_timeout <= 1; - // }}} - - // - // faulty_read_return - // {{{ - // To avoid returning a fault from the slave, it is important to - // determine within a single clock period whether or not the slaves - // return value is at fault or not. That's the purpose of the code - // below. - always @(*) - begin - faulty_read_return = 0; - if (M_AXI_RVALID) - begin - if (M_AXI_ARVALID) - // It is a fault to return data before the - // request has been accepted - faulty_read_return = 1; - if (M_AXI_RID != rfifo_id) - // It is a fault to return data from a - // different ID - faulty_read_return = 1; - if (rfifo_last && (S_AXI_RVALID || !M_AXI_RLAST)) - faulty_read_return = 1; - if (rfifo_penultimate && S_AXI_RVALID && (r_rvalid || !M_AXI_RLAST)) - faulty_read_return = 1; - if (M_AXI_RRESP == EXOKAY && (!OPT_EXCLUSIVE || !rfifo_lock)) - faulty_read_return = 1; - if (OPT_EXCLUSIVE && exread && M_AXI_RRESP == OKAY) - // Can't switch from EXOKAY to OKAY - faulty_read_return = 1; - if ((!OPT_EXCLUSIVE || (!rfifo_first && !exread)) - && M_AXI_RRESP == EXOKAY) - // Can't switch from OKAY to EXOKAY - faulty_read_return = 1; - end - end - // }}} - - // o_read_fault - // {{{ - initial o_read_fault = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || clear_fault) - o_read_fault <= 0; - else if ((!M_AXI_ARESETN && o_write_fault) || read_timeout) - o_read_fault <= 1; - else if (M_AXI_RVALID) - begin - if (faulty_read_return) - o_read_fault <= 1; - if (!raddr_valid) - // It is a fault if we haven't issued an AR* request - // yet, and a value is returned - o_read_fault <= 1; - end - // }}} - - // }}} - - // - // Read return/acknowledgment processing - // {{{ - - - // exread - // {{{ - always @(posedge S_AXI_ACLK) - if (!M_AXI_ARESETN || !OPT_EXCLUSIVE) - exread <= 0; - else if (M_AXI_RVALID && M_AXI_RREADY) - begin - if (!M_AXI_RRESP[1]) - exread <= (M_AXI_RRESP == EXOKAY); - end else if (S_AXI_RVALID && S_AXI_RREADY) - begin - if (S_AXI_RLAST) - exread <= 1'b0; - end - // }}} - - // r_rvalid - // {{{ - // Step one, set/create the read return double buffer. If r_rvalid - // is true, there's a valid value in the double buffer location. - // - initial r_rvalid = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || o_read_fault) - r_rvalid <= 0; - else if (!r_rvalid) - begin - // {{{ - // Refuse to set the double-buffer valid on any fault. - // That will also keep (below) M_AXI_RREADY high--so that - // following the fault the slave might still (pretend) to - // respond properly - if (faulty_read_return) - r_rvalid <= 0; - else if (o_read_fault) - r_rvalid <= 0; - // If there's nothing in the double buffer, then we might - // place something in there. The double buffer only gets - // filled under two conditions: 1) something is pending to be - // returned, and 2) there's another return that we can't - // stall and so need to accept here. - r_rvalid <= M_AXI_RVALID && M_AXI_RREADY - && (S_AXI_RVALID && !S_AXI_RREADY); - // }}} - end else if (S_AXI_RREADY) - // Once the up-stream read-channel clears, we can always - // clear the double buffer - r_rvalid <= 0; - // }}} - - // r_rresp, r_rdata - // {{{ - // Here's the actual values kept whenever r_rvalid is true. This is - // the double buffer. Notice that r_rid and r_last are generated - // locally, so not recorded here. - // - always @(posedge S_AXI_ACLK) - if (!r_rvalid) - begin - r_rresp <= M_AXI_RRESP; - r_rdata <= M_AXI_RDATA; - end - // }}} - - // M_AXI_RREADY - // {{{ - // Stall the downstream channel any time there's something in the - // double buffer. In spite of the ! here, this is a registered value. - assign M_AXI_RREADY = !r_rvalid; - // }}} - - // rfifo_id, rfifo_lock - // {{{ - // Copy the ID for later comparisons on the return - always @(*) - rfifo_id = r_arid; - always @(*) - rfifo_lock = r_arlock; - // }}} - - // rfifo_[counter|empty|last|penultimate - // {{{ - // Count the number of outstanding read elements. This is the number - // of read returns we still expect--from the upstream perspective. The - // downstream perspective will be off by both what's waiting for - // S_AXI_RREADY and what's in the double buffer - // - initial rfifo_counter = 0; - initial rfifo_empty = 1; - initial rfifo_last = 0; - initial rfifo_penultimate= 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - begin - rfifo_counter <= 0; - rfifo_empty <= 1; - rfifo_last <= 0; - rfifo_penultimate<= 0; - end else if (S_AXI_ARVALID && S_AXI_ARREADY) - begin - rfifo_counter <= S_AXI_ARLEN+1; - rfifo_empty <= 0; - rfifo_last <= (S_AXI_ARLEN == 0); - rfifo_penultimate <= (S_AXI_ARLEN == 1); - end else if (!rfifo_empty) - begin - if (S_AXI_RVALID && S_AXI_RREADY) - begin - rfifo_counter <= rfifo_counter - 1; - rfifo_empty <= (rfifo_counter <= 1); - rfifo_last <= (rfifo_counter == 2); - rfifo_penultimate <= (rfifo_counter == 3); - end - end - // }}} - - // lock_active - // {{{ - generate if (OPT_EXCLUSIVE) - begin : CALC_LOCK_ACTIVE - // {{{ - genvar gk; - - for(gk=0; gk<(1< 0) - assert((!M_AXI_WVALID || !M_AXI_WLAST) - &&(!r_wvalid || !r_wlast)); - if (!o_write_fault && M_AXI_WVALID && M_AXI_WLAST) - assert(!r_wvalid || !r_wlast); - end else begin - assert(s_wbursts == 0); - assert(!S_AXI_WREADY); - if (OPT_SELF_RESET) - begin - assert(1 || S_AXI_AWREADY || !M_AXI_ARESETN || !S_AXI_ARESETN); - end else - assert(S_AXI_AWREADY); - end - - // - // ... - // - - // - // AWREADY will always be low mid-burst - always @(posedge S_AXI_ACLK) - if (!f_past_valid || $past(!S_AXI_ARESETN)) - begin - assert(S_AXI_AWREADY == !OPT_SELF_RESET); - end else if (f_axi_wr_pending > 0) - begin - assert(!S_AXI_AWREADY); - end else if (s_wbursts) - begin - assert(!S_AXI_AWREADY); - end else if (!OPT_SELF_RESET) - begin - assert(S_AXI_AWREADY); - end else if (!o_write_fault && !o_read_fault) - assert(S_AXI_AWREADY || OPT_SELF_RESET); - - always @(*) - if (f_axi_wr_pending > 0) - begin - assert(s_wbursts == 0); - end else if (f_axi_awr_nbursts > 0) - begin - assert((s_wbursts ? 1:0) == f_axi_awr_nbursts); - end else - assert(s_wbursts == 0); - - always @(*) - if (!o_write_fault && S_AXI_AWREADY) - assert(!M_AXI_AWVALID); - - always @(*) - if (M_AXI_ARESETN && (f_axi_awr_nbursts == 0)) - begin - assert(o_write_fault || !M_AXI_AWVALID); - assert(!S_AXI_BVALID); - assert(s_wbursts == 0); - end else if (M_AXI_ARESETN && s_wbursts == 0) - assert(f_axi_wr_pending > 0); - - always @(*) - if (S_AXI_WREADY) - begin - assert(waddr_valid); - end else if (f_axi_wr_pending > 0) - begin - if (!o_write_fault) - assert(M_AXI_WVALID && r_wvalid); - end - - always @(*) - if (!OPT_SELF_RESET) - begin - assert(waddr_valid == !S_AXI_AWREADY); - end else begin - // ... - assert(waddr_valid == (f_axi_awr_nbursts > 0)); - end - - always @(*) - if (S_AXI_ARESETN && !o_write_fault && f_axi_wr_pending > 0 && !S_AXI_WREADY) - assert(M_AXI_WVALID); - - always @(*) - if (S_AXI_ARESETN && !o_write_fault && m_wempty) - begin - assert(M_AXI_AWVALID || !M_AXI_WVALID); - assert(M_AXI_AWVALID || f_axi_wr_pending == 0); - end - - always @(*) - if (S_AXI_ARESETN && M_AXI_AWVALID) - begin - if (!o_write_fault && !M_AXI_AWVALID) - begin - assert(f_axi_wr_pending + (M_AXI_WVALID ? 1:0) + (r_wvalid ? 1:0) == m_wpending); - end else if (!o_write_fault) - begin - assert(f_axi_wr_pending == M_AXI_AWLEN + 1 - (M_AXI_WVALID ? 1:0) - (r_wvalid ? 1:0)); - assert(m_wpending == 0); - end - end - - always @(*) - assert(m_wpending <= 9'h100); - - always @(*) - if (M_AXI_ARESETN && (!o_write_fault)&&(f_axi_awr_nbursts == 0)) - assert(!M_AXI_AWVALID); - - always @(*) - if (S_AXI_ARESETN && !o_write_fault) - begin - if (f_axi_awr_nbursts == 0) - begin - assert(!M_AXI_AWVALID); - assert(!M_AXI_WVALID); - end - - if (!M_AXI_AWVALID) - assert(f_axi_wr_pending - +(M_AXI_WVALID ? 1:0) - + (r_wvalid ? 1:0) - == m_wpending); - if (f_axi_awr_nbursts == (S_AXI_BVALID ? 1:0)) - begin - assert(!M_AXI_AWVALID); - assert(!M_AXI_WVALID); - end - - if (S_AXI_BVALID) - assert(f_axi_awr_nbursts == 1); - - if (M_AXI_AWVALID) - assert(m_wpending == 0); - - if (S_AXI_AWREADY) - assert(!M_AXI_AWVALID); - end - - always @(*) - assert(!r_awvalid); - - always @(*) - assert(m_wempty == (m_wpending == 0)); - always @(*) - assert(m_wlastctr == (m_wpending == 1)); - - // - // Verify the contents of the skid buffers - // - - // - // ... - // - - always @(*) - if (write_timer > OPT_TIMEOUT) - assert(o_write_fault || write_timeout); - - always @(*) - if (!OPT_SELF_RESET) - begin - assert(waddr_valid == !S_AXI_AWREADY); - end else if (waddr_valid) - assert(!S_AXI_AWREADY); - - always @(*) - if (!o_write_fault && M_AXI_ARESETN) - assert(waddr_valid == !S_AXI_AWREADY); - - always @(*) - if (f_axi_wr_pending == 0) - assert(!S_AXI_WREADY); - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Read induction properties - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - - always @(*) - assert(f_axi_rd_nbursts <= 1); - always @(*) - assert(raddr_valid == (f_axi_rd_nbursts>0)); - always @(*) - if (f_axi_rdid_nbursts > 0) - begin - assert(rfifo_id == f_axi_rd_checkid); - end else if (f_axi_rd_nbursts > 0) - assert(rfifo_id != f_axi_rd_checkid); - - always @(*) - if (f_axi_rd_nbursts > 0) - assert(raddr_valid); - - always @(*) - if (raddr_valid) - assert(!S_AXI_ARREADY); - - always @(*) - if (!OPT_SELF_RESET) - begin - assert(raddr_valid == !S_AXI_ARREADY); - end else begin - // ... - assert(raddr_valid == (f_axi_rd_nbursts > 0)); - end - - // - // ... - // - - always @(*) - if (f_axi_rd_outstanding == 0) - assert(!raddr_valid || OPT_SELF_RESET); - - always @(*) - if (!o_read_fault && S_AXI_ARREADY) - assert(!M_AXI_ARVALID); - - // Our "FIFO" counter - always @(*) - assert(rfifo_counter == f_axi_rd_outstanding); - - always @(*) - begin - assert(rfifo_empty == (rfifo_counter == 0)); - assert(rfifo_last == (rfifo_counter == 1)); - assert(rfifo_penultimate == (rfifo_counter == 2)); - end - - // - // ... - // - - always @(*) - if (r_arvalid) - assert(skid_arvalid); - - always @(*) - if (read_timer > OPT_TIMEOUT) - assert(read_timeout); - - - always @(posedge S_AXI_ACLK) - if (OPT_SELF_RESET && (!f_past_valid || !$past(M_AXI_ARESETN))) - begin - assume(!M_AXI_BVALID); - assume(!M_AXI_RVALID); - end - - always @(*) - if (!o_read_fault && M_AXI_ARESETN) - assert(raddr_valid == !S_AXI_ARREADY); - - always @(*) - if (f_axi_rd_nbursts > 0) - assert(raddr_valid); - - always @(*) - if (S_AXI_ARESETN && OPT_SELF_RESET) - begin - if (!M_AXI_ARESETN) - assert(o_read_fault || o_write_fault /* ... */ ); - end - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Exclusive access property checking - // {{{ - // - //////////////////////////////////////////////////////////////////////// - // - // ... - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Cover properties - // - //////////////////////////////////////////////////////////////////////// - // - // }}} - - //////////////////////////////////////////////////////////////////////// - // - // Good interface check - // - //////////////////////////////////////////////////////////////////////// - // - // - generate if (F_OPT_FAULTLESS) - begin : ASSUME_FAULTLESS - // {{{ - // - // ... - // - - faxi_master #( - // {{{ - .C_AXI_ID_WIDTH(C_S_AXI_ID_WIDTH), - .C_AXI_DATA_WIDTH(C_S_AXI_DATA_WIDTH), - .C_AXI_ADDR_WIDTH(C_S_AXI_ADDR_WIDTH) - // ... - // }}} - ) f_master( - // {{{ - .i_clk(S_AXI_ACLK), - .i_axi_reset_n(M_AXI_ARESETN), - // - // Address write channel - // {{{ - .i_axi_awid(M_AXI_AWID), - .i_axi_awaddr(M_AXI_AWADDR), - .i_axi_awlen(M_AXI_AWLEN), - .i_axi_awsize(M_AXI_AWSIZE), - .i_axi_awburst(M_AXI_AWBURST), - .i_axi_awlock(M_AXI_AWLOCK), - .i_axi_awcache(M_AXI_AWCACHE), - .i_axi_awprot(M_AXI_AWPROT), - .i_axi_awqos(M_AXI_AWQOS), - .i_axi_awvalid(M_AXI_AWVALID), - .i_axi_awready(M_AXI_AWREADY), - // }}} - // Write Data Channel - // {{{ - .i_axi_wvalid(M_AXI_WVALID), - .i_axi_wready(M_AXI_WREADY), - .i_axi_wdata(M_AXI_WDATA), - .i_axi_wstrb(M_AXI_WSTRB), - .i_axi_wlast(M_AXI_WLAST), - // }}} - // Write response channel - // {{{ - .i_axi_bvalid(M_AXI_BVALID), - .i_axi_bready(M_AXI_BREADY), - .i_axi_bid(M_AXI_BID), - .i_axi_bresp(M_AXI_BRESP), - // }}} - // Read address channel - // {{{ - .i_axi_arid(M_AXI_ARID), - .i_axi_araddr(M_AXI_ARADDR), - .i_axi_arlen(M_AXI_ARLEN), - .i_axi_arsize(M_AXI_ARSIZE), - .i_axi_arburst(M_AXI_ARBURST), - .i_axi_arlock(M_AXI_ARLOCK), - .i_axi_arcache(M_AXI_ARCACHE), - .i_axi_arprot(M_AXI_ARPROT), - .i_axi_arqos(M_AXI_ARQOS), - .i_axi_arvalid(M_AXI_ARVALID), - .i_axi_arready(M_AXI_ARREADY), - // }}} - // Read data return channel - // {{{ - .i_axi_rvalid(M_AXI_RVALID), - .i_axi_rready(M_AXI_RREADY), - .i_axi_rid(M_AXI_RID), - .i_axi_rdata(M_AXI_RDATA), - .i_axi_rresp(M_AXI_RRESP), - .i_axi_rlast(M_AXI_RLAST), - // }}} - // Formal outputs - // {{{ - .f_axi_awr_nbursts(fm_axi_awr_nbursts), - .f_axi_wr_pending(fm_axi_wr_pending), - .f_axi_rd_nbursts(fm_axi_rd_nbursts), - .f_axi_rd_outstanding(fm_axi_rd_outstanding) - // - // ... - // }}} - // }}} - ); - - //////////////////////////////////////////////////////////////// - // - // Contract: If the downstream has no faults, then we - // shouldn't detect any here. - // {{{ - //////////////////////////////////////////////////////////////// - // - // - - always @(*) - if (OPT_SELF_RESET) - begin - assert(!o_write_fault || !M_AXI_ARESETN); - end else - assert(!o_write_fault); - - always @(*) - if (OPT_SELF_RESET) - begin - assert(!o_read_fault || !M_AXI_ARESETN); - end else - assert(!o_read_fault); - - always @(*) - if (OPT_SELF_RESET) - begin - assert(!read_timeout || !M_AXI_ARESETN); - end else - assert(!read_timeout); - - always @(*) - if (OPT_SELF_RESET) - begin - assert(!write_timeout || !M_AXI_ARESETN); - end else - assert(!write_timeout); - - always @(*) - if (S_AXI_AWREADY) - assert(!M_AXI_AWVALID); - - // - // ... - // - - always @(*) - if (M_AXI_ARESETN && f_axi_rd_nbursts > 0) - assert(f_axi_rd_nbursts == fm_axi_rd_nbursts - + (M_AXI_ARVALID ? 1 : 0) - + (r_rvalid&&m_rlast ? 1 : 0) - + (S_AXI_RVALID&&S_AXI_RLAST ? 1 : 0)); - - always @(*) - if (M_AXI_ARESETN && f_axi_rd_outstanding > 0) - assert(f_axi_rd_outstanding == fm_axi_rd_outstanding - + (M_AXI_ARVALID ? M_AXI_ARLEN+1 : 0) - + (r_rvalid ? 1 : 0) - + (S_AXI_RVALID ? 1 : 0)); - - // - // ... - // - always @(*) - if (M_AXI_RVALID) - assert(!M_AXI_ARVALID); - - always @(*) - if (S_AXI_ARESETN) - assert(m_wpending == fm_axi_wr_pending); - - always @(*) - if (S_AXI_ARESETN && fm_axi_awr_nbursts > 0) - begin - assert(fm_axi_awr_nbursts== f_axi_awr_nbursts); - assert(fm_axi_awr_nbursts == 1); - // - // ... - // - end - // }}} - //////////////////////////////////////////////////////////////// - // - // Exclusive address checking - // {{{ - //////////////////////////////////////////////////////////////// - // - // - - // - // - // ... - // - - //////////////////////////////////////////////////////////////// - // - // Cover checks - // {{{ - //////////////////////////////////////////////////////////////// - // - // - - // }}} - //////////////////////////////////////////////////////////////// - // - // "Careless" assumptions - // {{{ - //////////////////////////////////////////////////////////////// - // - // - end endgenerate - - // - // ... - // - - //////////////////////////////////////////////////////////////////////// - // - // Never path check - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - (* anyconst *) reg [C_S_AXI_ADDR_WIDTH-1:0] fc_never_write_addr, - fc_never_read_addr; - (* anyconst *) reg [C_S_AXI_DATA_WIDTH + C_S_AXI_DATA_WIDTH/8-1:0] - fc_never_write_data; - (* anyconst *) reg [C_S_AXI_DATA_WIDTH-1:0] fc_never_read_data; - - // Write address - // {{{ - always @(posedge S_AXI_ACLK) - if (S_AXI_ARESETN && S_AXI_AWVALID) - assume(S_AXI_AWADDR != fc_never_write_addr); - - always @(posedge S_AXI_ACLK) - if (S_AXI_ARESETN && !o_write_fault && M_AXI_ARESETN && M_AXI_AWVALID) - assert(M_AXI_AWADDR != fc_never_write_addr); - // }}} - - // Write data - // {{{ - always @(posedge S_AXI_ACLK) - if (S_AXI_ARESETN && S_AXI_WVALID) - assume({ S_AXI_WDATA, S_AXI_WSTRB } != fc_never_write_data); - - always @(posedge S_AXI_ACLK) - if (S_AXI_ARESETN && !o_write_fault && M_AXI_ARESETN && M_AXI_WVALID) - begin - if (lock_failed) - assert(M_AXI_WSTRB == 0); - else - assert({ M_AXI_WDATA, M_AXI_WSTRB } != fc_never_write_data); - end - // }}} - - // Read address - // {{{ - always @(posedge S_AXI_ACLK) - if (S_AXI_ARESETN && S_AXI_ARVALID) - assume(S_AXI_ARADDR != fc_never_read_addr); - - always @(posedge S_AXI_ACLK) - if (S_AXI_ARESETN && r_arvalid) - assume(r_araddr != fc_never_read_addr); - - always @(posedge S_AXI_ACLK) - if (S_AXI_ARESETN && !o_read_fault && M_AXI_ARESETN && M_AXI_ARVALID) - assert(M_AXI_ARADDR != fc_never_read_addr); - // }}} - - // Read data - // {{{ - always @(posedge S_AXI_ACLK) - if (S_AXI_ARESETN && M_AXI_ARESETN && M_AXI_RVALID) - assume(M_AXI_RDATA != fc_never_read_data); - - always @(posedge S_AXI_ACLK) - if (S_AXI_ARESETN && S_AXI_RVALID && S_AXI_RRESP != SLAVE_ERROR) - assert(S_AXI_RDATA != fc_never_read_data); - // }}} - - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Cover properties - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // We'll use these to determine the best performance this core - // can achieve - // - reg [4:0] f_dbl_rd_count, f_dbl_wr_count; - reg [4:0] f_rd_count, f_wr_count; - - // f_wr_count - // {{{ - initial f_wr_count = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || o_write_fault) - f_wr_count <= 0; - else if (S_AXI_BVALID && S_AXI_BREADY) - begin - if (!(&f_wr_count)) - f_wr_count <= f_wr_count + 1; - end - // }}} - - // f_dbl_wr_count - // {{{ - initial f_dbl_wr_count = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || o_write_fault||(S_AXI_AWVALID && S_AXI_AWLEN < 3)) - f_dbl_wr_count <= 0; - else if (S_AXI_BVALID && S_AXI_BREADY) - begin - if (!(&f_dbl_wr_count)) - f_dbl_wr_count <= f_dbl_wr_count + 1; - end - // }}} - - // f_rd_count - // {{{ - initial f_rd_count = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || o_read_fault) - f_rd_count <= 0; - else if (S_AXI_RVALID && S_AXI_RREADY && S_AXI_RLAST) - begin - if (!(&f_rd_count)) - f_rd_count <= f_rd_count + 1; - end - // }}} - - // f_dbl_rd_count - // {{{ - initial f_dbl_rd_count = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || o_read_fault||(S_AXI_ARVALID && S_AXI_ARLEN < 3)) - f_dbl_rd_count <= 0; - else if (S_AXI_RVALID && S_AXI_RREADY && S_AXI_RLAST) - begin - if (!(&f_dbl_rd_count)) - f_dbl_rd_count <= f_dbl_rd_count + 1; - end - // }}} - - // Can we complete a single write burst without fault? - // {{{ - always @(*) - if (S_AXI_ARESETN) - cover((f_wr_count > 1) && (!o_write_fault)); - - always @(*) - if (S_AXI_ARESETN) - cover((f_dbl_wr_count > 1) && (!o_write_fault)); - // }}} - - // Can we complete four write bursts without fault? (and return to idle) - // {{{ - always @(*) - if (S_AXI_ARESETN) - cover((f_wr_count > 3) && (!o_write_fault) - &&(!S_AXI_AWVALID && !S_AXI_WVALID - && !S_AXI_BVALID) - && (f_axi_awr_nbursts == 0) - && (f_axi_wr_pending == 0)); - - always @(*) - if (S_AXI_ARESETN) - cover((f_dbl_wr_count > 3) && (!o_write_fault) - &&(!S_AXI_AWVALID && !S_AXI_WVALID - && !S_AXI_BVALID) - && (f_axi_awr_nbursts == 0) - && (f_axi_wr_pending == 0)); - // }}} - - // Can we complete a single read burst without fault? - // {{{ - always @(*) - if (S_AXI_ARESETN) - cover((f_rd_count > 1) && (!o_read_fault)); - - always @(*) - if (S_AXI_ARESETN) - cover((f_dbl_rd_count > 1) && (!o_read_fault)); - // }}} - - // Can we complete four read bursts without fault? - // {{{ - always @(*) - if (S_AXI_ARESETN) - cover((f_rd_count > 3) && (f_axi_rd_nbursts == 0) - && !S_AXI_ARVALID && !S_AXI_RVALID); - - always @(*) - if (S_AXI_ARESETN) - cover((f_dbl_rd_count > 3) && (f_axi_rd_nbursts == 0) - && !S_AXI_ARVALID && !S_AXI_RVALID); - // }}} -`endif -// }}} -endmodule -`ifndef YOSYS -`default_nettype wire -`endif diff --git a/rtl/wb2axip/axisbroadcast.v b/rtl/wb2axip/axisbroadcast.v index 719108f..9132463 100644 --- a/rtl/wb2axip/axisbroadcast.v +++ b/rtl/wb2axip/axisbroadcast.v @@ -35,7 +35,7 @@ // //////////////////////////////////////////////////////////////////////////////// // -`default_nettype none +//`default_nettype none // }}} module axisbroadcast #( parameter C_AXIS_DATA_WIDTH = 16, diff --git a/rtl/wb2axip/axisgdma.v b/rtl/wb2axip/axisgdma.v index dac2cbc..09c38b2 100644 --- a/rtl/wb2axip/axisgdma.v +++ b/rtl/wb2axip/axisgdma.v @@ -67,7 +67,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // `define AXI3 // }}} module axisgdma #( @@ -76,8 +76,8 @@ module axisgdma #( parameter C_AXI_ADDR_WIDTH = 32, parameter C_AXI_DATA_WIDTH = 64, // - localparam C_AXIL_ADDR_WIDTH = 4, - localparam C_AXIL_DATA_WIDTH = 32, + /*local*/parameter C_AXIL_ADDR_WIDTH = 4, + /*local*/parameter C_AXIL_DATA_WIDTH = 32, // // OPT_UNALIGNED turns on support for unaligned addresses, // whether source, destination, or length parameters. @@ -199,7 +199,7 @@ module axisgdma #( // // input wire M_AXI_BVALID, - output reg M_AXI_BREADY, + output wire M_AXI_BREADY, input wire [C_AXI_ID_WIDTH-1:0] M_AXI_BID, input wire [1:0] M_AXI_BRESP, // @@ -279,7 +279,8 @@ module axisgdma #( // {{{ reg axil_write_ready, axil_read_ready; reg [2*C_AXIL_DATA_WIDTH-1:0] wide_tbl, new_widetbl; - reg [C_AXI_ADDR_WIDTH-1:0] tbl_addr, r_tbl_addr; + wire [C_AXI_ADDR_WIDTH-1:0] tbl_addr; + reg [C_AXI_ADDR_WIDTH-1:0] r_tbl_addr; reg r_int_enable, r_int, r_err, r_abort; wire w_int, fsm_err; @@ -319,12 +320,12 @@ module axisgdma #( // DMA control registers/AXI-lite interface // {{{ wire dmac_awready_ignored; - reg [4:0] dmac_waddr; + wire [4:0] dmac_waddr; // - reg dmac_wvalid; + wire dmac_wvalid; wire dmac_wready; - reg [31:0] dmac_wdata; - reg [3:0] dmac_wstrb; + wire [31:0] dmac_wdata; + wire [3:0] dmac_wstrb; // wire dmac_bvalid; wire [1:0] dmac_bresp; diff --git a/rtl/wb2axip/axisgfsm.v b/rtl/wb2axip/axisgfsm.v index ea01515..2af84db 100644 --- a/rtl/wb2axip/axisgfsm.v +++ b/rtl/wb2axip/axisgfsm.v @@ -71,7 +71,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // `define AXI3 // }}} module axisgfsm #( @@ -80,8 +80,8 @@ module axisgfsm #( // Verilator lint_off UNUSED parameter C_AXI_DATA_WIDTH = 32, // Verilator lint_on UNUSED - localparam DMAC_ADDR_WIDTH = 5, - localparam DMAC_DATA_WIDTH = 32, + /*local*/parameter DMAC_ADDR_WIDTH = 5, + /*local*/parameter DMAC_DATA_WIDTH = 32, // // The "ABORT_KEY" is a byte that, if written to the control // word while the core is running, will cause the data transfer diff --git a/rtl/wb2axip/axispacker.v b/rtl/wb2axip/axispacker.v index 74b8f5b..67ee831 100644 --- a/rtl/wb2axip/axispacker.v +++ b/rtl/wb2axip/axispacker.v @@ -39,7 +39,7 @@ // //////////////////////////////////////////////////////////////////////////////// // -`default_nettype none +//`default_nettype none // }}} module axispacker #( parameter C_AXIS_DATA_WIDTH = 32, diff --git a/rtl/wb2axip/axisrandom.v b/rtl/wb2axip/axisrandom.v index 43d91f9..ce46d4c 100644 --- a/rtl/wb2axip/axisrandom.v +++ b/rtl/wb2axip/axisrandom.v @@ -32,11 +32,11 @@ //////////////////////////////////////////////////////////////////////////////// // }}} // -`default_nettype none +//`default_nettype none // module axisrandom #( // {{{ - localparam C_AXIS_DATA_WIDTH = 32 + /*local*/parameter C_AXIS_DATA_WIDTH = 32 // }}} ) ( // {{{ diff --git a/rtl/wb2axip/axissafety.v b/rtl/wb2axip/axissafety.v index 14a194d..d796eec 100644 --- a/rtl/wb2axip/axissafety.v +++ b/rtl/wb2axip/axissafety.v @@ -69,7 +69,7 @@ // //////////////////////////////////////////////////////////////////////////////// // -`default_nettype none +//`default_nettype none // // }}} module axissafety #( diff --git a/rtl/wb2axip/axisswitch.v b/rtl/wb2axip/axisswitch.v index bcae4a3..e8b4455 100644 --- a/rtl/wb2axip/axisswitch.v +++ b/rtl/wb2axip/axisswitch.v @@ -35,7 +35,7 @@ // //////////////////////////////////////////////////////////////////////////////// // -`default_nettype none +//`default_nettype none // }}} module axisswitch #( // {{{ @@ -44,7 +44,7 @@ module axisswitch #( // is fixed at a width of 32-bits by Xilinx def'n, and 2) since // we only ever have a single configuration words. parameter C_AXI_ADDR_WIDTH = 2, - localparam C_AXI_DATA_WIDTH = 32, + /*local*/parameter C_AXI_DATA_WIDTH = 32, // parameter NUM_STREAMS = 4, parameter C_AXIS_DATA_WIDTH = 32, @@ -284,7 +284,7 @@ module axisswitch #( // Place a skidbuffer on every incoming stream input // {{{ generate for(gk=0; gk C_AXI_ADDR_WIDTH, - LGFIFO => LGFIFO, - F_MAXSTALL => F_MAXSTALL, - F_MAXDELAY => F_MAXDELAY - ) - port map ( - i_clk => s_axi_aclk, - i_axi_reset_n => s_axi_aresetn, - o_axi_awready => s_axi_awready, - i_axi_awaddr => s_axi_awaddr, - i_axi_awcache => s_axi_awcache, - i_axi_awprot => s_axi_awprot, - i_axi_awvalid => s_axi_awvalid, - o_axi_wready => s_axi_wready, - i_axi_wdata => s_axi_wdata, - i_axi_wstrb => s_axi_wstrb, - i_axi_wvalid => s_axi_wvalid, - o_axi_bresp => s_axi_bresp, - o_axi_bvalid => s_axi_bvalid, - i_axi_bready => s_axi_bready, - o_axi_arready => s_axi_arready, - i_axi_araddr => s_axi_araddr, - i_axi_arcache => s_axi_arcache, - i_axi_arprot => s_axi_arprot, - i_axi_arvalid => s_axi_arvalid, - o_axi_rresp => s_axi_rresp, - o_axi_rvalid => s_axi_rvalid, - o_axi_rdata => s_axi_rdata, - i_axi_rready => s_axi_rready, - o_reset => m_wb_reset, - o_wb_cyc => m_wb_cyc, - o_wb_stb => m_wb_stb, - o_wb_we => m_wb_we, - o_wb_addr => m_wb_adr, - o_wb_data => m_wb_dat_w, - o_wb_sel => m_wb_sel, - i_wb_ack => m_wb_ack, - i_wb_stall => m_wb_stall, - i_wb_data => m_wb_dat_r, - i_wb_err => m_wb_err - ); - -end Behavioral; diff --git a/rtl/wb2axip/demoaxi.v b/rtl/wb2axip/demoaxi.v index 1babb05..2fd0d9d 100644 --- a/rtl/wb2axip/demoaxi.v +++ b/rtl/wb2axip/demoaxi.v @@ -47,7 +47,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // `timescale 1 ns / 1 ps // }}} @@ -716,5 +716,5 @@ module demoaxi #( `endif endmodule `ifndef YOSYS -`default_nettype wire +//`default_nettype wire `endif diff --git a/rtl/wb2axip/demofull.v b/rtl/wb2axip/demofull.v index 5d0c604..b27d0a7 100644 --- a/rtl/wb2axip/demofull.v +++ b/rtl/wb2axip/demofull.v @@ -40,7 +40,7 @@ // //////////////////////////////////////////////////////////////////////////////// // -`default_nettype none +//`default_nettype none // }}} module demofull #( // {{{ @@ -51,7 +51,7 @@ module demofull #( parameter [0:0] OPT_LOCKID = 1'b1, parameter [0:0] OPT_LOWPOWER = 1'b0, // Some useful short-hand definitions - localparam LSB = $clog2(C_S_AXI_DATA_WIDTH)-3 + /*local*/parameter LSB = $clog2(C_S_AXI_DATA_WIDTH)-3 // }}} ) ( // {{{ @@ -1281,5 +1281,5 @@ module demofull #( // }}} endmodule `ifndef YOSYS -`default_nettype wire +//`default_nettype wire `endif diff --git a/rtl/wb2axip/easyaxil.v b/rtl/wb2axip/easyaxil.v index 0c88b11..e96db11 100644 --- a/rtl/wb2axip/easyaxil.v +++ b/rtl/wb2axip/easyaxil.v @@ -40,7 +40,7 @@ // //////////////////////////////////////////////////////////////////////////////// // -`default_nettype none +//`default_nettype none // }}} module easyaxil #( // {{{ @@ -49,7 +49,7 @@ module easyaxil #( // is fixed at a width of 32-bits by Xilinx def'n, and 2) since // we only ever have 4 configuration words. parameter C_AXI_ADDR_WIDTH = 4, - localparam C_AXI_DATA_WIDTH = 32, + /*local*/parameter C_AXI_DATA_WIDTH = 32, parameter [0:0] OPT_SKIDBUFFER = 1'b0, parameter [0:0] OPT_LOWPOWER = 0 // }}} diff --git a/rtl/wb2axip/migsdram.v b/rtl/wb2axip/migsdram.v index c1671c8..d4153c2 100644 --- a/rtl/wb2axip/migsdram.v +++ b/rtl/wb2axip/migsdram.v @@ -42,7 +42,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module migsdram(i_clk, i_clk_200mhz, o_sys_clk, i_rst, o_sys_reset, // Wishbone components @@ -309,5 +309,5 @@ module migsdram(i_clk, i_clk_200mhz, o_sys_clk, i_rst, o_sys_reset, endmodule `ifndef YOSYS -`default_nettype wire +//`default_nettype wire `endif diff --git a/rtl/wb2axip/sfifo.v b/rtl/wb2axip/sfifo.v index c60dffe..dcaa961 100644 --- a/rtl/wb2axip/sfifo.v +++ b/rtl/wb2axip/sfifo.v @@ -21,7 +21,7 @@ // //////////////////////////////////////////////////////////////////////////////// // -`default_nettype none +//`default_nettype none // }}} module sfifo #( // {{{ @@ -478,5 +478,5 @@ module sfifo #( // }}} endmodule `ifndef YOSYS -`default_nettype wire +//`default_nettype wire `endif diff --git a/rtl/wb2axip/sfifothresh.v b/rtl/wb2axip/sfifothresh.v index 5d4a156..be6da60 100644 --- a/rtl/wb2axip/sfifothresh.v +++ b/rtl/wb2axip/sfifothresh.v @@ -34,7 +34,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module sfifothresh(i_clk, i_reset, i_wr, i_data, o_full, o_fill, diff --git a/rtl/wb2axip/skidbuffer.v b/rtl/wb2axip/skidbuffer.v index 3d19cbb..03b27b0 100644 --- a/rtl/wb2axip/skidbuffer.v +++ b/rtl/wb2axip/skidbuffer.v @@ -77,7 +77,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module skidbuffer #( // {{{ diff --git a/rtl/wb2axip/wbarbiter.v b/rtl/wb2axip/wbarbiter.v index e068278..aac1451 100644 --- a/rtl/wb2axip/wbarbiter.v +++ b/rtl/wb2axip/wbarbiter.v @@ -54,7 +54,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // `define WBA_ALTERNATING // }}} @@ -400,5 +400,5 @@ module wbarbiter #( `endif endmodule `ifndef YOSYS -`default_nettype wire +//`default_nettype wire `endif diff --git a/rtl/wb2axip/wbc2pipeline.v b/rtl/wb2axip/wbc2pipeline.v index ad6a11c..bae8f3a 100644 --- a/rtl/wb2axip/wbc2pipeline.v +++ b/rtl/wb2axip/wbc2pipeline.v @@ -35,7 +35,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module wbc2pipeline #( // {{{ @@ -184,5 +184,5 @@ module wbc2pipeline #( // }}} endmodule `ifndef YOSYS -`default_nettype wire +//`default_nettype wire `endif diff --git a/rtl/wb2axip/wbm2axilite.v b/rtl/wb2axip/wbm2axilite.v index 6cda44d..222d5ab 100644 --- a/rtl/wb2axip/wbm2axilite.v +++ b/rtl/wb2axip/wbm2axilite.v @@ -33,14 +33,14 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module wbm2axilite #( // {{{ parameter C_AXI_ADDR_WIDTH = 28,// AXI Address width - localparam C_AXI_DATA_WIDTH = 32,// Width of the AXI R&W data - localparam DW = C_AXI_DATA_WIDTH,// Wishbone data width - localparam AW = C_AXI_ADDR_WIDTH-2// WB addr width (log wordsize) + /*local*/parameter C_AXI_DATA_WIDTH = 32,// Width of the AXI R&W data + /*local*/parameter DW = C_AXI_DATA_WIDTH,// Wishbone data width + /*local*/parameter AW = C_AXI_ADDR_WIDTH-2// WB addr width (log wordsize) // }}} ) ( // {{{ @@ -681,5 +681,5 @@ module wbm2axilite #( // }}} endmodule `ifndef YOSYS -`default_nettype wire +//`default_nettype wire `endif diff --git a/rtl/wb2axip/wbm2axisp.v b/rtl/wb2axip/wbm2axisp.v index 9c7909a..b6055bd 100644 --- a/rtl/wb2axip/wbm2axisp.v +++ b/rtl/wb2axip/wbm2axisp.v @@ -44,7 +44,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module wbm2axisp #( // {{{ diff --git a/rtl/wb2axip/wbp2classic.v b/rtl/wb2axip/wbp2classic.v index 250489b..2867a13 100644 --- a/rtl/wb2axip/wbp2classic.v +++ b/rtl/wb2axip/wbp2classic.v @@ -32,7 +32,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module wbp2classic #( // {{{ @@ -201,5 +201,5 @@ module wbp2classic #( // }}} endmodule `ifndef YOSYS -`default_nettype wire +//`default_nettype wire `endif diff --git a/rtl/wb2axip/wbsafety.v b/rtl/wb2axip/wbsafety.v index 2636f11..9d7f9cf 100644 --- a/rtl/wb2axip/wbsafety.v +++ b/rtl/wb2axip/wbsafety.v @@ -57,7 +57,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module wbsafety #( // {{{ diff --git a/rtl/wb2axip/wbxbar.v b/rtl/wb2axip/wbxbar.v index 15d6587..c6d019d 100644 --- a/rtl/wb2axip/wbxbar.v +++ b/rtl/wb2axip/wbxbar.v @@ -71,7 +71,7 @@ // //////////////////////////////////////////////////////////////////////////////// // -`default_nettype none +//`default_nettype none // }}} module wbxbar #( // {{{ @@ -1786,5 +1786,5 @@ module wbxbar #( // }}} endmodule `ifndef YOSYS -`default_nettype wire +//`default_nettype wire `endif diff --git a/rtl/wb2axip/wbxclk.v b/rtl/wb2axip/wbxclk.v index 5f404b0..ff65d88 100644 --- a/rtl/wb2axip/wbxclk.v +++ b/rtl/wb2axip/wbxclk.v @@ -57,7 +57,7 @@ //////////////////////////////////////////////////////////////////////////////// // // -`default_nettype none +//`default_nettype none // }}} module wbxclk #( // {{{ -- cgit v1.2.3