Skip to content

Commit

Permalink
update
Browse files Browse the repository at this point in the history
  • Loading branch information
@ftqtfff
ftqtfff committed Jan 8, 2023
1 parent 99d39a3 commit 40b2b0a
Show file tree
Hide file tree
Showing 2 changed files with 389 additions and 0 deletions.
186 changes: 186 additions & 0 deletions bw_debug.sv
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,186 @@
module bandwith_reg #
(
// Users to add parameters here

// User parameters ends
// Do not modify the parameters beyond this line

// Width of S_AXI data bus
parameter C_AXIS_DATA_WIDTH = 512,
parameter TUSER_WIDTH = 10,
parameter TDEST_WIDTH = 1,
parameter USE_KEEP = 0,
parameter totalCycles = 200

// Width of S_AXI address bus

)
(
// Users to add ports here
(* X_INTERFACE_INFO = "xilinx.com:interface:axis:1.0 IN_DBG TDATA" *)
input wire [C_AXIS_DATA_WIDTH-1:0] S_AXIS_TDATA,
(* X_INTERFACE_INFO = "xilinx.com:interface:axis:1.0 IN_DBG TKEEP" *)
input wire [(C_AXIS_DATA_WIDTH/8)-1:0] S_AXIS_TKEEP,
(* X_INTERFACE_INFO = "xilinx.com:interface:axis:1.0 IN_DBG TSTRB" *)
input wire [(C_AXIS_DATA_WIDTH/8)-1:0] S_AXIS_TSTRB,
(* X_INTERFACE_INFO = "xilinx.com:interface:axis:1.0 IN_DBG TVALID" *)
input wire S_AXIS_TVALID,
(* X_INTERFACE_INFO = "xilinx.com:interface:axis:1.0 IN_DBG TREADY" *)
output wire S_AXIS_TREADY,
(* X_INTERFACE_INFO = "xilinx.com:interface:axis:1.0 IN_DBG TLAST" *)
input wire S_AXIS_TLAST,
(* X_INTERFACE_INFO = "xilinx.com:interface:axis:1.0 IN_DBG TUSER" *)
input wire [TUSER_WIDTH-1:0] S_AXIS_TUSER,
(* X_INTERFACE_INFO = "xilinx.com:interface:axis:1.0 IN_DBG TDEST" *)
input wire [TDEST_WIDTH-1:0] S_AXIS_TDEST,

(* X_INTERFACE_INFO = "xilinx.com:interface:axis:1.0 OUT_DBG TDATA" *)
output wire [C_AXIS_DATA_WIDTH-1:0] M_AXIS_TDATA,
(* X_INTERFACE_INFO = "xilinx.com:interface:axis:1.0 OUT_DBG TSTRB" *)
output wire [(C_AXIS_DATA_WIDTH/8)-1:0] M_AXIS_TSTRB,
(* X_INTERFACE_INFO = "xilinx.com:interface:axis:1.0 OUT_DBG TKEEP" *)
output wire [(C_AXIS_DATA_WIDTH/8)-1:0] M_AXIS_TKEEP,
(* X_INTERFACE_INFO = "xilinx.com:interface:axis:1.0 OUT_DBG TVALID" *)
output wire M_AXIS_TVALID,
(* X_INTERFACE_INFO = "xilinx.com:interface:axis:1.0 OUT_DBG TREADY" *)
input wire M_AXIS_TREADY,
(* X_INTERFACE_INFO = "xilinx.com:interface:axis:1.0 OUT_DBG TLAST" *)
output wire M_AXIS_TLAST,
(* X_INTERFACE_INFO = "xilinx.com:interface:axis:1.0 OUT_DBG TUSER" *)
output wire [TUSER_WIDTH-1:0] M_AXIS_TUSER,
(* X_INTERFACE_INFO = "xilinx.com:interface:axis:1.0 OUT_DBG TDEST" *)
output wire [TDEST_WIDTH-1:0] M_AXIS_TDEST,

(* X_INTERFACE_INFO = "xilinx.com:signal:clock:1.0 S_AXI_ACLK CLK" *)
(* X_INTERFACE_PARAMETER = "ASSOCIATED_BUSIF IN_DBG:OUT_DBG, ASSOCIATED_RESET S_AXI_ARESETN" *)
input wire clk,
// Global Reset Signal. This Signal is Active LOW
input wire S_AXI_ARESETN,

output reg [191:0] debug_slot,
input wire rst


);

