package dut_mem_pkg;
	typedef logic[31:0] width_t;    
endpackage: dut_mem_pkg

module dut_mem #(WR_PARAM =1, RD_PARAM=1, MEM_DEPTH_PARAM=1024) (
		input logic clk, rd, wr, rst_n, 
		input logic[31:0] address,
		output logic hold,
		inout logic[31:0] data);
	import dut_mem_pkg::*;
	//typedef enum {hold, READY} rdy_e;
	width_t mem[0:MEM_DEPTH_PARAM-1];
	logic[2:0] rd_ct, wr_ct; // rd, wr counts 
	logic wr_enb; 
	// rdy_e rdy; 
	default disable iff !rst_n;
	default clocking cb_ck1 @ (posedge clk);  endclocking 

	// RD_PARAM==0, WR_PARAM==0
//	ap_read0hold: assert property(
//		rd && RD_PARAM==0 |-> data==mem[address]);

//	property p_write0hold;
//		logic[31:0] v_data, v_address;
//		(wr && WR_PARAM==0, v_data=data, v_address=address) |-> 
//		##1 mem[v_address]==v_data;  // check into the memory
//	endproperty : p_write0hold
//	ap_write0hold: assert property(p_write0hold);
	//--------------------
	// RD_PARAM > 0 , WR_PARAM > 0
	generate 
		if(RD_PARAM > 0) begin 
			ap_readhold: assert property(@ (negedge clk)
					rd && hold==1'b0 |-> 
					@ (posedge clk) hold[*1:RD_PARAM] 
				##1   data==mem[address]);

			property p_write;
				logic[31:0] v_data, v_address;
				@ (negedge clk)
					(wr && hold==1'b0, v_data=data, v_address=address) 
					|-> @ (posedge clk) hold[*1:WR_PARAM] 
					##1 (1, v_data     =data, v_address=address) 
					##1 mem[v_address]==v_data;
			endproperty : p_write
			ap_write: assert property(p_write);
		end
		else begin 
			ap_readhold: assert property(@ (negedge clk)
					rd && hold==1'b0 |-> 
				@ (posedge clk) data==mem[address]);

			property p_write;
				logic[31:0] v_data, v_address;
				@ (negedge clk)
					(wr && hold==1'b0, v_data=data, v_address=address) 
					|-> @ (posedge clk) (1, v_data     =data, v_address=address) 
					##1 mem[v_address]==v_data;
			endproperty : p_write
			ap_write: assert property(p_write);
		end

	endgenerate




	ap_no_wr_rd: assume property(not(wr && rd)); 

	always_ff @ (negedge clk)  begin : aly 
		if(rd && rd_ct==3'b000) rd_ct  <= RD_PARAM; 
		else if(rd_ct != 3'b000) rd_ct <= rd_ct - 1'b1; 
		if(wr && wr_ct==3'b000) wr_ct  <= WR_PARAM; 
		else if(wr_ct != 3'b000) wr_ct <= wr_ct - 1'b1; 

		if(WR_PARAM==3'b0) wr_enb      <= 1'b1; 
		else if(wr_ct==3'b001) wr_enb  <= 1'b1; 
		else wr_enb                    <= 1'b0;
		//if(wr_enb && wr) mem[address]  <=data;

		if(!rst_n) begin 
			rd_ct                          <= 3'b000; 
			wr_ct                          <= 3'b000;
			wr_enb                         <= 1'b0; 
		end
	end  : aly

	always_ff @ (posedge clk)  
		if(wr_enb && wr) mem[address]  <=data;

	always_comb hold   =(rd_ct != 3'b000) || (wr_ct != 3'b000);

	assign data        = rd ? mem[address] : 'Z; 

endmodule :  dut_mem

module top_tb;
	logic clk          =1'b0, rd, wr, rst_n; 
	logic [31:0] address, data1;
	logic hold;
	bit go; 
	wire [31:0] data;
	// dut_mem  #(.RD_PARAM (1), .WR_PARAM(2)) dut_mem1 (.*); 
	dut_mem  #(.RD_PARAM (0), .WR_PARAM(0), .MEM_DEPTH_PARAM(16)) dut_mem0 (.*); 
	initial begin 
		forever begin 
			#8 clk             = !clk; 
			#2 clk             = !clk;
		end
	end
	initial begin
		automatic bit[3:0] v;
		@ (posedge clk) rst_n          <= 1'b0; 
		@ (posedge clk) rst_n          <= 1'b1; 
		for (int i         =0; i<16; i++) begin
			wr                             <= 1'b1;
			rd                             <= 1'b0; 
			address                        <= v; 
			if(!randomize(data1))  $error("randomization failure"); 
			@ (posedge clk);
			wait(hold==1'b0);
			@ (posedge clk);
			v                  = v + 1'b1;
		end
		go                             <= 1'b1; 
	end
	always @ (posedge clk)  begin : aly 
		#1;
		if(go && hold==0)
			if(!randomize(rd, wr, address, data1) 
					with {rd != wr || rd==1'b0 && wr==1'b0;
						address < 5; data1 <64000;})       
				$error("randomization failure"); 
	end  : aly

	assign  data       = rd ? 'Z : data1;

endmodule : top_tb