Created
June 7, 2021 14:37
-
-
Save ZipCPU/05c2182cd833a243709db537b7953821 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
[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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// `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