reg [63:0] time_counter;
reg [63:0] byte_counter;
reg [63:0] pkt_counter;
reg [63:0] globalTimer;
reg active_counter;
reg [63:0] inactive_cnt;
wire [6:0] number_of_ones;
reg [6:0] number_of_ones_1d;
reg tvalid_1d;
reg tready_1d;
reg tlast_1d;

reg [31:0] time_counter_lsb;
reg [31:0] time_counter_msb;

//absolute timer
always @(posedge clk) begin
if(rst) globalTimer<= 0;
else globalTimer <= globalTimer + 1;
end


always @( posedge clk ) begin
if ( S_AXI_ARESETN == 1'b0 || rst == 1'b1) begin
byte_counter <= 'h0;
time_counter <= 'h0;
active_counter <= 1'b0;
pkt_counter <= 'h0;
tvalid_1d <= 1'b0;
tready_1d <= 1'b0;
tlast_1d <= 1'b0;
number_of_ones_1d <= 'h0;
time_counter_lsb <= 'h0;
time_counter_msb <= 'h0;
inactive_cnt <= 'h0;
end
else begin

time_counter <= (active_counter) ? time_counter + 1 : time_counter;

if(~active_counter)inactive_cnt <= inactive_cnt + 1;

if (S_AXIS_TVALID && S_AXIS_TREADY) begin
active_counter <= 1'b1;
end

if (tvalid_1d && tready_1d) begin
byte_counter <= byte_counter + number_of_ones_1d;
time_counter_lsb <= time_counter[31:0];
time_counter_msb <= time_counter[63:32];
end

if (tvalid_1d && tready_1d && tlast_1d) begin
pkt_counter <= pkt_counter + 1;
end

number_of_ones_1d <= number_of_ones;
tvalid_1d <= S_AXIS_TVALID;
tready_1d <= S_AXIS_TREADY;
tlast_1d <= S_AXIS_TLAST;

end
end

always @( posedge clk ) begin
debug_slot <={time_counter_lsb,time_counter_msb, byte_counter[31:0],byte_counter[63:32],pkt_counter[31:0],pkt_counter[63:32]};
end

/*
generate
if (USE_KEEP == 1) begin : count_using_keep
counter64_7_v3 counter64_7_v3_i (
.x(S_AXIS_TKEEP ),
.s(number_of_ones)
);
end
else begin : count_using_strb
counter64_7_v3 counter64_7_v3_i (
.x(S_AXIS_TSTRB ),
.s(number_of_ones)
);
end
endgenerate
*/

// make bridge connections

assign M_AXIS_TDATA = S_AXIS_TDATA;
assign M_AXIS_TKEEP = S_AXIS_TKEEP;
assign M_AXIS_TSTRB = S_AXIS_TSTRB;
assign M_AXIS_TVALID = S_AXIS_TVALID;
assign S_AXIS_TREADY = M_AXIS_TREADY;
assign M_AXIS_TLAST = S_AXIS_TLAST;
assign M_AXIS_TUSER = S_AXIS_TUSER;
assign M_AXIS_TDEST = S_AXIS_TDEST;

`ifdef FORMAL
always @(posedge clk) begin
if(!$initstate) begin
assume(rst == 0 && S_AXI_ARESETN == 1);

//constraints

//-----//

//Invariant
assume(time_counter <= globalTimer);

//verify a property
assert(time_counter + inactive_cnt == globalTimer);
// assert(0);

end
else begin
assume(rst);
end
end
`endif


endmodule
203 changes: 203 additions & 0 deletions iperf_udp.sv
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,203 @@
/*WRITE_PKG ---> wordCount>=totalCount ---> recordTime, if Time>threshold last pkg, other wise not last pkg*/
//timeOut to avoid congestion, so we go to WAIT_RESPONSE state.

module iperfudp (
input clk,
input rst,
input initSeqNum,
(* anyseq *) input pktArrival,
input packetGap,
input receivedResponse,
output reg [31:0] counter, // comparator counter,
output wire timeOver,
output wire lastPkt
);

