////////////////////////////////////////////////////////////////////////////////
//
// Filename: 	easyprops
// {{{
// Project:	WB2AXIPSP: bus bridges and other odds and ends
//
// Purpose:	
//
// 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
//
module	easyprops #(
		// {{{
		//
		// 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 = 4,
		localparam	C_AXI_DATA_WIDTH = 32,
		parameter [0:0]	OPT_SKIDBUFFER = 1'b0,
		parameter [0:0]	OPT_LOWPOWER = 0,
		localparam	ADDRLSB = $clog2(C_AXI_DATA_WIDTH)-3
		// }}}
	) (
		// {{{
		input	wire					S_AXI_ACLK,
		input	wire					S_AXI_ARESETN,
		//
		input	wire					S_AXI_AWVALID,
		input	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,
		input	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,
		//
		input	wire					S_AXI_BVALID,
		input	wire					S_AXI_BREADY,
		input	wire	[1:0]				S_AXI_BRESP,
		//
		input	wire					S_AXI_ARVALID,
		input	wire					S_AXI_ARREADY,
		input	wire	[C_AXI_ADDR_WIDTH-1:0]		S_AXI_ARADDR,
		input	wire	[2:0]				S_AXI_ARPROT,
		//
		input	wire					S_AXI_RVALID,
		input	wire					S_AXI_RREADY,
		input	wire	[C_AXI_DATA_WIDTH-1:0]		S_AXI_RDATA,
		input	wire	[1:0]				S_AXI_RRESP,
		// }}}
		// input	wire	i_clk,
		input	wire	[31:0]	r0,
		input	wire	[31:0]	r1,
		input	wire	[31:0]	r2,
		input	wire	[31:0]	r3,
		input	wire	axil_read_ready, axil_write_ready,
		input	wire	[1:0]	awskd_addr, arskd_addr,
		input	wire	[31:0]	wskd_data,
		input	wire	[3:0]	wskd_strb
	);

`ifdef	FORMAL
	////////////////////////////////////////////////////////////////////////
	//
	// Formal properties used in verfiying this core
	//
	////////////////////////////////////////////////////////////////////////
	//
	// {{{
	reg	f_past_valid;
	initial	f_past_valid = 0;
	always @(posedge S_AXI_ACLK)
		f_past_valid <= 1;

	////////////////////////////////////////////////////////////////////////
	//
	// 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(3),
		.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_awcache(4'h0),
		.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_arcache(4'h0),
		.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

	always @(posedge S_AXI_ACLK)
	if (f_past_valid && $past(S_AXI_ARESETN
			&& axil_read_ready))
	begin
		assert(S_AXI_RVALID);
		case($past(arskd_addr))
		0: assert(S_AXI_RDATA == $past(r0));
		1: assert(S_AXI_RDATA == $past(r1));
		2: assert(S_AXI_RDATA == $past(r2));
		3: assert(S_AXI_RDATA == $past(r3));
		endcase
	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);

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

	// While there are already cover properties in the formal property
	// set above, you'll probably still want to cover something
	// application specific here

	// }}}
	// }}}

	////////////////////////////////////////////////////////////////////////
	//
	// Round #1 -- double check writes to registers
	//
	////////////////////////////////////////////////////////////////////////
	//
	//

	(* anyconst *)	reg[3:0]	f_addr;
	reg [7:0]	f_byte, f_rbyte;

	generate if (OPT_SKIDBUFFER)
	begin
		initial	f_byte = 0;
		always @(posedge S_AXI_ACLK)
		if (!S_AXI_ARESETN)
			f_byte <= 0;
		else if (axil_write_ready)
		begin
			if (awskd_addr == f_addr[3:2]
					&& wskd_strb[f_addr[1:0]])
				f_byte <= S_AXI_WDATA >> (8*f_addr[1:0]);
		end

	end else begin
	
		initial	f_byte = 0;
		always @(posedge S_AXI_ACLK)
		if (!S_AXI_ARESETN)
			f_byte <= 0;
		else if (S_AXI_AWVALID && S_AXI_WVALID && S_AXI_AWREADY && S_AXI_WREADY)
		begin
			if (S_AXI_AWADDR[3:2] == f_addr[3:2]
					&& S_AXI_WSTRB[f_addr[1:0]])
				f_byte <= S_AXI_WDATA >> (8*f_addr[1:0]);
		end

	end endgenerate

	always @(*)
	case(f_addr[3:2])
	2'b00: f_rbyte = (r0 >> (8*f_addr[1:0]));
	2'b01: f_rbyte = (r1 >> (8*f_addr[1:0]));
	2'b10: f_rbyte = (r2 >> (8*f_addr[1:0]));
	2'b11: f_rbyte = (r3 >> (8*f_addr[1:0]));
	endcase

	always @(*)
		assert(f_byte == f_rbyte);

	////////////////////////////////////////////////////////////////////////
	//
	// Round #2 -- double check ?WREADY signaling
	//
	////////////////////////////////////////////////////////////////////////
	//
	//

	// ???
`endif
endmodule


