| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Filename: xlnxdemo.v |
| // |
| // Project: WB2AXIPSP: bus bridges and other odds and ends |
| // |
| // Purpose: To test the formal tools on an AXI-lite core that is "known" |
| // to work. (Only this one doesn't--at least that was my purpose. |
| // Most of this code comes directly from Vivado's core generator--starting |
| // at the end of this comment block and going down directly to the |
| // `ifdef FORMAL block at the bottom. I have made superficial adjustments |
| // to Xilinx's code: I swapped spaces for tabs, I removed any white space |
| // at the ends of lines, I fixed a spelling error in the comments, added |
| // the default_nettype, added initial statements (at the bottom) for things |
| // that should've had them in the first place, etc. I may have even |
| // swapped an always @(somevalue) for an always @(*), but that's as far |
| // as I've gone. |
| // |
| // Since 2016, Vivado has made updates to their core. The last time I |
| // checked, however, it still failed to pass a formal verification check. |
| // |
| // This core will fail a verification check. |
| // |
| // Creator: Vivado, 2016 (I think it was 2016.1) |
| // |
| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // |
| `default_nettype none // Added to the raw demo |
| `timescale 1 ns / 1 ps |
| // |
| module xlnxdemo # |
| ( |
| // Users to add parameters here |
| |
| // User parameters ends |
| // Do not modify the parameters beyond this line |
| |
| // Width of S_AXI data bus |
| parameter integer C_S_AXI_DATA_WIDTH = 32, |
| // Width of S_AXI address bus |
| parameter integer C_S_AXI_ADDR_WIDTH = 7 |
| ) |
| ( |
| // Users to add ports here |
| |
| // 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, |
| // Write address (issued by master, acceped by Slave) |
| input wire [C_S_AXI_ADDR_WIDTH-1 : 0] S_AXI_AWADDR, |
| // Write channel Protection type. This signal indicates the |
| // privilege and security level of the transaction, and whether |
| // the transaction is a data access or an instruction access. |
| input wire [2 : 0] S_AXI_AWPROT, |
| // Write address valid. This signal indicates that the master signaling |
| // valid write address and control information. |
| input wire S_AXI_AWVALID, |
| // Write address ready. This signal indicates that the slave is ready |
| // to accept an address and associated control signals. |
| output wire S_AXI_AWREADY, |
| // Write data (issued by master, acceped by Slave) |
| input wire [C_S_AXI_DATA_WIDTH-1 : 0] S_AXI_WDATA, |
| // Write strobes. This signal indicates which byte lanes hold |
| // valid data. There is one write strobe bit for each eight |
| // bits of the write data bus. |
| input wire [(C_S_AXI_DATA_WIDTH/8)-1 : 0] S_AXI_WSTRB, |
| // Write valid. This signal indicates that valid write |
| // data and strobes are available. |
| input wire S_AXI_WVALID, |
| // Write ready. This signal indicates that the slave |
| // can accept the write data. |
| output wire S_AXI_WREADY, |
| // Write response. This signal indicates the status |
| // of the write transaction. |
| output wire [1 : 0] S_AXI_BRESP, |
| // Write response valid. This signal indicates that the channel |
| // is signaling a valid write response. |
| output wire S_AXI_BVALID, |
| // Response ready. This signal indicates that the master |
| // can accept a write response. |
| input wire S_AXI_BREADY, |
| // Read address (issued by master, acceped by Slave) |
| input wire [C_S_AXI_ADDR_WIDTH-1 : 0] S_AXI_ARADDR, |
| // Protection type. This signal indicates the privilege |
| // and security level of the transaction, and whether the |
| // transaction is a data access or an instruction access. |
| input wire [2 : 0] S_AXI_ARPROT, |
| // Read address valid. This signal indicates that the channel |
| // is signaling valid read address and control information. |
| input wire S_AXI_ARVALID, |
| // Read address ready. This signal indicates that the slave is |
| // ready to accept an address and associated control signals. |
| output wire S_AXI_ARREADY, |
| // Read data (issued by slave) |
| output wire [C_S_AXI_DATA_WIDTH-1 : 0] S_AXI_RDATA, |
| // Read response. This signal indicates the status of the |
| // read transfer. |
| output wire [1 : 0] S_AXI_RRESP, |
| // Read valid. This signal indicates that the channel is |
| // signaling the required read data. |
| output wire S_AXI_RVALID, |
| // Read ready. This signal indicates that the master can |
| // accept the read data and response information. |
| input wire S_AXI_RREADY |
| ); |
| |
| // AXI4LITE signals |
| reg [C_S_AXI_ADDR_WIDTH-1 : 0] axi_awaddr; |
| reg axi_awready; |
| reg axi_wready; |
| reg [1 : 0] axi_bresp; |
| reg axi_bvalid; |
| reg [C_S_AXI_ADDR_WIDTH-1 : 0] axi_araddr; |
| reg axi_arready; |
| reg [C_S_AXI_DATA_WIDTH-1 : 0] axi_rdata; |
| reg [1 : 0] axi_rresp; |
| reg axi_rvalid; |
| |
| // Example-specific design signals |
| // local parameter for addressing 32 bit / 64 bit C_S_AXI_DATA_WIDTH |
| // ADDR_LSB is used for addressing 32/64 bit registers/memories |
| // ADDR_LSB = 2 for 32 bits (n downto 2) |
| // ADDR_LSB = 3 for 64 bits (n downto 3) |
| localparam integer ADDR_LSB = (C_S_AXI_DATA_WIDTH/32) + 1; |
| localparam integer OPT_MEM_ADDR_BITS = 4; |
| //---------------------------------------------- |
| //-- Signals for user logic register space example |
| //------------------------------------------------ |
| //-- Number of Slave Registers 32 |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg0; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg1; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg2; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg3; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg4; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg5; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg6; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg7; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg8; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg9; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg10; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg11; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg12; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg13; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg14; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg15; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg16; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg17; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg18; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg19; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg20; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg21; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg22; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg23; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg24; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg25; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg26; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg27; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg28; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg29; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg30; |
| reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg31; |
| wire slv_reg_rden; |
| wire slv_reg_wren; |
| reg [C_S_AXI_DATA_WIDTH-1:0] reg_data_out; |
| integer byte_index; |
| |
| // I/O Connections assignments |
| |
| assign S_AXI_AWREADY = axi_awready; |
| assign S_AXI_WREADY = axi_wready; |
| assign S_AXI_BRESP = axi_bresp; |
| assign S_AXI_BVALID = axi_bvalid; |
| assign S_AXI_ARREADY = axi_arready; |
| assign S_AXI_RDATA = axi_rdata; |
| assign S_AXI_RRESP = axi_rresp; |
| assign S_AXI_RVALID = axi_rvalid; |
| // Implement axi_awready generation |
| // axi_awready is asserted for one S_AXI_ACLK clock cycle when both |
| // S_AXI_AWVALID and S_AXI_WVALID are asserted. axi_awready is |
| // de-asserted when reset is low. |
| |
| always @( posedge S_AXI_ACLK ) |
| begin |
| if ( S_AXI_ARESETN == 1'b0 ) |
| begin |
| axi_awready <= 1'b0; |
| end |
| else |
| begin |
| if (~axi_awready && S_AXI_AWVALID && S_AXI_WVALID) |
| begin |
| // slave is ready to accept write address when |
| // there is a valid write address and write data |
| // on the write address and data bus. This design |
| // expects no outstanding transactions. |
| axi_awready <= 1'b1; |
| end |
| else |
| begin |
| axi_awready <= 1'b0; |
| end |
| end |
| end |
| |
| // Implement axi_awaddr latching |
| // This process is used to latch the address when both |
| // S_AXI_AWVALID and S_AXI_WVALID are valid. |
| |
| always @( posedge S_AXI_ACLK ) |
| begin |
| if ( S_AXI_ARESETN == 1'b0 ) |
| begin |
| axi_awaddr <= 0; |
| end |
| else |
| begin |
| if (~axi_awready && S_AXI_AWVALID && S_AXI_WVALID) |
| begin |
| // Write Address latching |
| axi_awaddr <= S_AXI_AWADDR; |
| end |
| end |
| end |
| |
| // Implement axi_wready generation |
| // axi_wready is asserted for one S_AXI_ACLK clock cycle when both |
| // S_AXI_AWVALID and S_AXI_WVALID are asserted. axi_wready is |
| // de-asserted when reset is low. |
| |
| always @( posedge S_AXI_ACLK ) |
| begin |
| if ( S_AXI_ARESETN == 1'b0 ) |
| begin |
| axi_wready <= 1'b0; |
| end |
| else |
| begin |
| if (~axi_wready && S_AXI_WVALID && S_AXI_AWVALID) |
| begin |
| // slave is ready to accept write data when |
| // there is a valid write address and write data |
| // on the write address and data bus. This design |
| // expects no outstanding transactions. |
| axi_wready <= 1'b1; |
| end |
| else |
| begin |
| axi_wready <= 1'b0; |
| end |
| end |
| end |
| |
| // Implement memory mapped register select and write logic generation |
| // The write data is accepted and written to memory mapped registers when |
| // axi_awready, S_AXI_WVALID, axi_wready and S_AXI_WVALID are asserted. Write strobes are used to |
| // select byte enables of slave registers while writing. |
| // These registers are cleared when reset (active low) is applied. |
| // Slave register write enable is asserted when valid address and data are available |
| // and the slave is ready to accept the write address and write data. |
| assign slv_reg_wren = axi_wready && S_AXI_WVALID && axi_awready && S_AXI_AWVALID; |
| |
| always @( posedge S_AXI_ACLK ) |
| begin |
| if ( S_AXI_ARESETN == 1'b0 ) |
| begin |
| slv_reg0 <= 0; |
| slv_reg1 <= 0; |
| slv_reg2 <= 0; |
| slv_reg3 <= 0; |
| slv_reg4 <= 0; |
| slv_reg5 <= 0; |
| slv_reg6 <= 0; |
| slv_reg7 <= 0; |
| slv_reg8 <= 0; |
| slv_reg9 <= 0; |
| slv_reg10 <= 0; |
| slv_reg11 <= 0; |
| slv_reg12 <= 0; |
| slv_reg13 <= 0; |
| slv_reg14 <= 0; |
| slv_reg15 <= 0; |
| slv_reg16 <= 0; |
| slv_reg17 <= 0; |
| slv_reg18 <= 0; |
| slv_reg19 <= 0; |
| slv_reg20 <= 0; |
| slv_reg21 <= 0; |
| slv_reg22 <= 0; |
| slv_reg23 <= 0; |
| slv_reg24 <= 0; |
| slv_reg25 <= 0; |
| slv_reg26 <= 0; |
| slv_reg27 <= 0; |
| slv_reg28 <= 0; |
| slv_reg29 <= 0; |
| slv_reg30 <= 0; |
| slv_reg31 <= 0; |
| end |
| else begin |
| if (slv_reg_wren) |
| begin |
| case ( axi_awaddr[ADDR_LSB+OPT_MEM_ADDR_BITS:ADDR_LSB] ) |
| 5'h00: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 0 |
| slv_reg0[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h01: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 1 |
| slv_reg1[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h02: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 2 |
| slv_reg2[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h03: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 3 |
| slv_reg3[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h04: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 4 |
| slv_reg4[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h05: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 5 |
| slv_reg5[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h06: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 6 |
| slv_reg6[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h07: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 7 |
| slv_reg7[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h08: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 8 |
| slv_reg8[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h09: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 9 |
| slv_reg9[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h0A: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 10 |
| slv_reg10[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h0B: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 11 |
| slv_reg11[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h0C: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 12 |
| slv_reg12[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h0D: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 13 |
| slv_reg13[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h0E: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 14 |
| slv_reg14[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h0F: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 15 |
| slv_reg15[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h10: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 16 |
| slv_reg16[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h11: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 17 |
| slv_reg17[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h12: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 18 |
| slv_reg18[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h13: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 19 |
| slv_reg19[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h14: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 20 |
| slv_reg20[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h15: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 21 |
| slv_reg21[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h16: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 22 |
| slv_reg22[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h17: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 23 |
| slv_reg23[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h18: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 24 |
| slv_reg24[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h19: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 25 |
| slv_reg25[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h1A: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 26 |
| slv_reg26[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h1B: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 27 |
| slv_reg27[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h1C: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 28 |
| slv_reg28[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h1D: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 29 |
| slv_reg29[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h1E: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 30 |
| slv_reg30[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| 5'h1F: |
| for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 ) |
| if ( S_AXI_WSTRB[byte_index] == 1 ) begin |
| // Respective byte enables are asserted as per write strobes |
| // Slave register 31 |
| slv_reg31[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8]; |
| end |
| default : begin |
| slv_reg0 <= slv_reg0; |
| slv_reg1 <= slv_reg1; |
| slv_reg2 <= slv_reg2; |
| slv_reg3 <= slv_reg3; |
| slv_reg4 <= slv_reg4; |
| slv_reg5 <= slv_reg5; |
| slv_reg6 <= slv_reg6; |
| slv_reg7 <= slv_reg7; |
| slv_reg8 <= slv_reg8; |
| slv_reg9 <= slv_reg9; |
| slv_reg10 <= slv_reg10; |
| slv_reg11 <= slv_reg11; |
| slv_reg12 <= slv_reg12; |
| slv_reg13 <= slv_reg13; |
| slv_reg14 <= slv_reg14; |
| slv_reg15 <= slv_reg15; |
| slv_reg16 <= slv_reg16; |
| slv_reg17 <= slv_reg17; |
| slv_reg18 <= slv_reg18; |
| slv_reg19 <= slv_reg19; |
| slv_reg20 <= slv_reg20; |
| slv_reg21 <= slv_reg21; |
| slv_reg22 <= slv_reg22; |
| slv_reg23 <= slv_reg23; |
| slv_reg24 <= slv_reg24; |
| slv_reg25 <= slv_reg25; |
| slv_reg26 <= slv_reg26; |
| slv_reg27 <= slv_reg27; |
| slv_reg28 <= slv_reg28; |
| slv_reg29 <= slv_reg29; |
| slv_reg30 <= slv_reg30; |
| slv_reg31 <= slv_reg31; |
| end |
| endcase |
| end |
| end |
| end |
| |
| // Implement write response logic generation |
| // The write response and response valid signals are asserted by the slave |
| // when axi_wready, S_AXI_WVALID, axi_wready and S_AXI_WVALID are asserted. |
| // This marks the acceptance of address and indicates the status of |
| // write transaction. |
| |
| always @( posedge S_AXI_ACLK ) |
| begin |
| if ( S_AXI_ARESETN == 1'b0 ) |
| begin |
| axi_bvalid <= 0; |
| axi_bresp <= 2'b0; |
| end |
| else |
| begin |
| if (axi_awready && S_AXI_AWVALID && ~axi_bvalid && axi_wready && S_AXI_WVALID) |
| begin |
| // indicates a valid write response is available |
| axi_bvalid <= 1'b1; |
| axi_bresp <= 2'b0; // 'OKAY' response |
| end // work error responses in future |
| else |
| begin |
| if (S_AXI_BREADY && axi_bvalid) |
| //check if bready is asserted while bvalid is high) |
| //(there is a possibility that bready is always asserted high) |
| begin |
| axi_bvalid <= 1'b0; |
| end |
| end |
| end |
| end |
| |
| // Implement axi_arready generation |
| // axi_arready is asserted for one S_AXI_ACLK clock cycle when |
| // S_AXI_ARVALID is asserted. axi_awready is |
| // de-asserted when reset (active low) is asserted. |
| // The read address is also latched when S_AXI_ARVALID is |
| // asserted. axi_araddr is reset to zero on reset assertion. |
| |
| always @( posedge S_AXI_ACLK ) |
| begin |
| if ( S_AXI_ARESETN == 1'b0 ) |
| begin |
| axi_arready <= 1'b0; |
| axi_araddr <= 7'b0; |
| end |
| else |
| begin |
| if (~axi_arready && S_AXI_ARVALID) |
| begin |
| // indicates that the slave has acceped the valid read address |
| axi_arready <= 1'b1; |
| // Read address latching |
| axi_araddr <= S_AXI_ARADDR; |
| end |
| else |
| begin |
| axi_arready <= 1'b0; |
| end |
| end |
| end |
| |
| // Implement axi_arvalid generation |
| // axi_rvalid is asserted for one S_AXI_ACLK clock cycle when both |
| // S_AXI_ARVALID and axi_arready are asserted. The slave registers |
| // data are available on the axi_rdata bus at this instance. The |
| // assertion of axi_rvalid marks the validity of read data on the |
| // bus and axi_rresp indicates the status of read transaction.axi_rvalid |
| // is deasserted on reset (active low). axi_rresp and axi_rdata are |
| // cleared to zero on reset (active low). |
| always @( posedge S_AXI_ACLK ) |
| begin |
| if ( S_AXI_ARESETN == 1'b0 ) |
| begin |
| axi_rvalid <= 0; |
| axi_rresp <= 0; |
| end |
| else |
| begin |
| if (axi_arready && S_AXI_ARVALID && ~axi_rvalid) |
| begin |
| // Valid read data is available at the read data bus |
| axi_rvalid <= 1'b1; |
| axi_rresp <= 2'b0; // 'OKAY' response |
| end |
| else if (axi_rvalid && S_AXI_RREADY) |
| begin |
| // Read data is accepted by the master |
| axi_rvalid <= 1'b0; |
| end |
| end |
| end |
| |
| // Implement memory mapped register select and read logic generation |
| // Slave register read enable is asserted when valid address is available |
| // and the slave is ready to accept the read address. |
| assign slv_reg_rden = axi_arready & S_AXI_ARVALID & ~axi_rvalid; |
| always @(*) |
| begin |
| reg_data_out = 0; |
| // Address decoding for reading registers |
| case ( axi_araddr[ADDR_LSB+OPT_MEM_ADDR_BITS:ADDR_LSB] ) |
| 5'h00 : reg_data_out = slv_reg0; |
| 5'h01 : reg_data_out = slv_reg1; |
| 5'h02 : reg_data_out = slv_reg2; |
| 5'h03 : reg_data_out = slv_reg3; |
| 5'h04 : reg_data_out = slv_reg4; |
| 5'h05 : reg_data_out = slv_reg5; |
| 5'h06 : reg_data_out = slv_reg6; |
| 5'h07 : reg_data_out = slv_reg7; |
| 5'h08 : reg_data_out = slv_reg8; |
| 5'h09 : reg_data_out = slv_reg9; |
| 5'h0A : reg_data_out = slv_reg10; |
| 5'h0B : reg_data_out = slv_reg11; |
| 5'h0C : reg_data_out = slv_reg12; |
| 5'h0D : reg_data_out = slv_reg13; |
| 5'h0E : reg_data_out = slv_reg14; |
| 5'h0F : reg_data_out = slv_reg15; |
| 5'h10 : reg_data_out = slv_reg16; |
| 5'h11 : reg_data_out = slv_reg17; |
| 5'h12 : reg_data_out = slv_reg18; |
| 5'h13 : reg_data_out = slv_reg19; |
| 5'h14 : reg_data_out = slv_reg20; |
| 5'h15 : reg_data_out = slv_reg21; |
| 5'h16 : reg_data_out = slv_reg22; |
| 5'h17 : reg_data_out = slv_reg23; |
| 5'h18 : reg_data_out = slv_reg24; |
| 5'h19 : reg_data_out = slv_reg25; |
| 5'h1A : reg_data_out = slv_reg26; |
| 5'h1B : reg_data_out = slv_reg27; |
| 5'h1C : reg_data_out = slv_reg28; |
| 5'h1D : reg_data_out = slv_reg29; |
| 5'h1E : reg_data_out = slv_reg30; |
| 5'h1F : reg_data_out = slv_reg31; |
| default : reg_data_out = 0; |
| endcase |
| end |
| |
| // Output register or memory read data |
| always @( posedge S_AXI_ACLK ) |
| begin |
| if ( S_AXI_ARESETN == 1'b0 ) |
| begin |
| axi_rdata <= 0; |
| end |
| else |
| begin |
| // When there is a valid read address (S_AXI_ARVALID) with |
| // acceptance of read address by the slave (axi_arready), |
| // output the read data |
| if (slv_reg_rden) |
| begin |
| axi_rdata <= reg_data_out; // register read data |
| end |
| end |
| end |
| |
| // Add user logic here |
| |
| // User logic ends |
| // |
| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Formal Verification section begins here. |
| // |
| // The following code was not part of the original Xilinx demo. |
| // |
| //////////////////////////////////////////////////////////////////////////////// |
| `ifdef FORMAL |
| localparam F_LGDEPTH = 4; |
| |
| wire [(F_LGDEPTH-1):0] f_axi_awr_outstanding, |
| f_axi_wr_outstanding, |
| f_axi_rd_outstanding; |
| |
| // |
| // Connect our slave to the AXI-lite property set |
| // |
| faxil_slave #(// .C_AXI_DATA_WIDTH(C_S_AXI_DATA_WIDTH), |
| .C_AXI_ADDR_WIDTH(C_S_AXI_ADDR_WIDTH), |
| .F_LGDEPTH(F_LGDEPTH)) properties( |
| .i_clk(S_AXI_ACLK), |
| .i_axi_reset_n(S_AXI_ARESETN), |
| // |
| .i_axi_awaddr(S_AXI_AWADDR), |
| .i_axi_awcache(4'h0), |
| .i_axi_awprot(S_AXI_AWPROT), |
| .i_axi_awvalid(S_AXI_AWVALID), |
| .i_axi_awready(S_AXI_AWREADY), |
| // |
| .i_axi_wdata(S_AXI_WDATA), |
| .i_axi_wstrb(S_AXI_WSTRB), |
| .i_axi_wvalid(S_AXI_WVALID), |
| .i_axi_wready(S_AXI_WREADY), |
| // |
| .i_axi_bresp(S_AXI_BRESP), |
| .i_axi_bvalid(S_AXI_BVALID), |
| .i_axi_bready(S_AXI_BREADY), |
| // |
| .i_axi_araddr(S_AXI_ARADDR), |
| .i_axi_arprot(S_AXI_ARPROT), |
| .i_axi_arcache(4'h0), |
| .i_axi_arvalid(S_AXI_ARVALID), |
| .i_axi_arready(S_AXI_ARREADY), |
| // |
| .i_axi_rdata(S_AXI_RDATA), |
| .i_axi_rresp(S_AXI_RRESP), |
| .i_axi_rvalid(S_AXI_RVALID), |
| .i_axi_rready(S_AXI_RREADY), |
| // |
| .f_axi_rd_outstanding(f_axi_rd_outstanding), |
| .f_axi_wr_outstanding(f_axi_wr_outstanding), |
| .f_axi_awr_outstanding(f_axi_awr_outstanding)); |
| |
| reg f_past_valid; |
| initial f_past_valid = 1'b0; |
| always @(posedge S_AXI_ACLK) |
| f_past_valid <= 1'b1; |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| // Properties necessary to pass induction |
| // --- assuming we make it that far (we won't) |
| // |
| // |
| always @(*) |
| if (S_AXI_ARESETN) |
| begin |
| assert(f_axi_rd_outstanding == ((S_AXI_RVALID)? 1:0)); |
| assert(f_axi_wr_outstanding == ((S_AXI_BVALID)? 1:0)); |
| end |
| |
| always @(*) |
| assert(f_axi_awr_outstanding == f_axi_wr_outstanding); |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| // Cover properties |
| // |
| // |
| // Make sure it is possible to change our register |
| always @(posedge S_AXI_ACLK) |
| cover($changed(slv_reg0)&&(slv_reg0 == 32'hdeadbeef)); |
| |
| always @(posedge S_AXI_ACLK) |
| cover((axi_rvalid)&&(axi_rdata == 32'hdeadbeef) |
| &&($past(axi_araddr[ADDR_LSB+OPT_MEM_ADDR_BITS:ADDR_LSB] == 0))); |
| |
| // Make sure it is possible to read from our register |
| always @(posedge S_AXI_ACLK) |
| cover($past(reg_data_out == slv_reg0) |
| &&($past(axi_araddr[ADDR_LSB+OPT_MEM_ADDR_BITS:ADDR_LSB])==0) |
| &&(axi_rdata == slv_reg0)); |
| |
| // Performance test. See if we can retire a request on every other |
| // instruction |
| // |
| // --- This first pair of cover statements will pass as written |
| // |
| // First a write check |
| always @(posedge S_AXI_ACLK) |
| cover( ((S_AXI_BVALID)&&(S_AXI_BREADY)) |
| &&(!$past((S_AXI_BVALID)&&(S_AXI_BREADY),1)) |
| &&( $past((S_AXI_BVALID)&&(S_AXI_BREADY),2)) |
| &&(!$past((S_AXI_BVALID)&&(S_AXI_BREADY),3))); |
| |
| // Now a read check |
| always @(posedge S_AXI_ACLK) |
| cover( ((S_AXI_RVALID)&&(S_AXI_RREADY)) |
| &&(!$past((S_AXI_RVALID)&&(S_AXI_RREADY),1)) |
| &&( $past((S_AXI_RVALID)&&(S_AXI_RREADY),2)) |
| &&(!$past((S_AXI_RVALID)&&(S_AXI_RREADY),3))); |
| |
| // Now let's see if we can retire one value every clock tick |
| // |
| // --- These two cover statements will fail, even though the ones |
| // above will pass. This is why I call the design "crippled". |
| // |
| // First a write check |
| always @(posedge S_AXI_ACLK) |
| cover( ((S_AXI_BVALID)&&(S_AXI_BREADY)) |
| &&($past((S_AXI_BVALID)&&(S_AXI_BREADY),1)) |
| &&($past((S_AXI_BVALID)&&(S_AXI_BREADY),2)) |
| &&($past((S_AXI_BVALID)&&(S_AXI_BREADY),3))); |
| |
| // Now a read check |
| always @(posedge S_AXI_ACLK) |
| cover( ((S_AXI_RVALID)&&(S_AXI_RREADY)) |
| &&($past((S_AXI_RVALID)&&(S_AXI_RREADY),1)) |
| &&($past((S_AXI_RVALID)&&(S_AXI_RREADY),2)) |
| &&($past((S_AXI_RVALID)&&(S_AXI_RREADY),3))); |
| |
| // Now let's spend some time to develop a more complicated read |
| // trace, showing the capabilities of the core. We'll avoid the |
| // broken parts of the core, and just present ... something useful. |
| // |
| reg [12:0] fr_rdcover, fw_rdcover; |
| |
| initial fr_rdcover = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| fr_rdcover <= 0; |
| else |
| fr_rdcover <= fw_rdcover; |
| |
| always @(*) |
| if ((!S_AXI_ARESETN)||(S_AXI_AWVALID)||(S_AXI_WVALID)) |
| fw_rdcover = 0; |
| else begin |
| // |
| // A basic read request |
| fw_rdcover[0] = (S_AXI_ARVALID) |
| &&(S_AXI_RREADY); |
| fw_rdcover[1] = fr_rdcover[0] |
| &&(S_AXI_ARVALID) |
| &&(S_AXI_RREADY); |
| fw_rdcover[2] = fr_rdcover[1] |
| &&(!S_AXI_ARVALID) |
| &&(S_AXI_RREADY); |
| fw_rdcover[3] = fr_rdcover[2] |
| &&(!S_AXI_ARVALID) |
| &&(S_AXI_RREADY); |
| fw_rdcover[4] = fr_rdcover[3] |
| &&(!S_AXI_ARVALID) |
| &&(S_AXI_RREADY); |
| // |
| // A high speed/pipelined read request |
| fw_rdcover[5] = fr_rdcover[4] |
| &&(S_AXI_ARVALID) |
| &&(S_AXI_RREADY); |
| fw_rdcover[6] = fr_rdcover[5] |
| &&(S_AXI_ARVALID) |
| &&(S_AXI_RREADY); |
| fw_rdcover[7] = fr_rdcover[6] |
| &&(S_AXI_ARVALID) |
| &&(S_AXI_RREADY); |
| fw_rdcover[8] = fr_rdcover[7] |
| &&(S_AXI_ARVALID) |
| &&(S_AXI_RREADY); |
| fw_rdcover[9] = fr_rdcover[8] |
| &&(S_AXI_ARVALID) |
| &&(S_AXI_RREADY); |
| fw_rdcover[10] = fr_rdcover[9] |
| &&(S_AXI_ARVALID) |
| &&(S_AXI_RREADY); |
| fw_rdcover[11] = fr_rdcover[10] |
| &&(!S_AXI_ARVALID) |
| &&(S_AXI_RREADY); |
| fw_rdcover[12] = fr_rdcover[11] |
| &&(!S_AXI_ARVALID) |
| &&(S_AXI_RREADY); |
| end |
| |
| always @(*) |
| begin |
| cover(fw_rdcover[0]); |
| cover(fw_rdcover[1]); |
| cover(fw_rdcover[2]); |
| cover(fw_rdcover[3]); |
| cover(fw_rdcover[4]); |
| cover(fw_rdcover[5]); // |
| cover(fw_rdcover[6]); |
| cover(fw_rdcover[7]); |
| cover(fw_rdcover[8]); |
| cover(fw_rdcover[9]); |
| cover(fw_rdcover[10]); |
| cover(fw_rdcover[11]); |
| cover(fw_rdcover[12]); |
| end |
| |
| // |
| // Now let's repeat our complicated cover approach for the write |
| // channel. |
| // |
| reg [24:0] fr_wrcover, fw_wrcover; |
| |
| initial fr_wrcover = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| fr_wrcover <= 0; |
| else |
| fr_wrcover <= fw_wrcover; |
| |
| always @(*) |
| if ((!S_AXI_ARESETN)||(S_AXI_ARVALID)||(!S_AXI_BREADY)) |
| fw_wrcover = 0; |
| else begin |
| // |
| // A basic (synchronized) write request |
| fw_wrcover[0] = (S_AXI_AWVALID) |
| &&(S_AXI_WVALID); |
| fw_wrcover[1] = fr_wrcover[0] |
| &&(S_AXI_AWVALID) |
| &&(S_AXI_WVALID); |
| fw_wrcover[2] = fr_wrcover[1] |
| &&(!S_AXI_AWVALID) |
| &&(!S_AXI_WVALID); |
| fw_wrcover[3] = fr_wrcover[2] |
| &&(!S_AXI_AWVALID) |
| &&(!S_AXI_WVALID); |
| fw_wrcover[4] = fr_wrcover[3] |
| &&(!S_AXI_ARVALID) |
| &&(S_AXI_RREADY); |
| // |
| // Address before data |
| fw_wrcover[5] = fr_wrcover[4] |
| &&(S_AXI_AWVALID) |
| &&(!S_AXI_WVALID); |
| fw_wrcover[6] = fr_wrcover[5] |
| &&(S_AXI_AWVALID) |
| &&(!S_AXI_WVALID); |
| fw_wrcover[7] = fr_wrcover[6] |
| &&(S_AXI_AWVALID) |
| &&(S_AXI_WVALID); |
| fw_wrcover[8] = fr_wrcover[7] |
| &&(S_AXI_AWVALID) |
| &&(S_AXI_WVALID); |
| fw_wrcover[9] = fr_wrcover[8] |
| &&(!S_AXI_AWVALID) |
| &&(!S_AXI_WVALID); |
| fw_wrcover[10] = fr_wrcover[9] |
| &&(!S_AXI_AWVALID) |
| &&(!S_AXI_WVALID); |
| // |
| // Data before address |
| fw_wrcover[11] = fr_wrcover[10] |
| &&(!S_AXI_AWVALID) |
| &&(S_AXI_WVALID); |
| fw_wrcover[12] = fr_wrcover[11] |
| &&(S_AXI_AWVALID) |
| &&(S_AXI_WVALID); |
| fw_wrcover[13] = fr_wrcover[12] |
| &&(S_AXI_AWVALID) |
| &&(S_AXI_WVALID); |
| fw_wrcover[14] = fr_wrcover[13] |
| &&(!S_AXI_AWVALID) |
| &&(!S_AXI_WVALID); |
| fw_wrcover[15] = fr_wrcover[14] |
| &&(!S_AXI_AWVALID) |
| &&(!S_AXI_WVALID); |
| // |
| // A high speed/pipelined read request |
| fw_wrcover[16] = fr_wrcover[15] |
| &&(S_AXI_AWVALID) |
| &&(S_AXI_WVALID); |
| fw_wrcover[17] = fr_wrcover[16] |
| &&(S_AXI_AWVALID) |
| &&(S_AXI_WVALID); |
| fw_wrcover[18] = fr_wrcover[17] |
| &&(S_AXI_AWVALID) |
| &&(S_AXI_WVALID); |
| fw_wrcover[19] = fr_wrcover[18] |
| &&(S_AXI_AWVALID) |
| &&(S_AXI_WVALID); |
| fw_wrcover[20] = fr_wrcover[19] |
| &&(S_AXI_AWVALID) |
| &&(S_AXI_WVALID); |
| fw_wrcover[21] = fr_wrcover[20] |
| &&(S_AXI_AWVALID) |
| &&(S_AXI_WVALID); |
| fw_wrcover[22] = fr_wrcover[21] |
| &&(!S_AXI_AWVALID) |
| &&(!S_AXI_WVALID); |
| fw_wrcover[23] = fr_wrcover[22] |
| &&(!S_AXI_AWVALID) |
| &&(!S_AXI_WVALID); |
| fw_wrcover[24] = fr_wrcover[23] |
| &&(!S_AXI_AWVALID) |
| &&(!S_AXI_WVALID); |
| end |
| |
| always @(*) |
| begin |
| cover(fw_wrcover[0]); |
| cover(fw_wrcover[1]); |
| cover(fw_wrcover[2]); |
| cover(fw_wrcover[3]); |
| cover(fw_wrcover[4]); |
| cover(fw_wrcover[5]); // |
| cover(fw_wrcover[6]); |
| cover(fw_wrcover[7]); |
| cover(fw_wrcover[8]); |
| cover(fw_wrcover[9]); |
| cover(fw_wrcover[11]); |
| cover(fw_wrcover[12]); |
| cover(fw_wrcover[13]); |
| cover(fw_wrcover[14]); |
| cover(fw_wrcover[15]); |
| cover(fw_wrcover[16]); |
| cover(fw_wrcover[17]); |
| cover(fw_wrcover[18]); |
| cover(fw_wrcover[19]); |
| cover(fw_wrcover[20]); |
| cover(fw_wrcover[21]); |
| cover(fw_wrcover[22]); |
| cover(fw_wrcover[23]); |
| cover(fw_wrcover[24]); |
| end |
| `endif |
| // |
| // |
| // Bug fixes section |
| // |
| // The lines below contain assumptions necessary to get the design |
| // to work. They represent things Xilinx never thought of when |
| // building their demo. |
| // |
| // The following lines are only questionable a bug |
| initial axi_arready = 1'b0; |
| initial axi_awready = 1'b0; |
| initial axi_wready = 1'b0; |
| initial axi_bvalid = 1'b0; |
| initial axi_rvalid = 1'b0; |
| |
| // |
| // This here is necessary to avoid the biggest bug within the design. |
| // |
| // If you uncomment the following two lines, the design will work as |
| // intended. Only ... the bus now has more requirements to it. |
| // |
| // always @(posedge S_AXI_ACLK) |
| // if ($past(S_AXI_ARESETN)) |
| // assume((S_AXI_RREADY)&&(S_AXI_BREADY)); |
| |
| // verilator lint_off UNUSED |
| wire [9:0] unused; |
| assign unused = { S_AXI_ARPROT, S_AXI_AWPROT, |
| axi_awaddr[1:0], axi_araddr[1:0] }; |
| // verilator lint_on UNUSED |
| endmodule |
