data/full_repos/permissive/211907249/spidergon_node.v
1: b"%Error: data/full_repos/permissive/211907249/spidergon_node.v:200: Cannot find file containing module: 'arbiter'\narbiter #(NUM_OF_PORTS) rr_arb_port_to_cpu\n^~~~~~~\n        ... Looked in:\n             data/full_repos/permissive/211907249,data/full_repos/permissive/211907249/arbiter\n             data/full_repos/permissive/211907249,data/full_repos/permissive/211907249/arbiter.v\n             data/full_repos/permissive/211907249,data/full_repos/permissive/211907249/arbiter.sv\n             arbiter\n             arbiter.v\n             arbiter.sv\n             obj_dir/arbiter\n             obj_dir/arbiter.v\n             obj_dir/arbiter.sv\n%Error: data/full_repos/permissive/211907249/spidergon_node.v:205: Cannot find file containing module: 'oh_to_idx'\noh_to_idx #(NUM_OF_PORTS) port_index (.one_hot(granted_port), .index(granted_port_index));\n^~~~~~~~~\n%Error: data/full_repos/permissive/211907249/spidergon_node.v:312: Cannot find file containing module: 'arbiter'\n  arbiter #(NUM_OF_VIRTUAL_CHANNELS) rr_arb_vc_to_cpu\n  ^~~~~~~\n%Error: data/full_repos/permissive/211907249/spidergon_node.v:320: Cannot find file containing module: 'oh_to_idx'\n  oh_to_idx #(NUM_OF_VIRTUAL_CHANNELS) vc_index \n  ^~~~~~~~~\n%Error: data/full_repos/permissive/211907249/spidergon_node.v:329: Cannot find file containing module: 'router'\n  router #(NUM_OF_NODES) rt \n  ^~~~~~\n%Error: data/full_repos/permissive/211907249/spidergon_node.v:365: Cannot find file containing module: 'arbiter'\n  arbiter #(NUM_OF_VIRTUAL_CHANNELS) rr_arb_data_to_vc\n  ^~~~~~~\n%Error: data/full_repos/permissive/211907249/spidergon_node.v:574: Cannot find file containing module: 'sync_fifo'\n   sync_fifo \n   ^~~~~~~~~\n%Error: data/full_repos/permissive/211907249/spidergon_node.v:776: Cannot find file containing module: 'oh_to_idx'\n  oh_to_idx #(NUM_OF_VIRTUAL_CHANNELS) port_index\n  ^~~~~~~~~\n%Error: Exiting due to 8 error(s)\n"
module spidergon_node
#(
	`ifdef FORMAL	
		parameter NUM_OF_NODES=8, 
		parameter FLIT_DATA_WIDTH=10,
		parameter NODE_BUFFER_WIDTH=2*FLIT_DATA_WIDTH,
	`else
		parameter NUM_OF_NODES=8,
		parameter FLIT_DATA_WIDTH=16,
		parameter NODE_BUFFER_WIDTH=2*FLIT_DATA_WIDTH,
	`endif

	parameter NODE_IDENTIFIER=0,  
	parameter NUM_OF_VIRTUAL_CHANNELS=2
) 
(
	clk, reset, 
	`ifdef FORMAL
	input_flit_type,
	out_port_num,
	`endif
 	flit_data_input_across, flit_data_input_clockwise, flit_data_input_anticlockwise,
 	flit_data_output_across, flit_data_output_clockwise, flit_data_output_anticlockwise, 
	node_data_from_cpu, node_data_to_cpu, data_input,
	flit_data_input_are_valid, flit_data_output_are_valid,
	current_node_is_ready, adjacent_nodes_are_ready,
	current_node_vc_are_almost_full, adjacent_node_vc_are_almost_full,
	current_node_previous_vc_table, adjacent_node_previous_vc_table
);


parameter DEST_NODE_WIDTH = $clog2(NUM_OF_NODES);
parameter VIRTUAL_CHANNELS_BITWIDTH = $clog2(NUM_OF_VIRTUAL_CHANNELS);


localparam STOP = 3;
localparam ACROSS = 2;
localparam CLOCKWISE = 1;
localparam ANTI_CLOCKWISE = 0;







localparam HEAD_FLIT = 2'b01;
localparam HEADER = 2'b11;
localparam BODY_FLIT = 2'b10;
localparam TAIL_FLIT = 2'b00;

localparam HEAD_TAIL = 2;
localparam FLIT_TOTAL_WIDTH = HEAD_TAIL+$clog2(NUM_OF_VIRTUAL_CHANNELS)+FLIT_DATA_WIDTH;
localparam ACTUAL_DATA_PAYLOAD_WIDTH = FLIT_DATA_WIDTH-DEST_NODE_WIDTH-DEST_NODE_WIDTH;

localparam NUM_OF_PORTS = 3;
localparam BIDIRECTIONAL_PER_PORT = 2;


input clk, reset;

input [FLIT_TOTAL_WIDTH-1:0] data_input;

input [FLIT_TOTAL_WIDTH-1:0] flit_data_input_across;
input [FLIT_TOTAL_WIDTH-1:0] flit_data_input_clockwise;
input [FLIT_TOTAL_WIDTH-1:0] flit_data_input_anticlockwise;

input [FLIT_TOTAL_WIDTH-1:0] node_data_from_cpu;
output reg [FLIT_TOTAL_WIDTH-1:0] node_data_to_cpu;

output [FLIT_TOTAL_WIDTH-1:0] flit_data_output_across;
output [FLIT_TOTAL_WIDTH-1:0] flit_data_output_clockwise;
output [FLIT_TOTAL_WIDTH-1:0] flit_data_output_anticlockwise;

input [NUM_OF_PORTS-1:0] flit_data_input_are_valid;
output [NUM_OF_PORTS-1:0] flit_data_output_are_valid;


input [NUM_OF_PORTS*NUM_OF_VIRTUAL_CHANNELS-1:0] adjacent_nodes_are_ready;


output [NUM_OF_PORTS*NUM_OF_VIRTUAL_CHANNELS-1:0] current_node_is_ready;


input [NUM_OF_PORTS*NUM_OF_VIRTUAL_CHANNELS-1:0] adjacent_node_vc_are_almost_full;
output [NUM_OF_PORTS*NUM_OF_VIRTUAL_CHANNELS-1:0] current_node_vc_are_almost_full;


input [NUM_OF_PORTS*NUM_OF_VIRTUAL_CHANNELS*(VIRTUAL_CHANNELS_BITWIDTH+1)-1:0] adjacent_node_previous_vc_table;
output [NUM_OF_PORTS*NUM_OF_VIRTUAL_CHANNELS*(VIRTUAL_CHANNELS_BITWIDTH+1)-1:0] current_node_previous_vc_table;


`ifdef FORMAL
	output [NUM_OF_PORTS*HEAD_TAIL-1:0] input_flit_type;
	output [NUM_OF_PORTS*DIRECTION_WIDTH-1:0] out_port_num;
	reg [FLIT_TOTAL_WIDTH-1:0] flit_data_input_previously [NUM_OF_PORTS-1:0];
`else
	wire [NUM_OF_PORTS*HEAD_TAIL-1:0] input_flit_type;

`endif


wire [NUM_OF_PORTS*NUM_OF_VIRTUAL_CHANNELS-1:0] current_node_vc_are_full;

wire [NUM_OF_PORTS-1:0] valid_output;
reg [NUM_OF_PORTS-1:0] valid_output_previously;

wire [FLIT_TOTAL_WIDTH-1:0] flit_data_input [NUM_OF_PORTS-1:0];
reg [FLIT_TOTAL_WIDTH-1:0] flit_data_output [NUM_OF_PORTS-1:0];


assign flit_data_input[ACROSS] = flit_data_input_across;
assign flit_data_input[CLOCKWISE] = flit_data_input_clockwise;
assign flit_data_input[ANTI_CLOCKWISE] = flit_data_input_anticlockwise;

assign flit_data_output_across = flit_data_output[ACROSS];
assign flit_data_output_clockwise = flit_data_output[CLOCKWISE];
assign flit_data_output_anticlockwise = flit_data_output[ANTI_CLOCKWISE];


`ifdef FORMAL
reg first_clock_had_passed = 0;
reg second_clock_had_passed = 0;
reg third_clock_had_passed = 0;

always @(posedge clk) first_clock_had_passed <= 1;
always @(posedge clk) second_clock_had_passed <= first_clock_had_passed;
always @(posedge clk) third_clock_had_passed <= second_clock_had_passed;
`endif


reg  [FLIT_TOTAL_WIDTH-1:0] data_out_from_vc [NUM_OF_PORTS-1:0][NUM_OF_VIRTUAL_CHANNELS-1:0];
wire [FLIT_TOTAL_WIDTH-1:0] data_output_from_vc [NUM_OF_PORTS-1:0][NUM_OF_VIRTUAL_CHANNELS-1:0];
wire [FLIT_TOTAL_WIDTH-1:0] data_input_to_vc [NUM_OF_PORTS-1:0][NUM_OF_VIRTUAL_CHANNELS-1:0];

wire [NUM_OF_VIRTUAL_CHANNELS-1:0] vc_is_available [NUM_OF_PORTS-1:0];
wire [NUM_OF_VIRTUAL_CHANNELS-1:0] vc_buffer_is_empty [NUM_OF_PORTS-1:0];





reg [NUM_OF_VIRTUAL_CHANNELS-1:0] req [NUM_OF_PORTS-1:0];

reg [NUM_OF_VIRTUAL_CHANNELS-1:0] req_previous [NUM_OF_PORTS-1:0];


wire [NUM_OF_VIRTUAL_CHANNELS-1:0] vc_is_to_be_allocated [NUM_OF_PORTS-1:0];
wire [NUM_OF_VIRTUAL_CHANNELS-1:0] vc_is_to_be_deallocated [NUM_OF_PORTS-1:0];