module skidprops #(
	parameter	[0:0]	OPT_LOWPOWER = 0,
	parameter	[0:0]	OPT_OUTREG = 1,
	//
	parameter	[0:0]	OPT_PASSTHROUGH = 0,
	parameter		DW = 8
	) (
	input	wire			i_clk, i_reset,
	input	wire			i_valid,
	input	wire			o_ready,
	input	wire	[DW-1:0]	i_data,
	input	wire			o_valid,
	input	wire			i_ready,
	input	wire	[DW-1:0]	o_data,

	input	wire	[DW-1:0]	r_data
	);

	// Reset properties
	property RESET_CLEARS_IVALID;
		@(posedge i_clk) i_reset |=> !i_valid;
	endproperty

	property IDATA_HELD_WHEN_NOT_READY;
		@(posedge i_clk) disable iff (i_reset)
		i_valid && !o_ready |=> i_valid && $stable(i_data);
	endproperty

	assert	property (IDATA_HELD_WHEN_NOT_READY);

	generate if (!OPT_PASSTHROUGH)
	begin

		assert property (@(posedge i_clk)
			OPT_OUTREG && i_reset |=> o_ready && !o_valid);

		assert property (@(posedge i_clk)
			!OPT_OUTREG && i_reset |-> !o_valid);

		// Rule #1:
		//	Once o_valid goes high, the data cannot change until the
		//	clock after i_ready
		assert property (@(posedge i_clk)
			disable iff (i_reset)
			o_valid && !i_ready
			|=> (o_valid && $stable(o_data)));

		// Rule #2:
		//	All incoming data must either go directly to the
		//	output port, or into the skid buffer
		assert property (@(posedge i_clk)
			disable iff (i_reset)
			(i_valid && o_ready
				&& (!OPT_OUTREG || o_valid) && !i_ready)
				|=> (!o_ready && r_data == $past(i_data)));

		// Rule #3:
		//	After the last transaction, o_valid should become idle
		if (!OPT_OUTREG)
		begin

			assert property (@(posedge i_clk)
				disable iff (i_reset)
				i_ready |=> (o_valid == i_valid));

		end else begin

			assert property (@(posedge i_clk)
				disable iff (i_reset)
				i_valid && o_ready |=> o_valid);

			assert property (@(posedge i_clk)
				disable iff (i_reset)
				!i_valid && o_ready && i_ready |=> !o_valid);

		end

		// Rule #4
		//	Same thing, but this time for r_valid
		assert property (@(posedge i_clk)
			!o_ready && i_ready |=> o_ready);


		if (OPT_LOWPOWER)
		begin
			//
			// If OPT_LOWPOWER is set, o_data and r_data both need
			// to be zero any time !o_valid or !r_valid respectively
			assert property (@(posedge i_clk)
				(OPT_OUTREG || !i_reset) && !o_valid |-> o_data == 0);

			assert property (@(posedge i_clk)
				o_ready |-> r_data == 0);

			// else
			//	if OPT_LOWPOWER isn't set, we can lower our
			//	logic count by not forcing these values to zero.
		end

	end endgenerate

endmodule

bind easyaxil easyprops copy (.*);
`ifdef	CHECK_SKID
bind easyaxil.SKIDBUFFER_WRITE.axilawskid skidprops #(.OPT_OUTREG(0), .OPT_LOWPOWER(easyaxil.OPT_LOWPOWER), .DW(2)) copy (.*);
bind easyaxil.SKIDBUFFER_WRITE.axilwskid  skidprops #(.OPT_OUTREG(0), .OPT_LOWPOWER(easyaxil.OPT_LOWPOWER), .DW(36)) copy (.*);
bind easyaxil.SKIDBUFFER_READ.axilarskid  skidprops #(.OPT_OUTREG(0), .OPT_LOWPOWER(easyaxil.OPT_LOWPOWER), .DW(2)) copy (.*);
`endif