diff options
Diffstat (limited to 'rtl/wb2axip/axilgpio.v')
| -rw-r--r-- | rtl/wb2axip/axilgpio.v | 808 |
1 files changed, 808 insertions, 0 deletions
diff --git a/rtl/wb2axip/axilgpio.v b/rtl/wb2axip/axilgpio.v new file mode 100644 index 0000000..0a6e90c --- /dev/null +++ b/rtl/wb2axip/axilgpio.v @@ -0,0 +1,808 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// Filename: axilgpio +// {{{ +// Project: WB2AXIPSP: bus bridges and other odds and ends +// +// Purpose: A simple and basic AXI-lite input and output module. +// Tristates are not supported internally, although output bits +// may be used externally to create a tristate input. For example, when +// driving an I2C controller, you might wish to do something like: +// +// assign i2c_scl = gpio_output[1] ? 1'bz : gpio_output[1]; +// assign i2c_sda = gpio_output[0] ? 1'bz : gpio_output[0]; +// +// Or, as another example: +// +// assign generic_io = gpio_output[3] ? 1'bz : gpio_output[2]; +// +// Registers: +// 0: LOAD +// Write to this register will overwrite the output data bits. +// 4: SET +// Writes to this register will set every output data bit where +// the written bit is set. +// +// OUTPUT[k] = OLD BIT[k] || NEW_BIT[k] +// +// 8: CLEAR +// Writes to this register will clear every output data bit where +// the written bit is set. +// +// OUTPUT[k] = OLD BIT[k] && (!NEW_BIT[k]) +// +// 12: TOGGLE +// Writes to this register will toggle every output bit where +// the bit written is set. +// +// OUTPUT[k] = OLD BIT[k] ^ NEW_BIT[k] +// +// The next four registers are present if (and only if) NIN > 0. If not, +// the prior four registers will be repeated. +// +// 16: Input data (if NIN > 0) +// This is the input data, following a two-register CDC. +// 20: Input data toggle detection +// A bit will be set in this register if ever the associated +// input data bit toggles. To clear, write a '1' to the toggled +// bit in this register. +// +// Bits from this register that are set will then create an +// outgoing interrupt--provided they are not masked. +// +// 24: Input data interrupt mask +// If any "mask" bit is set, then toggled data will not trigger +// an interrupt. +// 28: Input data interrupts active +// This is the AND of toggled data and a clear interrupt mask bit. +// +// An output interrupt is generated if any of the bits in the interrupt +// active register is high. +// +// Creator: Dan Gisselquist, Ph.D. +// Gisselquist Technology, LLC +// +//////////////////////////////////////////////////////////////////////////////// +// }}} +// Copyright (C) 2021-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 axilgpio #( + // {{{ + // + // 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 = 5, + localparam C_AXI_DATA_WIDTH = 32, + // OPT_SKIDBUFFER will increase throughput to 100% from 50% + parameter [0:0] OPT_SKIDBUFFER = 1'b1, + // OPT_LOWPOWER will force RDATA to zero if ever !RVALID + parameter [0:0] OPT_LOWPOWER = 0, + // NOUT : Number of output bits. Must be > 0 + parameter NOUT = 30, + // NIN: Number of input bits. May be zero if desired. + parameter NIN = 5, + parameter [NOUT-1:0] DEFAULT_OUTPUT = 0 + // }}} + ) ( + // {{{ + input wire S_AXI_ACLK, + input wire S_AXI_ARESETN, + // AXI-lite interface + // {{{ + 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, + // }}} + output wire [NOUT-1:0] o_gpio, + input wire [((NIN>0) ? (NIN-1):0):0] i_gpio, + output wire o_int + // }}} + ); + + //////////////////////////////////////////////////////////////////////// + // + // Register/wire signal declarations + // {{{ + //////////////////////////////////////////////////////////////////////// + // + localparam ADDRLSB = $clog2(C_AXI_DATA_WIDTH)-3; + localparam [2:0] // ADDR_LOAD = 3'b000, + // ADDR_SET = 3'b001, + // ADDR_CLEAR = 3'b010, + // ADDR_TOGGLE = 3'b011, + ADDR_INDATA = 3'b100, + ADDR_CHANGED= 3'b101, + ADDR_MASK = 3'b110, + ADDR_INT = 3'b111; + + + 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; + // + 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; + + reg [31:0] r_gpio; + wire [31:0] ck_gpio, ck_toggled, w_mask, int_toggled, wskd_gpio; + + + // }}} + //////////////////////////////////////////////////////////////////////// + // + // AXI-lite signaling + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + + // + // Write signaling + // + // {{{ + + generate if (OPT_SKIDBUFFER) + begin : SKIDBUFFER_WRITE + // {{{ + wire awskd_valid, wskd_valid; + + 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); + // }}} + end else begin : SIMPLE_WRITES + // {{{ + reg axil_awready; + + initial axil_awready = 1'b0; + always @(posedge S_AXI_ACLK) + if (!S_AXI_ARESETN) + axil_awready <= 1'b0; + else + axil_awready <= !axil_awready + && (S_AXI_AWVALID && S_AXI_WVALID) + && (!S_AXI_BVALID || S_AXI_BREADY); + + assign S_AXI_AWREADY = axil_awready; + assign S_AXI_WREADY = axil_awready; + + assign awskd_addr = S_AXI_AWADDR[C_AXI_ADDR_WIDTH-1:ADDRLSB]; + assign wskd_data = S_AXI_WDATA; + assign wskd_strb = S_AXI_WSTRB; + + assign axil_write_ready = axil_awready; + // }}} + 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; + assign S_AXI_BRESP = 2'b00; + // }}} + + // + // Read signaling + // + // {{{ + + generate if (OPT_SKIDBUFFER) + begin : SKIDBUFFER_READ + // {{{ + 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 + && (!axil_read_valid || S_AXI_RREADY); + // }}} + end else begin : SIMPLE_READS + // {{{ + reg axil_arready; + + always @(*) + axil_arready = !S_AXI_RVALID; + + assign arskd_addr = S_AXI_ARADDR[C_AXI_ADDR_WIDTH-1:ADDRLSB]; + assign S_AXI_ARREADY = axil_arready; + assign axil_read_ready = (S_AXI_ARVALID && S_AXI_ARREADY); + // }}} + end endgenerate + + 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; + assign S_AXI_RDATA = axil_read_data; + assign S_AXI_RRESP = 2'b00; + // }}} + + // }}} + //////////////////////////////////////////////////////////////////////// + // + // AXI-lite register logic + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + + assign wskd_gpio = apply_wstrb(r_gpio, wskd_data, wskd_strb); + + // r_gpio, o_gpio + // {{{ + initial r_gpio = 0; + always @(posedge S_AXI_ACLK) + begin + if (axil_write_ready) + begin + case({ (awskd_addr[2] && (NIN > 0)), awskd_addr[1:0] }) + 3'b000: r_gpio <= wskd_gpio; + 3'b001: begin // SET + // {{{ + if (wskd_strb[0]) + r_gpio[ 7: 0]<= r_gpio[ 7: 0]| wskd_data[ 7: 0]; + if (wskd_strb[1]) + r_gpio[15: 8]<= r_gpio[15: 8]| wskd_data[15: 8]; + if (wskd_strb[2]) + r_gpio[23:16]<= r_gpio[23:16]| wskd_data[23:16]; + if (wskd_strb[3]) + r_gpio[31:24]<= r_gpio[31:24]| wskd_data[31:24]; + end + // }}} + 3'b010: begin // CLEAR + // {{{ + if (wskd_strb[0]) + r_gpio[ 7: 0]<= r_gpio[ 7: 0]&~wskd_data[ 7: 0]; + if (wskd_strb[1]) + r_gpio[15: 8]<= r_gpio[15: 8]&~wskd_data[15: 8]; + if (wskd_strb[2]) + r_gpio[23:16]<= r_gpio[23:16]&~wskd_data[23:16]; + if (wskd_strb[3]) + r_gpio[31:24]<= r_gpio[31:24]&~wskd_data[31:24]; + end + // }}} + 3'b011: begin // TOGGLE + // {{{ + if (wskd_strb[0]) + r_gpio[ 7: 0]<=r_gpio[ 7: 0] ^ wskd_data[ 7: 0]; + if (wskd_strb[1]) + r_gpio[15: 8]<=r_gpio[15: 8] ^ wskd_data[15: 8]; + if (wskd_strb[2]) + r_gpio[23:16]<=r_gpio[23:16] ^ wskd_data[23:16]; + if (wskd_strb[3]) + r_gpio[31:24]<=r_gpio[31:24] ^ wskd_data[31:24]; + end + // }}} + default: begin end // Input registers + endcase + end + + if (i_reset) + r_gpio[NOUT-1:0] <= DEFAULT_OUTPUT; + if (NOUT < 32) + r_gpio[31:((NOUT < 32) ? NOUT : 31)] <= 0; + end + + assign o_gpio = r_gpio[NOUT-1:0]; + // }}} + + // i_gpio -> ck_gpio, $changed(i_gpio) -> ck_toggled, r_mask + // {{{ + generate if (NIN > 0) + begin : INPUT_HANDLING + // {{{ + // Poss interrupts: Toggle, Rise, Fall + // Only toggle is implemented here + reg [NIN-1:0] last_gpio, qq_gpio, q_gpio, toggled, + r_mask; + wire [31:0] wstrb_mask; + reg r_int; + integer ik; + + // r_int + // {{{ + initial r_int = 0; + always @(posedge S_AXI_ACLK) + if (i_reset) + r_int <= 0; + else + r_int <= |(r_mask & toggled); + // }}} + + // Two clock CDC: last_gpio, qq_gpio, q_gpio + // {{{ + initial { last_gpio, qq_gpio, q_gpio } = 0; + always @(posedge S_AXI_ACLK) + if (i_reset) + { last_gpio, qq_gpio, q_gpio } <= 0; + else + { last_gpio, qq_gpio, q_gpio } + <= { qq_gpio, q_gpio, i_gpio }; + // }}} + + // Toggled + // {{{ + initial toggled = 0; + always @(posedge S_AXI_ACLK) + if (i_reset) + toggled <= 0; + else begin + for(ik=0; ik<NIN; ik=ik+1) + begin + if (axil_write_ready && awskd_addr == 3'b101 + && wskd_strb[ik/8] && wskd_data[ik]) + toggled[ik] <= 1'b0; + if (last_gpio[ik] ^ qq_gpio[ik]) + toggled[ik] <= 1'b1; + end + end + // }}} + + // r_mask + // {{{ + assign wstrb_mask = apply_wstrb(w_mask, wskd_data, wskd_strb); + + initial r_mask = 0; + always @(posedge S_AXI_ACLK) + if (i_reset) + r_mask <= 0; + else if (axil_write_ready && awskd_addr == 3'b110) + r_mask <= wstrb_mask[NIN-1:0]; + // }}} + + assign ck_gpio = { {(32-NIN){1'b0}}, qq_gpio }; + assign ck_toggled = { {(32-NIN){1'b0}}, toggled }; + assign w_mask = { {(32-NIN){1'b0}}, r_mask }; + assign int_toggled = { {(32-NIN){1'b0}}, (r_mask & toggled) }; + assign o_int = r_int; + + // Make Verilator happy + // {{{ + // Verilator lint_off UNUSED + wire unused_inputs; + assign unused_inputs = &{ 1'b0, wstrb_mask[31:NIN] }; + // Verilator lint_on UNUSED + // }}} + // }}} + end else begin : NO_INPUTS + // {{{ + assign ck_gpio = 32'h0; + assign ck_toggled = 32'h0; + assign w_mask = 32'h0; + assign int_toggled = 32'h0; + assign o_int = 1'b0; + + // Make Verilator happy + // {{{ + // Verilator lint_off UNUSED + wire unused_inputs; + assign unused_inputs = &{ 1'b0, i_gpio }; + // Verilator lint_on UNUSED + // }}} + // }}} + end endgenerate + // }}} + + // axil_read_data + // {{{ + 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({ ((NIN>0)&& arskd_addr[2]), arskd_addr[1:0] }) + 3'b0??: axil_read_data[NOUT-1:0] <= r_gpio[NOUT-1:0]; + ADDR_INDATA: axil_read_data <= ck_gpio; + ADDR_CHANGED: axil_read_data <= ck_toggled; + ADDR_MASK: axil_read_data <= w_mask; + ADDR_INT: axil_read_data <= int_toggled; + endcase + + if (OPT_LOWPOWER && !axil_read_ready) + axil_read_data <= 0; + end + // }}} + + function [C_AXI_DATA_WIDTH-1:0] apply_wstrb; + // {{{ + input [C_AXI_DATA_WIDTH-1:0] prior_data; + input [C_AXI_DATA_WIDTH-1:0] new_data; + input [C_AXI_DATA_WIDTH/8-1:0] wstrb; + + integer k; + for(k=0; k<C_AXI_DATA_WIDTH/8; k=k+1) + begin + apply_wstrb[k*8 +: 8] + = wstrb[k] ? new_data[k*8 +: 8] : prior_data[k*8 +: 8]; + end + endfunction + // }}} + // }}} + + // 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] }; + // Verilator lint_on UNUSED + // }}} +//////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +// +// Formal properties +// {{{ +//////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +`ifdef FORMAL + //////////////////////////////////////////////////////////////////////// + // + // 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(3), + .F_AXI_MAXDELAY(3), + .F_AXI_MAXRSTALL(5), + .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 @(*) + if (OPT_SKIDBUFFER) + 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 else begin + assert(faxil_wr_outstanding == (S_AXI_BVALID ? 1:0)); + assert(faxil_awr_outstanding == faxil_wr_outstanding); + + assert(faxil_rd_outstanding == (S_AXI_RVALID ? 1:0)); + 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); + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Register return checking + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // +`define CHECK_REGISTERS +`ifdef CHECK_REGISTERS + (* anyconst *) reg [$clog2(NOUT)-1:0] f_obit; + + always @(*) + assume(f_obit < NOUT); + + // Verify o_gpio + // {{{ + always @(posedge S_AXI_ACLK) + if ($past(i_reset) || i_reset) + begin + if ($past(i_reset)) + assert(o_gpio[f_obit] == DEFAULT_OUTPUT[f_obit]); + end else if ($past(axil_write_ready && wskd_strb[f_obit/8])) + begin + case($past(awskd_addr[2:0])) + 3'b000: assert(o_gpio[f_obit] == $past(wskd_data[f_obit])); + 3'b001: assert(o_gpio[f_obit] == $past(o_gpio[f_obit] || wskd_data[f_obit])); + 3'b010: assert(o_gpio[f_obit] == $past(o_gpio[f_obit] && !wskd_data[f_obit])); + 3'b011: assert(o_gpio[f_obit] == $past(o_gpio[f_obit] ^ wskd_data[f_obit])); + default: begin end + endcase + end + + faxil_register #( + // {{{ + .AW(C_AXI_ADDR_WIDTH), + .DW(C_AXI_DATA_WIDTH), + .ADDR({ 3'b000, {(ADDRLSB){1'b0}} }), + .MASK({(C_AXI_DATA_WIDTH){1'b0}}) + // }}} + ) foutputs ( + // {{{ + .S_AXI_ACLK(S_AXI_ACLK), + .S_AXI_ARESETN(S_AXI_ARESETN), + .S_AXIL_AWW(axil_write_ready), + .S_AXIL_AWADDR({ awskd_addr[2], {(ADDRLSB+2){1'b0}} }), + .S_AXIL_WDATA(wskd_data), + .S_AXIL_WSTRB(wskd_strb), + .S_AXIL_BVALID(S_AXI_BVALID), + .S_AXIL_AR(axil_read_ready), + .S_AXIL_ARADDR({ arskd_addr[2], {(ADDRLSB+2){1'b0}} }), + .S_AXIL_RVALID(S_AXI_RVALID), + .S_AXIL_RDATA(S_AXI_RDATA), + .i_register(o_gpio) + // }}} + ); + + // }}} + + generate if (NIN > 0) + begin : CHECK_INPUT + (* anyconst *) reg [$clog2(NIN)-1:0] f_ibit; + + always @(*) + assume(f_ibit < NIN); + + always @(posedge S_AXI_ACLK) + if ($past(i_reset) || i_reset) + begin + if ($past(i_reset)) + assert(!ck_gpio[f_ibit]); + end else begin + if (!$past(i_reset, 2) + && $past(ck_gpio[f_ibit]) != $past(ck_gpio[f_ibit],2)) + assert(ck_toggled[f_ibit]); + else if ($past(axil_write_ready + && awskd_addr == ADDR_CHANGED + && wskd_strb[f_ibit/8] + && wskd_data[f_ibit])) + assert(!ck_toggled[f_ibit]); + end + + faxil_register #( + // {{{ + .AW(C_AXI_ADDR_WIDTH), + .DW(C_AXI_DATA_WIDTH), + .ADDR({ ADDR_INDATA, {(ADDRLSB){1'b0}} }), + .MASK({(C_AXI_DATA_WIDTH){1'b0}}) + // }}} + ) finputs ( + // {{{ + .S_AXI_ACLK(S_AXI_ACLK), + .S_AXI_ARESETN(S_AXI_ARESETN), + .S_AXIL_AWW(axil_write_ready), + .S_AXIL_AWADDR({ awskd_addr, {(ADDRLSB){1'b0}} }), + .S_AXIL_WDATA(wskd_data), + .S_AXIL_WSTRB(wskd_strb), + .S_AXIL_BVALID(S_AXI_BVALID), + .S_AXIL_AR(axil_read_ready), + .S_AXIL_ARADDR({ arskd_addr, {(ADDRLSB){1'b0}} }), + .S_AXIL_RVALID(S_AXI_RVALID), + .S_AXIL_RDATA(S_AXI_RDATA), + .i_register(ck_gpio) + // }}} + ); + + faxil_register #( + // {{{ + .AW(C_AXI_ADDR_WIDTH), + .DW(C_AXI_DATA_WIDTH), + .ADDR({ ADDR_CHANGED, {(ADDRLSB){1'b0}} }), + .MASK({(C_AXI_DATA_WIDTH){1'b0}}) + // }}} + ) ftoggled ( + // {{{ + .S_AXI_ACLK(S_AXI_ACLK), + .S_AXI_ARESETN(S_AXI_ARESETN), + .S_AXIL_AWW(axil_write_ready), + .S_AXIL_AWADDR({ awskd_addr, {(ADDRLSB){1'b0}} }), + .S_AXIL_WDATA(wskd_data), + .S_AXIL_WSTRB(wskd_strb), + .S_AXIL_BVALID(S_AXI_BVALID), + .S_AXIL_AR(axil_read_ready), + .S_AXIL_ARADDR({ arskd_addr, {(ADDRLSB){1'b0}} }), + .S_AXIL_RVALID(S_AXI_RVALID), + .S_AXIL_RDATA(S_AXI_RDATA), + .i_register(ck_toggled) + // }}} + ); + + faxil_register #( + // {{{ + .AW(C_AXI_ADDR_WIDTH), + .DW(C_AXI_DATA_WIDTH), + .ADDR({ ADDR_MASK, {(ADDRLSB){1'b0}} }), + .MASK({ {(C_AXI_DATA_WIDTH-NIN){1'b0}}, {(NIN){1'b1}} }) + // }}} + ) fmask ( + // {{{ + .S_AXI_ACLK(S_AXI_ACLK), + .S_AXI_ARESETN(S_AXI_ARESETN), + .S_AXIL_AWW(axil_write_ready), + .S_AXIL_AWADDR({ awskd_addr, {(ADDRLSB){1'b0}} }), + .S_AXIL_WDATA(wskd_data), + .S_AXIL_WSTRB(wskd_strb), + .S_AXIL_BVALID(S_AXI_BVALID), + .S_AXIL_AR(axil_read_ready), + .S_AXIL_ARADDR({ arskd_addr, {(ADDRLSB){1'b0}} }), + .S_AXIL_RVALID(S_AXI_RVALID), + .S_AXIL_RDATA(S_AXI_RDATA), + .i_register(w_mask) + // }}} + ); + end endgenerate +`endif + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Induction checks + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Cover checks + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + + always @(posedge S_AXI_ACLK) + if (!i_reset) + cover(o_int); + + always @(posedge S_AXI_ACLK) + if (!i_reset) + cover($fell(o_int)); + + // }}} +`endif +// }}} +endmodule |