`ifdef FORMAL


reg [$clog2(NUM_OF_NODES)-1:0] vc_reserved_time [NUM_OF_PORTS-1:0][NUM_OF_VIRTUAL_CHANNELS-1:0]; 

reg [NUM_OF_VIRTUAL_CHANNELS-1:0] vc_is_to_be_allocated_previously [NUM_OF_PORTS-1:0];
reg [NUM_OF_VIRTUAL_CHANNELS-1:0] vc_is_to_be_deallocated_previously [NUM_OF_PORTS-1:0];

reg [NUM_OF_VIRTUAL_CHANNELS-1:0] vc_is_allocated_by_head_flit [NUM_OF_PORTS-1:0];
reg [NUM_OF_VIRTUAL_CHANNELS-1:0] vc_is_allocated_by_head_flit_previously [NUM_OF_PORTS-1:0];

reg [FLIT_TOTAL_WIDTH-1:0] previous_data_input_to_vc [NUM_OF_PORTS-1:0][NUM_OF_VIRTUAL_CHANNELS-1:0];
`endif

localparam DIRECTION_WIDTH = 2;
wire [DIRECTION_WIDTH-1:0] direction [NUM_OF_PORTS-1:0];

wire [DEST_NODE_WIDTH-1:0] dest_node [NUM_OF_PORTS-1:0];


