Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
[tasks]
prf
cvr
[options]
prf: mode prove
cvr: mode cover
prf: depth 40
cvr: depth 40
[engines]
smtbmc
[script]
read -formal rggen_axi4lite_skid_buffer.v
read -formal rggen_mux.v
read -formal rggen_adapter_common.v
read -formal rggen_register_common.v
read -formal rggen_axi4lite_adapter.v
read -formal rggen_external_register.v
read -formal rggen_indirect_register.v
read -formal rggen_default_register.v
read -formal rggen_bit_field.v
read -formal rggen_bit_field_w01trg.v
read -formal rggen_address_decoder.v
read -formal block_0.v
read -formal blk0wrapper.v
read -formal faxil_slave.v
prep -top blk0wrapper
[files]
../../rggen-verilog-rtl/rggen_axi4lite_skid_buffer.v
../../rggen-verilog-rtl/rggen_adapter_common.v
../../rggen-verilog-rtl/rggen_register_common.v
../../rggen-verilog-rtl/rggen_axi4lite_adapter.v
../../rggen-verilog-rtl/rggen_mux.v
../../rggen-verilog-rtl/rggen_rtl_macros.vh
../../rggen-verilog-rtl/rggen_external_register.v
../../rggen-verilog-rtl/rggen_indirect_register.v
../../rggen-verilog-rtl/rggen_default_register.v
../../rggen-verilog-rtl/rggen_bit_field_w01trg.v
../../rggen-verilog-rtl/rggen_bit_field.v
../../rggen-verilog-rtl/rggen_address_decoder.v
../../rggen-sample-testbench/rtl/axi4lite/block_0.v
blk0wrapper.v
faxil_slave.v
// `include "rggen_rtl_macros.vh"
module blk0wrapper #(
// {{{
parameter ADDRESS_WIDTH = 8,
parameter PRE_DECODE = 0,
parameter [ADDRESS_WIDTH-1:0] BASE_ADDRESS = {ADDRESS_WIDTH{1'b0}},
parameter ERROR_STATUS = 0,
parameter [31:0] DEFAULT_READ_DATA = {32{1'b0}},
parameter ID_WIDTH = 0,
parameter WRITE_FIRST = 1,
parameter ACTUAL_ID_WIDTH = 1
// }}}
)(
// {{{
input i_clk,
input i_rst_n,
// AXI4-lite inputs
// {{{
input i_awvalid,
output wire o_awready,
input [ACTUAL_ID_WIDTH-1:0] i_awid,
input [ADDRESS_WIDTH-1:0] i_awaddr,
input [2:0] i_awprot,
input i_wvalid,
output wire o_wready,
input [31:0] i_wdata,
input [3:0] i_wstrb,
output wire o_bvalid,
input i_bready,
output wire [ACTUAL_ID_WIDTH-1:0] o_bid,
output wire [1:0] o_bresp,
input i_arvalid,
output wire o_arready,
input [ACTUAL_ID_WIDTH-1:0] i_arid,
input [ADDRESS_WIDTH-1:0] i_araddr,
input [2:0] i_arprot,
output wire o_rvalid,
input i_rready,
output wire [ACTUAL_ID_WIDTH-1:0] o_rid,
output wire [1:0] o_rresp,
output wire [32-1:0] o_rdata,
// }}}
// REGISTER outputs
// {{{
output [3:0] o_register_0_bit_field_0,
output [3:0] o_register_0_bit_field_1,
output o_register_0_bit_field_2,
output [1:0] o_register_0_bit_field_3,
output [1:0] o_register_0_bit_field_4,
output [1:0] o_register_0_bit_field_5,
output o_register_1,
input [3:0] i_register_2_bit_field_0,
input [3:0] i_register_2_bit_field_1,
output [3:0] o_register_3_bit_field_0,
output [3:0] o_register_3_bit_field_1,
output [3:0] o_register_3_bit_field_2_trigger,
output [3:0] o_register_3_bit_field_3_trigger,
input [3:0] i_register_4_bit_field_0_set,
output [3:0] o_register_4_bit_field_0,
input [3:0] i_register_4_bit_field_1_set,
output [3:0] o_register_4_bit_field_1,
output [3:0] o_register_4_bit_field_1_unmasked,
input [3:0] i_register_4_bit_field_3_clear,
output [3:0] o_register_4_bit_field_3,
input i_register_5_bit_field_0_clear,
output [1:0] o_register_5_bit_field_0,
output [1:0] o_register_5_bit_field_1,
input i_register_5_bit_field_2_set,
input [1:0] i_register_5_bit_field_2,
output [1:0] o_register_5_bit_field_2,
input [1:0] i_register_5_bit_field_3,
output [1:0] o_register_5_bit_field_3,
input i_register_5_bit_field_4_enable,
output [1:0] o_register_5_bit_field_4,
output [1:0] o_register_5_bit_field_5,
output [1:0] o_register_5_bit_field_6,
input i_register_5_bit_field_7_lock,
output [1:0] o_register_5_bit_field_7,
output [1:0] o_register_5_bit_field_8,
output [1:0] o_register_5_bit_field_9,
input [3:0] i_register_6_bit_field_0_set,
output [3:0] o_register_6_bit_field_0,
input [3:0] i_register_6_bit_field_1_set,
output [3:0] o_register_6_bit_field_1,
output [3:0] o_register_6_bit_field_1_unmasked,
input [3:0] i_register_6_bit_field_3_set,
output [3:0] o_register_6_bit_field_3,
input [3:0] i_register_6_bit_field_4_set,
output [3:0] o_register_6_bit_field_4,
output [3:0] o_register_6_bit_field_4_unmasked,
input [3:0] i_register_6_bit_field_6_clear,
output [3:0] o_register_6_bit_field_6,
input [3:0] i_register_6_bit_field_7_clear,
output [3:0] o_register_6_bit_field_7,
output [3:0] o_register_6_bit_field_8,
output [3:0] o_register_6_bit_field_9,
output [3:0] o_register_7_bit_field_0,
output [3:0] o_register_7_bit_field_1,
output [3:0] o_register_7_bit_field_2,
output [3:0] o_register_7_bit_field_3,
input [3:0] i_register_8_bit_field_0_set,
output [3:0] o_register_8_bit_field_0,
input [3:0] i_register_8_bit_field_1_clear,
output [3:0] o_register_8_bit_field_1,
input [3:0] i_register_8_bit_field_2_set,
output [3:0] o_register_8_bit_field_2,
input [3:0] i_register_8_bit_field_3_clear,
output [3:0] o_register_8_bit_field_3,
output [3:0] o_register_8_bit_field_4,
output [3:0] o_register_8_bit_field_5,
output [63:0] o_register_9_bit_field_0,
output [63:0] o_register_9_bit_field_1,
output [63:0] o_register_9_bit_field_2,
output [255:0] o_register_10_bit_field_0,
output [255:0] o_register_10_bit_field_1,
output o_register_11_bit_field_0,
output o_register_12_bit_field_0,
output o_register_14_valid,
output [1:0] o_register_14_access,
output [7:0] o_register_14_address,
output [31:0] o_register_14_data,
output [3:0] o_register_14_strobe,
input i_register_14_ready,
input [1:0] i_register_14_status,
input [31:0] i_register_14_data
// }}}
// }}}
);
block_0 #(
// {{{
.ADDRESS_WIDTH(ADDRESS_WIDTH),
.PRE_DECODE(PRE_DECODE),
.BASE_ADDRESS(BASE_ADDRESS),
.ERROR_STATUS(ERROR_STATUS),
.DEFAULT_READ_DATA(DEFAULT_READ_DATA),
.ID_WIDTH(ID_WIDTH),
.WRITE_FIRST(WRITE_FIRST)
// }}}
) mut (
// {{{
.i_clk(i_clk),
.i_rst_n(i_rst_n),
// AXI-4 lite signaling
// {{{
.i_awvalid(i_awvalid),
.o_awready(o_awready),
.i_awid(i_awid),
.i_awaddr(i_awaddr),
.i_awprot(i_awprot),
//
.i_wvalid(i_wvalid),
.o_wready(o_wready),
.i_wdata(i_wdata),
.i_wstrb(i_wstrb),
//
.o_bvalid(o_bvalid),
.i_bready(i_bready),
.o_bid(o_bid),
.o_bresp(o_bresp),
//
.i_arvalid(i_arvalid),
.o_arready(o_arready),
.i_arid(i_arid),
.i_araddr(i_araddr),
.i_arprot(i_arprot),
//
.o_rvalid(o_rvalid),
.i_rready(i_rready),
.o_rid(o_rid),
.o_rresp(o_rresp),
.o_rdata(o_rdata),
// }}}
// Register access
// {{{
.o_register_0_bit_field_0(o_register_0_bit_field_0),
.o_register_0_bit_field_1(o_register_0_bit_field_1),
.o_register_0_bit_field_2(o_register_0_bit_field_2),
.o_register_0_bit_field_3(o_register_0_bit_field_3),
.o_register_0_bit_field_4(o_register_0_bit_field_4),
.o_register_0_bit_field_5(o_register_0_bit_field_5),
.o_register_1(o_register_1),
.i_register_2_bit_field_0(i_register_2_bit_field_0),
.i_register_2_bit_field_1(i_register_2_bit_field_1),
.o_register_3_bit_field_0(o_register_3_bit_field_0),
.o_register_3_bit_field_1(o_register_3_bit_field_1),
.o_register_3_bit_field_2_trigger(o_register_3_bit_field_2_trigger),
.o_register_3_bit_field_3_trigger(o_register_3_bit_field_3_trigger),
.i_register_4_bit_field_0_set(i_register_4_bit_field_0_set),
.o_register_4_bit_field_0(o_register_4_bit_field_0),
.i_register_4_bit_field_1_set(i_register_4_bit_field_1_set),
.o_register_4_bit_field_1(o_register_4_bit_field_1),
.o_register_4_bit_field_1_unmasked(o_register_4_bit_field_1_unmasked),
.i_register_4_bit_field_3_clear(i_register_4_bit_field_3_clear),
.o_register_4_bit_field_3(o_register_4_bit_field_3),
.i_register_5_bit_field_0_clear(i_register_5_bit_field_0_clear),
.o_register_5_bit_field_0(o_register_5_bit_field_0),
.o_register_5_bit_field_1(o_register_5_bit_field_1),
.i_register_5_bit_field_2_set(i_register_5_bit_field_2_set),
.i_register_5_bit_field_2(i_register_5_bit_field_2),
.o_register_5_bit_field_2(o_register_5_bit_field_2),
.i_register_5_bit_field_3(i_register_5_bit_field_3),
.o_register_5_bit_field_3(o_register_5_bit_field_3),
.i_register_5_bit_field_4_enable(i_register_5_bit_field_4_enable),
.o_register_5_bit_field_4(o_register_5_bit_field_4),
.o_register_5_bit_field_5(o_register_5_bit_field_5),
.o_register_5_bit_field_6(o_register_5_bit_field_6),
.i_register_5_bit_field_7_lock(i_register_5_bit_field_7_lock),
.o_register_5_bit_field_7(o_register_5_bit_field_7),
.o_register_5_bit_field_8(o_register_5_bit_field_8),
.o_register_5_bit_field_9(o_register_5_bit_field_9),
.i_register_6_bit_field_0_set(i_register_6_bit_field_0_set),
.o_register_6_bit_field_0(o_register_6_bit_field_0),
.i_register_6_bit_field_1_set(i_register_6_bit_field_1_set),
.o_register_6_bit_field_1(o_register_6_bit_field_1),
.o_register_6_bit_field_1_unmasked(o_register_6_bit_field_1_unmasked),
.i_register_6_bit_field_3_set(i_register_6_bit_field_3_set),
.o_register_6_bit_field_3(o_register_6_bit_field_3),
.i_register_6_bit_field_4_set(i_register_6_bit_field_4_set),
.o_register_6_bit_field_4(o_register_6_bit_field_4),
.o_register_6_bit_field_4_unmasked(o_register_6_bit_field_4_unmasked),
.i_register_6_bit_field_6_clear(i_register_6_bit_field_6_clear),
.o_register_6_bit_field_6(o_register_6_bit_field_6),
.i_register_6_bit_field_7_clear(i_register_6_bit_field_7_clear),
.o_register_6_bit_field_7(o_register_6_bit_field_7),
.o_register_6_bit_field_8(o_register_6_bit_field_8),
.o_register_6_bit_field_9(o_register_6_bit_field_9),
.o_register_7_bit_field_0(o_register_7_bit_field_0),
.o_register_7_bit_field_1(o_register_7_bit_field_1),
.o_register_7_bit_field_2(o_register_7_bit_field_2),
.o_register_7_bit_field_3(o_register_7_bit_field_3),
.i_register_8_bit_field_0_set(i_register_8_bit_field_0_set),
.o_register_8_bit_field_0(o_register_8_bit_field_0),
.i_register_8_bit_field_1_clear(i_register_8_bit_field_1_clear),
.o_register_8_bit_field_1(o_register_8_bit_field_1),
.i_register_8_bit_field_2_set(i_register_8_bit_field_2_set),
.o_register_8_bit_field_2(o_register_8_bit_field_2),
.i_register_8_bit_field_3_clear(i_register_8_bit_field_3_clear),
.o_register_8_bit_field_3(o_register_8_bit_field_3),
.o_register_8_bit_field_4(o_register_8_bit_field_4),
.o_register_8_bit_field_5(o_register_8_bit_field_5),
.o_register_9_bit_field_0(o_register_9_bit_field_0),
.o_register_9_bit_field_1(o_register_9_bit_field_1),
.o_register_9_bit_field_2(o_register_9_bit_field_2),
.o_register_10_bit_field_0(o_register_10_bit_field_0),
.o_register_10_bit_field_1(o_register_10_bit_field_1),
.o_register_11_bit_field_0(o_register_11_bit_field_0),
.o_register_12_bit_field_0(o_register_12_bit_field_0),
.o_register_14_valid(o_register_14_valid),
.o_register_14_access(o_register_14_access),
.o_register_14_address(o_register_14_address),
.o_register_14_data(o_register_14_data),
.o_register_14_strobe(o_register_14_strobe),
.i_register_14_ready(i_register_14_ready),
.i_register_14_status(i_register_14_status),
.i_register_14_data(i_register_14_data)
// }}}
// }}}
);
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
// Formal property section
// {{{
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
`ifdef FORMAL
localparam F_LGDEPTH = 4;
wire [F_LGDEPTH-1:0] faxil_rd_outstanding, faxil_wr_outstanding,
faxil_awr_outstanding;
////////////////////////////////////////////////////////////////////////
//
// Bus interface properties
// {{{
////////////////////////////////////////////////////////////////////////
//
//
faxil_slave #(
// {{{
.C_AXI_ADDR_WIDTH(ADDRESS_WIDTH),
.C_AXI_DATA_WIDTH(32),
.F_OPT_COVER_BURST(4),
.F_OPT_INITIAL(1'b0),
.F_LGDEPTH(F_LGDEPTH)
// }}}
) faxil (
// {{{
.i_clk(i_clk),
.i_axi_reset_n(i_rst_n),
// AXI-4 lite signaling
// {{{
.i_axi_awvalid(i_awvalid),
.i_axi_awready(o_awready),
// .i_axi_awid(i_awid),
.i_axi_awaddr(i_awaddr),
.i_axi_awprot(i_awprot),
//
.i_axi_wvalid(i_wvalid),
.i_axi_wready(o_wready),
.i_axi_wdata(i_wdata),
.i_axi_wstrb(i_wstrb),
//
.i_axi_bvalid(o_bvalid),
.i_axi_bready(i_bready),
// .i_axi_bid(o_bid),
.i_axi_bresp(o_bresp),
//
.i_axi_arvalid(i_arvalid),
.i_axi_arready(o_arready),
// .i_axi_arid(i_arid),
.i_axi_araddr(i_araddr),
.i_axi_arprot(i_arprot),
//
.i_axi_rvalid(o_rvalid),
.i_axi_rready(i_rready),
// .i_axi_rid(o_rid),
.i_axi_rresp(o_rresp),
.i_axi_rdata(o_rdata),
// }}}
.f_axi_rd_outstanding(faxil_rd_outstanding),
.f_axi_wr_outstanding(faxil_wr_outstanding),
.f_axi_awr_outstanding(faxil_awr_outstanding)
// }}}
);
// The number of write address and write data transactions should
// match, save for any differences to be found in the skid buffers.
always @(*)
if (i_rst_n)
assert(faxil_wr_outstanding + (o_awready ? 0:1)
== faxil_awr_outstanding + (o_wready ? 0:1));
// Ideally we should have an equality assertion here regarding the total
// number of outstanding read transactions, and another one for the
// total number of outstanding write transactions. Such an assertion
// is *required* in order to pass an induction check. It should look
// like:
//
// assert(faxil_rd_outstanding == /* some formula */);
//
// I'm just not the author of this design, so I don't necessarily know
// how to set the formula correctly. The following assertions pass a
// bounded model check--they're just not (yet) sufficient for passing
// an induction check.
always @(*)
if (i_rst_n)
assert(faxil_rd_outstanding <= (o_arready ? 0:1) + 1);
always @(*)
if (i_rst_n)
assert(faxil_awr_outstanding <= (o_awready ? 0:1) + 1);
// }}}
////////////////////////////////////////////////////////////////////////
//
// Necessary assumptions to avoid known bugs
// {{{
////////////////////////////////////////////////////////////////////////
//
//
//
// BUG #1 in pre_decode:
// {{{
// Doesn't decode axaddr[ADDRESS_WIDTH-1:2], but rather
// [ADDRESS_WIDTH-1:0]. The last address will fail to decode
// if axaddr[1:0] != 0.
//
// This was found via a desk check, rather than anything formal.
//
// }}}
// BUG #2: Read backpressure
// {{{
// This design can't handle back pressure on the R* channel.
//
// always @(posedge i_clk)
// if ($past(o_rvalid && !i_rready))
// assume(o_rvalid);
//
// }}}
// BUG #3: Write backpressure
// {{{
// This design can't handle back pressure on the B* channel.
//
// always @(posedge i_clk)
// if ($past(o_bvalid && !i_bready))
// assume(o_bvalid);
//
// }}}
// AXI-SLAVE PROPERTY LIMITATION #1:
// {{{
// My properties count the amount of clock periods something is waiting, and
// generate a fault if they wait too long. However, these counters are
// (currently) separate--one for reads and one for writes. This design combines
// reads and writes together, so reads have to wait for writes to complete
// and vice versa. This can cause the other channel to starve. Here, we'll
// simply assume this that if the read channel is busy, then the write channel
// must be idle to keep this check from taking place.
//
always @(posedge i_clk)
if (faxil_rd_outstanding > 0)
begin
assume(faxil_wr_outstanding == 0);
assume(faxil_awr_outstanding == 0);
end
// }}}
// AXI-SLAVE PROPERTY LIMITATION #2:
// {{{
// This is basically the same limitation as the one above, except now we're
// assuming that if the write channel is busy then nothing should be ongoing on
// the read channel. Do note, however, that this sort of interferes with our
// assumption in order to correct the read backpressure bug above. As a result,
// this approach might fail when the design's handling of read backpressure
// gets fixed.
//
always @(posedge i_clk)
if ((faxil_wr_outstanding >= 1)
|| (faxil_awr_outstanding >= 1))
begin
assume(faxil_rd_outstanding == (o_rvalid ? 1:0));
end
// }}}
//
// REGISTER 14 ASSUMPTION
// {{{
// I'm not really certain what the protocol for register 14 is supposed to be,
// so let's just assume that register 14 is just never accessed. This isn't
// a great assumption, and should be fixed/changed later, but it works for an
// initial AXI4-lite protocol check--especially since the initial check finds
// the bugs listed above.
//
always @(*)
assume(o_register_14_access == 2'b00);
always @(*)
assume(!i_register_14_ready);
always @(*)
if (i_register_14_ready)
assume(i_register_14_status != 2'b01);
// }}}
// }}}
`endif
// }}}
endmodule
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment