diff --git a/PTP-clock.sv b/PTP-clock.sv new file mode 100644 index 0000000..dd6bb72 --- /dev/null +++ b/PTP-clock.sv @@ -0,0 +1,187 @@ +/* + +Copyright (c) 2015-2019 Alex Forencich + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN +THE SOFTWARE. + +*/ + +// Language: Verilog 2001 + +`timescale 1ns / 1ps +`default_nettype none + +/* + * PTP clock module + */ +module ptp_clock # +( + parameter DRIFT_NS = 4'h0, + parameter DRIFT_RATE = 16'h0005, + parameter totalCycles = 500, + parameter timeUnit = 31, +) +( + input wire clk, + input wire rst, + input wire input_ts_96_valid, + input wire input_period_valid, + input wire input_adj_valid, + input wire input_drift_valid, + + /* + * Timestamp outputs + */ + output wire [timeUnit-1:0] output_ts_96 +); + + + /* + * Timestamp inputs for synchronization + */ + (* anyconst *) reg [timeUnit-5:0] input_ts_96; + + + /* + * Period adjustment + */ + (* anyconst *) reg [timeUnit-5:0] input_period_ns; + reg [timeUnit-5:0] period_ns_reg; + + + /* + * Offset adjustment + */ + (* anyconst *) reg [timeUnit-5:0] input_adj_ns; + (* anyconst *) reg [timeUnit-5:0] input_adj_count; + reg [timeUnit-5:0] adj_ns_reg; + reg [timeUnit-5:0] adj_count_reg; + + + /* + * Drift adjustment + */ + (* anyconst *) reg [timeUnit-5:0] input_drift_ns; + (* anyconst *) reg [timeUnit-5:0] input_drift_count; + reg [timeUnit-5:0] drift_ns_reg; + reg [timeUnit-5:0] drift_cnt; + + + +reg [timeUnit-1:0] outputTime; +assign output_ts_96 = outputTime; +//---formal verification----// +reg [timeUnit-1:0] globalTimer; + + +always @(posedge clk) begin + if(!rst) begin + // latch parameters + if (input_period_valid) begin + period_ns_reg <= input_period_ns; + end + + if (input_adj_valid) begin + adj_ns_reg <= input_adj_ns; + end + + if (input_drift_valid) begin + drift_ns_reg <= input_drift_ns; + end + + // timestamp increment calculation + outputTime <= input_ts_96 + period_ns_reg + ( (drift_cnt==0)? drift_ns_reg : 0) + + ((adj_count_reg == 0) ? adj_ns_reg : 0); + + // offset adjust counter + if (adj_count_reg > 0) begin + adj_count_reg <= adj_count_reg - 1; + end + else begin + adj_count_reg <= adj_count_reg; + end + + // drift counter + if (drift_cnt > 0) begin + drift_cnt <= drift_cnt - 1; + end else begin + drift_cnt <= 0; //reset + end + + // 96 bit timestamp + // no increment seconds field, pre-compute both normal increment and overflow values + + end + + else begin //rst + period_ns_reg <= 0; + adj_count_reg <= input_adj_count; + drift_cnt <= input_drift_count; + adj_ns_reg <= 0; + drift_ns_reg <= 0; + outputTime <= 0; + end +end + + +//absolute timer +always @(posedge clk) begin + if(rst) globalTimer <= 0; + else globalTimer <= globalTimer + 1; +end + + +`ifdef FORMAL + always @(posedge clk) begin + //system configurations// + assume(input_period_valid); + assume(input_adj_valid); + assume(input_drift_valid); + assume(input_adj_count + input_drift_count == totalCycles ); + /*self-test + assume(input_start == 0); + assume(input_ts_96 == 160); + assume(input_period == 60); pulseCounter == 3 + */ + if(!$initstate) begin + assume(rst == 0); + + //a timing property + if( globalTimer < totalCycles ) assert( outputTime <= adj_ns_reg + drift_ns_reg + period_ns_reg + input_ts_96 ); + + // if( globalTimer == totalCycles )assert(pulseCounter == 2); + + //Invariant + // assume(pulseCounter <= input_ts_96 - input_start ); //-- not automatic + // assume(pulseCounter <= 10 ); //-- not automatic + //maxValue of input_period: maxPeriod as a efficient + //-----// + end + else begin + assume(rst); + end + end +`endif + + + + +endmodule + +`resetall diff --git a/PTP-perout.sv b/PTP-perout.sv new file mode 100644 index 0000000..c2aa745 --- /dev/null +++ b/PTP-perout.sv @@ -0,0 +1,272 @@ +/* + +Copyright (c) 2019 Alex Forencich + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN +THE SOFTWARE. + +*/ + +// Language: Verilog 2001 + +/* + * PTP period out module. NS is 31-bit + */ +module ptp_perout # //set period, width, start time of a clock +( + parameter totalCycles = 595, + parameter TIME_WIDTH = 30 +) +( + input wire clk, + input wire rst, + + /* + * Timestamp input from PTP clock + */ + input wire input_start_valid, + input wire input_period_valid, + input wire input_width_valid, + + output wire output_error, + output wire output_pulse +); + + +(* anyconst *) reg [TIME_WIDTH:0] input_ts_96; +(* anyconst *) reg [TIME_WIDTH:0] input_start; +(* anyconst *) reg [TIME_WIDTH:0] input_period; +(* anyconst *) reg [TIME_WIDTH:0] input_width; + + +localparam [2:0] + STATE_IDLE = 3'd0, + STATE_UPDATE_RISE_1 = 3'd1, //update edges + STATE_UPDATE_RISE_2 = 3'd2, //check overflow + STATE_UPDATE_FALL_1 = 3'd3, //update edges + STATE_UPDATE_FALL_2 = 3'd4, //check overflow + STATE_WAIT_EDGE = 3'd5; + +reg [2:0] state_reg = STATE_IDLE, state_next; +reg [30:0] now_ns_reg = 0, now_ns_next; +reg [30:0] next_rise_ns_reg = 0, next_rise_ns_next; +reg [30:0] next_fall_ns_reg = 0, next_fall_ns_next; +reg [30:0] period_ns_reg; +reg [30:0] width_ns_reg; +reg [30:0] ts_96_ns_inc_reg = 0, ts_96_ns_inc_next; + +reg output_reg = 1'b0, output_next = 1'b0; +reg output_error_reg = 1'b0, output_error_next; +assign output_pulse = output_reg; +assign output_error = output_error_reg; + +reg [10:0] pulseCounter; + +//---formal verification----// +reg [30:0] globalTimer; + + +always @(posedge clk) begin + if(rst)pulseCounter <= 0; + else if(output_reg == 1'b0 && output_next == 1'b1) + pulseCounter <= pulseCounter+1; + else pulseCounter<=pulseCounter; +end + + +always @* begin + next_rise_ns_next = next_rise_ns_reg; + next_fall_ns_next = next_fall_ns_reg; + ts_96_ns_inc_next = ts_96_ns_inc_reg; + now_ns_next = now_ns_reg + 1; + output_error_next = 1'b0; + state_next = state_reg; + + case (state_reg) + STATE_IDLE: begin + output_next = 1'b0; + if(now_ns_reg>input_ts_96) begin + output_error_next = 1'b1; + state_next = STATE_IDLE; + end + + if (input_start_valid && input_period_valid && input_width_valid) begin + next_rise_ns_next = now_ns_reg; + state_next = STATE_WAIT_EDGE; + end + + else begin + state_next = STATE_IDLE; + end + end + STATE_UPDATE_RISE_1: begin + // set next rise time to next rise time plus period + ts_96_ns_inc_next = next_rise_ns_reg + period_ns_reg; + state_next = STATE_UPDATE_RISE_2; + end + + STATE_UPDATE_RISE_2: begin + next_rise_ns_next = ts_96_ns_inc_reg; + state_next = STATE_WAIT_EDGE; + end + + + STATE_UPDATE_FALL_1: begin + // set next fall time to next rise time plus width + ts_96_ns_inc_next = next_rise_ns_reg + width_ns_reg; + state_next = STATE_UPDATE_FALL_2; + end + + STATE_UPDATE_FALL_2: begin + next_fall_ns_next = ts_96_ns_inc_reg; + state_next = STATE_WAIT_EDGE; + end + + STATE_WAIT_EDGE: begin + if(now_ns_reg<=input_ts_96) begin + if(now_ns_reg>=next_rise_ns_reg && output_reg == 1'b0) begin + output_next = 1'b1; + state_next = STATE_UPDATE_FALL_1; + end + + else if(now_ns_reg>=next_fall_ns_reg && output_reg == 1'b1) begin + output_next = 1'b0; + state_next = STATE_UPDATE_RISE_1; + end + + else state_next = STATE_WAIT_EDGE; + end + + else begin + output_next = 1'b0; + end + end + endcase +end + +always @(posedge clk) begin + state_reg <= state_next; + output_reg <= output_next; + output_error_reg <= output_error_next; + next_rise_ns_reg <= next_rise_ns_next; + next_fall_ns_reg <= next_fall_ns_next; + ts_96_ns_inc_reg <= ts_96_ns_inc_next; + + if (rst) begin + state_reg <= STATE_IDLE; + output_reg <= 1'b0; + output_error_reg <= 1'b0; + + if (input_period_valid) begin + period_ns_reg <= input_period; + end + + else begin + period_ns_reg <= 0; + end + + if (input_width_valid) begin + width_ns_reg <= input_width; + end + + else begin + width_ns_reg <= 0; + end + + + if(input_start_valid) begin + now_ns_reg <= input_start; + end + + else begin + now_ns_reg <= 0; + end + + + end //rst + + else begin //!rst + now_ns_reg <= now_ns_next; + end + +end //always + + +//absolute timer +always @(posedge clk) begin + if(rst) globalTimer<= 0; + else globalTimer <= globalTimer + 1; +end + + +`ifdef FORMAL + always @(posedge clk) begin + //system configurations// + assume(input_start_valid); + assume(input_period_valid); + assume(input_width_valid); + assume(input_start == 0); + assume(input_ts_96 > input_start); + assume(input_ts_96 - input_start < totalCycles); + assume(input_ts_96 - input_start > input_period); + assume(input_width < input_period); + assume(input_width > 4); + + /*self-test + assume(input_start == 0); + assume(input_ts_96 == 160); + assume(input_period == 60); pulseCounter == 3 + */ + if(!$initstate) begin + assume(rst == 0); + + //a timing property + if( globalTimer == totalCycles ) assert( (pulseCounter + 1) * input_period > (input_ts_96 - input_start)); + // if( globalTimer == totalCycles )assert(pulseCounter == 2); + + //Invariant + assume(pulseCounter <= input_ts_96 - input_start ); //-- not automatic + //assume(pulseCounter <= 10 ); //-- not automatic + //maxValue of input_period: maxPeriod as a efficient + //-----// + + + end + + + else begin + assume(rst); + end + end +`endif + + +endmodule + + + + + + + + + + + + + diff --git a/bwe.sv b/bwe.sv new file mode 100644 index 0000000..52bea65 --- /dev/null +++ b/bwe.sv @@ -0,0 +1,80 @@ +module bwe ( + input clk, + input rst, + (* anyseq *) input pktArrival, + output reg [31:0] counter // comparator counter +); + + reg [31:0] globalTimer; + reg [31:0] IPDTimer; + reg [31:0] pktCnt; + + parameter pktNumber = 3, + senderIPD = 10, + totalCycles = 162, + rangeMax = totalCycles / pktNumber, + rangeMin = senderIPD; + + +//relative timer + always @(posedge clk) begin + if(rst || pktArrival) + IPDTimer <= 0; + else + IPDTimer <= IPDTimer + 1; + end + + + always @(posedge clk) begin + if(rst) + counter <= 0; + else + if (pktArrival && (IPDTimer >= senderIPD) ) + counter <= counter + 1; + else + counter <= counter; + end + + //absolute timer + always @(posedge clk) begin + if(rst) globalTimer<= 0; + else globalTimer <= globalTimer + 1; + end + + always @(posedge clk) begin + if(rst) + pktCnt <= 0; + else + if(pktArrival) + pktCnt <= pktCnt + 1; + else + pktCnt <= pktCnt; + end + +`ifdef FORMAL + always @(posedge clk) begin + if(!$initstate) begin + assume(rst == 0); + + //IPDTimer belongs to the range (rangeMin, rangeMax) + assume(IPDTimer < rangeMax); + if(pktArrival) assume(IPDTimer > senderIPD); + if(globalTimer == totalCycles )assume(pktCnt == pktNumber); + //-----// + + //Invariant + assume(counter <= pktCnt); + + //verify a timing property + if(globalTimer == totalCycles) assert(counter == 3); + + //verify the invariant + // assert(counter <= pktCnt); + + end + else begin + assume(rst); + end + end +`endif +endmodule diff --git a/execute_modelChecking.sby b/execute_modelChecking.sby new file mode 100644 index 0000000..52b280b --- /dev/null +++ b/execute_modelChecking.sby @@ -0,0 +1,14 @@ +[options] +mode bmc +depth 165 + + +[engines] +smtbmc + +[script] +read -formal bwe.sv +prep -top bwe + +[files] +bwe.sv diff --git a/lfsr.v b/lfsr.v new file mode 100644 index 0000000..0247244 --- /dev/null +++ b/lfsr.v @@ -0,0 +1,446 @@ +/* + +Copyright (c) 2016-2018 Alex Forencich + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN +THE SOFTWARE. + +*/ + +// Language: Verilog 2001 + +`resetall +`timescale 1ns / 1ps +`default_nettype none + +/* + * Parametrizable combinatorial parallel LFSR/CRC + */ +module lfsr # +( + // width of LFSR + parameter LFSR_WIDTH = 31, + // LFSR polynomial + parameter LFSR_POLY = 31'h10000001, + // LFSR configuration: "GALOIS", "FIBONACCI" + parameter LFSR_CONFIG = "FIBONACCI", + // LFSR feed forward enable + parameter LFSR_FEED_FORWARD = 0, + // bit-reverse input and output + parameter REVERSE = 0, + // width of data input + parameter DATA_WIDTH = 8, + // implementation style: "AUTO", "LOOP", "REDUCTION" + parameter STYLE = "AUTO" +) +( + input wire [DATA_WIDTH-1:0] data_in, + input wire [LFSR_WIDTH-1:0] state_in, + output wire [DATA_WIDTH-1:0] data_out, + output wire [LFSR_WIDTH-1:0] state_out +); + +/* + +Fully parametrizable combinatorial parallel LFSR/CRC module. Implements an unrolled LFSR +next state computation, shifting DATA_WIDTH bits per pass through the module. Input data +is XORed with LFSR feedback path, tie data_in to zero if this is not required. + +Works in two parts: statically computes a set of bit masks, then uses these bit masks to +select bits for XORing to compute the next state. + +Ports: + +data_in + +Data bits to be shifted through the LFSR (DATA_WIDTH bits) + +state_in + +LFSR/CRC current state input (LFSR_WIDTH bits) + +data_out + +Data bits shifted out of LFSR (DATA_WIDTH bits) + +state_out + +LFSR/CRC next state output (LFSR_WIDTH bits) + +Parameters: + +LFSR_WIDTH + +Specify width of LFSR/CRC register + +LFSR_POLY + +Specify the LFSR/CRC polynomial in hex format. For example, the polynomial + +x^32 + x^26 + x^23 + x^22 + x^16 + x^12 + x^11 + x^10 + x^8 + x^7 + x^5 + x^4 + x^2 + x + 1 + +would be represented as + +32'h04c11db7 + +Note that the largest term (x^32) is suppressed. This term is generated automatically based +on LFSR_WIDTH. + +LFSR_CONFIG + +Specify the LFSR configuration, either Fibonacci or Galois. Fibonacci is generally used +for linear-feedback shift registers (LFSR) for pseudorandom binary sequence (PRBS) generators, +scramblers, and descrambers, while Galois is generally used for cyclic redundancy check +generators and checkers. + +Fibonacci style (example for 64b66b scrambler, 0x8000000001) + + DIN (LSB first) + | + V + (+)<---------------------------(+)<-----------------------------. + | ^ | + | .----. .----. .----. | .----. .----. .----. | + +->| 0 |->| 1 |->...->| 38 |-+->| 39 |->...->| 56 |->| 57 |--' + | '----' '----' '----' '----' '----' '----' + V + DOUT + +Galois style (example for CRC16, 0x8005) + + ,-------------------+-------------------------+----------(+)<-- DIN (MSB first) + | | | ^ + | .----. .----. V .----. .----. V .----. | + `->| 0 |->| 1 |->(+)->| 2 |->...->| 14 |->(+)->| 15 |--+---> DOUT + '----' '----' '----' '----' '----' + +LFSR_FEED_FORWARD + +Generate feed forward instead of feed back LFSR. Enable this for PRBS checking and self- +synchronous descrambling. + +Fibonacci feed-forward style (example for 64b66b descrambler, 0x8000000001) + + DIN (LSB first) + | + | .----. .----. .----. .----. .----. .----. + +->| 0 |->| 1 |->...->| 38 |-+->| 39 |->...->| 56 |->| 57 |--. + | '----' '----' '----' | '----' '----' '----' | + | V | + (+)<---------------------------(+)------------------------------' + | + V + DOUT + +Galois feed-forward style + + ,-------------------+-------------------------+------------+--- DIN (MSB first) + | | | | + | .----. .----. V .----. .----. V .----. V + `->| 0 |->| 1 |->(+)->| 2 |->...->| 14 |->(+)->| 15 |->(+)-> DOUT + '----' '----' '----' '----' '----' + +REVERSE + +Bit-reverse LFSR input and output. Shifts MSB first by default, set REVERSE for LSB first. + +DATA_WIDTH + +Specify width of input and output data bus. The module will perform one shift per input +data bit, so if the input data bus is not required tie data_in to zero and set DATA_WIDTH +to the required number of shifts per clock cycle. + +STYLE + +Specify implementation style. Can be "AUTO", "LOOP", or "REDUCTION". When "AUTO" +is selected, implemenation will be "LOOP" or "REDUCTION" based on synthesis translate +directives. "REDUCTION" and "LOOP" are functionally identical, however they simulate +and synthesize differently. "REDUCTION" is implemented with a loop over a Verilog +reduction operator. "LOOP" is implemented as a doubly-nested loop with no reduction +operator. "REDUCTION" is very fast for simulation in iverilog and synthesizes well in +Quartus but synthesizes poorly in ISE, likely due to large inferred XOR gates causing +problems with the optimizer. "LOOP" synthesizes will in both ISE and Quartus. "AUTO" +will default to "REDUCTION" when simulating and "LOOP" for synthesizers that obey +synthesis translate directives. + +Settings for common LFSR/CRC implementations: + +Name Configuration Length Polynomial Initial value Notes +CRC16-IBM Galois, bit-reverse 16 16'h8005 16'hffff +CRC16-CCITT Galois 16 16'h1021 16'h1d0f +CRC32 Galois, bit-reverse 32 32'h04c11db7 32'hffffffff Ethernet FCS; invert final output +PRBS6 Fibonacci 6 6'h21 any +PRBS7 Fibonacci 7 7'h41 any +PRBS9 Fibonacci 9 9'h021 any ITU V.52 +PRBS10 Fibonacci 10 10'h081 any ITU +PRBS11 Fibonacci 11 11'h201 any ITU O.152 +PRBS15 Fibonacci, inverted 15 15'h4001 any ITU O.152 +PRBS17 Fibonacci 17 17'h04001 any +PRBS20 Fibonacci 20 20'h00009 any ITU V.57 +PRBS23 Fibonacci, inverted 23 23'h040001 any ITU O.151 +PRBS29 Fibonacci, inverted 29 29'h08000001 any +PRBS31 Fibonacci, inverted 31 31'h10000001 any +64b66b Fibonacci, bit-reverse 58 58'h8000000001 any 10G Ethernet +128b130b Galois, bit-reverse 23 23'h210125 any PCIe gen 3 + +*/ + +reg [LFSR_WIDTH-1:0] lfsr_mask_state[LFSR_WIDTH-1:0]; +reg [DATA_WIDTH-1:0] lfsr_mask_data[LFSR_WIDTH-1:0]; +reg [LFSR_WIDTH-1:0] output_mask_state[DATA_WIDTH-1:0]; +reg [DATA_WIDTH-1:0] output_mask_data[DATA_WIDTH-1:0]; + +reg [LFSR_WIDTH-1:0] state_val = 0; +reg [DATA_WIDTH-1:0] data_val = 0; + +integer i, j, k; + +initial begin + // init bit masks + for (i = 0; i < LFSR_WIDTH; i = i + 1) begin + lfsr_mask_state[i] = {LFSR_WIDTH{1'b0}}; + lfsr_mask_state[i][i] = 1'b1; + lfsr_mask_data[i] = {DATA_WIDTH{1'b0}}; + end + for (i = 0; i < DATA_WIDTH; i = i + 1) begin + output_mask_state[i] = {LFSR_WIDTH{1'b0}}; + if (i < LFSR_WIDTH) begin + output_mask_state[i][i] = 1'b1; + end + output_mask_data[i] = {DATA_WIDTH{1'b0}}; + end + + // simulate shift register + if (LFSR_CONFIG == "FIBONACCI") begin + // Fibonacci configuration + for (i = DATA_WIDTH-1; i >= 0; i = i - 1) begin + // determine shift in value + // current value in last FF, XOR with input data bit (MSB first) + state_val = lfsr_mask_state[LFSR_WIDTH-1]; + data_val = lfsr_mask_data[LFSR_WIDTH-1]; + data_val = data_val ^ (1 << i); + + // add XOR inputs from correct indicies + for (j = 1; j < LFSR_WIDTH; j = j + 1) begin + if (LFSR_POLY & (1 << j)) begin + state_val = lfsr_mask_state[j-1] ^ state_val; + data_val = lfsr_mask_data[j-1] ^ data_val; + end + end + + // shift + for (j = LFSR_WIDTH-1; j > 0; j = j - 1) begin + lfsr_mask_state[j] = lfsr_mask_state[j-1]; + lfsr_mask_data[j] = lfsr_mask_data[j-1]; + end + for (j = DATA_WIDTH-1; j > 0; j = j - 1) begin + output_mask_state[j] = output_mask_state[j-1]; + output_mask_data[j] = output_mask_data[j-1]; + end + output_mask_state[0] = state_val; + output_mask_data[0] = data_val; + if (LFSR_FEED_FORWARD) begin + // only shift in new input data + state_val = {LFSR_WIDTH{1'b0}}; + data_val = 1 << i; + end + lfsr_mask_state[0] = state_val; + lfsr_mask_data[0] = data_val; + end + end else if (LFSR_CONFIG == "GALOIS") begin + // Galois configuration + for (i = DATA_WIDTH-1; i >= 0; i = i - 1) begin + // determine shift in value + // current value in last FF, XOR with input data bit (MSB first) + state_val = lfsr_mask_state[LFSR_WIDTH-1]; + data_val = lfsr_mask_data[LFSR_WIDTH-1]; + data_val = data_val ^ (1 << i); + + // shift + for (j = LFSR_WIDTH-1; j > 0; j = j - 1) begin + lfsr_mask_state[j] = lfsr_mask_state[j-1]; + lfsr_mask_data[j] = lfsr_mask_data[j-1]; + end + for (j = DATA_WIDTH-1; j > 0; j = j - 1) begin + output_mask_state[j] = output_mask_state[j-1]; + output_mask_data[j] = output_mask_data[j-1]; + end + output_mask_state[0] = state_val; + output_mask_data[0] = data_val; + if (LFSR_FEED_FORWARD) begin + // only shift in new input data + state_val = {LFSR_WIDTH{1'b0}}; + data_val = 1 << i; + end + lfsr_mask_state[0] = state_val; + lfsr_mask_data[0] = data_val; + + // add XOR inputs at correct indicies + for (j = 1; j < LFSR_WIDTH; j = j + 1) begin + if (LFSR_POLY & (1 << j)) begin + lfsr_mask_state[j] = lfsr_mask_state[j] ^ state_val; + lfsr_mask_data[j] = lfsr_mask_data[j] ^ data_val; + end + end + end + end else begin + $error("Error: unknown configuration setting!"); + $finish; + end + + // reverse bits if selected + if (REVERSE) begin + // reverse order + for (i = 0; i < LFSR_WIDTH/2; i = i + 1) begin + state_val = lfsr_mask_state[i]; + data_val = lfsr_mask_data[i]; + lfsr_mask_state[i] = lfsr_mask_state[LFSR_WIDTH-i-1]; + lfsr_mask_data[i] = lfsr_mask_data[LFSR_WIDTH-i-1]; + lfsr_mask_state[LFSR_WIDTH-i-1] = state_val; + lfsr_mask_data[LFSR_WIDTH-i-1] = data_val; + end + for (i = 0; i < DATA_WIDTH/2; i = i + 1) begin + state_val = output_mask_state[i]; + data_val = output_mask_data[i]; + output_mask_state[i] = output_mask_state[DATA_WIDTH-i-1]; + output_mask_data[i] = output_mask_data[DATA_WIDTH-i-1]; + output_mask_state[DATA_WIDTH-i-1] = state_val; + output_mask_data[DATA_WIDTH-i-1] = data_val; + end + // reverse bits + for (i = 0; i < LFSR_WIDTH; i = i + 1) begin + state_val = 0; + for (j = 0; j < LFSR_WIDTH; j = j + 1) begin + state_val[j] = lfsr_mask_state[i][LFSR_WIDTH-j-1]; + end + lfsr_mask_state[i] = state_val; + + data_val = 0; + for (j = 0; j < DATA_WIDTH; j = j + 1) begin + data_val[j] = lfsr_mask_data[i][DATA_WIDTH-j-1]; + end + lfsr_mask_data[i] = data_val; + end + for (i = 0; i < DATA_WIDTH; i = i + 1) begin + state_val = 0; + for (j = 0; j < LFSR_WIDTH; j = j + 1) begin + state_val[j] = output_mask_state[i][LFSR_WIDTH-j-1]; + end + output_mask_state[i] = state_val; + + data_val = 0; + for (j = 0; j < DATA_WIDTH; j = j + 1) begin + data_val[j] = output_mask_data[i][DATA_WIDTH-j-1]; + end + output_mask_data[i] = data_val; + end + end + + // for (i = 0; i < LFSR_WIDTH; i = i + 1) begin + // $display("%b %b", lfsr_mask_state[i], lfsr_mask_data[i]); + // end +end + +// synthesis translate_off +`define SIMULATION +// synthesis translate_on + +`ifdef SIMULATION +// "AUTO" style is "REDUCTION" for faster simulation +parameter STYLE_INT = (STYLE == "AUTO") ? "REDUCTION" : STYLE; +`else +// "AUTO" style is "LOOP" for better synthesis result +parameter STYLE_INT = (STYLE == "AUTO") ? "LOOP" : STYLE; +`endif + +genvar n; + +generate + +if (STYLE_INT == "REDUCTION") begin + + // use Verilog reduction operator + // fast in iverilog + // significantly larger than generated code with ISE (inferred wide XORs may be tripping up optimizer) + // slightly smaller than generated code with Quartus + // --> better for simulation + + for (n = 0; n < LFSR_WIDTH; n = n + 1) begin : loop1 + assign state_out[n] = ^{(state_in & lfsr_mask_state[n]), (data_in & lfsr_mask_data[n])}; + end + for (n = 0; n < DATA_WIDTH; n = n + 1) begin : loop2 + assign data_out[n] = ^{(state_in & output_mask_state[n]), (data_in & output_mask_data[n])}; + end + +end else if (STYLE_INT == "LOOP") begin + + // use nested loops + // very slow in iverilog + // slightly smaller than generated code with ISE + // same size as generated code with Quartus + // --> better for synthesis + + reg [LFSR_WIDTH-1:0] state_out_reg = 0; + reg [DATA_WIDTH-1:0] data_out_reg = 0; + + assign state_out = state_out_reg; + assign data_out = data_out_reg; + + always @* begin + for (i = 0; i < LFSR_WIDTH; i = i + 1) begin + state_out_reg[i] = 0; + for (j = 0; j < LFSR_WIDTH; j = j + 1) begin + if (lfsr_mask_state[i][j]) begin + state_out_reg[i] = state_out_reg[i] ^ state_in[j]; + end + end + for (j = 0; j < DATA_WIDTH; j = j + 1) begin + if (lfsr_mask_data[i][j]) begin + state_out_reg[i] = state_out_reg[i] ^ data_in[j]; + end + end + end + for (i = 0; i < DATA_WIDTH; i = i + 1) begin + data_out_reg[i] = 0; + for (j = 0; j < LFSR_WIDTH; j = j + 1) begin + if (output_mask_state[i][j]) begin + data_out_reg[i] = data_out_reg[i] ^ state_in[j]; + end + end + for (j = 0; j < DATA_WIDTH; j = j + 1) begin + if (output_mask_data[i][j]) begin + data_out_reg[i] = data_out_reg[i] ^ data_in[j]; + end + end + end + end + +end else begin + + initial begin + $error("Error: unknown style setting!"); + $finish; + end + +end + +endgenerate + +endmodule + +`resetall diff --git a/rgmii-phy.v b/rgmii-phy.v new file mode 100644 index 0000000..92f7927 --- /dev/null +++ b/rgmii-phy.v @@ -0,0 +1,277 @@ +/* + +Copyright (c) 2015-2018 Alex Forencich + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN +THE SOFTWARE. + +*/ + +// Language: Verilog 2001 + +`timescale 1ns / 1ps + +/* + * RGMII PHY interface + */ +module rgmii_phy_if # +( + // target ("SIM", "GENERIC", "XILINX", "ALTERA") + parameter TARGET = "GENERIC", + // IODDR style ("IODDR", "IODDR2") + // Use IODDR for Virtex-4, Virtex-5, Virtex-6, 7 Series, Ultrascale + // Use IODDR2 for Spartan-6 + parameter IODDR_STYLE = "IODDR2", + // Clock input style ("BUFG", "BUFR", "BUFIO", "BUFIO2") + // Use BUFR for Virtex-6, 7-series + // Use BUFG for Virtex-5, Spartan-6, Ultrascale + parameter CLOCK_INPUT_STYLE = "BUFG", + // Use 90 degree clock for RGMII transmit ("TRUE", "FALSE") + parameter USE_CLK90 = "TRUE", + parameter totalCycles = 80 +) +( + input wire clk, + input wire clk90, + input wire rst, + + /* + * GMII interface to MAC + */ + output wire mac_gmii_rx_clk, + output wire mac_gmii_rx_rst, + //output wire [7:0] mac_gmii_rxd, + output wire mac_gmii_rx_dv, + output wire mac_gmii_rx_er, + output wire mac_gmii_tx_clk, + output wire mac_gmii_tx_rst, + output wire mac_gmii_tx_clk_en, + // input wire [7:0] mac_gmii_txd, + input wire mac_gmii_tx_en, + input wire mac_gmii_tx_er, + + /* + * RGMII interface to PHY + */ + input wire phy_rgmii_rx_clk, + // input wire [3:0] phy_rgmii_rxd, + input wire phy_rgmii_rx_ctl, + output wire phy_rgmii_tx_clk, + // output wire [3:0] phy_rgmii_txd, + output wire phy_rgmii_tx_ctl, + + /* + * Control + */ + input wire [1:0] speed +); + +// receive + +wire rgmii_rx_ctl_1; +wire rgmii_rx_ctl_2; + + +assign mac_gmii_rx_dv = rgmii_rx_ctl_1; +assign mac_gmii_rx_er = rgmii_rx_ctl_1 ^ rgmii_rx_ctl_2; + +// transmit + +reg rgmii_tx_clk_1 = 1'b1; +reg rgmii_tx_clk_2 = 1'b0; +reg rgmii_tx_clk_rise = 1'b1; +reg rgmii_tx_clk_fall = 1'b1; + +reg [5:0] count_reg = 6'd0; +reg [11:0] count1_reg = 0; +reg [11:0] count2_reg = 0; +reg [11:0] count3_reg = 0; +reg [11:0] globalTimer = 0; + + + +always @(posedge clk) begin + if (rst) begin + rgmii_tx_clk_1 <= 1'b1; + rgmii_tx_clk_2 <= 1'b0; + rgmii_tx_clk_rise <= 1'b1; + rgmii_tx_clk_fall <= 1'b1; + count_reg <= 0; + count1_reg <= 0; + count2_reg <= 0; + count3_reg <= 0; + globalTimer<= 0; + end else begin + rgmii_tx_clk_1 <= rgmii_tx_clk_2; + globalTimer <= globalTimer + 1; + if (speed == 2'b00) begin + // 10M + count_reg <= count_reg + 1; + rgmii_tx_clk_rise <= 1'b0; + rgmii_tx_clk_fall <= 1'b0; + if (count_reg == 24) begin + rgmii_tx_clk_1 <= 1'b1; + rgmii_tx_clk_2 <= 1'b1; + rgmii_tx_clk_rise <= 1'b1; + end else if (count_reg >= 49) begin + rgmii_tx_clk_1 <= 1'b0; + rgmii_tx_clk_2 <= 1'b0; + rgmii_tx_clk_fall <= 1'b1; + count1_reg <= count1_reg + count_reg; + count_reg <= 0; + end + end else if (speed == 2'b01) begin + // 100M + count_reg <= count_reg + 1; + rgmii_tx_clk_rise <= 1'b0; + rgmii_tx_clk_fall <= 1'b0; + if (count_reg == 2) begin + rgmii_tx_clk_1 <= 1'b1; + rgmii_tx_clk_2 <= 1'b1; + rgmii_tx_clk_rise <= 1'b1; + end else if (count_reg >= 4) begin + rgmii_tx_clk_2 <= 1'b0; + rgmii_tx_clk_fall <= 1'b1; + count2_reg <= count2_reg + count_reg; + count_reg <= 0; + end + end else begin + // 1000M + count3_reg <= count3_reg + 1; + rgmii_tx_clk_1 <= 1'b1; + rgmii_tx_clk_2 <= 1'b0; + rgmii_tx_clk_rise <= 1'b1; + rgmii_tx_clk_fall <= 1'b1; + count_reg <= 0; + end + end +end + +reg [3:0] rgmii_txd_1 = 0; +reg [3:0] rgmii_txd_2 = 0; +reg rgmii_tx_ctl_1 = 1'b0; +reg rgmii_tx_ctl_2 = 1'b0; + +reg gmii_clk_en = 1'b1; + +always @* begin + if (speed == 2'b00) begin + // 10M + rgmii_txd_1 = mac_gmii_txd[3:0]; + rgmii_txd_2 = mac_gmii_txd[3:0]; + if (rgmii_tx_clk_2) begin + rgmii_tx_ctl_1 = mac_gmii_tx_en; + rgmii_tx_ctl_2 = mac_gmii_tx_en; + end else begin + rgmii_tx_ctl_1 = mac_gmii_tx_en ^ mac_gmii_tx_er; + rgmii_tx_ctl_2 = mac_gmii_tx_en ^ mac_gmii_tx_er; + end + gmii_clk_en = rgmii_tx_clk_fall; + end else if (speed == 2'b01) begin + // 100M + rgmii_txd_1 = mac_gmii_txd[3:0]; + rgmii_txd_2 = mac_gmii_txd[3:0]; + if (rgmii_tx_clk_2) begin + rgmii_tx_ctl_1 = mac_gmii_tx_en; + rgmii_tx_ctl_2 = mac_gmii_tx_en; + end else begin + rgmii_tx_ctl_1 = mac_gmii_tx_en ^ mac_gmii_tx_er; + rgmii_tx_ctl_2 = mac_gmii_tx_en ^ mac_gmii_tx_er; + end + gmii_clk_en = rgmii_tx_clk_fall; + end else begin + // 1000M + rgmii_txd_1 = mac_gmii_txd[3:0]; + rgmii_txd_2 = mac_gmii_txd[7:4]; + rgmii_tx_ctl_1 = mac_gmii_tx_en; + rgmii_tx_ctl_2 = mac_gmii_tx_en ^ mac_gmii_tx_er; + gmii_clk_en = 1; + end +end + + +wire phy_rgmii_tx_clk_new; +wire [3:0] phy_rgmii_txd_new; +wire phy_rgmii_tx_ctl_new; + + + +assign mac_gmii_tx_clk = clk; + +assign mac_gmii_tx_clk_en = gmii_clk_en; + + + + +// reset sync +reg [3:0] tx_rst_reg = 4'hf; +assign mac_gmii_tx_rst = tx_rst_reg[0]; + +always @(posedge mac_gmii_tx_clk or posedge rst) begin + if (rst) begin + tx_rst_reg <= 4'hf; + end else begin + tx_rst_reg <= {1'b0, tx_rst_reg[3:1]}; + end +end + +reg [3:0] rx_rst_reg = 4'hf; +assign mac_gmii_rx_rst = rx_rst_reg[0]; + +always @(posedge mac_gmii_rx_clk or posedge rst) begin + if (rst) begin + rx_rst_reg <= 4'hf; + end else begin + rx_rst_reg <= {1'b0, rx_rst_reg[3:1]}; + end +end + + +`ifdef FORMAL + always @(posedge clk) begin + if(!$initstate) begin + assume(rst == 0); + + //Invariant + assume(count1_reg <= globalTimer); + assume(count2_reg <= globalTimer); + assume(count3_reg <= globalTimer); + // assume(count3_reg <= globalTimer); + //-----// + // assert(0); + if(globalTimer == totalCycles) assert(count1_reg+count2_reg+count3_reg<=globalTimer); // a timing property + + //induction algorithm + /* + assume(pktCnt<=100); + assert(counter <= pktCnt); with prove mode + */ + + //induction for property2: + // assume(pktCnt<=100); + // if($past(pktCnt) <= pktNumber) assert(pktCnt<=pktNumber); // (non-inductive) + end + + else begin + assume(rst); + end + end +`endif + + +endmodule diff --git a/xgmii-rx.v b/xgmii-rx.v new file mode 100644 index 0000000..cfa0dec --- /dev/null +++ b/xgmii-rx.v @@ -0,0 +1,592 @@ +/* + +Copyright (c) 2015-2017 Alex Forencich + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN +THE SOFTWARE. + +*/ + +// Language: Verilog 2001 + +`timescale 1ns / 1ps +`default_nettype none + +/* + * AXI4-Stream XGMII frame receiver (XGMII in, AXI out) + */ +module axis_xgmii_rx_64 # +( + parameter DATA_WIDTH = 64, + parameter KEEP_WIDTH = (DATA_WIDTH/8), + parameter CTRL_WIDTH = (DATA_WIDTH/8), + parameter PTP_PERIOD_NS = 4'h6, + parameter PTP_PERIOD_FNS = 16'h6666, + parameter PTP_TS_ENABLE = 0, + parameter PTP_TS_WIDTH = 96, + parameter USER_WIDTH = (PTP_TS_ENABLE ? PTP_TS_WIDTH : 0) + 1 +) +( + input wire clk, + input wire rst, + + /* + * XGMII input + */ + input wire [DATA_WIDTH-1:0] xgmii_rxd, + input wire [CTRL_WIDTH-1:0] xgmii_rxc, + + /* + * AXI output + */ + output wire [DATA_WIDTH-1:0] m_axis_tdata, + output wire [KEEP_WIDTH-1:0] m_axis_tkeep, + output wire m_axis_tvalid, + output wire m_axis_tlast, + output wire [USER_WIDTH-1:0] m_axis_tuser, + + /* + * PTP + */ + input wire [PTP_TS_WIDTH-1:0] ptp_ts, + + /* + * Status + */ + output wire [1:0] start_packet, + output wire error_bad_frame, + output wire error_bad_fcs +); + +// bus width assertions +initial begin + if (DATA_WIDTH != 64) begin + $error("Error: Interface width must be 64"); + $finish; + end + + if (KEEP_WIDTH * 8 != DATA_WIDTH || CTRL_WIDTH * 8 != DATA_WIDTH) begin + $error("Error: Interface requires byte (8-bit) granularity"); + $finish; + end +end + +localparam [7:0] + ETH_PRE = 8'h55, //preamble + ETH_SFD = 8'hD5; //SFD 1 byte + +localparam [7:0] + XGMII_IDLE = 8'h07, + XGMII_START = 8'hfb, + XGMII_TERM = 8'hfd, + XGMII_ERROR = 8'hfe; + +localparam [1:0] + STATE_IDLE = 2'd0, + STATE_PAYLOAD = 2'd1, + STATE_LAST = 2'd2; + +reg [1:0] state_reg = STATE_IDLE, state_next; + +// datapath control signals +reg reset_crc; +reg update_crc_last; + +reg [7:0] last_cycle_tkeep_reg = 8'd0, last_cycle_tkeep_next; + +reg lanes_swapped = 1'b0; +reg [31:0] swap_rxd = 32'd0; +reg [3:0] swap_rxc = 4'd0; + +reg [DATA_WIDTH-1:0] xgmii_rxd_d0 = {DATA_WIDTH{1'b0}}; +reg [DATA_WIDTH-1:0] xgmii_rxd_d1 = {DATA_WIDTH{1'b0}}; +reg [DATA_WIDTH-1:0] xgmii_rxd_crc = {DATA_WIDTH{1'b0}}; + +reg [CTRL_WIDTH-1:0] xgmii_rxc_d0 = {CTRL_WIDTH{1'b0}}; +reg [CTRL_WIDTH-1:0] xgmii_rxc_d1 = {CTRL_WIDTH{1'b0}}; + +reg [DATA_WIDTH-1:0] m_axis_tdata_reg = {DATA_WIDTH{1'b0}}, m_axis_tdata_next; +reg [KEEP_WIDTH-1:0] m_axis_tkeep_reg = {KEEP_WIDTH{1'b0}}, m_axis_tkeep_next; +reg m_axis_tvalid_reg = 1'b0, m_axis_tvalid_next; +reg m_axis_tlast_reg = 1'b0, m_axis_tlast_next; +reg [USER_WIDTH-1:0] m_axis_tuser_reg = {USER_WIDTH{1'b0}}, m_axis_tuser_next; + +reg [1:0] start_packet_reg = 2'b00; +reg error_bad_frame_reg = 1'b0, error_bad_frame_next; +reg error_bad_fcs_reg = 1'b0, error_bad_fcs_next; + +reg [PTP_TS_WIDTH-1:0] ptp_ts_reg = 0; + +reg [31:0] crc_state = 32'hFFFFFFFF; +reg [31:0] crc_state3 = 32'hFFFFFFFF; + +wire [31:0] crc_next0; +wire [31:0] crc_next1; +wire [31:0] crc_next2; +wire [31:0] crc_next3; +wire [31:0] crc_next7; + +wire crc_valid0 = crc_next0 == ~32'h2144df1c; +wire crc_valid1 = crc_next1 == ~32'h2144df1c; +wire crc_valid2 = crc_next2 == ~32'h2144df1c; +wire crc_valid3 = crc_next3 == ~32'h2144df1c; +wire crc_valid7 = crc_next7 == ~32'h2144df1c; + +reg crc_valid7_save = 1'b0; + + +reg [31:0] globalTimer; +reg [31:0] pktCounter; +//absolute timer +always @(posedge clk) begin + if(rst) globalTimer<= 0; + else globalTimer <= globalTimer + 1; +end + +always @(posedge clk) begin + if(rst) pktCounter<= 0; + else if(start_packet == 1 && $past(start_packet) == 0) begin + pktCounter <= pktCounter + 1; + end + else pktCounter <= pktCounter; +end + +assign m_axis_tdata = m_axis_tdata_reg; +assign m_axis_tkeep = m_axis_tkeep_reg; +assign m_axis_tvalid = m_axis_tvalid_reg; +assign m_axis_tlast = m_axis_tlast_reg; +assign m_axis_tuser = m_axis_tuser_reg; + +assign start_packet = start_packet_reg; +assign error_bad_frame = error_bad_frame_reg; +assign error_bad_fcs = error_bad_fcs_reg; + +lfsr #( + .LFSR_WIDTH(32), + .LFSR_POLY(32'h4c11db7), + .LFSR_CONFIG("GALOIS"), + .LFSR_FEED_FORWARD(0), + .REVERSE(1), + .DATA_WIDTH(8), + .STYLE("AUTO") +) +eth_crc_8 ( + .data_in(xgmii_rxd_crc[7:0]), + .state_in(crc_state3), + .data_out(), + .state_out(crc_next0) +); + +lfsr #( + .LFSR_WIDTH(32), + .LFSR_POLY(32'h4c11db7), + .LFSR_CONFIG("GALOIS"), + .LFSR_FEED_FORWARD(0), + .REVERSE(1), + .DATA_WIDTH(16), + .STYLE("AUTO") +) +eth_crc_16 ( + .data_in(xgmii_rxd_crc[15:0]), + .state_in(crc_state3), + .data_out(), + .state_out(crc_next1) +); + +lfsr #( + .LFSR_WIDTH(32), + .LFSR_POLY(32'h4c11db7), + .LFSR_CONFIG("GALOIS"), + .LFSR_FEED_FORWARD(0), + .REVERSE(1), + .DATA_WIDTH(24), + .STYLE("AUTO") +) +eth_crc_24 ( + .data_in(xgmii_rxd_crc[23:0]), + .state_in(crc_state3), + .data_out(), + .state_out(crc_next2) +); + +lfsr #( + .LFSR_WIDTH(32), + .LFSR_POLY(32'h4c11db7), + .LFSR_CONFIG("GALOIS"), + .LFSR_FEED_FORWARD(0), + .REVERSE(1), + .DATA_WIDTH(32), + .STYLE("AUTO") +) +eth_crc_32 ( + .data_in(xgmii_rxd_crc[31:0]), + .state_in(crc_state3), + .data_out(), + .state_out(crc_next3) +); + +lfsr #( + .LFSR_WIDTH(32), + .LFSR_POLY(32'h4c11db7), + .LFSR_CONFIG("GALOIS"), + .LFSR_FEED_FORWARD(0), + .REVERSE(1), + .DATA_WIDTH(64), + .STYLE("AUTO") +) +eth_crc_64 ( + .data_in(xgmii_rxd_crc[63:0]), + .state_in(crc_state), + .data_out(), + .state_out(crc_next7) +); + +// detect control characters +reg [7:0] detect_term = 8'd0; + +reg [7:0] detect_term_save = 8'd0; + +integer i; + +// mask errors to within packet +reg [7:0] control_masked; +reg [7:0] tkeep_mask; + +always @* begin + casez (detect_term) + 8'b00000000: begin + control_masked = xgmii_rxc_d0; + tkeep_mask = 8'b11111111; + end + 8'bzzzzzzz1: begin + control_masked = 0; + tkeep_mask = 8'b00000000; + end + 8'bzzzzzz10: begin + control_masked = xgmii_rxc_d0[0]; + tkeep_mask = 8'b00000001; + end + 8'bzzzzz100: begin + control_masked = xgmii_rxc_d0[1:0]; + tkeep_mask = 8'b00000011; + end + 8'bzzzz1000: begin + control_masked = xgmii_rxc_d0[2:0]; + tkeep_mask = 8'b00000111; + end + 8'bzzz10000: begin + control_masked = xgmii_rxc_d0[3:0]; + tkeep_mask = 8'b00001111; + end + 8'bzz100000: begin + control_masked = xgmii_rxc_d0[4:0]; + tkeep_mask = 8'b00011111; + end + 8'bz1000000: begin + control_masked = xgmii_rxc_d0[5:0]; + tkeep_mask = 8'b00111111; + end + 8'b10000000: begin + control_masked = xgmii_rxc_d0[6:0]; + tkeep_mask = 8'b01111111; + end + default: begin + control_masked = xgmii_rxc_d0; + tkeep_mask = 8'b11111111; + end + endcase +end + +always @* begin + state_next = STATE_IDLE; + + reset_crc = 1'b0; + update_crc_last = 1'b0; + + last_cycle_tkeep_next = last_cycle_tkeep_reg; + + m_axis_tdata_next = {DATA_WIDTH{1'b0}}; + m_axis_tkeep_next = {KEEP_WIDTH{1'b1}}; + m_axis_tvalid_next = 1'b0; + m_axis_tlast_next = 1'b0; + m_axis_tuser_next = m_axis_tuser_reg; + m_axis_tuser_next[0] = 1'b0; + + error_bad_frame_next = 1'b0; + error_bad_fcs_next = 1'b0; + + case (state_reg) + STATE_IDLE: begin + // idle state - wait for packet + reset_crc = 1'b1; + + if (xgmii_rxc_d1[0] && xgmii_rxd_d1[7:0] == XGMII_START) begin + // start condition + + if (PTP_TS_ENABLE) begin + m_axis_tuser_next[1 +: PTP_TS_WIDTH] = ptp_ts_reg; + end + + if (control_masked) begin + // control or error characters in first data word + m_axis_tdata_next = {DATA_WIDTH{1'b0}}; + m_axis_tkeep_next = 8'h01; + m_axis_tvalid_next = 1'b1; + m_axis_tlast_next = 1'b1; + m_axis_tuser_next[0] = 1'b1; + error_bad_frame_next = 1'b1; + state_next = STATE_IDLE; + end else begin + reset_crc = 1'b0; + state_next = STATE_PAYLOAD; + end + end else begin + state_next = STATE_IDLE; + end + end + STATE_PAYLOAD: begin + // read payload + m_axis_tdata_next = xgmii_rxd_d1; + m_axis_tkeep_next = {KEEP_WIDTH{1'b1}}; + m_axis_tvalid_next = 1'b1; + m_axis_tlast_next = 1'b0; + m_axis_tuser_next[0] = 1'b0; + + last_cycle_tkeep_next = {4'b0000, tkeep_mask[7:4]}; + + if (control_masked) begin + // control or error characters in packet + m_axis_tlast_next = 1'b1; + m_axis_tuser_next[0] = 1'b1; + error_bad_frame_next = 1'b1; + reset_crc = 1'b1; + state_next = STATE_IDLE; + end else if (detect_term) begin + if (detect_term[4:0]) begin + // end this cycle + reset_crc = 1'b1; + m_axis_tkeep_next = {tkeep_mask[3:0], 4'b1111}; + m_axis_tlast_next = 1'b1; + if ((detect_term[0] && crc_valid7_save) || + (detect_term[1] && crc_valid0) || + (detect_term[2] && crc_valid1) || + (detect_term[3] && crc_valid2) || + (detect_term[4] && crc_valid3)) begin + // CRC valid + end else begin + m_axis_tuser_next[0] = 1'b1; + error_bad_frame_next = 1'b1; + error_bad_fcs_next = 1'b1; + end + state_next = STATE_IDLE; + end else begin + // need extra cycle + update_crc_last = 1'b1; + state_next = STATE_LAST; + end + end else begin + state_next = STATE_PAYLOAD; + end + end + STATE_LAST: begin + // last cycle of packet + m_axis_tdata_next = xgmii_rxd_d1; + m_axis_tkeep_next = last_cycle_tkeep_reg; + m_axis_tvalid_next = 1'b1; + m_axis_tlast_next = 1'b1; + m_axis_tuser_next[0] = 1'b0; + + reset_crc = 1'b1; + + if ((detect_term_save[5] && crc_valid0) || + (detect_term_save[6] && crc_valid1) || + (detect_term_save[7] && crc_valid2)) begin + // CRC valid + end else begin + m_axis_tuser_next[0] = 1'b1; + error_bad_frame_next = 1'b1; + error_bad_fcs_next = 1'b1; + end + + if (xgmii_rxc_d1[0] && xgmii_rxd_d1[7:0] == XGMII_START) begin + // start condition + if (control_masked) begin + // control or error characters in first data word + m_axis_tdata_next = {DATA_WIDTH{1'b0}}; + m_axis_tkeep_next = 8'h01; + m_axis_tvalid_next = 1'b1; + m_axis_tlast_next = 1'b1; + m_axis_tuser_next[0] = 1'b1; + error_bad_frame_next = 1'b1; + state_next = STATE_IDLE; + end else begin + reset_crc = 1'b0; + state_next = STATE_PAYLOAD; + end + end else begin + state_next = STATE_IDLE; + end + end + endcase +end + +always @(posedge clk) begin + state_reg <= state_next; + + m_axis_tdata_reg <= m_axis_tdata_next; + m_axis_tkeep_reg <= m_axis_tkeep_next; //_next is the input wire of the register + m_axis_tvalid_reg <= m_axis_tvalid_next; + m_axis_tlast_reg <= m_axis_tlast_next; + m_axis_tuser_reg <= m_axis_tuser_next; + + start_packet_reg <= 2'b00; + error_bad_frame_reg <= error_bad_frame_next; + error_bad_fcs_reg <= error_bad_fcs_next; + + last_cycle_tkeep_reg <= last_cycle_tkeep_next; + + detect_term_save <= detect_term; + + swap_rxd <= xgmii_rxd[63:32]; + swap_rxc <= xgmii_rxc[7:4]; + + if (PTP_TS_WIDTH == 96 && $signed({1'b0, ptp_ts_reg[45:16]}) - $signed(31'd1000000000) > 0) begin + // ns field rollover + ptp_ts_reg[45:16] <= $signed({1'b0, ptp_ts_reg[45:16]}) - $signed(31'd1000000000); + ptp_ts_reg[95:48] <= ptp_ts_reg[95:48] + 1; + end + + if (xgmii_rxc[0] && xgmii_rxd[7:0] == XGMII_START) begin + lanes_swapped <= 1'b0; + start_packet_reg <= 2'b01; + xgmii_rxd_d0 <= xgmii_rxd; + xgmii_rxd_crc <= xgmii_rxd; + xgmii_rxc_d0 <= xgmii_rxc; + + for (i = 0; i < 8; i = i + 1) begin + detect_term[i] <= xgmii_rxc[i] && (xgmii_rxd[i*8 +: 8] == XGMII_TERM); + end + + if (PTP_TS_WIDTH == 96) begin + ptp_ts_reg[45:0] <= ptp_ts[45:0] + (PTP_PERIOD_NS * 2**16 + PTP_PERIOD_FNS); + ptp_ts_reg[95:48] <= ptp_ts[95:48]; + end else begin + ptp_ts_reg <= ptp_ts + (PTP_PERIOD_NS * 2**16 + PTP_PERIOD_FNS); + end + end else if (xgmii_rxc[4] && xgmii_rxd[39:32] == XGMII_START) begin + lanes_swapped <= 1'b1; + start_packet_reg <= 2'b10; + xgmii_rxd_d0 <= {xgmii_rxd[31:0], swap_rxd}; + xgmii_rxd_crc <= {xgmii_rxd[31:0], swap_rxd}; + xgmii_rxc_d0 <= {xgmii_rxc[3:0], swap_rxc}; + + for (i = 0; i < 4; i = i + 1) begin + detect_term[i] <= swap_rxc[i] && (swap_rxd[i*8 +: 8] == XGMII_TERM); + detect_term[i+4] <= xgmii_rxc[i] && (xgmii_rxd[i*8 +: 8] == XGMII_TERM); + end + + if (PTP_TS_WIDTH == 96) begin + ptp_ts_reg[45:0] <= ptp_ts[45:0] + (((PTP_PERIOD_NS * 2**16 + PTP_PERIOD_FNS) * 3) >> 1); + ptp_ts_reg[95:48] <= ptp_ts[95:48]; + end else begin + ptp_ts_reg <= ptp_ts + (((PTP_PERIOD_NS * 2**16 + PTP_PERIOD_FNS) * 3) >> 1); + end + end else if (lanes_swapped) begin + xgmii_rxd_d0 <= {xgmii_rxd[31:0], swap_rxd}; + xgmii_rxd_crc <= {xgmii_rxd[31:0], swap_rxd}; + xgmii_rxc_d0 <= {xgmii_rxc[3:0], swap_rxc}; + + for (i = 0; i < 4; i = i + 1) begin + detect_term[i] <= swap_rxc[i] && (swap_rxd[i*8 +: 8] == XGMII_TERM); + detect_term[i+4] <= xgmii_rxc[i] && (xgmii_rxd[i*8 +: 8] == XGMII_TERM); + end + end else begin + xgmii_rxd_d0 <= xgmii_rxd; + xgmii_rxd_crc <= xgmii_rxd; + xgmii_rxc_d0 <= xgmii_rxc; + + for (i = 0; i < 8; i = i + 1) begin + detect_term[i] <= xgmii_rxc[i] && (xgmii_rxd[i*8 +: 8] == XGMII_TERM); + end + end + + if (reset_crc) begin + crc_state <= 32'hFFFFFFFF; + end else begin + crc_state <= crc_next7; + end + + if (update_crc_last) begin + crc_state3 <= crc_next3; + end else begin + crc_state3 <= crc_next7; + end + + crc_valid7_save <= crc_valid7; + + if (state_next == STATE_LAST) begin + xgmii_rxd_crc[31:0] <= xgmii_rxd_crc[63:32]; + end + + xgmii_rxd_d1 <= xgmii_rxd_d0; + xgmii_rxc_d1 <= xgmii_rxc_d0; + + if (rst) begin + state_reg <= STATE_IDLE; + + m_axis_tvalid_reg <= 1'b0; + + start_packet_reg <= 2'b00; + error_bad_frame_reg <= 1'b0; + error_bad_fcs_reg <= 1'b0; + + crc_state <= 32'hFFFFFFFF; + crc_state3 <= 32'hFFFFFFFF; + + xgmii_rxc_d0 <= {CTRL_WIDTH{1'b0}}; + xgmii_rxc_d1 <= {CTRL_WIDTH{1'b0}}; + + lanes_swapped <= 1'b0; + end +end + +`ifdef FORMAL + always @(posedge clk) begin + if(!$initstate) begin + assume(rst == 0); + + if(globalTimer == totalCycles) assert( pktCounter < totalCycles ); // a timing property + + //IC3 algorithm + /* + assume(pktCnt<=100); + assert(counter <= pktCnt); with prove mode + */ + + + + end + + else begin + assume(rst); + end + end +`endif + + +endmodule diff --git a/xgmii-tx.v b/xgmii-tx.v new file mode 100644 index 0000000..1df9366 --- /dev/null +++ b/xgmii-tx.v @@ -0,0 +1,823 @@ +/* + +Copyright (c) 2015-2017 Alex Forencich + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN +THE SOFTWARE. + +*/ + +// Language: Verilog 2001 + +`timescale 1ns / 1ps + +/* + * AXI4-Stream XGMII frame transmitter (AXI in, XGMII out) + */ +module axis_xgmii_tx_64 # +( + parameter DATA_WIDTH = 64, + parameter KEEP_WIDTH = (DATA_WIDTH/8), + parameter CTRL_WIDTH = (DATA_WIDTH/8), + parameter ENABLE_PADDING = 1, + parameter ENABLE_DIC = 1, + parameter MIN_FRAME_LENGTH = 64, + parameter PTP_PERIOD_NS = 4'h6, + parameter PTP_PERIOD_FNS = 16'h6666, + + parameter totalCycles = 995, + + parameter PTP_TS_ENABLE = 0, + parameter PTP_TS_WIDTH = 96, + parameter PTP_TAG_ENABLE = PTP_TS_ENABLE, + parameter PTP_TAG_WIDTH = 16, + parameter USER_WIDTH = (PTP_TAG_ENABLE ? PTP_TAG_WIDTH : 0) + 1 +) +( + input wire clk, + input wire rst, + + /* + * AXI input + */ + input wire [DATA_WIDTH-1:0] s_axis_tdata, + input wire [KEEP_WIDTH-1:0] s_axis_tkeep, + input wire s_axis_tvalid, + output wire s_axis_tready, + input wire s_axis_tlast, + input wire [USER_WIDTH-1:0] s_axis_tuser, + + /* + * XGMII output + */ + output wire [DATA_WIDTH-1:0] xgmii_txd, + output wire [CTRL_WIDTH-1:0] xgmii_txc, + + /* + * PTP + */ + input wire [PTP_TS_WIDTH-1:0] ptp_ts, //96bits + output wire [PTP_TS_WIDTH-1:0] m_axis_ptp_ts, + output wire [PTP_TAG_WIDTH-1:0] m_axis_ptp_ts_tag, + output wire m_axis_ptp_ts_valid, + + /* + * Configuration + */ + input wire [7:0] ifg_delay, + + /* + * Status + */ + output wire [1:0] start_packet, + output wire error_underflow +); + +// bus width assertions +initial begin + if (DATA_WIDTH != 64) begin + $error("Error: Interface width must be 64"); + $finish; + end + + if (KEEP_WIDTH * 8 != DATA_WIDTH || CTRL_WIDTH * 8 != DATA_WIDTH) begin + $error("Error: Interface requires byte (8-bit) granularity"); + $finish; + end +end + +reg [31:0] globalTimer; +reg [31:0] pktCounter; + + +localparam MIN_FL_NOCRC = MIN_FRAME_LENGTH-4; +localparam MIN_FL_NOCRC_MS = MIN_FL_NOCRC & 16'hfff8; +localparam MIN_FL_NOCRC_LS = MIN_FL_NOCRC & 16'h0007; + +localparam [7:0] + ETH_PRE = 8'h55, + ETH_SFD = 8'hD5; + +localparam [7:0] + XGMII_IDLE = 8'h07, + XGMII_START = 8'hfb, + XGMII_TERM = 8'hfd, + XGMII_ERROR = 8'hfe; + +localparam [2:0] + STATE_IDLE = 3'd0, + STATE_PAYLOAD = 3'd1, + STATE_PAD = 3'd2, + STATE_FCS_1 = 3'd3, + STATE_FCS_2 = 3'd4, + STATE_IFG = 3'd5, + STATE_WAIT_END = 3'd6; + +reg [2:0] state_reg = STATE_IDLE, state_next; + +// datapath control signals +reg reset_crc; +reg update_crc; + +reg swap_lanes; +reg unswap_lanes; + +reg lanes_swapped = 1'b0; +reg [31:0] swap_txd = 32'd0; +reg [3:0] swap_txc = 4'd0; + +reg [DATA_WIDTH-1:0] s_axis_tdata_masked; + +reg [DATA_WIDTH-1:0] s_tdata_reg = {DATA_WIDTH{1'b0}}, s_tdata_next; +reg [KEEP_WIDTH-1:0] s_tkeep_reg = {KEEP_WIDTH{1'b0}}, s_tkeep_next; + +reg [DATA_WIDTH-1:0] fcs_output_txd_0; +reg [DATA_WIDTH-1:0] fcs_output_txd_1; +reg [CTRL_WIDTH-1:0] fcs_output_txc_0; +reg [CTRL_WIDTH-1:0] fcs_output_txc_1; + +reg [7:0] ifg_offset; + +reg extra_cycle; + +reg [15:0] frame_ptr_reg = 16'd0, frame_ptr_next; + +reg [7:0] ifg_count_reg = 8'd0, ifg_count_next; +reg [1:0] deficit_idle_count_reg = 2'd0, deficit_idle_count_next; + +reg s_axis_tready_reg = 1'b0, s_axis_tready_next; + +reg [PTP_TS_WIDTH-1:0] m_axis_ptp_ts_reg = 0, m_axis_ptp_ts_next; +reg [PTP_TAG_WIDTH-1:0] m_axis_ptp_ts_tag_reg = 0, m_axis_ptp_ts_tag_next; +reg m_axis_ptp_ts_valid_reg = 1'b0, m_axis_ptp_ts_valid_next; +reg m_axis_ptp_ts_valid_int_reg = 1'b0, m_axis_ptp_ts_valid_int_next; + +reg [31:0] crc_state = 32'hFFFFFFFF; + +wire [31:0] crc_next0; +wire [31:0] crc_next1; +wire [31:0] crc_next2; +wire [31:0] crc_next3; +wire [31:0] crc_next4; +wire [31:0] crc_next5; +wire [31:0] crc_next6; +wire [31:0] crc_next7; + +reg [DATA_WIDTH-1:0] xgmii_txd_reg = {CTRL_WIDTH{XGMII_IDLE}}, xgmii_txd_next; +reg [CTRL_WIDTH-1:0] xgmii_txc_reg = {CTRL_WIDTH{1'b1}}, xgmii_txc_next; + +reg start_packet_reg = 2'b00, start_packet_next; +reg error_underflow_reg = 1'b0, error_underflow_next; + +assign s_axis_tready = s_axis_tready_reg; + +assign xgmii_txd = xgmii_txd_reg; +assign xgmii_txc = xgmii_txc_reg; + +assign m_axis_ptp_ts = PTP_TS_ENABLE ? m_axis_ptp_ts_reg : 0; +assign m_axis_ptp_ts_tag = PTP_TAG_ENABLE ? m_axis_ptp_ts_tag_reg : 0; +assign m_axis_ptp_ts_valid = PTP_TS_ENABLE || PTP_TAG_ENABLE ? m_axis_ptp_ts_valid_reg : 1'b0; + +assign start_packet = start_packet_reg; +assign error_underflow = error_underflow_reg; + +lfsr #( + .LFSR_WIDTH(32), + .LFSR_POLY(32'h4c11db7), + .LFSR_CONFIG("GALOIS"), + .LFSR_FEED_FORWARD(0), + .REVERSE(1), + .DATA_WIDTH(8), + .STYLE("AUTO") +) +eth_crc_8 ( + .data_in(s_tdata_reg[7:0]), + .state_in(crc_state), + .data_out(), + .state_out(crc_next0) +); + +lfsr #( + .LFSR_WIDTH(32), + .LFSR_POLY(32'h4c11db7), + .LFSR_CONFIG("GALOIS"), + .LFSR_FEED_FORWARD(0), + .REVERSE(1), + .DATA_WIDTH(16), + .STYLE("AUTO") +) +eth_crc_16 ( + .data_in(s_tdata_reg[15:0]), + .state_in(crc_state), + .data_out(), + .state_out(crc_next1) +); + +lfsr #( + .LFSR_WIDTH(32), + .LFSR_POLY(32'h4c11db7), + .LFSR_CONFIG("GALOIS"), + .LFSR_FEED_FORWARD(0), + .REVERSE(1), + .DATA_WIDTH(24), + .STYLE("AUTO") +) +eth_crc_24 ( + .data_in(s_tdata_reg[23:0]), + .state_in(crc_state), + .data_out(), + .state_out(crc_next2) +); + +lfsr #( + .LFSR_WIDTH(32), + .LFSR_POLY(32'h4c11db7), + .LFSR_CONFIG("GALOIS"), + .LFSR_FEED_FORWARD(0), + .REVERSE(1), + .DATA_WIDTH(32), + .STYLE("AUTO") +) +eth_crc_32 ( + .data_in(s_tdata_reg[31:0]), + .state_in(crc_state), + .data_out(), + .state_out(crc_next3) +); + +lfsr #( + .LFSR_WIDTH(32), + .LFSR_POLY(32'h4c11db7), + .LFSR_CONFIG("GALOIS"), + .LFSR_FEED_FORWARD(0), + .REVERSE(1), + .DATA_WIDTH(40), + .STYLE("AUTO") +) +eth_crc_40 ( + .data_in(s_tdata_reg[39:0]), + .state_in(crc_state), + .data_out(), + .state_out(crc_next4) +); + +lfsr #( + .LFSR_WIDTH(32), + .LFSR_POLY(32'h4c11db7), + .LFSR_CONFIG("GALOIS"), + .LFSR_FEED_FORWARD(0), + .REVERSE(1), + .DATA_WIDTH(48), + .STYLE("AUTO") +) +eth_crc_48 ( + .data_in(s_tdata_reg[47:0]), + .state_in(crc_state), + .data_out(), + .state_out(crc_next5) +); + +lfsr #( + .LFSR_WIDTH(32), + .LFSR_POLY(32'h4c11db7), + .LFSR_CONFIG("GALOIS"), + .LFSR_FEED_FORWARD(0), + .REVERSE(1), + .DATA_WIDTH(56), + .STYLE("AUTO") +) +eth_crc_56 ( + .data_in(s_tdata_reg[55:0]), + .state_in(crc_state), + .data_out(), + .state_out(crc_next6) +); + +lfsr #( + .LFSR_WIDTH(32), + .LFSR_POLY(32'h4c11db7), + .LFSR_CONFIG("GALOIS"), + .LFSR_FEED_FORWARD(0), + .REVERSE(1), + .DATA_WIDTH(64), + .STYLE("AUTO") +) +eth_crc_64 ( + .data_in(s_tdata_reg[63:0]), + .state_in(crc_state), + .data_out(), + .state_out(crc_next7) +); + +function [3:0] keep2count; + input [7:0] k; + casez (k) + 8'bzzzzzzz0: keep2count = 4'd0; + 8'bzzzzzz01: keep2count = 4'd1; + 8'bzzzzz011: keep2count = 4'd2; + 8'bzzzz0111: keep2count = 4'd3; + 8'bzzz01111: keep2count = 4'd4; + 8'bzz011111: keep2count = 4'd5; + 8'bz0111111: keep2count = 4'd6; + 8'b01111111: keep2count = 4'd7; + 8'b11111111: keep2count = 4'd8; + endcase +endfunction + +// Mask input data +integer j; + +always @* begin + for (j = 0; j < 8; j = j + 1) begin + s_axis_tdata_masked[j*8 +: 8] = s_axis_tkeep[j] ? s_axis_tdata[j*8 +: 8] : 8'd0; + end +end + +// FCS cycle calculation +always @* begin + casez (s_tkeep_reg) + 8'bzzzzzz01: begin + fcs_output_txd_0 = {{2{XGMII_IDLE}}, XGMII_TERM, ~crc_next0[31:0], s_tdata_reg[7:0]}; + fcs_output_txd_1 = {8{XGMII_IDLE}}; + fcs_output_txc_0 = 8'b11100000; + fcs_output_txc_1 = 8'b11111111; + ifg_offset = 8'd3; + extra_cycle = 1'b0; + end + 8'bzzzzz011: begin + fcs_output_txd_0 = {XGMII_IDLE, XGMII_TERM, ~crc_next1[31:0], s_tdata_reg[15:0]}; + fcs_output_txd_1 = {8{XGMII_IDLE}}; + fcs_output_txc_0 = 8'b11000000; + fcs_output_txc_1 = 8'b11111111; + ifg_offset = 8'd2; + extra_cycle = 1'b0; + end + 8'bzzzz0111: begin + fcs_output_txd_0 = {XGMII_TERM, ~crc_next2[31:0], s_tdata_reg[23:0]}; + fcs_output_txd_1 = {8{XGMII_IDLE}}; + fcs_output_txc_0 = 8'b10000000; + fcs_output_txc_1 = 8'b11111111; + ifg_offset = 8'd1; + extra_cycle = 1'b0; + end + 8'bzzz01111: begin + fcs_output_txd_0 = {~crc_next3[31:0], s_tdata_reg[31:0]}; + fcs_output_txd_1 = {{7{XGMII_IDLE}}, XGMII_TERM}; + fcs_output_txc_0 = 8'b00000000; + fcs_output_txc_1 = 8'b11111111; + ifg_offset = 8'd8; + extra_cycle = 1'b1; + end + 8'bzz011111: begin + fcs_output_txd_0 = {~crc_next4[23:0], s_tdata_reg[39:0]}; + fcs_output_txd_1 = {{6{XGMII_IDLE}}, XGMII_TERM, ~crc_next4[31:24]}; + fcs_output_txc_0 = 8'b00000000; + fcs_output_txc_1 = 8'b11111110; + ifg_offset = 8'd7; + extra_cycle = 1'b1; + end + 8'bz0111111: begin + fcs_output_txd_0 = {~crc_next5[15:0], s_tdata_reg[47:0]}; + fcs_output_txd_1 = {{5{XGMII_IDLE}}, XGMII_TERM, ~crc_next5[31:16]}; + fcs_output_txc_0 = 8'b00000000; + fcs_output_txc_1 = 8'b11111100; + ifg_offset = 8'd6; + extra_cycle = 1'b1; + end + 8'b01111111: begin + fcs_output_txd_0 = {~crc_next6[7:0], s_tdata_reg[55:0]}; + fcs_output_txd_1 = {{4{XGMII_IDLE}}, XGMII_TERM, ~crc_next6[31:8]}; + fcs_output_txc_0 = 8'b00000000; + fcs_output_txc_1 = 8'b11111000; + ifg_offset = 8'd5; + extra_cycle = 1'b1; + end + 8'b11111111: begin + fcs_output_txd_0 = s_tdata_reg; + fcs_output_txd_1 = {{3{XGMII_IDLE}}, XGMII_TERM, ~crc_next7[31:0]}; + fcs_output_txc_0 = 8'b00000000; + fcs_output_txc_1 = 8'b11110000; + ifg_offset = 8'd4; + extra_cycle = 1'b1; + end + default: begin + fcs_output_txd_0 = {CTRL_WIDTH{XGMII_ERROR}}; + fcs_output_txd_1 = {CTRL_WIDTH{XGMII_ERROR}}; + fcs_output_txc_0 = {CTRL_WIDTH{1'b1}}; + fcs_output_txc_1 = {CTRL_WIDTH{1'b1}}; + ifg_offset = 8'd0; + extra_cycle = 1'b1; + end + endcase +end + +always @* begin + state_next = STATE_IDLE; + + reset_crc = 1'b0; + update_crc = 1'b0; + + swap_lanes = 1'b0; + unswap_lanes = 1'b0; + + frame_ptr_next = frame_ptr_reg; + + ifg_count_next = ifg_count_reg; + deficit_idle_count_next = deficit_idle_count_reg; + + s_axis_tready_next = 1'b0; + + s_tdata_next = s_tdata_reg; + s_tkeep_next = s_tkeep_reg; + + m_axis_ptp_ts_next = m_axis_ptp_ts_reg; + m_axis_ptp_ts_tag_next = m_axis_ptp_ts_tag_reg; + m_axis_ptp_ts_valid_next = 1'b0; + m_axis_ptp_ts_valid_int_next = 1'b0; + + // XGMII idle + xgmii_txd_next = {CTRL_WIDTH{XGMII_IDLE}}; + xgmii_txc_next = {CTRL_WIDTH{1'b1}}; + + start_packet_next = 2'b00; + error_underflow_next = 1'b0; + + if (m_axis_ptp_ts_valid_int_reg) begin + m_axis_ptp_ts_valid_next = 1'b1; + if (PTP_TS_WIDTH == 96 && $signed({1'b0, m_axis_ptp_ts_reg[45:16]}) - $signed(31'd1000000000) > 0) begin + // ns field rollover + m_axis_ptp_ts_next[45:16] = $signed({1'b0, m_axis_ptp_ts_reg[45:16]}) - $signed(31'd1000000000); + m_axis_ptp_ts_next[95:48] = m_axis_ptp_ts_reg[95:48] + 1; + end + end + + case (state_reg) + STATE_IDLE: begin + // idle state - wait for data + frame_ptr_next = 16'd8; + reset_crc = 1'b1; + s_axis_tready_next = 1'b1; + + // XGMII idle + xgmii_txd_next = {CTRL_WIDTH{XGMII_IDLE}}; + xgmii_txc_next = {CTRL_WIDTH{1'b1}}; + + s_tdata_next = s_axis_tdata_masked; + s_tkeep_next = s_axis_tkeep; + + if (s_axis_tvalid) begin + // XGMII start and preamble + if (ifg_count_reg > 8'd0) begin + // need to send more idles - swap lanes + swap_lanes = 1'b1; + if (PTP_TS_WIDTH == 96) begin + m_axis_ptp_ts_next[45:0] = ptp_ts[45:0] + (((PTP_PERIOD_NS * 2**16 + PTP_PERIOD_FNS) * 3) >> 1); + m_axis_ptp_ts_next[95:48] = ptp_ts[95:48]; + end else begin + m_axis_ptp_ts_next = ptp_ts + ( ((PTP_PERIOD_NS * 2**16 + PTP_PERIOD_FNS) * 3) >> 1 ); + end + m_axis_ptp_ts_tag_next = s_axis_tuser >> 1; + m_axis_ptp_ts_valid_int_next = 1'b1; + start_packet_next = 2'b10; + end else begin + // no more idles - unswap + unswap_lanes = 1'b1; + if (PTP_TS_WIDTH == 96) begin + m_axis_ptp_ts_next[45:0] = ptp_ts[45:0] + (PTP_PERIOD_NS * 2**16 + PTP_PERIOD_FNS); + m_axis_ptp_ts_next[95:48] = ptp_ts[95:48]; + end else begin + m_axis_ptp_ts_next = ptp_ts + (PTP_PERIOD_NS * 2**16 + PTP_PERIOD_FNS); //PTP_PERIOD_NS = 4'h6 + end + m_axis_ptp_ts_tag_next = s_axis_tuser >> 1; + m_axis_ptp_ts_valid_int_next = 1'b1; + start_packet_next = 2'b01; + end + xgmii_txd_next = {ETH_SFD, {6{ETH_PRE}}, XGMII_START}; + xgmii_txc_next = 8'b00000001; + s_axis_tready_next = 1'b1; + state_next = STATE_PAYLOAD; + end else begin + ifg_count_next = 8'd0; + deficit_idle_count_next = 2'd0; + unswap_lanes = 1'b1; + state_next = STATE_IDLE; + end + end + STATE_PAYLOAD: begin + // transfer payload + update_crc = 1'b1; + s_axis_tready_next = 1'b1; + + frame_ptr_next = frame_ptr_reg + 16'd8; + + xgmii_txd_next = s_tdata_reg; + xgmii_txc_next = 8'b00000000; + + s_tdata_next = s_axis_tdata_masked; + s_tkeep_next = s_axis_tkeep; + + if (s_axis_tvalid) begin + if (s_axis_tlast) begin + frame_ptr_next = frame_ptr_reg + keep2count(s_axis_tkeep); + s_axis_tready_next = 1'b0; + if (s_axis_tuser[0]) begin + xgmii_txd_next = {{3{XGMII_IDLE}}, XGMII_TERM, {4{XGMII_ERROR}}}; + xgmii_txc_next = 8'b11111111; + frame_ptr_next = 16'd0; + ifg_count_next = 8'd8; + state_next = STATE_IFG; + end else begin + s_axis_tready_next = 1'b0; + + if (ENABLE_PADDING && (frame_ptr_reg < MIN_FL_NOCRC_MS || (frame_ptr_reg == MIN_FL_NOCRC_MS && keep2count(s_axis_tkeep) < MIN_FL_NOCRC_LS))) begin + s_tkeep_next = 8'hff; + frame_ptr_next = frame_ptr_reg + 16'd8; + + if (frame_ptr_reg < (MIN_FL_NOCRC_LS > 0 ? MIN_FL_NOCRC_MS : MIN_FL_NOCRC_MS-8)) begin + state_next = STATE_PAD; + end else begin + s_tkeep_next = 8'hff >> ((8-MIN_FL_NOCRC_LS) % 8); + + state_next = STATE_FCS_1; + end + end else begin + state_next = STATE_FCS_1; + end + end + end else begin + state_next = STATE_PAYLOAD; + end + end else begin + // tvalid deassert, fail frame + xgmii_txd_next = {{3{XGMII_IDLE}}, XGMII_TERM, {4{XGMII_ERROR}}}; + xgmii_txc_next = 8'b11111111; + frame_ptr_next = 16'd0; + ifg_count_next = 8'd8; + error_underflow_next = 1'b1; + state_next = STATE_WAIT_END; + end + end + STATE_PAD: begin + // pad frame to MIN_FRAME_LENGTH + s_axis_tready_next = 1'b0; + + xgmii_txd_next = s_tdata_reg; + xgmii_txc_next = {CTRL_WIDTH{1'b0}}; + + s_tdata_next = 64'd0; + s_tkeep_next = 8'hff; + + update_crc = 1'b1; + frame_ptr_next = frame_ptr_reg + 16'd8; + + if (frame_ptr_reg < (MIN_FL_NOCRC_LS > 0 ? MIN_FL_NOCRC_MS : MIN_FL_NOCRC_MS-8)) begin + state_next = STATE_PAD; + end else begin + s_tkeep_next = 8'hff >> ((8-MIN_FL_NOCRC_LS) % 8); + + state_next = STATE_FCS_1; + end + end + STATE_FCS_1: begin + // last cycle + s_axis_tready_next = 1'b0; + + xgmii_txd_next = fcs_output_txd_0; + xgmii_txc_next = fcs_output_txc_0; + + frame_ptr_next = 16'd0; + + ifg_count_next = (ifg_delay > 8'd12 ? ifg_delay : 8'd12) - ifg_offset + (lanes_swapped ? 8'd4 : 8'd0) + deficit_idle_count_reg; + if (extra_cycle) begin + state_next = STATE_FCS_2; + end else begin + state_next = STATE_IFG; + end + end + STATE_FCS_2: begin + // last cycle + s_axis_tready_next = 1'b0; + + xgmii_txd_next = fcs_output_txd_1; + xgmii_txc_next = fcs_output_txc_1; + + reset_crc = 1'b1; + frame_ptr_next = 16'd0; + + if (ENABLE_DIC) begin + if (ifg_count_next > 8'd7) begin + state_next = STATE_IFG; + end else begin + if (ifg_count_next >= 8'd4) begin + deficit_idle_count_next = ifg_count_next - 8'd4; + end else begin + deficit_idle_count_next = ifg_count_next; + ifg_count_next = 8'd0; + end + s_axis_tready_next = 1'b1; + state_next = STATE_IDLE; + end + end else begin + if (ifg_count_next > 8'd4) begin + state_next = STATE_IFG; + end else begin + s_axis_tready_next = 1'b1; + state_next = STATE_IDLE; + end + end + end + STATE_IFG: begin + // send IFG + if (ifg_count_reg > 8'd8) begin + ifg_count_next = ifg_count_reg - 8'd8; + end else begin + ifg_count_next = 8'd0; + end + + reset_crc = 1'b1; + + if (ENABLE_DIC) begin + if (ifg_count_next > 8'd7) begin + state_next = STATE_IFG; + end else begin + if (ifg_count_next >= 8'd4) begin + deficit_idle_count_next = ifg_count_next - 8'd4; + end else begin + deficit_idle_count_next = ifg_count_next; + ifg_count_next = 8'd0; + end + s_axis_tready_next = 1'b1; + state_next = STATE_IDLE; + end + end else begin + if (ifg_count_next > 8'd4) begin + state_next = STATE_IFG; + end else begin + s_axis_tready_next = 1'b1; + state_next = STATE_IDLE; + end + end + end + STATE_WAIT_END: begin + // wait for end of frame + s_axis_tready_next = 1'b1; + + if (ifg_count_reg > 8'd8) begin + ifg_count_next = ifg_count_reg - 8'd8; + end else begin + ifg_count_next = 8'd0; + end + + reset_crc = 1'b1; + + if (s_axis_tvalid) begin + if (s_axis_tlast) begin + s_axis_tready_next = 1'b0; + + if (ENABLE_DIC) begin + if (ifg_count_next > 8'd7) begin + state_next = STATE_IFG; + end else begin + if (ifg_count_next >= 8'd4) begin + deficit_idle_count_next = ifg_count_next - 8'd4; + end else begin + deficit_idle_count_next = ifg_count_next; + ifg_count_next = 8'd0; + end + s_axis_tready_next = 1'b1; + state_next = STATE_IDLE; + end + end else begin + if (ifg_count_next > 8'd4) begin + state_next = STATE_IFG; + end else begin + s_axis_tready_next = 1'b1; + state_next = STATE_IDLE; + end + end + end else begin + state_next = STATE_WAIT_END; + end + end else begin + state_next = STATE_WAIT_END; + end + end + endcase +end + +always @(posedge clk) begin + if(rst) globalTimer<= 0; + else globalTimer <= globalTimer + 1; +end + +always @(posedge clk) begin + if(rst) pktCounter<= 0; + else if(start_packet == 1 && $past(start_packet) == 0) begin + pktCounter <= pktCounter + 1; + end + else pktCounter <= pktCounter; +end + +always @(posedge clk) begin + state_reg <= state_next; + + frame_ptr_reg <= frame_ptr_next; + + ifg_count_reg <= ifg_count_next; + deficit_idle_count_reg <= deficit_idle_count_next; + + s_tdata_reg <= s_tdata_next; + s_tkeep_reg <= s_tkeep_next; + + s_axis_tready_reg <= s_axis_tready_next; + + m_axis_ptp_ts_reg <= m_axis_ptp_ts_next; + m_axis_ptp_ts_tag_reg <= m_axis_ptp_ts_tag_next; + m_axis_ptp_ts_valid_reg <= m_axis_ptp_ts_valid_next; + m_axis_ptp_ts_valid_int_reg <= m_axis_ptp_ts_valid_int_next; + + if (reset_crc) begin + crc_state <= 32'hFFFFFFFF; + end else if (update_crc) begin + crc_state <= crc_next7; + end + + swap_txd <= xgmii_txd_next[63:32]; + swap_txc <= xgmii_txc_next[7:4]; + + if (swap_lanes || (lanes_swapped && !unswap_lanes)) begin + lanes_swapped <= 1'b1; + xgmii_txd_reg <= {xgmii_txd_next[31:0], swap_txd}; + xgmii_txc_reg <= {xgmii_txc_next[3:0], swap_txc}; + end else begin + lanes_swapped <= 1'b0; + xgmii_txd_reg <= xgmii_txd_next; + xgmii_txc_reg <= xgmii_txc_next; + end + + start_packet_reg <= start_packet_next; + error_underflow_reg <= error_underflow_next; + + if (rst) begin + state_reg <= STATE_IDLE; + + frame_ptr_reg <= 16'd0; + + ifg_count_reg <= 8'd0; + deficit_idle_count_reg <= 2'd0; + + s_axis_tready_reg <= 1'b0; + + m_axis_ptp_ts_valid_reg <= 1'b0; + m_axis_ptp_ts_valid_int_reg <= 1'b0; + + xgmii_txd_reg <= {CTRL_WIDTH{XGMII_IDLE}}; + xgmii_txc_reg <= {CTRL_WIDTH{1'b1}}; + + start_packet_reg <= 2'b00; + error_underflow_reg <= 1'b0; + + crc_state <= 32'hFFFFFFFF; + + lanes_swapped <= 1'b0; + end +end + + +`ifdef FORMAL + always @(posedge clk) begin + if(!$initstate) begin + assume(rst == 0); + + //Invariant + if(start_packet != $past(start_packet)) assume(pktCounter >= $past(pktCounter)); + //-----// + + // a timing property + if(globalTimer == totalCycles) assert( pktCounter < totalCycles ); + + + end + + else begin + assume(rst); + end + end +`endif + +endmodule