localparam NON_EXISTENCE_VC_NUM = {(VIRTUAL_CHANNELS_BITWIDTH+1){1'b1}};


wire [NUM_OF_PORTS-1:0] req_port;




wire [NUM_OF_VIRTUAL_CHANNELS-1:0] granted_vc [NUM_OF_PORTS-1:0];
wire [NUM_OF_PORTS-1:0] granted_port;


wire [$clog2(NUM_OF_VIRTUAL_CHANNELS)-1:0] granted_vc_index [NUM_OF_PORTS-1:0];
wire [$clog2(NUM_OF_PORTS)-1:0] granted_port_index;



wire [NUM_OF_PORTS-1:0] requests_in_ports_have_been_served = req_port & granted_port;
wire [NUM_OF_PORTS-1:0] outstanding_requests_in_multiple_ports = req_port;




wire requests_from_multiple_ports = !((req_port != 0) && ((req_port & (req_port - 1)) == 0));



arbiter #(NUM_OF_PORTS) rr_arb_port_to_cpu
(.clk(clk), .reset(reset), .req(outstanding_requests_in_multiple_ports), .grant(granted_port));



oh_to_idx #(NUM_OF_PORTS) port_index (.one_hot(granted_port), .index(granted_port_index));



reg [NUM_OF_PORTS-1:0] past_req_port;
always @(posedge clk) past_req_port <= req_port;

always @(*)
begin
	if(reset & reset_previously)
		node_data_to_cpu = data_input;

	else if(reset || (past_req_port == 0) || 
			(vc_buffer_is_empty[granted_port_index][granted_vc_index[granted_port_index]])) 
		node_data_to_cpu = 0;

	else node_data_to_cpu = data_out_from_vc[granted_port_index][granted_vc_index[granted_port_index]];
end


wire [$clog2(NUM_OF_NODES)-1:0] current_node = NODE_IDENTIFIER;



reg reset_previously;
always @(posedge clk) reset_previously <= reset;


`ifdef FORMAL

reg [DEST_NODE_WIDTH-1:0] dest_node_for_sending_node_own_data [NUM_OF_PORTS-1:0];
reg [NUM_OF_PORTS-1:0] node_needs_to_send_its_own_data;
reg [ACTUAL_DATA_PAYLOAD_WIDTH-1:0] sum_data [NUM_OF_PORTS-1:0][NUM_OF_VIRTUAL_CHANNELS-1:0];
reg [DEST_NODE_WIDTH-1:0] previous_dest_node_for_sending_node_own_data [NUM_OF_PORTS-1:0];
reg [NUM_OF_PORTS-1:0] node_needs_to_send_its_own_data_previously;
`else

wire [DEST_NODE_WIDTH-1:0] dest_node_for_sending_node_own_data [NUM_OF_PORTS-1:0];
wire [NUM_OF_PORTS-1:0] node_needs_to_send_its_own_data;
`endif

wire [FLIT_TOTAL_WIDTH-1:0] node_own_data [NUM_OF_PORTS-1:0];



























reg [VIRTUAL_CHANNELS_BITWIDTH:0] previous_vc [NUM_OF_PORTS-1:0][NUM_OF_VIRTUAL_CHANNELS-1:0];
	

wire enqueue_en [NUM_OF_PORTS-1:0][NUM_OF_VIRTUAL_CHANNELS-1:0];


genvar port_num;
genvar vc_num;

generate

	for(port_num=0; port_num<NUM_OF_PORTS; port_num=port_num+1)
	begin : PORTS	




		arbiter #(NUM_OF_VIRTUAL_CHANNELS) rr_arb_vc_to_cpu
		(.clk(clk), .reset(reset), 
		 .req(req[port_num]), 
		 .grant(granted_vc[port_num]));




		oh_to_idx #(NUM_OF_VIRTUAL_CHANNELS) vc_index 
		(
			.one_hot(granted_vc[port_num]), 
			.index(granted_vc_index[port_num])
		);

		wire stop_flow;


		router #(NUM_OF_NODES) rt 
		(



			.dest_node((stop_flow && !node_needs_to_send_its_own_data[port_num]) ? 
							current_node :
							(node_needs_to_send_its_own_data[port_num]) ?
							 dest_node_for_sending_node_own_data[port_num] : dest_node[port_num]), 
			.current_node(current_node), 
			.direction(direction[port_num])
		);
		

		`ifdef FORMAL
			assign out_port_num[port_num*DIRECTION_WIDTH +: DIRECTION_WIDTH] = direction[port_num];
		`endif


		assign req_port[port_num] = |req[port_num]; 


		assign input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] = 
						flit_data_input[port_num][(FLIT_TOTAL_WIDTH-1) -: HEAD_TAIL] ;


		wire [VIRTUAL_CHANNELS_BITWIDTH-1:0] prev_vc = 
				flit_data_input[port_num][(FLIT_TOTAL_WIDTH-HEAD_TAIL-1) -: VIRTUAL_CHANNELS_BITWIDTH] ;


		wire [NUM_OF_VIRTUAL_CHANNELS-1:0] adjacent_nodes_vc_are_reserved_and_not_almost_full;

		wire [NUM_OF_VIRTUAL_CHANNELS-1:0] granted_vc_enqueue;



		arbiter #(NUM_OF_VIRTUAL_CHANNELS) rr_arb_data_to_vc
		(
			.clk(clk), 
			.reset(reset), 
		 	.req(current_node_is_ready[port_num*NUM_OF_VIRTUAL_CHANNELS +: NUM_OF_VIRTUAL_CHANNELS]), 
		 	.grant(granted_vc_enqueue)
		);

		`ifdef FORMAL
		always @(posedge clk) 
			flit_data_input_previously[port_num] <= flit_data_input[port_num];
		`endif

		wire [NUM_OF_VIRTUAL_CHANNELS-1:0] matching_vc;
		(* keep *) wire [VIRTUAL_CHANNELS_BITWIDTH-1:0] matching_vc_number;

		for(vc_num=0; vc_num<NUM_OF_VIRTUAL_CHANNELS; vc_num=vc_num+1)
		begin : VIRTUAL_CHANNELS







			assign current_node_is_ready[port_num*NUM_OF_VIRTUAL_CHANNELS + vc_num] =
					vc_is_available[port_num][vc_num] &&
					~current_node_vc_are_almost_full[port_num*NUM_OF_VIRTUAL_CHANNELS + vc_num];

			assign current_node_previous_vc_table
			 [((port_num*NUM_OF_VIRTUAL_CHANNELS+vc_num)*(VIRTUAL_CHANNELS_BITWIDTH+1)) +:
			  												(VIRTUAL_CHANNELS_BITWIDTH+1)]
			 			= previous_vc[port_num][vc_num];





			wire dequeue_en = ((direction[port_num] == STOP) || (node_needs_to_send_its_own_data[port_num])) ?
			 					1'b0 :
			

			  (((((data_output_from_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -: HEAD_TAIL] == HEAD_FLIT) || 
			      (data_output_from_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -: HEAD_TAIL] == HEADER)) && 
			      (|adjacent_nodes_are_ready[direction[port_num]*NUM_OF_VIRTUAL_CHANNELS +:
						NUM_OF_VIRTUAL_CHANNELS])) || 
					

				(((data_output_from_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -: HEAD_TAIL] == BODY_FLIT) || 
				  (data_output_from_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -: HEAD_TAIL] == TAIL_FLIT)) &&
				 (adjacent_nodes_vc_are_reserved_and_not_almost_full[direction[port_num]*NUM_OF_VIRTUAL_CHANNELS 
				  + matching_vc_number])))
				  
				&& (!requests_from_multiple_ports ||
					requests_from_multiple_ports &&
				 	requests_in_ports_have_been_served[port_num]));


			assign adjacent_nodes_vc_are_reserved_and_not_almost_full[vc_num] = 


			  ((!adjacent_nodes_are_ready[direction[port_num]*NUM_OF_VIRTUAL_CHANNELS + vc_num]) 
			  & (!adjacent_node_vc_are_almost_full[direction[port_num]*NUM_OF_VIRTUAL_CHANNELS + vc_num]));


			always @(posedge clk)
			begin
				if(reset) 
					previous_vc[port_num][vc_num] <= 
						NON_EXISTENCE_VC_NUM;
				
				else if(vc_is_to_be_allocated[port_num][vc_num])
					previous_vc[port_num][vc_num] <= {1'b0, prev_vc};
					


			end





			assign enqueue_en[port_num][vc_num] = (!reset & reset_previously) ? 
				flit_data_input_are_valid[port_num] && (vc_num == 0) :

				flit_data_input_are_valid[port_num] &&
				((vc_is_available[port_num][vc_num] && granted_vc_enqueue[vc_num] && 
				 ((input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == HEADER) ||
				  (input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == HEAD_FLIT))) ||
				(!vc_is_available[port_num][vc_num] && ({1'b0, prev_vc} == previous_vc[port_num][vc_num]) &&
 				 ((input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == BODY_FLIT) ||
				  (input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == TAIL_FLIT)))) &&

				(!current_node_vc_are_full[port_num*NUM_OF_VIRTUAL_CHANNELS + vc_num]);

			`ifdef FORMAL
			

			
			always @(posedge clk) 
				vc_is_to_be_allocated_previously[port_num][vc_num] <=
				vc_is_to_be_allocated[port_num][vc_num];

			always @(posedge clk) 
				vc_is_to_be_deallocated_previously[port_num][vc_num] <=
				vc_is_to_be_deallocated[port_num][vc_num];

			always @(posedge clk) 
				vc_is_allocated_by_head_flit_previously[port_num][vc_num] <=
				vc_is_allocated_by_head_flit[port_num][vc_num];			
				
			
			always @(posedge clk)
			begin
				if(reset || 

				  (vc_is_to_be_deallocated[port_num][vc_num] && 
				   vc_is_allocated_by_head_flit[port_num][vc_num])) 
				   
					vc_is_allocated_by_head_flit[port_num][vc_num] <= 0;
				
				else if(enqueue_en[port_num][vc_num] && (input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == HEAD_FLIT))
					vc_is_allocated_by_head_flit[port_num][vc_num] <= 1;
			end

			always @(posedge clk) 
				cover(enqueue_en[port_num][vc_num] && (input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] != HEADER) &&
				 		vc_is_allocated_by_head_flit[port_num][vc_num]);
			
			always @(posedge clk)
			begin
				if(reset || 
				   vc_is_to_be_deallocated_previously[port_num][vc_num])
						sum_data[port_num][vc_num] <= 0;
					
				else if(enqueue_en[port_num][vc_num] && 
				        ((input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == HEAD_FLIT) ||  
						 (input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == BODY_FLIT)))
					sum_data[port_num][vc_num] <= sum_data[port_num][vc_num] + 
													flit_data_input[port_num][0 +: ACTUAL_DATA_PAYLOAD_WIDTH];
			end
			
			always @(posedge clk)
			begin
				if(first_clock_had_passed)
				begin
					if($past(reset) || $past(vc_is_to_be_deallocated_previously[port_num][vc_num]))
						assert(sum_data[port_num][vc_num] == 0);

					else if($past(enqueue_en[port_num][vc_num]) && 
						   (($past(input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL]) == HEAD_FLIT) ||
							 vc_is_allocated_by_head_flit_previously[port_num][vc_num]))
						
							assert(sum_data[port_num][vc_num] == $past(sum_data[port_num][vc_num]) + 
									flit_data_input_previously[port_num][0 +: ACTUAL_DATA_PAYLOAD_WIDTH]);
				
					else if(vc_is_allocated_by_head_flit_previously[port_num][vc_num] && 
								vc_is_to_be_deallocated_previously[port_num][vc_num])
								
							assert(sum_data[port_num][vc_num] ==
									flit_data_input_previously[port_num][0 +: ACTUAL_DATA_PAYLOAD_WIDTH]);
								
					else assert(sum_data[port_num][vc_num] == $past(sum_data[port_num][vc_num]));
				end
			end

			always @(posedge clk)
				previous_data_input_to_vc[port_num][vc_num] <= data_input_to_vc[port_num][vc_num];

			always @(posedge clk)
			begin
				if(first_clock_had_passed)
				begin
					if($past(reset) || $past(vc_is_to_be_deallocated_previously[port_num][vc_num]))
						assert(sum_data[port_num][vc_num] == 0);
				
					else if($past(flit_data_input_are_valid[port_num]) &&
					    $past(enqueue_en[port_num][vc_num]))
					begin
						if((previous_data_input_to_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -: 
							HEAD_TAIL] == TAIL_FLIT) && 
							($past(previous_data_input_to_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -:
						    HEAD_TAIL]) == BODY_FLIT))
					    
							assert(sum_data[port_num][vc_num] == 
								previous_data_input_to_vc[port_num][vc_num][0 +: ACTUAL_DATA_PAYLOAD_WIDTH]);
								
								
						else if(previous_data_input_to_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -:
					    		HEAD_TAIL] == HEAD_FLIT)
					    
							assert(sum_data[port_num][vc_num] == 
								previous_data_input_to_vc[port_num][vc_num][0 +: ACTUAL_DATA_PAYLOAD_WIDTH]);
								
								
						else if(previous_data_input_to_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -:
					    		HEAD_TAIL] == BODY_FLIT)
					    
							assert(sum_data[port_num][vc_num] == $past(sum_data[port_num][vc_num]) +
								previous_data_input_to_vc[port_num][vc_num][0 +: ACTUAL_DATA_PAYLOAD_WIDTH]);
					end
					
					else assert(sum_data[port_num][vc_num] == $past(sum_data[port_num][vc_num]));
				end
			end
			
			`endif


			sync_fifo 
			#(
				.WIDTH(FLIT_TOTAL_WIDTH),
				.SIZE(NODE_BUFFER_WIDTH/FLIT_DATA_WIDTH)
			)
			fifo
			(
				.clk(clk), .reset(reset),
				.full(current_node_vc_are_full[port_num*NUM_OF_VIRTUAL_CHANNELS + vc_num]), 
				.almost_full(current_node_vc_are_almost_full[port_num*NUM_OF_VIRTUAL_CHANNELS + vc_num]), 
				.enqueue_en(enqueue_en[port_num][vc_num]), 
				.enqueue_value(data_input_to_vc[port_num][vc_num]),


				.empty(vc_buffer_is_empty[port_num][vc_num]),
			 	.dequeue_en(dequeue_en),
				.dequeue_value(data_output_from_vc[port_num][vc_num])
			);
	
			assign data_input_to_vc[port_num][vc_num] = flit_data_input[port_num];
	
			always @(posedge clk)
			begin
				data_out_from_vc[port_num][vc_num] <=
				{
					data_output_from_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -: HEAD_TAIL],
				 	vc_num[VIRTUAL_CHANNELS_BITWIDTH-1:0],
				 	data_output_from_vc[port_num][vc_num][0 +: FLIT_DATA_WIDTH]
				};
			end

			assign vc_is_available[port_num][vc_num] = !req[port_num][vc_num];


			always @(posedge clk) 
			begin
				if(reset) req_previous[port_num][vc_num] <= 0;

				else req_previous[port_num][vc_num] <= req[port_num][vc_num];
			end




			assign vc_is_to_be_allocated[port_num][vc_num] = (!reset & reset_previously) ? 
					((flit_data_input_are_valid[port_num]) && (vc_num == 0)) :

					(granted_vc_enqueue[vc_num] && (vc_is_available[port_num][vc_num]) && 
					((input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == HEADER) ||
					 (input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == HEAD_FLIT)));



			assign vc_is_to_be_deallocated[port_num][vc_num] = 
					(req_previous[port_num][vc_num] && flit_data_input_are_valid[port_num] &&
					(input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == TAIL_FLIT) &&
					(enqueue_en[port_num][vc_num]) &&
					({1'b0, prev_vc} == previous_vc[port_num][vc_num])) &&
					(requests_in_ports_have_been_served[port_num]);

			initial req[port_num][vc_num] = 0;


			always @(posedge clk) 
			begin
				if(reset && reset_previously) req[port_num][vc_num] <= vc_is_to_be_allocated[port_num][vc_num];

				else if ((vc_is_to_be_allocated[port_num][vc_num] && !vc_is_to_be_deallocated[port_num][vc_num]) 
					 || (!vc_is_to_be_allocated[port_num][vc_num] && vc_is_to_be_deallocated[port_num][vc_num]))
				begin







					case(input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL]) 
					


						BODY_FLIT : req[port_num][vc_num] <= 1;


						TAIL_FLIT : req[port_num][vc_num] <= 0;


						HEAD_FLIT : req[port_num][vc_num] <= 1;


						HEADER : req[port_num][vc_num] <= 0;

						default : req[port_num][vc_num] <= 0;

					endcase
				end


			end

			`ifdef FORMAL
			

			always @(posedge clk) 
			begin
				if(first_clock_had_passed)
				begin
					if($past(reset) && $past(reset_previously) && second_clock_had_passed) 
						assert(req[port_num][vc_num] == vc_is_to_be_allocated_previously[port_num][vc_num]);

					else if (($past(vc_is_to_be_allocated[port_num][vc_num]) && 
							  !$past(vc_is_to_be_deallocated[port_num][vc_num]))
							   
						 || (!$past(vc_is_to_be_allocated[port_num][vc_num]) && 
						 	  $past(vc_is_to_be_deallocated[port_num][vc_num])))
					begin







						case($past(input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL]))
						


							BODY_FLIT : assert(req[port_num][vc_num] == 1);


							TAIL_FLIT : assert(req[port_num][vc_num] == 0);


							HEAD_FLIT : assert(req[port_num][vc_num] == 1);


							HEADER : assert(req[port_num][vc_num] == 0);

							default : assert(req[port_num][vc_num] == 0);

						endcase
					end
				end
			end






			
			always @(posedge clk)
			begin
				if(reset || (!req[port_num][vc_num])) vc_reserved_time[port_num][vc_num] <= 0;
				
				else if(req[port_num][vc_num]) 
					vc_reserved_time[port_num][vc_num] <= vc_reserved_time[port_num][vc_num] + 1;
			end
			
			always @(posedge clk) assert(vc_reserved_time[port_num][vc_num] < NUM_OF_NODES);




			always @(posedge clk)
			begin
				cover(input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == BODY_FLIT);
				cover(input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == TAIL_FLIT);
				cover(input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == HEAD_FLIT);
				cover(input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == HEADER);
			end

			`endif



			
			assign matching_vc[vc_num] = (direction[port_num] == port_num) && 
							(node_needs_to_send_its_own_data[port_num]) ?
			
				(adjacent_node_previous_vc_table[((port_num*NUM_OF_VIRTUAL_CHANNELS+vc_num)*
												(VIRTUAL_CHANNELS_BITWIDTH+1)) +: (VIRTUAL_CHANNELS_BITWIDTH+1)] 
				  	== {1'b0, node_own_data[port_num][FLIT_DATA_WIDTH +: VIRTUAL_CHANNELS_BITWIDTH]}) :
		 														
				(adjacent_node_previous_vc_table[((port_num*NUM_OF_VIRTUAL_CHANNELS+vc_num)*
												(VIRTUAL_CHANNELS_BITWIDTH+1)) +: (VIRTUAL_CHANNELS_BITWIDTH+1)] 
				  	== {1'b0, data_out_from_vc[port_num][vc_num][FLIT_DATA_WIDTH +:
				  	 												VIRTUAL_CHANNELS_BITWIDTH]});

		end
		



		oh_to_idx #(NUM_OF_VIRTUAL_CHANNELS) port_index
		 		(.one_hot(matching_vc), .index(matching_vc_number));
			 		
			 		
		wire [(HEAD_TAIL-1) : 0] output_flit_type = (node_needs_to_send_its_own_data[port_num]) ?
										node_own_data[port_num][(FLIT_TOTAL_WIDTH-1) -: HEAD_TAIL] :
										node_data_from_cpu[(FLIT_TOTAL_WIDTH-1) -: HEAD_TAIL];



		assign stop_flow = (reset) ?  
						(data_input[FLIT_DATA_WIDTH +: HEAD_TAIL] == TAIL_FLIT) : 
						(output_flit_type == TAIL_FLIT);


		assign dest_node[port_num] = (!reset & reset_previously) ? 
				data_input[(FLIT_DATA_WIDTH-1) -: DEST_NODE_WIDTH] :
				flit_data_input[port_num][(FLIT_DATA_WIDTH-1) -: DEST_NODE_WIDTH];



		initial valid_output_previously[port_num] = 0;
		always @(posedge clk) valid_output_previously[port_num] <= valid_output[port_num];


		assign flit_data_output_are_valid[port_num] = valid_output_previously[port_num];	

		localparam NUM_OF_CLOCK_CYCLES_BEFORE_SENDING_NODE_OWN_DATA = 8;
		reg [$clog2(NUM_OF_CLOCK_CYCLES_BEFORE_SENDING_NODE_OWN_DATA)-1:0] start_sending_node_own_data;
		
		always @(posedge clk) 
		begin
			if(reset) start_sending_node_own_data <= 0;
			
			else if(~&start_sending_node_own_data)
				start_sending_node_own_data <= start_sending_node_own_data + 1;
		end


		`ifdef FORMAL

			reg [ACTUAL_DATA_PAYLOAD_WIDTH-1:0] random_generated_data;
			
			reg [HEAD_TAIL-1:0] random_generated_head;
			reg [HEAD_TAIL-1:0] previous_random_generated_head;
			reg [VIRTUAL_CHANNELS_BITWIDTH-1:0] random_generated_vc;
			reg [VIRTUAL_CHANNELS_BITWIDTH-1:0] previous_random_generated_vc;
			
			always @(posedge clk) previous_random_generated_head <= random_generated_head;
			always @(posedge clk) previous_random_generated_vc <= random_generated_vc;
		
			always @(posedge clk)
				previous_dest_node_for_sending_node_own_data[port_num] <= 
				dest_node_for_sending_node_own_data[port_num];

			initial previous_random_generated_head = 0;


			wire header_or_head_flit = $anyseq;


			localparam OVERFLOW_PROTECT = 2;
			
			wire [ACTUAL_DATA_PAYLOAD_WIDTH-OVERFLOW_PROTECT-1:0] data0 = $anyseq;
			wire [ACTUAL_DATA_PAYLOAD_WIDTH-OVERFLOW_PROTECT-1:0] data1 = $anyseq;
			wire [ACTUAL_DATA_PAYLOAD_WIDTH-OVERFLOW_PROTECT-1:0] data2 = $anyseq;
			
			always @(*) assume(data0 != 0);
			always @(*) assume(data1 != 0);
			always @(*) assume(data2 != 0);
			

			reg [ACTUAL_DATA_PAYLOAD_WIDTH-OVERFLOW_PROTECT-1:0] data0_reg;
			reg [ACTUAL_DATA_PAYLOAD_WIDTH-OVERFLOW_PROTECT-1:0] data1_reg;
			reg [ACTUAL_DATA_PAYLOAD_WIDTH-OVERFLOW_PROTECT-1:0] data2_reg;
			

			wire [ACTUAL_DATA_PAYLOAD_WIDTH-1:0] data_sum = data0_reg + data1_reg + data2_reg;
			
			always @(posedge clk)
			begin
				if(reset)
				begin
					data0_reg <= 0;
					data1_reg <= 0;
					data2_reg <= 0;
				end
				
				else begin
					
					case(random_generated_head)
					
						HEAD_FLIT	: begin
										data0_reg <= data0;
										data1_reg <= $anyseq;
										data2_reg <= $anyseq;
									  end
					

						BODY_FLIT	: begin
										if(previous_random_generated_head == HEAD_FLIT)
										begin
											data0_reg <= data0_reg;
											data1_reg <= data1;
											data2_reg <= $anyseq;
										end
											
										else begin
											data0_reg <= data0_reg;
											data1_reg <= data1_reg;
											data2_reg <= data2;
										end
									  end
						

						TAIL_FLIT	: begin
										data0_reg <= data0_reg;
										data1_reg <= data1_reg;
										data2_reg <= data2_reg;
									  end
						
						HEADER		: begin
										data0_reg <= $anyseq;
										data1_reg <= $anyseq;
										data2_reg <= $anyseq;
									  end
						
						default		: begin
										data0_reg <= $anyseq;
										data1_reg <= $anyseq;
										data2_reg <= $anyseq;
									  end
					endcase					
				
				end
			end
			
			initial random_generated_head = TAIL_FLIT;
			
			always @(posedge clk)
			begin
				if(reset)
				begin
					random_generated_head <= TAIL_FLIT;
				end
				

				else if(valid_output[port_num]) begin
				
					case(random_generated_head)
					
						HEAD_FLIT	: begin
										random_generated_head <= BODY_FLIT;
									  end
					

						BODY_FLIT	: begin
										if(previous_random_generated_head == HEAD_FLIT) 
										begin
											random_generated_head <= BODY_FLIT;
										end
											
										else begin
											random_generated_head <= TAIL_FLIT; 
										end
									  end
						

						TAIL_FLIT	: begin
										random_generated_head <=
												node_needs_to_send_its_own_data_previously[port_num] ? 
															  ((header_or_head_flit) ? HEADER : HEAD_FLIT) : 
															  TAIL_FLIT;
									  end
						
						HEADER		: begin
										random_generated_head <=
										 		node_needs_to_send_its_own_data_previously[port_num] ? 
															  ((header_or_head_flit) ? HEADER : HEAD_FLIT) : 
															  TAIL_FLIT;
									  end
					endcase
				end
			end

			always @(*)
			begin
				if(reset)
				begin
					random_generated_data =
							{ACTUAL_DATA_PAYLOAD_WIDTH{1'b1}};
				end
				
				else begin
				
					case(random_generated_head)
					
						HEAD_FLIT	: begin
										random_generated_data = {{OVERFLOW_PROTECT{1'b0}}, data0};
									  end
					

						BODY_FLIT	: begin
										if(previous_random_generated_head == HEAD_FLIT) 
										begin
											random_generated_data = {{OVERFLOW_PROTECT{1'b0}}, data1};
										end
											
										else begin
											random_generated_data = {{OVERFLOW_PROTECT{1'b0}}, data2};
										end
									  end
						

						TAIL_FLIT	: begin				  
										if(previous_random_generated_head == BODY_FLIT)
											random_generated_data = data_sum;
											
										else random_generated_data =
											{ACTUAL_DATA_PAYLOAD_WIDTH{1'b1}};
									  end
						
						HEADER		: begin
										random_generated_data = data0;
									  end
					endcase
				end
			end
		
			always @(*)
			begin
				case(random_generated_head)
				
					HEAD_FLIT 	: 
					begin
						random_generated_vc = $anyseq;
						dest_node_for_sending_node_own_data[port_num] = $anyseq;
						node_needs_to_send_its_own_data[port_num] = 1;
					end
								  
					BODY_FLIT 	: 
					begin
						random_generated_vc = previous_random_generated_vc;
						
						dest_node_for_sending_node_own_data[port_num] =
							previous_dest_node_for_sending_node_own_data[port_num];
							
						node_needs_to_send_its_own_data[port_num] =
							node_needs_to_send_its_own_data_previously[port_num];
					end
					
					TAIL_FLIT 	: 
					begin
						random_generated_vc = previous_random_generated_vc;
						
						dest_node_for_sending_node_own_data[port_num] =
							previous_dest_node_for_sending_node_own_data[port_num];
							
						node_needs_to_send_its_own_data[port_num] =
							node_needs_to_send_its_own_data_previously[port_num];
					end
								  			
					HEADER	 	: 
					begin
						random_generated_vc = $anyseq;
						dest_node_for_sending_node_own_data[port_num] = $anyseq;
						node_needs_to_send_its_own_data[port_num] = $anyseq;
					end
					
				endcase
			end		
			
			assign node_own_data[port_num] = 
					{
						random_generated_head, random_generated_vc, 
					 	dest_node_for_sending_node_own_data[port_num],
						current_node,

						random_generated_data
					};	
					
			always @(posedge clk)
				assume(dest_node_for_sending_node_own_data[port_num] != current_node);	
				
			always @(posedge clk) 
				node_needs_to_send_its_own_data_previously[port_num] <=
			 			   node_needs_to_send_its_own_data[port_num];				
				
		`else

			reg [ACTUAL_DATA_PAYLOAD_WIDTH-1:0] random_generated_data;
			 
			always @(posedge clk)
			begin
				if(reset) random_generated_data <= 0;
				 
				else random_generated_data <= random_generated_data + 1;
			end
				
			assign dest_node_for_sending_node_own_data[port_num] = 0;
			assign node_needs_to_send_its_own_data[port_num] = (&start_sending_node_own_data);
			assign node_own_data[port_num] = 
					{
						HEADER, {$clog2(NUM_OF_VIRTUAL_CHANNELS){1'b0}}, 
					 	dest_node_for_sending_node_own_data[port_num],
						current_node,
						
						random_generated_data+
						{{(FLIT_TOTAL_WIDTH-HEAD_TAIL-$clog2(NUM_OF_VIRTUAL_CHANNELS)-
 						DEST_NODE_WIDTH-DEST_NODE_WIDTH-NUM_OF_PORTS){1'b0}},
			 	  		port_num[NUM_OF_PORTS-1:0]}
					}; 	
		`endif		


		assign valid_output[port_num] = (reset) ? 

			(direction[port_num] == port_num) &&
			((output_flit_type == HEAD_FLIT) || (output_flit_type == HEADER)) :
			
			(direction[port_num] == port_num) &&


			
			((((output_flit_type == HEAD_FLIT) || (output_flit_type == HEADER)) && 
			

			(|adjacent_nodes_are_ready[direction[port_num]*NUM_OF_VIRTUAL_CHANNELS +:
												VIRTUAL_CHANNELS_BITWIDTH])) ||
			((valid_output_previously[port_num] && 
			 ((output_flit_type == BODY_FLIT) || (output_flit_type == TAIL_FLIT)) &&
			 

			(~adjacent_node_vc_are_almost_full[direction[port_num]*NUM_OF_VIRTUAL_CHANNELS+
												matching_vc_number]))));

		`ifdef FORMAL
		
		(* keep *) wire [$clog2(NUM_OF_PORTS*NUM_OF_VIRTUAL_CHANNELS)-1:0] debug_signal_1 =
								direction[port_num]*NUM_OF_VIRTUAL_CHANNELS + 
											matching_vc_number;
		`endif

		initial flit_data_output[port_num] = 0;

		always @(posedge clk)
		begin


			if(reset) 
			begin
				if(valid_output[port_num])
					flit_data_output[port_num] <= data_input;

				else flit_data_output[port_num] <= 0;
			end
			
			else if(valid_output[port_num]) begin

				flit_data_output[port_num] <= (node_needs_to_send_its_own_data[port_num]) ?
												node_own_data[port_num] : node_data_from_cpu;
			end

			else flit_data_output[port_num] <=0;
		end

	end

endgenerate

endmodule
module spidergon_node
#(
	`ifdef FORMAL	
		parameter NUM_OF_NODES=8, 
		parameter FLIT_DATA_WIDTH=10,
		parameter NODE_BUFFER_WIDTH=2*FLIT_DATA_WIDTH,
	`else
		parameter NUM_OF_NODES=8,
		parameter FLIT_DATA_WIDTH=16,
		parameter NODE_BUFFER_WIDTH=2*FLIT_DATA_WIDTH,
	`endif

	parameter NODE_IDENTIFIER=0,  
	parameter NUM_OF_VIRTUAL_CHANNELS=2
) 
(
	clk, reset, 
	`ifdef FORMAL
	input_flit_type,
	out_port_num,
	`endif
 	flit_data_input_across, flit_data_input_clockwise, flit_data_input_anticlockwise,
 	flit_data_output_across, flit_data_output_clockwise, flit_data_output_anticlockwise, 
	node_data_from_cpu, node_data_to_cpu, data_input,
	flit_data_input_are_valid, flit_data_output_are_valid,
	current_node_is_ready, adjacent_nodes_are_ready,
	current_node_vc_are_almost_full, adjacent_node_vc_are_almost_full,
	current_node_previous_vc_table, adjacent_node_previous_vc_table
);



parameter DEST_NODE_WIDTH = $clog2(NUM_OF_NODES);
parameter VIRTUAL_CHANNELS_BITWIDTH = $clog2(NUM_OF_VIRTUAL_CHANNELS);


localparam STOP = 3;
localparam ACROSS = 2;
localparam CLOCKWISE = 1;
localparam ANTI_CLOCKWISE = 0;







localparam HEAD_FLIT = 2'b01;
localparam HEADER = 2'b11;
localparam BODY_FLIT = 2'b10;
localparam TAIL_FLIT = 2'b00;

localparam HEAD_TAIL = 2;
localparam FLIT_TOTAL_WIDTH = HEAD_TAIL+$clog2(NUM_OF_VIRTUAL_CHANNELS)+FLIT_DATA_WIDTH;
localparam ACTUAL_DATA_PAYLOAD_WIDTH = FLIT_DATA_WIDTH-DEST_NODE_WIDTH-DEST_NODE_WIDTH;

localparam NUM_OF_PORTS = 3;
localparam BIDIRECTIONAL_PER_PORT = 2;


input clk, reset;

input [FLIT_TOTAL_WIDTH-1:0] data_input;

input [FLIT_TOTAL_WIDTH-1:0] flit_data_input_across;
input [FLIT_TOTAL_WIDTH-1:0] flit_data_input_clockwise;
input [FLIT_TOTAL_WIDTH-1:0] flit_data_input_anticlockwise;

input [FLIT_TOTAL_WIDTH-1:0] node_data_from_cpu;
output reg [FLIT_TOTAL_WIDTH-1:0] node_data_to_cpu;

output [FLIT_TOTAL_WIDTH-1:0] flit_data_output_across;
output [FLIT_TOTAL_WIDTH-1:0] flit_data_output_clockwise;
output [FLIT_TOTAL_WIDTH-1:0] flit_data_output_anticlockwise;

input [NUM_OF_PORTS-1:0] flit_data_input_are_valid;
output [NUM_OF_PORTS-1:0] flit_data_output_are_valid;


input [NUM_OF_PORTS*NUM_OF_VIRTUAL_CHANNELS-1:0] adjacent_nodes_are_ready;


output [NUM_OF_PORTS*NUM_OF_VIRTUAL_CHANNELS-1:0] current_node_is_ready;


input [NUM_OF_PORTS*NUM_OF_VIRTUAL_CHANNELS-1:0] adjacent_node_vc_are_almost_full;
output [NUM_OF_PORTS*NUM_OF_VIRTUAL_CHANNELS-1:0] current_node_vc_are_almost_full;


input [NUM_OF_PORTS*NUM_OF_VIRTUAL_CHANNELS*(VIRTUAL_CHANNELS_BITWIDTH+1)-1:0] adjacent_node_previous_vc_table;
output [NUM_OF_PORTS*NUM_OF_VIRTUAL_CHANNELS*(VIRTUAL_CHANNELS_BITWIDTH+1)-1:0] current_node_previous_vc_table;


`ifdef FORMAL
	output [NUM_OF_PORTS*HEAD_TAIL-1:0] input_flit_type;
	output [NUM_OF_PORTS*DIRECTION_WIDTH-1:0] out_port_num;
	reg [FLIT_TOTAL_WIDTH-1:0] flit_data_input_previously [NUM_OF_PORTS-1:0];
`else
	wire [NUM_OF_PORTS*HEAD_TAIL-1:0] input_flit_type;

`endif


wire [NUM_OF_PORTS*NUM_OF_VIRTUAL_CHANNELS-1:0] current_node_vc_are_full;

wire [NUM_OF_PORTS-1:0] valid_output;
reg [NUM_OF_PORTS-1:0] valid_output_previously;

wire [FLIT_TOTAL_WIDTH-1:0] flit_data_input [NUM_OF_PORTS-1:0];
reg [FLIT_TOTAL_WIDTH-1:0] flit_data_output [NUM_OF_PORTS-1:0];


assign flit_data_input[ACROSS] = flit_data_input_across;
assign flit_data_input[CLOCKWISE] = flit_data_input_clockwise;
assign flit_data_input[ANTI_CLOCKWISE] = flit_data_input_anticlockwise;

assign flit_data_output_across = flit_data_output[ACROSS];
assign flit_data_output_clockwise = flit_data_output[CLOCKWISE];
assign flit_data_output_anticlockwise = flit_data_output[ANTI_CLOCKWISE];


`ifdef FORMAL
reg first_clock_had_passed = 0;
reg second_clock_had_passed = 0;
reg third_clock_had_passed = 0;

always @(posedge clk) first_clock_had_passed <= 1;
always @(posedge clk) second_clock_had_passed <= first_clock_had_passed;
always @(posedge clk) third_clock_had_passed <= second_clock_had_passed;
`endif


reg  [FLIT_TOTAL_WIDTH-1:0] data_out_from_vc [NUM_OF_PORTS-1:0][NUM_OF_VIRTUAL_CHANNELS-1:0];
wire [FLIT_TOTAL_WIDTH-1:0] data_output_from_vc [NUM_OF_PORTS-1:0][NUM_OF_VIRTUAL_CHANNELS-1:0];
wire [FLIT_TOTAL_WIDTH-1:0] data_input_to_vc [NUM_OF_PORTS-1:0][NUM_OF_VIRTUAL_CHANNELS-1:0];

wire [NUM_OF_VIRTUAL_CHANNELS-1:0] vc_is_available [NUM_OF_PORTS-1:0];
wire [NUM_OF_VIRTUAL_CHANNELS-1:0] vc_buffer_is_empty [NUM_OF_PORTS-1:0];





reg [NUM_OF_VIRTUAL_CHANNELS-1:0] req [NUM_OF_PORTS-1:0];

reg [NUM_OF_VIRTUAL_CHANNELS-1:0] req_previous [NUM_OF_PORTS-1:0];


wire [NUM_OF_VIRTUAL_CHANNELS-1:0] vc_is_to_be_allocated [NUM_OF_PORTS-1:0];
wire [NUM_OF_VIRTUAL_CHANNELS-1:0] vc_is_to_be_deallocated [NUM_OF_PORTS-1:0];

`ifdef FORMAL


reg [$clog2(NUM_OF_NODES)-1:0] vc_reserved_time [NUM_OF_PORTS-1:0][NUM_OF_VIRTUAL_CHANNELS-1:0]; 

reg [NUM_OF_VIRTUAL_CHANNELS-1:0] vc_is_to_be_allocated_previously [NUM_OF_PORTS-1:0];
reg [NUM_OF_VIRTUAL_CHANNELS-1:0] vc_is_to_be_deallocated_previously [NUM_OF_PORTS-1:0];

reg [NUM_OF_VIRTUAL_CHANNELS-1:0] vc_is_allocated_by_head_flit [NUM_OF_PORTS-1:0];
reg [NUM_OF_VIRTUAL_CHANNELS-1:0] vc_is_allocated_by_head_flit_previously [NUM_OF_PORTS-1:0];

reg [FLIT_TOTAL_WIDTH-1:0] previous_data_input_to_vc [NUM_OF_PORTS-1:0][NUM_OF_VIRTUAL_CHANNELS-1:0];
`endif

localparam DIRECTION_WIDTH = 2;
wire [DIRECTION_WIDTH-1:0] direction [NUM_OF_PORTS-1:0];

wire [DEST_NODE_WIDTH-1:0] dest_node [NUM_OF_PORTS-1:0];


localparam NON_EXISTENCE_VC_NUM = {(VIRTUAL_CHANNELS_BITWIDTH+1){1'b1}};


wire [NUM_OF_PORTS-1:0] req_port;




wire [NUM_OF_VIRTUAL_CHANNELS-1:0] granted_vc [NUM_OF_PORTS-1:0];
wire [NUM_OF_PORTS-1:0] granted_port;


wire [$clog2(NUM_OF_VIRTUAL_CHANNELS)-1:0] granted_vc_index [NUM_OF_PORTS-1:0];
wire [$clog2(NUM_OF_PORTS)-1:0] granted_port_index;



wire [NUM_OF_PORTS-1:0] requests_in_ports_have_been_served = req_port & granted_port;
wire [NUM_OF_PORTS-1:0] outstanding_requests_in_multiple_ports = req_port;




wire requests_from_multiple_ports = !((req_port != 0) && ((req_port & (req_port - 1)) == 0));



arbiter #(NUM_OF_PORTS) rr_arb_port_to_cpu
(.clk(clk), .reset(reset), .req(outstanding_requests_in_multiple_ports), .grant(granted_port));



oh_to_idx #(NUM_OF_PORTS) port_index (.one_hot(granted_port), .index(granted_port_index));



reg [NUM_OF_PORTS-1:0] past_req_port;
always @(posedge clk) past_req_port <= req_port;

always @(*)
begin
	if(reset & reset_previously)
		node_data_to_cpu = data_input;

	else if(reset || (past_req_port == 0) || 
			(vc_buffer_is_empty[granted_port_index][granted_vc_index[granted_port_index]])) 
		node_data_to_cpu = 0;

	else node_data_to_cpu = data_out_from_vc[granted_port_index][granted_vc_index[granted_port_index]];
end


wire [$clog2(NUM_OF_NODES)-1:0] current_node = NODE_IDENTIFIER;



reg reset_previously;
always @(posedge clk) reset_previously <= reset;


`ifdef FORMAL

reg [DEST_NODE_WIDTH-1:0] dest_node_for_sending_node_own_data [NUM_OF_PORTS-1:0];
reg [NUM_OF_PORTS-1:0] node_needs_to_send_its_own_data;
reg [ACTUAL_DATA_PAYLOAD_WIDTH-1:0] sum_data [NUM_OF_PORTS-1:0][NUM_OF_VIRTUAL_CHANNELS-1:0];
reg [DEST_NODE_WIDTH-1:0] previous_dest_node_for_sending_node_own_data [NUM_OF_PORTS-1:0];
reg [NUM_OF_PORTS-1:0] node_needs_to_send_its_own_data_previously;
`else

wire [DEST_NODE_WIDTH-1:0] dest_node_for_sending_node_own_data [NUM_OF_PORTS-1:0];
wire [NUM_OF_PORTS-1:0] node_needs_to_send_its_own_data;
`endif

wire [FLIT_TOTAL_WIDTH-1:0] node_own_data [NUM_OF_PORTS-1:0];



























reg [VIRTUAL_CHANNELS_BITWIDTH:0] previous_vc [NUM_OF_PORTS-1:0][NUM_OF_VIRTUAL_CHANNELS-1:0];
	

wire enqueue_en [NUM_OF_PORTS-1:0][NUM_OF_VIRTUAL_CHANNELS-1:0];


genvar port_num;
genvar vc_num;

generate

	for(port_num=0; port_num<NUM_OF_PORTS; port_num=port_num+1)
	begin : PORTS	




		arbiter #(NUM_OF_VIRTUAL_CHANNELS) rr_arb_vc_to_cpu
		(.clk(clk), .reset(reset), 
		 .req(req[port_num]), 
		 .grant(granted_vc[port_num]));




		oh_to_idx #(NUM_OF_VIRTUAL_CHANNELS) vc_index 
		(
			.one_hot(granted_vc[port_num]), 
			.index(granted_vc_index[port_num])
		);

		wire stop_flow;


		router #(NUM_OF_NODES) rt 
		(



			.dest_node((stop_flow && !node_needs_to_send_its_own_data[port_num]) ? 
							current_node :
							(node_needs_to_send_its_own_data[port_num]) ?
							 dest_node_for_sending_node_own_data[port_num] : dest_node[port_num]), 
			.current_node(current_node), 
			.direction(direction[port_num])
		);
		

		`ifdef FORMAL
			assign out_port_num[port_num*DIRECTION_WIDTH +: DIRECTION_WIDTH] = direction[port_num];
		`endif


		assign req_port[port_num] = |req[port_num]; 


		assign input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] = 
						flit_data_input[port_num][(FLIT_TOTAL_WIDTH-1) -: HEAD_TAIL] ;


		wire [VIRTUAL_CHANNELS_BITWIDTH-1:0] prev_vc = 
				flit_data_input[port_num][(FLIT_TOTAL_WIDTH-HEAD_TAIL-1) -: VIRTUAL_CHANNELS_BITWIDTH] ;


		wire [NUM_OF_VIRTUAL_CHANNELS-1:0] adjacent_nodes_vc_are_reserved_and_not_almost_full;

		wire [NUM_OF_VIRTUAL_CHANNELS-1:0] granted_vc_enqueue;



		arbiter #(NUM_OF_VIRTUAL_CHANNELS) rr_arb_data_to_vc
		(
			.clk(clk), 
			.reset(reset), 
		 	.req(current_node_is_ready[port_num*NUM_OF_VIRTUAL_CHANNELS +: NUM_OF_VIRTUAL_CHANNELS]), 
		 	.grant(granted_vc_enqueue)
		);

		`ifdef FORMAL
		always @(posedge clk) 
			flit_data_input_previously[port_num] <= flit_data_input[port_num];
		`endif

		wire [NUM_OF_VIRTUAL_CHANNELS-1:0] matching_vc;
		(* keep *) wire [VIRTUAL_CHANNELS_BITWIDTH-1:0] matching_vc_number;

		for(vc_num=0; vc_num<NUM_OF_VIRTUAL_CHANNELS; vc_num=vc_num+1)
		begin : VIRTUAL_CHANNELS







			assign current_node_is_ready[port_num*NUM_OF_VIRTUAL_CHANNELS + vc_num] =
					vc_is_available[port_num][vc_num] &&
					~current_node_vc_are_almost_full[port_num*NUM_OF_VIRTUAL_CHANNELS + vc_num];

			assign current_node_previous_vc_table
			 [((port_num*NUM_OF_VIRTUAL_CHANNELS+vc_num)*(VIRTUAL_CHANNELS_BITWIDTH+1)) +:
			  												(VIRTUAL_CHANNELS_BITWIDTH+1)]
			 			= previous_vc[port_num][vc_num];





			wire dequeue_en = ((direction[port_num] == STOP) || (node_needs_to_send_its_own_data[port_num])) ?
			 					1'b0 :
			

			  (((((data_output_from_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -: HEAD_TAIL] == HEAD_FLIT) || 
			      (data_output_from_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -: HEAD_TAIL] == HEADER)) && 
			      (|adjacent_nodes_are_ready[direction[port_num]*NUM_OF_VIRTUAL_CHANNELS +:
						NUM_OF_VIRTUAL_CHANNELS])) || 
					

				(((data_output_from_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -: HEAD_TAIL] == BODY_FLIT) || 
				  (data_output_from_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -: HEAD_TAIL] == TAIL_FLIT)) &&
				 (adjacent_nodes_vc_are_reserved_and_not_almost_full[direction[port_num]*NUM_OF_VIRTUAL_CHANNELS 
				  + matching_vc_number])))
				  
				&& (!requests_from_multiple_ports ||
					requests_from_multiple_ports &&
				 	requests_in_ports_have_been_served[port_num]));


			assign adjacent_nodes_vc_are_reserved_and_not_almost_full[vc_num] = 


			  ((!adjacent_nodes_are_ready[direction[port_num]*NUM_OF_VIRTUAL_CHANNELS + vc_num]) 
			  & (!adjacent_node_vc_are_almost_full[direction[port_num]*NUM_OF_VIRTUAL_CHANNELS + vc_num]));


			always @(posedge clk)
			begin
				if(reset) 
					previous_vc[port_num][vc_num] <= 
						NON_EXISTENCE_VC_NUM;
				
				else if(vc_is_to_be_allocated[port_num][vc_num])
					previous_vc[port_num][vc_num] <= {1'b0, prev_vc};
					


			end





			assign enqueue_en[port_num][vc_num] = (!reset & reset_previously) ? 
				flit_data_input_are_valid[port_num] && (vc_num == 0) :

				flit_data_input_are_valid[port_num] &&
				((vc_is_available[port_num][vc_num] && granted_vc_enqueue[vc_num] && 
				 ((input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == HEADER) ||
				  (input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == HEAD_FLIT))) ||
				(!vc_is_available[port_num][vc_num] && ({1'b0, prev_vc} == previous_vc[port_num][vc_num]) &&
 				 ((input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == BODY_FLIT) ||
				  (input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == TAIL_FLIT)))) &&

				(!current_node_vc_are_full[port_num*NUM_OF_VIRTUAL_CHANNELS + vc_num]);

			`ifdef FORMAL
			

			
			always @(posedge clk) 
				vc_is_to_be_allocated_previously[port_num][vc_num] <=
				vc_is_to_be_allocated[port_num][vc_num];

			always @(posedge clk) 
				vc_is_to_be_deallocated_previously[port_num][vc_num] <=
				vc_is_to_be_deallocated[port_num][vc_num];

			always @(posedge clk) 
				vc_is_allocated_by_head_flit_previously[port_num][vc_num] <=
				vc_is_allocated_by_head_flit[port_num][vc_num];			
				
			
			always @(posedge clk)
			begin
				if(reset || 

				  (vc_is_to_be_deallocated[port_num][vc_num] && 
				   vc_is_allocated_by_head_flit[port_num][vc_num])) 
				   
					vc_is_allocated_by_head_flit[port_num][vc_num] <= 0;
				
				else if(enqueue_en[port_num][vc_num] && (input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == HEAD_FLIT))
					vc_is_allocated_by_head_flit[port_num][vc_num] <= 1;
			end

			always @(posedge clk) 
				cover(enqueue_en[port_num][vc_num] && (input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] != HEADER) &&
				 		vc_is_allocated_by_head_flit[port_num][vc_num]);
			
			always @(posedge clk)
			begin
				if(reset || 
				   vc_is_to_be_deallocated_previously[port_num][vc_num])
						sum_data[port_num][vc_num] <= 0;
					
				else if(enqueue_en[port_num][vc_num] && 
				        ((input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == HEAD_FLIT) ||  
						 (input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == BODY_FLIT)))
					sum_data[port_num][vc_num] <= sum_data[port_num][vc_num] + 
													flit_data_input[port_num][0 +: ACTUAL_DATA_PAYLOAD_WIDTH];
			end
			
			always @(posedge clk)
			begin
				if(first_clock_had_passed)
				begin
					if($past(reset) || $past(vc_is_to_be_deallocated_previously[port_num][vc_num]))
						assert(sum_data[port_num][vc_num] == 0);

					else if($past(enqueue_en[port_num][vc_num]) && 
						   (($past(input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL]) == HEAD_FLIT) ||
							 vc_is_allocated_by_head_flit_previously[port_num][vc_num]))
						
							assert(sum_data[port_num][vc_num] == $past(sum_data[port_num][vc_num]) + 
									flit_data_input_previously[port_num][0 +: ACTUAL_DATA_PAYLOAD_WIDTH]);
				
					else if(vc_is_allocated_by_head_flit_previously[port_num][vc_num] && 
								vc_is_to_be_deallocated_previously[port_num][vc_num])
								
							assert(sum_data[port_num][vc_num] ==
									flit_data_input_previously[port_num][0 +: ACTUAL_DATA_PAYLOAD_WIDTH]);
								
					else assert(sum_data[port_num][vc_num] == $past(sum_data[port_num][vc_num]));
				end
			end

			always @(posedge clk)
				previous_data_input_to_vc[port_num][vc_num] <= data_input_to_vc[port_num][vc_num];

			always @(posedge clk)
			begin
				if(first_clock_had_passed)
				begin
					if($past(reset) || $past(vc_is_to_be_deallocated_previously[port_num][vc_num]))
						assert(sum_data[port_num][vc_num] == 0);
				
					else if($past(flit_data_input_are_valid[port_num]) &&
					    $past(enqueue_en[port_num][vc_num]))
					begin
						if((previous_data_input_to_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -: 
							HEAD_TAIL] == TAIL_FLIT) && 
							($past(previous_data_input_to_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -:
						    HEAD_TAIL]) == BODY_FLIT))
					    
							assert(sum_data[port_num][vc_num] == 
								previous_data_input_to_vc[port_num][vc_num][0 +: ACTUAL_DATA_PAYLOAD_WIDTH]);
								
								
						else if(previous_data_input_to_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -:
					    		HEAD_TAIL] == HEAD_FLIT)
					    
							assert(sum_data[port_num][vc_num] == 
								previous_data_input_to_vc[port_num][vc_num][0 +: ACTUAL_DATA_PAYLOAD_WIDTH]);
								
								
						else if(previous_data_input_to_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -:
					    		HEAD_TAIL] == BODY_FLIT)
					    
							assert(sum_data[port_num][vc_num] == $past(sum_data[port_num][vc_num]) +
								previous_data_input_to_vc[port_num][vc_num][0 +: ACTUAL_DATA_PAYLOAD_WIDTH]);
					end
					
					else assert(sum_data[port_num][vc_num] == $past(sum_data[port_num][vc_num]));
				end
			end
			
			`endif


			sync_fifo 
			#(
				.WIDTH(FLIT_TOTAL_WIDTH),
				.SIZE(NODE_BUFFER_WIDTH/FLIT_DATA_WIDTH)
			)
			fifo
			(
				.clk(clk), .reset(reset),
				.full(current_node_vc_are_full[port_num*NUM_OF_VIRTUAL_CHANNELS + vc_num]), 
				.almost_full(current_node_vc_are_almost_full[port_num*NUM_OF_VIRTUAL_CHANNELS + vc_num]), 
				.enqueue_en(enqueue_en[port_num][vc_num]), 
				.enqueue_value(data_input_to_vc[port_num][vc_num]),


				.empty(vc_buffer_is_empty[port_num][vc_num]),
			 	.dequeue_en(dequeue_en),
				.dequeue_value(data_output_from_vc[port_num][vc_num])
			);
	
			assign data_input_to_vc[port_num][vc_num] = flit_data_input[port_num];
	
			always @(posedge clk)
			begin
				data_out_from_vc[port_num][vc_num] <=
				{
					data_output_from_vc[port_num][vc_num][(FLIT_TOTAL_WIDTH-1) -: HEAD_TAIL],
				 	vc_num[VIRTUAL_CHANNELS_BITWIDTH-1:0],
				 	data_output_from_vc[port_num][vc_num][0 +: FLIT_DATA_WIDTH]
				};
			end

			assign vc_is_available[port_num][vc_num] = !req[port_num][vc_num];


			always @(posedge clk) 
			begin
				if(reset) req_previous[port_num][vc_num] <= 0;

				else req_previous[port_num][vc_num] <= req[port_num][vc_num];
			end




			assign vc_is_to_be_allocated[port_num][vc_num] = (!reset & reset_previously) ? 
					((flit_data_input_are_valid[port_num]) && (vc_num == 0)) :

					(granted_vc_enqueue[vc_num] && (vc_is_available[port_num][vc_num]) && 
					((input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == HEADER) ||
					 (input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == HEAD_FLIT)));



			assign vc_is_to_be_deallocated[port_num][vc_num] = 
					(req_previous[port_num][vc_num] && flit_data_input_are_valid[port_num] &&
					(input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == TAIL_FLIT) &&
					(enqueue_en[port_num][vc_num]) &&
					({1'b0, prev_vc} == previous_vc[port_num][vc_num])) &&
					(requests_in_ports_have_been_served[port_num]);

			initial req[port_num][vc_num] = 0;


			always @(posedge clk) 
			begin
				if(reset && reset_previously) req[port_num][vc_num] <= vc_is_to_be_allocated[port_num][vc_num];

				else if ((vc_is_to_be_allocated[port_num][vc_num] && !vc_is_to_be_deallocated[port_num][vc_num]) 
					 || (!vc_is_to_be_allocated[port_num][vc_num] && vc_is_to_be_deallocated[port_num][vc_num]))
				begin







					case(input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL]) 
					


						BODY_FLIT : req[port_num][vc_num] <= 1;


						TAIL_FLIT : req[port_num][vc_num] <= 0;


						HEAD_FLIT : req[port_num][vc_num] <= 1;


						HEADER : req[port_num][vc_num] <= 0;

						default : req[port_num][vc_num] <= 0;

					endcase
				end


			end

			`ifdef FORMAL
			

			always @(posedge clk) 
			begin
				if(first_clock_had_passed)
				begin
					if($past(reset) && $past(reset_previously) && second_clock_had_passed) 
						assert(req[port_num][vc_num] == vc_is_to_be_allocated_previously[port_num][vc_num]);

					else if (($past(vc_is_to_be_allocated[port_num][vc_num]) && 
							  !$past(vc_is_to_be_deallocated[port_num][vc_num]))
							   
						 || (!$past(vc_is_to_be_allocated[port_num][vc_num]) && 
						 	  $past(vc_is_to_be_deallocated[port_num][vc_num])))
					begin







						case($past(input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL]))
						


							BODY_FLIT : assert(req[port_num][vc_num] == 1);


							TAIL_FLIT : assert(req[port_num][vc_num] == 0);


							HEAD_FLIT : assert(req[port_num][vc_num] == 1);


							HEADER : assert(req[port_num][vc_num] == 0);

							default : assert(req[port_num][vc_num] == 0);

						endcase
					end
				end
			end






			
			always @(posedge clk)
			begin
				if(reset || (!req[port_num][vc_num])) vc_reserved_time[port_num][vc_num] <= 0;
				
				else if(req[port_num][vc_num]) 
					vc_reserved_time[port_num][vc_num] <= vc_reserved_time[port_num][vc_num] + 1;
			end
			
			always @(posedge clk) assert(vc_reserved_time[port_num][vc_num] < NUM_OF_NODES);




			always @(posedge clk)
			begin
				cover(input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == BODY_FLIT);
				cover(input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == TAIL_FLIT);
				cover(input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == HEAD_FLIT);
				cover(input_flit_type[port_num*HEAD_TAIL +: HEAD_TAIL] == HEADER);
			end

			`endif



			
			assign matching_vc[vc_num] = (direction[port_num] == port_num) && 
							(node_needs_to_send_its_own_data[port_num]) ?
			
				(adjacent_node_previous_vc_table[((port_num*NUM_OF_VIRTUAL_CHANNELS+vc_num)*
												(VIRTUAL_CHANNELS_BITWIDTH+1)) +: (VIRTUAL_CHANNELS_BITWIDTH+1)] 
				  	== {1'b0, node_own_data[port_num][FLIT_DATA_WIDTH +: VIRTUAL_CHANNELS_BITWIDTH]}) :
		 														
				(adjacent_node_previous_vc_table[((port_num*NUM_OF_VIRTUAL_CHANNELS+vc_num)*
												(VIRTUAL_CHANNELS_BITWIDTH+1)) +: (VIRTUAL_CHANNELS_BITWIDTH+1)] 
				  	== {1'b0, data_out_from_vc[port_num][vc_num][FLIT_DATA_WIDTH +:
				  	 												VIRTUAL_CHANNELS_BITWIDTH]});

		end
		



		oh_to_idx #(NUM_OF_VIRTUAL_CHANNELS) port_index
		 		(.one_hot(matching_vc), .index(matching_vc_number));
			 		
			 		
		wire [(HEAD_TAIL-1) : 0] output_flit_type = (node_needs_to_send_its_own_data[port_num]) ?
										node_own_data[port_num][(FLIT_TOTAL_WIDTH-1) -: HEAD_TAIL] :
										node_data_from_cpu[(FLIT_TOTAL_WIDTH-1) -: HEAD_TAIL];



		assign stop_flow = (reset) ?  
						(data_input[FLIT_DATA_WIDTH +: HEAD_TAIL] == TAIL_FLIT) : 
						(output_flit_type == TAIL_FLIT);


		assign dest_node[port_num] = (!reset & reset_previously) ? 
				data_input[(FLIT_DATA_WIDTH-1) -: DEST_NODE_WIDTH] :
				flit_data_input[port_num][(FLIT_DATA_WIDTH-1) -: DEST_NODE_WIDTH];



		initial valid_output_previously[port_num] = 0;
		always @(posedge clk) valid_output_previously[port_num] <= valid_output[port_num];


		assign flit_data_output_are_valid[port_num] = valid_output_previously[port_num];	

		localparam NUM_OF_CLOCK_CYCLES_BEFORE_SENDING_NODE_OWN_DATA = 8;
		reg [$clog2(NUM_OF_CLOCK_CYCLES_BEFORE_SENDING_NODE_OWN_DATA)-1:0] start_sending_node_own_data;
		
		always @(posedge clk) 
		begin
			if(reset) start_sending_node_own_data <= 0;
			
			else if(~&start_sending_node_own_data)
				start_sending_node_own_data <= start_sending_node_own_data + 1;
		end


		`ifdef FORMAL

			reg [ACTUAL_DATA_PAYLOAD_WIDTH-1:0] random_generated_data;
			
			reg [HEAD_TAIL-1:0] random_generated_head;
			reg [HEAD_TAIL-1:0] previous_random_generated_head;
			reg [VIRTUAL_CHANNELS_BITWIDTH-1:0] random_generated_vc;
			reg [VIRTUAL_CHANNELS_BITWIDTH-1:0] previous_random_generated_vc;
			
			always @(posedge clk) previous_random_generated_head <= random_generated_head;
			always @(posedge clk) previous_random_generated_vc <= random_generated_vc;
		
			always @(posedge clk)
				previous_dest_node_for_sending_node_own_data[port_num] <= 
				dest_node_for_sending_node_own_data[port_num];

			initial previous_random_generated_head = 0;


			wire header_or_head_flit = $anyseq;


			localparam OVERFLOW_PROTECT = 2;
			
			wire [ACTUAL_DATA_PAYLOAD_WIDTH-OVERFLOW_PROTECT-1:0] data0 = $anyseq;
			wire [ACTUAL_DATA_PAYLOAD_WIDTH-OVERFLOW_PROTECT-1:0] data1 = $anyseq;
			wire [ACTUAL_DATA_PAYLOAD_WIDTH-OVERFLOW_PROTECT-1:0] data2 = $anyseq;
			
			always @(*) assume(data0 != 0);
			always @(*) assume(data1 != 0);
			always @(*) assume(data2 != 0);
			

			reg [ACTUAL_DATA_PAYLOAD_WIDTH-OVERFLOW_PROTECT-1:0] data0_reg;
			reg [ACTUAL_DATA_PAYLOAD_WIDTH-OVERFLOW_PROTECT-1:0] data1_reg;
			reg [ACTUAL_DATA_PAYLOAD_WIDTH-OVERFLOW_PROTECT-1:0] data2_reg;
			

			wire [ACTUAL_DATA_PAYLOAD_WIDTH-1:0] data_sum = data0_reg + data1_reg + data2_reg;
			
			always @(posedge clk)
			begin
				if(reset)
				begin
					data0_reg <= 0;
					data1_reg <= 0;
					data2_reg <= 0;
				end
				
				else begin
					
					case(random_generated_head)
					
						HEAD_FLIT	: begin
										data0_reg <= data0;
										data1_reg <= $anyseq;
										data2_reg <= $anyseq;
									  end
					

						BODY_FLIT	: begin
										if(previous_random_generated_head == HEAD_FLIT)
										begin
											data0_reg <= data0_reg;
											data1_reg <= data1;
											data2_reg <= $anyseq;
										end
											
										else begin
											data0_reg <= data0_reg;
											data1_reg <= data1_reg;
											data2_reg <= data2;
										end
									  end
						

						TAIL_FLIT	: begin
										data0_reg <= data0_reg;
										data1_reg <= data1_reg;
										data2_reg <= data2_reg;
									  end
						
						HEADER		: begin
										data0_reg <= $anyseq;
										data1_reg <= $anyseq;
										data2_reg <= $anyseq;
									  end
						
						default		: begin
										data0_reg <= $anyseq;
										data1_reg <= $anyseq;
										data2_reg <= $anyseq;
									  end
					endcase					
				
				end
			end
			
			initial random_generated_head = TAIL_FLIT;
			
			always @(posedge clk)
			begin
				if(reset)
				begin
					random_generated_head <= TAIL_FLIT;
				end
				

				else if(valid_output[port_num]) begin
				
					case(random_generated_head)
					
						HEAD_FLIT	: begin
										random_generated_head <= BODY_FLIT;
									  end
					

						BODY_FLIT	: begin
										if(previous_random_generated_head == HEAD_FLIT) 
										begin
											random_generated_head <= BODY_FLIT;
										end
											
										else begin
											random_generated_head <= TAIL_FLIT; 
										end
									  end
						

						TAIL_FLIT	: begin
										random_generated_head <=
												node_needs_to_send_its_own_data_previously[port_num] ? 
															  ((header_or_head_flit) ? HEADER : HEAD_FLIT) : 
															  TAIL_FLIT;
									  end
						
						HEADER		: begin
										random_generated_head <=
										 		node_needs_to_send_its_own_data_previously[port_num] ? 
															  ((header_or_head_flit) ? HEADER : HEAD_FLIT) : 
															  TAIL_FLIT;
									  end
					endcase
				end
			end

			always @(*)
			begin
				if(reset)
				begin
					random_generated_data =
							{ACTUAL_DATA_PAYLOAD_WIDTH{1'b1}};
				end
				
				else begin
				
					case(random_generated_head)
					
						HEAD_FLIT	: begin
										random_generated_data = {{OVERFLOW_PROTECT{1'b0}}, data0};
									  end
					

						BODY_FLIT	: begin
										if(previous_random_generated_head == HEAD_FLIT) 
										begin
											random_generated_data = {{OVERFLOW_PROTECT{1'b0}}, data1};
										end
											
										else begin
											random_generated_data = {{OVERFLOW_PROTECT{1'b0}}, data2};
										end
									  end
						

						TAIL_FLIT	: begin				  
										if(previous_random_generated_head == BODY_FLIT)
											random_generated_data = data_sum;
											
										else random_generated_data =
											{ACTUAL_DATA_PAYLOAD_WIDTH{1'b1}};
									  end
						
						HEADER		: begin
										random_generated_data = data0;
									  end
					endcase
				end
			end
		
			always @(*)
			begin
				case(random_generated_head)
				
					HEAD_FLIT 	: 
					begin
						random_generated_vc = $anyseq;
						dest_node_for_sending_node_own_data[port_num] = $anyseq;
						node_needs_to_send_its_own_data[port_num] = 1;
					end
								  
					BODY_FLIT 	: 
					begin
						random_generated_vc = previous_random_generated_vc;
						
						dest_node_for_sending_node_own_data[port_num] =
							previous_dest_node_for_sending_node_own_data[port_num];
							
						node_needs_to_send_its_own_data[port_num] =
							node_needs_to_send_its_own_data_previously[port_num];
					end
					
					TAIL_FLIT 	: 
					begin
						random_generated_vc = previous_random_generated_vc;
						
						dest_node_for_sending_node_own_data[port_num] =
							previous_dest_node_for_sending_node_own_data[port_num];
							
						node_needs_to_send_its_own_data[port_num] =
							node_needs_to_send_its_own_data_previously[port_num];
					end
								  			
					HEADER	 	: 
					begin
						random_generated_vc = $anyseq;
						dest_node_for_sending_node_own_data[port_num] = $anyseq;
						node_needs_to_send_its_own_data[port_num] = $anyseq;
					end
					
				endcase
			end		
			
			assign node_own_data[port_num] = 
					{
						random_generated_head, random_generated_vc, 
					 	dest_node_for_sending_node_own_data[port_num],
						current_node,

						random_generated_data
					};	
					
			always @(posedge clk)
				assume(dest_node_for_sending_node_own_data[port_num] != current_node);	
				
			always @(posedge clk) 
				node_needs_to_send_its_own_data_previously[port_num] <=
			 			   node_needs_to_send_its_own_data[port_num];				
				
		`else

			reg [ACTUAL_DATA_PAYLOAD_WIDTH-1:0] random_generated_data;
			 
			always @(posedge clk)
			begin
				if(reset) random_generated_data <= 0;
				 
				else random_generated_data <= random_generated_data + 1;
			end
				
			assign dest_node_for_sending_node_own_data[port_num] = 0;
			assign node_needs_to_send_its_own_data[port_num] = (&start_sending_node_own_data);
			assign node_own_data[port_num] = 
					{
						HEADER, {$clog2(NUM_OF_VIRTUAL_CHANNELS){1'b0}}, 
					 	dest_node_for_sending_node_own_data[port_num],
						current_node,
						
						random_generated_data+
						{{(FLIT_TOTAL_WIDTH-HEAD_TAIL-$clog2(NUM_OF_VIRTUAL_CHANNELS)-
 						DEST_NODE_WIDTH-DEST_NODE_WIDTH-NUM_OF_PORTS){1'b0}},
			 	  		port_num[NUM_OF_PORTS-1:0]}
					}; 	
		`endif		


		assign valid_output[port_num] = (reset) ? 

			(direction[port_num] == port_num) &&
			((output_flit_type == HEAD_FLIT) || (output_flit_type == HEADER)) :
			
			(direction[port_num] == port_num) &&


			
			((((output_flit_type == HEAD_FLIT) || (output_flit_type == HEADER)) && 
			

			(|adjacent_nodes_are_ready[direction[port_num]*NUM_OF_VIRTUAL_CHANNELS +:
												VIRTUAL_CHANNELS_BITWIDTH])) ||
			((valid_output_previously[port_num] && 
			 ((output_flit_type == BODY_FLIT) || (output_flit_type == TAIL_FLIT)) &&
			 

			(~adjacent_node_vc_are_almost_full[direction[port_num]*NUM_OF_VIRTUAL_CHANNELS+
												matching_vc_number]))));

		`ifdef FORMAL
		
		(* keep *) wire [$clog2(NUM_OF_PORTS*NUM_OF_VIRTUAL_CHANNELS)-1:0] debug_signal_1 =
								direction[port_num]*NUM_OF_VIRTUAL_CHANNELS + 
											matching_vc_number;
		`endif

		initial flit_data_output[port_num] = 0;

		always @(posedge clk)
		begin


			if(reset) 
			begin
				if(valid_output[port_num])
					flit_data_output[port_num] <= data_input;

				else flit_data_output[port_num] <= 0;
			end
			
			else if(valid_output[port_num]) begin

				flit_data_output[port_num] <= (node_needs_to_send_its_own_data[port_num]) ?
												node_own_data[port_num] : node_data_from_cpu;
			end

			else flit_data_output[port_num] <=0;
		end

	end

endgenerate

endmodule