reg [31:0] PktTimer;
reg [31:0] pktCnt;
reg [3:0] iperfFsmState;
reg timeOverReg;
reg lastPktReg;
reg [7:0] wordCount;
reg [31:0] seqNumber;
reg [31:0] cycleCounter;

reg [31:0] waitCounter;
reg [31:0] pkgHeaderCount;
reg [31:0] packetGapCounter;

parameter pktNumber = 3,
senderIPD = 10,
totalCycles = 995,
//Other parameters:
pkgTotalWord = 1000,
headerWord = 40,
timeOverValue = 200,
WAIT_END = 100,
//state
IDLE = 0, //end of a sequence of packets, go back to IDLE
CONSTRUCT_HEADER = 1, //end of a packet, go back to CONSTRUCT_HEADER
HEADER = 2,
WRITE_PKG = 3,
WAIT_RESPONSE = 4,
PKG_GAP = 5;

/*
initial begin
assume(rst);
end
*/

//net connection
assign timeOver = timeOverReg;
assign lastPkt = lastPktReg;

//absolute timer
always @(posedge clk) begin
if(rst)begin
cycleCounter <= 0;
end

else begin
cycleCounter<=cycleCounter+1;
end
end




//packet counter
always @(posedge clk) begin
if(rst)
pktCnt <= 0;
else
if(pktArrival)
pktCnt <= pktCnt + 1;
else
pktCnt <= pktCnt;
end

//FSM
always @(posedge clk) begin
if(rst) begin
seqNumber <= initSeqNum;
packetGapCounter <= 0;
waitCounter <= 0;
end
else begin //!rst
case(iperfFsmState)
IDLE: begin
timeOverReg <= 0;
lastPktReg <= 0;
PktTimer <= cycleCounter;
wordCount <= 0;
iperfFsmState <= CONSTRUCT_HEADER;
end

CONSTRUCT_HEADER: begin
seqNumber <= seqNumber + 1;
iperfFsmState <= HEADER;
end

HEADER: begin
//header write
if(wordCount>headerWord) begin
iperfFsmState <= WRITE_PKG;
end

else begin
wordCount<=wordCount+1;
end
end

WRITE_PKG: begin
if (wordCount < pkgTotalWord) begin
wordCount <= wordCount + 1;
end

else //wordCount>=pkgTotalWord, finish transmitting one packet
//timeOut to avoid congestion, marked as the last packet, so we go to WAIT_RESPONSE state.
if(cycleCounter - PktTimer>timeOverValue) begin
timeOverReg <= 1;
lastPktReg <= 1;
if(receivedResponse) begin
iperfFsmState <= IDLE;
end

else begin
iperfFsmState <= WAIT_RESPONSE;
end
end

else begin
timeOverReg <= 0;
PktTimer <= cycleCounter - PktTimer;

if(packetGap != 0) begin
iperfFsmState <= PKG_GAP;
end
else begin
iperfFsmState <= IDLE;
end
end
end
end

WAIT_RESPONSE: begin
waitCounter <= waitCounter + 1;
if(waitCounter >= WAIT_END) begin
waitCounter <= 0;
iperfFsmState <= IDLE;
end
end

PKG_GAP: begin
if(packetGapCounter >= packetGap) begin
packetGapCounter <= 0;
iperfFsmState <= IDLE;
end

else begin
packetGapCounter <= packetGapCounter + 1;
end
end

default : begin

end
endcase
end
end


`ifdef FORMAL
always @(posedge clk) begin
if(!$initstate) begin
assume(rst == 0);

//packet time simulation
assume(IPDTimer < rangeMax);
if(pktArrival) assume(IPDTimer > rangeMin);
if(globalTimer == totalCycles )assume(pktCnt == pktNumber);
assume(pktCnt<=10000);
//-----//

//Invariant
assume(counter <= pktCnt); //-- not automatic
//assume(counter <= globalTimer / rangeMin); //-- not automatic
//-----//


// a property
if(globalTimer == totalCycles) assert(counter == 3);


end

else begin
assume(rst);
end
end
`endif

endmodule

0 comments on commit 40b2b0a

Please sign in to comment.