blk0wrapper.sby

[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

blk0wrapper.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