////////////////////////////////////////////////////////////////////////////////
//
// Filename: 	axisgfsm.v
// {{{
// Project:	WB2AXIPSP: bus bridges and other odds and ends
//
// Purpose:	Scripts an AXI DMA via in-memory tables: reads from the tables,
//		commands the DMA.
//
// Registers:
//
//	0. Control
//		8b	KEY
//			3'b PROT
//			4'b QOS
//		1b	Abort: Either aborting or aborted
//		1b	Err: Ended on an error
//		1b	Busy
//		1b	Interrupt Enable
//		1b	Interrupt Set
//		1b	Start
//	1. Reserved
//	2-3. First table entry address
//		(Current) table entry address on read, if in progress
// (Optional)
//	4-5. Current read address
//	6-7. Current write address
//	1.   Remaining amount to be written (this entry)
//
// Table format:
//	Table entries either consist of five 32-bit words, or three 32-bit
//	words, depending upon the size of the address bus.
//
//	Address bus > 30 bits: five 32-bit words
//	0-1:	64b: { 2'bflags, 62'b SOURCE ADDRESS (bytes) }
//			00: Continue after this to next
//			01: Last item in chain
//			10: Skip this address
//			11: Jump to new address
//	2-3:	64b: { int_en, 1'b0,  DESTINATION ADDRESS (bytes) }
//	4:	32b Transfer length (in bytes)
//
//	Address bus <= 30 bits: three 32-bit words
//	0:	32b: { 2'bflags, 30'b SOURCE ADDRESS (bytes) }
//	1:	32b: { int_en, 1'b0, 30'b DESTINATION ADDRESS (bytes) }
//	2:	32b LENGTH (in bytes)
//
//
// Creator:	Dan Gisselquist, Ph.D.
//		Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
// }}}
// Copyright (C) 2020, 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
// `define			AXI3
// }}}
module	axisgfsm #(
		// {{{
		parameter	C_AXI_ADDR_WIDTH = 30,
		parameter	C_AXI_DATA_WIDTH = 32,
		localparam DMAC_ADDR_WIDTH = 5,
		localparam DMAC_DATA_WIDTH = 32,
		//
		// The "ABORT_KEY" is a byte that, if written to the control
		// word while the core is running, will cause the data transfer
		// to be aborted.
		parameter	[7:0]			ABORT_KEY  = 8'h6d
		// }}}
	) (
		// {{{
		input	wire	S_AXI_ACLK,
		input	wire	S_AXI_ARESETN,
		//
		// The control interface
		// {{{
		input	wire				i_start, i_abort,
		input	wire	[C_AXI_ADDR_WIDTH-1:0]	i_tbl_addr,
		input	wire	[3:0]			i_qos,
		input	wire	[2:0]			i_prot,
		output	reg				o_busy,
		output	reg				o_done,
		output	reg				o_int,
		output	reg				o_err,
		output	reg	[C_AXI_ADDR_WIDTH-1:0]	o_tbl_addr,
		// }}}
		//
		// The prefetch interface
		// {{{
		output	reg				o_new_pc,
		output	reg				o_pf_clear_cache,
		output	reg				o_pf_ready,
		output	reg	[C_AXI_ADDR_WIDTH-1:0]	o_pf_pc,
		input	wire				i_pf_valid,
		input	wire	[31:0]			i_pf_insn,
		input	wire	[C_AXI_ADDR_WIDTH-1:0]	i_pf_pc,
		input	wire				i_pf_illegal,
		// }}}
		//
		// The DMA submodule's AXI4-lite control interface
		// {{{
		output	reg				o_dmac_wvalid,
		input	wire				i_dmac_wready,
		output	reg [DMAC_ADDR_WIDTH-1:0]	o_dmac_waddr,
		output	reg [DMAC_DATA_WIDTH-1:0]	o_dmac_wdata,
		output	reg [DMAC_DATA_WIDTH/8-1:0]	o_dmac_wstrb,
		input	wire [DMAC_DATA_WIDTH-1:0]	i_dmac_rdata,
		input	wire				i_dma_complete
		// }}}
		// }}}
	);

	// Local parameter definitions
	// {{{

	// Scatter gather state machine states
	// {{{
	// States:
	// - 0. IDLE (nothing going on, waiting for a new program counter)
	//	Enter on completion, reset, or (abort and DMA complete)
	// - 1. READ_LOSRC -> DMA
	// - 2. READ_HISRC -> DMA (Optional)
	//	((Skip || JUMP) ->READ_LOSRC)
	// - 3. READ_LODST -> DMA
	// - 4. READ_HIDST -> DMA (Optional)
	// - 5. READ_LEN   -> DMA
	// - 6. READ_FLAGS -> SETS -> START DMA
	// - 7. Wait on DMA
	//	(Set interrupt if INT complete)
	//	(If last, go to idle, else jump to #1)
	//	(Set LAST on abort)
	//
	localparam [2:0]	SG_IDLE    = 3'h0,
				SG_SRCHALF = 3'h1,
				SG_SRCADDR = 3'h2,
				SG_DSTHALF = 3'h3,
				SG_DSTADDR = 3'h4,
				SG_LENGTH  = 3'h5,
				SG_CONTROL = 3'h6,
				SG_WAIT    = 3'h7;
	// }}}

	// DMA device internal addresses
	// {{{
	localparam [4:0]	DMA_CONTROL= 5'b00000,
				DMA_UNUSED = 5'b00100,
				DMA_SRCLO  = 5'b01000,
				DMA_SRCHI  = 5'b01100,
				DMA_DSTLO  = 5'b10000,
				DMA_DSTHI  = 5'b10100,
				DMA_LENLO  = 5'b11000,
				DMA_LENHI  = 5'b11100;
	// }}}

	localparam [C_AXI_ADDR_WIDTH-1:0] TBL_SIZE
				= (C_AXI_ADDR_WIDTH <= 30) ? (4*3) : (4*5);

	// }}}

	// Register/net declarations
	// {{{
	reg		tbl_last, tbl_int_enable;
	reg	[2:0]	sgstate;
	reg		dma_err, dma_abort, dma_done, dma_busy;
	reg	[59:0]	r_pf_pc;
	// }}}

	////////////////////////////////////////////////////////////////////////
	//
	// FSM Control states
	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	//

	// o_pf_ready
	// {{{
	always @(*)
	begin
		case(sgstate)
		SG_IDLE:	o_pf_ready = 1'b0;
		SG_SRCHALF:	o_pf_ready = (!o_dmac_wvalid || i_dmac_wready);
		SG_SRCADDR:	o_pf_ready = (!o_dmac_wvalid || i_dmac_wready);
		SG_DSTHALF:	o_pf_ready = (!o_dmac_wvalid || i_dmac_wready);
		SG_DSTADDR:	o_pf_ready = (!o_dmac_wvalid || i_dmac_wready);
		SG_LENGTH:	o_pf_ready = (!o_dmac_wvalid || i_dmac_wready);
		SG_CONTROL:	o_pf_ready = 1'b0;
		SG_WAIT:	o_pf_ready = 1'b0;
		endcase

		if (!o_busy || o_pf_clear_cache || o_new_pc)
			o_pf_ready = 0;
	end
	// }}}

	// w_int
	// {{{
	always @(*)
	begin
		o_int = 1'b0;

		if (sgstate == SG_WAIT && i_dma_complete
					&& (tbl_last || tbl_int_enable))
			o_int = 1'b1;
		if (i_pf_valid && o_pf_ready && i_pf_illegal)
			o_int = 1'b1;
	end
	// }}}

	// Returns from the DMA controller (one clock later)
	// {{{
	always @(*)
	begin
		dma_err   = i_dmac_rdata[4];
		dma_abort = i_dmac_rdata[3];
		dma_done  = i_dmac_rdata[1];
		dma_busy  = i_dmac_rdata[0];
	end
	// }}}

	// The GIANT FSM itself
	// new_pc, pf_clear_cache, dmac_wvalid, dmac_waddr, dmac_wdata,
	// dmac_wstrb, ipc,
	// {{{
	initial	r_pf_pc  = 0;
	initial	sgstate  = SG_IDLE;
	initial	o_new_pc = 1'b0;
	initial	o_busy   = 1'b0;
	initial	o_done   = 1'b0;
	initial	o_err    = 1'b0;
	initial	o_dmac_wvalid = 1'b0;
	always @(posedge S_AXI_ACLK)
	begin
		// Auto-cleared values
		// {{{
		o_new_pc <= 1'b0;
		o_pf_clear_cache <= 1'b0;
		if (i_dmac_wready)
			o_dmac_wvalid <= 1'b0;
		if (!o_dmac_wvalid || i_dmac_wready)
			o_dmac_wstrb <= 4'hf;
		o_done <= 1'b0;
		o_err  <= 1'b0;
		// }}}

		case(sgstate)
		SG_IDLE: // IDLE -- waiting for start
			// {{{
			begin
			r_pf_pc[C_AXI_ADDR_WIDTH-1:0] <= i_tbl_addr;
			if (i_start)
			begin
				o_new_pc <= 1'b1;
				if (C_AXI_ADDR_WIDTH > 30)
					sgstate <= SG_SRCHALF;
				else
					sgstate <= SG_SRCADDR;
				o_busy <= 1'b1;
			end else begin
				o_new_pc <= 1'b0;
				o_pf_clear_cache <= 1'b1;
				o_busy <= 1'b0;
			end end
			// }}}
		SG_SRCHALF: // Get the first source address
			// {{{
			if (i_pf_valid && (!o_dmac_wvalid || i_dmac_wready))
			begin
			o_dmac_wvalid <= 1'b1;
			o_dmac_waddr  <= DMA_SRCLO;
			o_dmac_wdata  <= i_pf_insn;
			sgstate <= SG_SRCADDR;
			// r_pf_pc[31:0] <= i_pf_insn;
			o_tbl_addr <= i_pf_pc;
			end
			// }}}
		SG_SRCADDR: // Second half of the source address
			// {{{
			if (i_pf_valid && o_pf_ready)
			begin
			o_dmac_wvalid <= i_pf_valid && !i_pf_insn[31];
			o_dmac_waddr  <= (C_AXI_ADDR_WIDTH<=30)
						? DMA_SRCLO : DMA_SRCHI;
			o_dmac_wdata  <= i_pf_insn;
			// r_pf_pc[31:0] <= i_pf_insn;
			if (C_AXI_ADDR_WIDTH <= 30)
			begin
				sgstate <= SG_DSTADDR;
				o_tbl_addr <= i_pf_pc;
				// // r_pf_pc[30-1:0] <= i_pf_insn[30-1:0];
			end else begin
				sgstate <= SG_DSTHALF;
				// r_pf_pc[60-1:30] <= i_pf_insn[30-1:0];
			end

			tbl_last <= 1'b0;
			case(i_pf_insn[31:30])
			2'b00: // Other items still to follow
				tbl_last <= 1'b0;
			2'b01: // Last item in the chain
				tbl_last <= 1'b1;
			2'b10: begin // Skip
				tbl_last <= 1'b0;
				if (C_AXI_ADDR_WIDTH > 30)
					sgstate <= SG_SRCHALF;
				else
					sgstate <= SG_SRCADDR;
				o_new_pc <= 1'b1;
				r_pf_pc[C_AXI_ADDR_WIDTH-1:0]
						<= r_pf_pc[C_AXI_ADDR_WIDTH-1:0] + TBL_SIZE;
				end
			2'b11: begin // Jump
				o_new_pc <= 1'b1;
				// ipc <= // already set from above
				if (C_AXI_ADDR_WIDTH > 30)
					sgstate <= SG_SRCHALF;
				else
					sgstate <= SG_SRCADDR;
				r_pf_pc[C_AXI_ADDR_WIDTH-1:0] <= i_pf_insn[C_AXI_ADDR_WIDTH-1:0];
				end
			endcase
			end
			// }}}
		SG_DSTHALF: // Get the first half of the destination address
			// {{{
			if (i_pf_valid && (!o_dmac_wvalid || i_dmac_wready))
			begin
			o_dmac_wvalid<= 1'b1;
			o_dmac_waddr <= DMA_DSTLO;
			o_dmac_wdata <= i_pf_insn;
			sgstate    <= SG_DSTADDR;
			end
			// }}}
		SG_DSTADDR: // Second half of the destination address
			// {{{
			if (i_pf_valid && (!o_dmac_wvalid || i_dmac_wready))
			begin
			o_dmac_wvalid <= 1'b1;
			o_dmac_waddr  <= (C_AXI_ADDR_WIDTH<=30)
						? DMA_DSTLO : DMA_DSTHI;
			o_dmac_wdata <= { 2'b0, i_pf_insn[29:0] };
			sgstate    <= SG_LENGTH;
			tbl_int_enable <= i_pf_insn[31];
			end
			// }}}
		SG_LENGTH: // The length word
			// {{{
			if (i_pf_valid && (!o_dmac_wvalid || i_dmac_wready))
			begin
			o_dmac_wvalid <= 1'b1;
			o_dmac_waddr  <= DMA_LENLO;
			o_dmac_wdata <= i_pf_insn;
			sgstate    <= SG_CONTROL;
			if (i_pf_insn <= 0)
			begin
				if (tbl_last)
				begin
					sgstate    <= SG_IDLE;
					o_new_pc   <= 1'b0;
				end else begin
					sgstate    <= SG_SRCADDR;
					o_new_pc   <= 1'b1;
				end
			end
			end
			// }}}
		SG_CONTROL: // The control word to get us started
			// {{{
			if (!o_dmac_wvalid || i_dmac_wready)
			begin
			o_dmac_wvalid <= 1'b1;
			o_dmac_waddr  <= DMA_CONTROL;
			o_dmac_wdata <= { 9'h0, i_prot, i_qos,
					11'h0,
					1'h1, // Clear any errors
					1'b1, // Clr abort flag
					1'b1, // Set int enable, int
					1'b1, // Clr any prior interrupt
					1'b1 };
			sgstate    <= SG_WAIT;
			o_tbl_addr <= o_tbl_addr + TBL_SIZE;
			end
			// }}}
		SG_WAIT: // Wait for the DMA transfer to complete
			// {{{
			if (i_dma_complete && !o_dmac_wvalid)
			begin
				// o_int <= int_enable;
				if (tbl_last || (dma_err && !o_busy)
							|| i_pf_illegal)
				begin
					o_pf_clear_cache <= 1'b1;
					sgstate <= SG_IDLE;
					o_busy <= 1'b0;
					o_done <= 1'b1;
					o_err  <= dma_err || dma_abort;
					if (!i_pf_illegal)
						// Halt at the beginning
						// of the TBL
						r_pf_pc[C_AXI_ADDR_WIDTH-1:0] <= o_tbl_addr;
					else
						r_pf_pc[C_AXI_ADDR_WIDTH-1:0] <= i_pf_pc;
				end else if (C_AXI_ADDR_WIDTH > 30)
					sgstate <= SG_SRCHALF;
				else
					sgstate <= SG_SRCADDR;
			end
			// }}}
		endcase

		if (i_pf_valid && i_pf_illegal
			&& sgstate != SG_CONTROL && sgstate != SG_WAIT
			&& !o_new_pc && !o_pf_clear_cache)
		begin
			// {{{
			sgstate <= SG_IDLE;
			o_pf_clear_cache <= 1'b1;
			o_done <= 1'b1;
			o_busy <= 1'b0;
			o_err  <= 1'b1;
			// }}}
		end

		if (i_abort && (!o_dmac_wvalid || i_dmac_wready))
		begin
			// {{{
			o_dmac_wstrb <= 4'h8;
			o_dmac_wdata[31:24] <= ABORT_KEY;
			o_dmac_wvalid <= !dma_abort && (sgstate == SG_WAIT);
			// }}}
			if (!dma_busy)
				sgstate <= SG_IDLE;
		end

		if (!S_AXI_ARESETN)
		begin
			// {{{
			sgstate <= SG_IDLE;
			o_pf_clear_cache <= 1'b1;
			o_new_pc <= 1'b0;
			o_dmac_wvalid <= 1'b0;
			r_pf_pc <= 0;
			o_busy <= 1'b0;
			o_done <= 1'b0;
			o_err  <= 1'b0;
			// }}}
		end

		r_pf_pc[60-1:C_AXI_ADDR_WIDTH] <= 0;
	end

	always @(*)
		o_pf_pc = { r_pf_pc[C_AXI_ADDR_WIDTH-1:2], 2'b00 };
	// }}}

	// }}}

	// Make Verilator happy
	// {{{
	// Verilatar lint_off UNUSED
	wire	unused;
	assign	unused = &{ 1'b0, dma_done, i_dmac_rdata[31:5],
				i_dmac_rdata[2],
				r_pf_pc[59:C_AXI_ADDR_WIDTH] };
	// Verilatar lint_on  UNUSED
	// }}}
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
// Formal properties
// {{{
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
`ifdef	FORMAL
	////////////////////////////////////////////////////////////////////////
	//
	////////////////////////////////////////////////////////////////////////
	//
	localparam	F_LGDEPTH = 4;
	reg	f_past_valid;
	(* anyseq *) reg [TBL_SIZE*8-1:0] f_tblentry;
	reg	[C_AXI_ADDR_WIDTH-1 :0]	f_tbladdr, f_pc;
	(* anyconst *) reg		f_never_abort;
	// (* anyconst *) reg [C_AXI_ADDR_WIDTH-1:0]	f_skip_addr;
	reg				f_tbl_last, f_tbl_skip, f_tbl_jump,
					f_tbl_int_enable;
	reg	[C_AXI_ADDR_WIDTH-1:0]	f_tbl_src;
	reg				f_dma_arvalid, f_dma_arready,
					f_dma_awready;


	initial	f_past_valid = 0;
	always @(posedge S_AXI_ACLK)
		f_past_valid <= 1;

	always @(*)
	if (!f_past_valid)
		assume(!S_AXI_ARESETN);

	always @(*)
	if (i_start)
	begin
		assume(!i_abort);
		assume(i_tbl_addr[1:0] == 2'b00);
	end

	////////////////////////////////////////////////////////////////////////
	//
	// Prefetch interface property checks
	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	//

	// Prefetch properties

	assume property (@(posedge S_AXI_ACLK)
		S_AXI_ARESETN && i_pf_valid && !o_pf_ready
			&& !o_pf_clear_cache && !o_new_pc
		|=> i_pf_valid && $stable({
				i_pf_insn, i_pf_pc, i_pf_illegal }));

	always @(*)
	if (o_new_pc)
		assert(o_pf_pc[1:0] == 2'b00);

	always @(posedge S_AXI_ACLK)
	if (o_new_pc)
		f_pc <= o_pf_pc;
	else if (i_pf_valid && o_pf_ready)
		f_pc <= f_pc + 4;

	always @(*)
	if (i_pf_valid)
		assume(i_pf_pc == f_pc);

	always @(*)
	if (S_AXI_ARESETN && !o_new_pc && !o_pf_clear_cache)
		assert(f_pc[1:0] == 2'b00);

	always @(posedge S_AXI_ACLK)
	if (!f_past_valid || $past(!S_AXI_ARESETN || o_new_pc
				|| o_pf_clear_cache))
		assume(!i_pf_illegal);
	else if (!$rose(i_pf_valid))
		assume(!$rose(i_pf_illegal));
	else
		assume($stable(i_pf_illegal));
	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// AXI-lite interface property checks
	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	//
	reg	[F_LGDEPTH-1:0]	fdma_rd_outstanding, fdma_wr_outstanding,
				fdma_awr_outstanding;
	reg			f_dma_bvalid;

	faxil_master #(
		.C_AXI_DATA_WIDTH(32),
		.C_AXI_ADDR_WIDTH(DMAC_ADDR_WIDTH),
		.F_OPT_BRESP(1'b1),
		.F_OPT_RRESP(1'b0),
		.F_OPT_NO_RESET(1'b1),
		.F_LGDEPTH(F_LGDEPTH)
	) faxi(
		.i_clk(S_AXI_ACLK), .i_axi_reset_n(S_AXI_ARESETN),
		//
		.i_axi_awready(i_dmac_wready),
		.i_axi_awaddr(o_dmac_waddr),
		.i_axi_awcache(4'h0),
		.i_axi_awprot( 3'h0),
		.i_axi_awvalid(o_dmac_wvalid),
		//
		.i_axi_wready(i_dmac_wready),
		.i_axi_wdata( o_dmac_wdata),
		.i_axi_wstrb( o_dmac_wstrb),
		.i_axi_wvalid(o_dmac_wvalid),
		//
		.i_axi_bready(1'b1),
		.i_axi_bresp( 2'b00),
		.i_axi_bvalid(f_dma_bvalid),
		//
		.i_axi_arready(f_dma_arready),
		.i_axi_araddr(DMA_CONTROL),
		.i_axi_arcache(4'h0),
		.i_axi_arprot(3'h0),
		.i_axi_arvalid(f_dma_arvalid),
		//
		.i_axi_rresp(2'b00),
		.i_axi_rvalid(f_dma_arvalid),
		.i_axi_rdata(i_dmac_rdata),
		.i_axi_rready(1'b1),
		//
		.f_axi_rd_outstanding(fdma_rd_outstanding),
		.f_axi_wr_outstanding(fdma_wr_outstanding),
		.f_axi_awr_outstanding(fdma_awr_outstanding)
	);

	initial	f_dma_arvalid = 1'b0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		f_dma_arvalid = 1'b0;
	else
		f_dma_arvalid <= 1'b1;

	always @(*)
		f_dma_arready = 1'b1;

	assert property (@(posedge S_AXI_ACLK)
		!S_AXI_ARESETN
		|=> sgstate == SG_IDLE && !o_dmac_wvalid);


	assert property (@(posedge S_AXI_ACLK)
		S_AXI_ARESETN && o_dmac_wvalid && !i_dmac_wready
		|=> o_dmac_wvalid && $stable({
			o_dmac_waddr, o_dmac_wdata, o_dmac_wstrb }));

	assert property (@(posedge S_AXI_ACLK)
		fdma_wr_outstanding == fdma_awr_outstanding);

	assert property (@(posedge S_AXI_ACLK)
		fdma_wr_outstanding == (f_dma_bvalid ? 1:0));

	initial	f_dma_bvalid = 1'b0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		f_dma_bvalid <= 0;
	else if (o_dmac_wvalid && i_dmac_wready)
		f_dma_bvalid <= 1;
	else
		f_dma_bvalid <= 0;
	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// DMA busy and read interface properties
	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	//

			reg	f_dma_busy;
	(* anyseq *)	reg	f_dma_complete;

	initial	f_dma_busy = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		f_dma_busy <= 0;
	else if (o_dmac_wvalid && i_dmac_wready && o_dmac_waddr == 0
			&& o_dmac_wstrb[0] && o_dmac_wdata[0])
		f_dma_busy <= 1'b1;
	else if (f_dma_busy)
		f_dma_busy <= !f_dma_complete;

	assume property (@(posedge S_AXI_ACLK)
		##1 dma_busy == $past(f_dma_busy));
	assume property (@(posedge S_AXI_ACLK)
		!f_dma_busy |-> !f_dma_complete);

	assume property (@(posedge S_AXI_ACLK)
		##1 i_dma_complete == $past(f_dma_complete));

//	assume property (@(posedge S_AXI_ACLK)
//		dma_busy |=> dma_busy [*0:$]
//		##1 dma_busy && i_dma_complete
//		##1 !dma_busy);

	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// State machine checks
	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	//

	always @(*)
		f_tbl_src = f_tblentry[C_AXI_ADDR_WIDTH-1:0];

	always @(*)
	if (o_new_pc)
	begin
		if (C_AXI_ADDR_WIDTH <= 30)
			assert(sgstate == SG_SRCADDR);
		else
			assert(sgstate == SG_SRCHALF);
	end

	generate if (C_AXI_ADDR_WIDTH > 30)
	begin
		always @(*)
		begin
			f_tbl_last = (f_tblentry[63:62] == 2'b01);
			f_tbl_skip = (f_tblentry[63:62] == 2'b10);
			f_tbl_jump = (f_tblentry[63:62] == 2'b11);
			f_tbl_int_enable = f_tblentry[127];
		end
	end else begin
		always @(*)
		begin
			f_tbl_last = (f_tblentry[31:30] == 2'b01);
			f_tbl_skip = (f_tblentry[31:30] == 2'b10);
			f_tbl_jump = (f_tblentry[31:30] == 2'b11);
			f_tbl_int_enable = f_tblentry[63];
		end
	end endgenerate

	always @(posedge S_AXI_ACLK)
	if (S_AXI_ARESETN
		&& (sgstate != SG_IDLE)
			&&(sgstate != SG_SRCADDR || $stable(sgstate)))
		assume($stable(f_tblentry));

	always @(posedge S_AXI_ACLK)
	if (o_new_pc)
		f_tbladdr <= o_pf_pc;

	assert property (@(posedge S_AXI_ACLK)
		disable iff (!S_AXI_ARESETN)
		sgstate == SG_IDLE && !i_start
		|=> sgstate == SG_IDLE && o_pf_clear_cache);

	generate if (C_AXI_ADDR_WIDTH <= 30)
	begin : SMALL_ADDRESS_SPACE
		// {{{
		reg	[5:0]	f_dma_seq;

		always @(*)
		begin
			assert(sgstate != SG_SRCHALF);
			assert(sgstate != SG_DSTHALF);
		end

		always @(*)
		if (i_pf_valid)
		case(sgstate)
		// SG_IDLE:	begin end
		// SG_SRCHALF:	begin end
		// SG_DSTHALF:	begin end
		// SG_LENGTH:	begin end
		// SG_CONTROL:	begin end
		// SG_WAIT:	begin end
		SG_SRCADDR: assume(i_pf_insn == f_tblentry[31:0]
				&&(i_pf_pc == f_tbladdr));
		SG_DSTADDR: assume(i_pf_insn == f_tblentry[63:32]
				&&(i_pf_pc == f_tbladdr + 4));
		SG_LENGTH: assume(i_pf_insn == f_tblentry[95:64]
				&&(i_pf_pc == f_tbladdr + 8));
		endcase

		assert property (@(posedge S_AXI_ACLK)
			disable iff (!S_AXI_ARESETN)
			sgstate == SG_IDLE && i_start
			|=> o_new_pc && !o_pf_clear_cache
				&& sgstate == SG_SRCADDR
				&& r_pf_pc[C_AXI_ADDR_WIDTH-1:0]
					== $past(i_tbl_addr));

		initial	f_dma_seq = 0;
		always @(posedge S_AXI_ACLK)
		if (!S_AXI_ARESETN || i_abort)
			f_dma_seq <= 0;
		else begin

			// SG_SRCADDR, or entering SG_SRCADDR
			// {{{
			if ((f_dma_seq == 0)&&(i_start))
				f_dma_seq <= 1;

			if (f_dma_seq[0] || o_new_pc)
			begin
				assert(sgstate == SG_SRCADDR);
				assert(!o_dmac_wvalid);
				assert(!dma_busy);
				f_dma_seq <= 1;
				if (i_pf_valid && o_pf_ready)
				begin
					f_dma_seq <= 2;

					if (f_tbl_jump || f_tbl_skip)
						f_dma_seq <= 1;
				end

				if (!o_new_pc)
				begin
					assert(o_pf_pc == f_tbladdr);
					assert(f_pc == o_pf_pc);
				end

				if ($past(sgstate == SG_SRCADDR
					&& i_pf_valid && o_pf_ready))
				begin
					// Jump or skip

					assert(o_new_pc);
					// Check the jump address
					// if ($past(i_pf_insn[31:30] == 2'b11))
					if ($past(f_tbl_jump))
						assert(o_pf_pc == { $past(i_pf_insn[C_AXI_ADDR_WIDTH-1:2]), 2'b00 });
					else // Skip
						assert(o_pf_pc == $past(f_tbladdr + TBL_SIZE));
				end
			end
			// }}}

			// SG_DSTADDR
			// {{{
			if (f_dma_seq[1])
			begin
				assert(sgstate == SG_DSTADDR);
				assert(tbl_last == f_tbl_last);
				assert(o_tbl_addr == f_tbladdr);
				if ($rose(f_dma_seq[1]))
					assert(o_dmac_wvalid);
				assert(o_dmac_waddr == DMA_SRCLO);
				assert(o_dmac_wdata == f_tblentry[31:0]);
				assert(&o_dmac_wstrb);
				assert(!dma_busy);
				assert(o_pf_pc == f_tbladdr);
				// assert(f_pc == o_pf_pc + 4);
				f_dma_seq <= 2;
				if (i_pf_valid && o_pf_ready)
					f_dma_seq <= 4;
			end
			// }}}

			// SG_LENGTH
			// {{{
			if (f_dma_seq[2])
			begin
				assert(sgstate == SG_LENGTH);
				assert(tbl_last == f_tbl_last);
				assert(tbl_int_enable == f_tbl_int_enable);
				assert(o_tbl_addr == f_tbladdr);
				if ($rose(f_dma_seq[2]))
					assert(o_dmac_wvalid);
				assert(o_dmac_waddr == DMA_DSTLO);
				assert(o_dmac_wdata == { 2'b00, f_tblentry[61:32] });
				assert(&o_dmac_wstrb);
				assert(!dma_busy);
				assert(o_pf_pc == f_tbladdr);
				// assert(f_pc == o_pf_pc + 8);
				f_dma_seq <= 4;
				if (i_pf_valid && o_pf_ready)
					f_dma_seq <= 8;
			end
			// }}}

			// SG_CONTROL
			// {{{
			if (f_dma_seq[3])
			begin
				assert(sgstate == SG_CONTROL);
				assert(tbl_last == f_tbl_last);
				assert(o_tbl_addr == f_tbladdr);
				assert(o_dmac_wvalid);
				assert(o_dmac_waddr == DMA_LENLO);
				assert(o_dmac_wdata == f_tblentry[95:64]);
				assert(&o_dmac_wstrb);
				assert(!dma_busy);
				assert(o_pf_pc == f_tbladdr);
				// assert(f_pc == o_pf_pc);
				f_dma_seq <= 8;
				if (i_dmac_wready)
					f_dma_seq <= 16;
			end
			// }}}

			// SG_WAIT && o_dmac_wvalid
			// {{{
			if (f_dma_seq[4])
			begin
				assert(sgstate == SG_WAIT);
				assert(tbl_last == f_tbl_last);
				assert(o_tbl_addr == f_tbladdr + TBL_SIZE);
				assert(o_dmac_wvalid);
				assert(o_dmac_waddr == DMA_CONTROL);
				assert(o_dmac_wdata[15:0] == 16'h1f);
				assert(&o_dmac_wstrb);
				assert(!dma_busy);
				assert(o_pf_pc == f_tbladdr);
				// assert(f_pc == o_pf_pc);
				f_dma_seq <= 16;
				if (o_dmac_wvalid && i_dmac_wready)
					f_dma_seq <= 32;
			end
			// }}}

			// SG_WAIT && !o_dmac_wvalid
			// {{{
			if (f_dma_seq[5])
			begin
				assert(sgstate == SG_WAIT);
				assert(!o_dmac_wvalid);
				assert(tbl_last == f_tbl_last);
				assert(o_tbl_addr == f_tbladdr + TBL_SIZE);
				assert(!o_dmac_wvalid);
				assert(o_dmac_waddr == DMA_CONTROL);
				// assert(o_dmac_wdata == f_tblentry[95:64]);
				assert(&o_dmac_wstrb);
				f_dma_seq <= 32;
				assert(o_pf_pc == f_tbladdr);
				// assert(f_pc == o_pf_pc);
				if (i_dma_complete)
					f_dma_seq <= 0;
			end
			// }}}

			// pf_illegal
			// {{{
			if (f_dma_seq[2:0] && i_pf_illegal)
				f_dma_seq <= 0;
			// }}}

			// i_abort
			// if (f_dma_seq[2:0] && i_abort
			//		&& (!o_dmac_wvalid || i_dmac_wready))
			//	f_dma_seq <= 0;
		end

		always @(*)
		if (f_dma_seq == 0)
		begin
			assert(sgstate == SG_IDLE);
			assert(!o_new_pc);
			assert(!o_dmac_wvalid);
		end

		always @(posedge S_AXI_ACLK)
		if (!f_past_valid || $past(!S_AXI_ARESETN))
		begin end
		else if (sgstate == 0)
		begin
			assert(o_pf_clear_cache);
			assert(!dma_busy);
		end

		cover property (@(posedge S_AXI_ACLK)
			f_dma_seq[5]);

		cover property (@(posedge S_AXI_ACLK)
			disable iff (!S_AXI_ARESETN || i_abort || i_pf_illegal
				|| dma_err)
			f_dma_seq[0] ##1 1[*0:$] ##1 f_dma_seq[5]
			##1 f_dma_seq == 0);	// !!!

		cover property (@(posedge S_AXI_ACLK)
			f_dma_seq[5] && !tbl_last && f_dma_busy && dma_busy);

		cover property (@(posedge S_AXI_ACLK)
			f_dma_seq[5] && tbl_last && f_dma_busy && dma_busy);

		cover property (@(posedge S_AXI_ACLK)
			f_dma_seq[5] ##2 f_dma_seq[0]);	// !!!

		cover property (@(posedge S_AXI_ACLK)
			f_dma_seq[5] && tbl_last && i_dma_complete);	// !!!

		cover property (@(posedge S_AXI_ACLK)
			f_dma_seq[5] && i_dma_complete);	// !!!
		// }}}
	end else begin : BIG_ADDR
	end endgenerate

	always @(*)
		assert(o_busy == (sgstate != SG_IDLE));

	always @(*)
	if (o_busy)
	begin
		assert(!o_done);
		assert(!o_err);
	end

	assert property (@(posedge S_AXI_ACLK)
		S_AXI_ARESETN && o_busy ##1 !o_busy |-> o_done);

//	assert property (@(posedge S_AXI_ACLK)
//		!o_done |-> !o_int);

	assert property (@(posedge S_AXI_ACLK)
		!o_done && !o_busy |-> !o_err);

	always @(*)
	if (o_pf_ready)
		assert(!o_dmac_wvalid || i_dmac_wready);

	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// Cover checks
	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	//

	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// Careless assumptions (i.e. constraints)
	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	//

	always @(*)
		assume(!i_abort);

	always @(*)
	if (sgstate == SG_SRCHALF)
		assume(!i_abort);
	// }}}
`endif
// }}}
endmodule