ADDED example2/rx.v
Index: example2/rx.v
==================================================================
--- /dev/null
+++ example2/rx.v
@@ -0,0 +1,649 @@
+////////////////////////////////////////////////////////////////////////////////
+//
+// Filename: rxuartlite.v
+//
+// Project: wbuart32, a full featured UART with simulator
+//
+// Purpose: Receive and decode inputs from a single UART line.
+//
+//
+// To interface with this module, connect it to your system clock,
+// and a UART input. Set the parameter to the number of clocks per
+// baud. When data becomes available, the o_wr line will be asserted
+// for one clock cycle.
+//
+// This interface only handles 8N1 serial port communications. It does
+// not handle the break, parity, or frame error conditions.
+//
+//
+// Creator: Dan Gisselquist, Ph.D.
+// Gisselquist Technology, LLC
+//
+////////////////////////////////////////////////////////////////////////////////
+//
+// Copyright (C) 2015-2020, Gisselquist Technology, LLC
+//
+// This program is free software (firmware): you can redistribute it and/or
+// modify it under the terms of the GNU General Public License as published
+// by the Free Software Foundation, either version 3 of the License, or (at
+// your option) any later version.
+//
+// This program is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
+// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
+// for more details.
+//
+// You should have received a copy of the GNU General Public License along
+// with this program. (It's in the $(ROOT)/doc directory. Run make with no
+// target there if the PDF file isn't present.) If not, see
+// for a copy.
+//
+// License: GPL, v3, as defined and found on www.gnu.org,
+// http://www.gnu.org/licenses/gpl.html
+//
+//
+////////////////////////////////////////////////////////////////////////////////
+//
+//
+`default_nettype none
+//
+`define RXUL_BIT_ZERO 4'h0
+`define RXUL_BIT_ONE 4'h1
+`define RXUL_BIT_TWO 4'h2
+`define RXUL_BIT_THREE 4'h3
+`define RXUL_BIT_FOUR 4'h4
+`define RXUL_BIT_FIVE 4'h5
+`define RXUL_BIT_SIX 4'h6
+`define RXUL_BIT_SEVEN 4'h7
+`define RXUL_STOP 4'h8
+`define RXUL_WAIT 4'h9
+`define RXUL_IDLE 4'hf
+
+module rxuartlite(i_clk, i_uart_rx, o_wr, o_data);
+ parameter TIMER_BITS = 10;
+`ifdef FORMAL
+ parameter [(TIMER_BITS-1):0] CLOCKS_PER_BAUD = 16; // Necessary for formal proof
+`else
+ parameter [(TIMER_BITS-1):0] CLOCKS_PER_BAUD = 868; // 115200 MBaud at 100MHz
+`endif
+ localparam TB = TIMER_BITS;
+ input wire i_clk;
+ input wire i_uart_rx;
+ output reg o_wr;
+ output reg [7:0] o_data;
+
+
+ wire [(TB-1):0] half_baud;
+ reg [3:0] state;
+
+ assign half_baud = { 1'b0, CLOCKS_PER_BAUD[(TB-1):1] };
+ reg [(TB-1):0] baud_counter;
+ reg zero_baud_counter;
+
+
+ // Since this is an asynchronous receiver, we need to register our
+ // input a couple of clocks over to avoid any problems with
+ // metastability. We do that here, and then ignore all but the
+ // ck_uart wire.
+ reg q_uart, qq_uart, ck_uart;
+ initial q_uart = 1'b1;
+ initial qq_uart = 1'b1;
+ initial ck_uart = 1'b1;
+ always @(posedge i_clk)
+ { ck_uart, qq_uart, q_uart } <= { qq_uart, q_uart, i_uart_rx };
+
+ // Keep track of the number of clocks since the last change.
+ //
+ // This is used to determine if we are in either a break or an idle
+ // condition, as discussed further below.
+ reg [(TB-1):0] chg_counter;
+ initial chg_counter = {(TB){1'b1}};
+ always @(posedge i_clk)
+ if (qq_uart != ck_uart)
+ chg_counter <= 0;
+ else if (chg_counter != { (TB){1'b1} })
+ chg_counter <= chg_counter + 1;
+
+ // Are we in the middle of a baud iterval? Specifically, are we
+ // in the middle of a start bit? Set this to high if so. We'll use
+ // this within our state machine to transition out of the IDLE
+ // state.
+ reg half_baud_time;
+ initial half_baud_time = 0;
+ always @(posedge i_clk)
+ half_baud_time <= (!ck_uart)&&(chg_counter >= half_baud-1'b1-1'b1);
+
+
+ initial state = `RXUL_IDLE;
+ always @(posedge i_clk)
+ if (state == `RXUL_IDLE)
+ begin // Idle state, independent of baud counter
+ // By default, just stay in the IDLE state
+ state <= `RXUL_IDLE;
+ if ((!ck_uart)&&(half_baud_time))
+ // UNLESS: We are in the center of a valid
+ // start bit
+ state <= `RXUL_BIT_ZERO;
+ end else if ((state >= `RXUL_WAIT)&&(ck_uart))
+ state <= `RXUL_IDLE;
+ else if (zero_baud_counter)
+ begin
+ if (state <= `RXUL_STOP)
+ // Data arrives least significant bit first.
+ // By the time this is clocked in, it's what
+ // you'll have.
+ state <= state + 1;
+ end
+
+ // Data bit capture logic.
+ //
+ // This is drastically simplified from the state machine above, based
+ // upon: 1) it doesn't matter what it is until the end of a captured
+ // byte, and 2) the data register will flush itself of any invalid
+ // data in all other cases. Hence, let's keep it real simple.
+ reg [7:0] data_reg;
+ always @(posedge i_clk)
+ if ((zero_baud_counter)&&(state != `RXUL_STOP))
+ data_reg <= { qq_uart, data_reg[7:1] };
+
+ // Our data bit logic doesn't need nearly the complexity of all that
+ // work above. Indeed, we only need to know if we are at the end of
+ // a stop bit, in which case we copy the data_reg into our output
+ // data register, o_data, and tell others (for one clock) that data is
+ // available.
+ //
+ initial o_wr = 1'b0;
+ initial o_data = 8'h00;
+ always @(posedge i_clk)
+ if ((zero_baud_counter)&&(state == `RXUL_STOP)&&(ck_uart))
+ begin
+ o_wr <= 1'b1;
+ o_data <= data_reg;
+ end else
+ o_wr <= 1'b0;
+
+ // The baud counter
+ //
+ // This is used as a "clock divider" if you will, but the clock needs
+ // to be reset before any byte can be decoded. In all other respects,
+ // we set ourselves up for CLOCKS_PER_BAUD counts between baud
+ // intervals.
+ initial baud_counter = 0;
+ always @(posedge i_clk)
+ if (((state==`RXUL_IDLE))&&(!ck_uart)&&(half_baud_time))
+ baud_counter <= CLOCKS_PER_BAUD-1'b1;
+ else if (state == `RXUL_WAIT)
+ baud_counter <= 0;
+ else if ((zero_baud_counter)&&(state < `RXUL_STOP))
+ baud_counter <= CLOCKS_PER_BAUD-1'b1;
+ else if (!zero_baud_counter)
+ baud_counter <= baud_counter-1'b1;
+
+ // zero_baud_counter
+ //
+ // Rather than testing whether or not (baud_counter == 0) within our
+ // (already too complicated) state transition tables, we use
+ // zero_baud_counter to pre-charge that test on the clock
+ // before--cleaning up some otherwise difficult timing dependencies.
+ initial zero_baud_counter = 1'b1;
+ always @(posedge i_clk)
+ if ((state == `RXUL_IDLE)&&(!ck_uart)&&(half_baud_time))
+ zero_baud_counter <= 1'b0;
+ else if (state == `RXUL_WAIT)
+ zero_baud_counter <= 1'b1;
+ else if ((zero_baud_counter)&&(state < `RXUL_STOP))
+ zero_baud_counter <= 1'b0;
+ else if (baud_counter == 1)
+ zero_baud_counter <= 1'b1;
+
+`ifdef FORMAL
+`define FORMAL_VERILATOR
+`else
+`ifdef VERILATOR
+`define FORMAL_VERILATOR
+`endif
+`endif
+
+`ifdef FORMAL
+`define ASSUME assume
+`define ASSERT assert
+`ifdef VERIFIC
+ (* gclk *) wire gbl_clk;
+ global clocking @(posedge gbl_clk); endclocking
+`endif
+
+
+ localparam F_CKRES = 10;
+
+ (* anyseq *) wire f_tx_start;
+ (* anyconst *) wire [(F_CKRES-1):0] f_tx_step;
+ reg f_tx_zclk;
+ reg [(TB-1):0] f_tx_timer;
+ wire [7:0] f_rx_newdata;
+ reg [(TB-1):0] f_tx_baud;
+ wire f_tx_zbaud;
+
+ wire [(TB-1):0] f_max_baud_difference;
+ reg [(TB-1):0] f_baud_difference;
+ reg [(TB+3):0] f_tx_count, f_rx_count;
+ (* anyseq *) wire [7:0] f_tx_data;
+
+
+
+ wire f_txclk;
+ reg [1:0] f_rx_clock;
+ reg [(F_CKRES-1):0] f_tx_clock;
+ reg f_past_valid, f_past_valid_tx;
+
+ initial f_past_valid = 1'b0;
+ always @(posedge i_clk)
+ f_past_valid <= 1'b1;
+
+ initial f_rx_clock = 3'h0;
+ always @($global_clock)
+ f_rx_clock <= f_rx_clock + 1'b1;
+
+ always @(*)
+ assume(i_clk == f_rx_clock[1]);
+ ///////////////////////////////////////////////////////////
+ //
+ //
+ // Generate a transmitted signal
+ //
+ //
+ ///////////////////////////////////////////////////////////
+ // First, calculate the transmit clock
+ localparam [(F_CKRES-1):0] F_MIDSTEP = { 2'b01, {(F_CKRES-2){1'b0}} };
+ //
+ // Need to allow us to slip by half a baud clock over 10 baud intervals
+ //
+ // (F_STEP / (2^F_CKRES)) * (CLOCKS_PER_BAUD)*10 < CLOCKS_PER_BAUD/2
+ // F_STEP * 2 * 10 < 2^F_CKRES
+ localparam [(F_CKRES-1):0] F_HALFSTEP= F_MIDSTEP/32;
+ localparam [(F_CKRES-1):0] F_MINSTEP = F_MIDSTEP - F_HALFSTEP + 1;
+ localparam [(F_CKRES-1):0] F_MAXSTEP = F_MIDSTEP + F_HALFSTEP - 1;
+ initial assert(F_MINSTEP <= F_MIDSTEP);
+ initial assert(F_MIDSTEP <= F_MAXSTEP);
+ // assume((f_tx_step >= F_MINSTEP)&&(f_tx_step <= F_MAXSTEP));
+ //
+ //
+ always @(*) assume((f_tx_step == F_MINSTEP)
+ ||(f_tx_step == F_MIDSTEP)
+ ||(f_tx_step == F_MAXSTEP));
+ always @($global_clock)
+ f_tx_clock <= f_tx_clock + f_tx_step;
+ assign f_txclk = f_tx_clock[F_CKRES-1];
+ //
+ initial f_past_valid_tx = 1'b0;
+ always @(posedge f_txclk)
+ f_past_valid_tx <= 1'b1;
+ initial assume(i_uart_rx);
+ //////////////////////////////////////////////
+ //
+ //
+ // Build a simulated transmitter
+ //
+ //
+ //////////////////////////////////////////////
+ //
+ // First, the simulated timing generator
+ // parameter TIMER_BITS = 10;
+ // parameter [(TIMER_BITS-1):0] CLOCKS_PER_BAUD = 868;
+ // localparam TB = TIMER_BITS;
+ always @(*)
+ if (f_tx_busy)
+ assume(!f_tx_start);
+ initial f_tx_baud = 0;
+ always @(posedge f_txclk)
+ if ((f_tx_zbaud)&&((f_tx_busy)||(f_tx_start)))
+ f_tx_baud <= CLOCKS_PER_BAUD-1'b1;
+ else if (!f_tx_zbaud)
+ f_tx_baud <= f_tx_baud - 1'b1;
+ always @(*)
+ `ASSERT(f_tx_baud < CLOCKS_PER_BAUD);
+ always @(*)
+ if (!f_tx_busy)
+ `ASSERT(f_tx_baud == 0);
+ assign f_tx_zbaud = (f_tx_baud == 0);
+ // But only if we aren't busy
+ initial assume(f_tx_data == 0);
+ always @(posedge f_txclk)
+ if ((!f_tx_zbaud)||(f_tx_busy)||(!f_tx_start))
+ assume(f_tx_data == $past(f_tx_data));
+ // Force the data to change on a clock only
+ always @($global_clock)
+ if ((f_past_valid)&&(!$rose(f_txclk)))
+ assume($stable(f_tx_data));
+ else if (f_tx_busy)
+ assume($stable(f_tx_data));
+ //
+ always @($global_clock)
+ if ((!f_past_valid)||(!$rose(f_txclk)))
+ begin
+ assume($stable(f_tx_start));
+ assume($stable(f_tx_data));
+ end
+ //
+ //
+ //
+ reg [9:0] f_tx_reg;
+ reg f_tx_busy;
+ // Here's the transmitter itself (roughly)
+ initial f_tx_busy = 1'b0;
+ initial f_tx_reg = 0;
+ always @(posedge f_txclk)
+ if (!f_tx_zbaud)
+ begin
+ `ASSERT(f_tx_busy);
+ end else begin
+ f_tx_reg <= { 1'b0, f_tx_reg[9:1] };
+ if (f_tx_start)
+ f_tx_reg <= { 1'b1, f_tx_data, 1'b0 };
+ end
+ // Create a busy flag that we'll use
+ always @(*)
+ if (!f_tx_zbaud)
+ f_tx_busy <= 1'b1;
+ else if (|f_tx_reg)
+ f_tx_busy <= 1'b1;
+ else
+ f_tx_busy <= 1'b0;
+ //
+ // Tie the TX register to the TX data
+ always @(posedge f_txclk)
+ if (f_tx_reg[9])
+ `ASSERT(f_tx_reg[8:0] == { f_tx_data, 1'b0 });
+ else if (f_tx_reg[8])
+ `ASSERT(f_tx_reg[7:0] == f_tx_data[7:0] );
+ else if (f_tx_reg[7])
+ `ASSERT(f_tx_reg[6:0] == f_tx_data[7:1] );
+ else if (f_tx_reg[6])
+ `ASSERT(f_tx_reg[5:0] == f_tx_data[7:2] );
+ else if (f_tx_reg[5])
+ `ASSERT(f_tx_reg[4:0] == f_tx_data[7:3] );
+ else if (f_tx_reg[4])
+ `ASSERT(f_tx_reg[3:0] == f_tx_data[7:4] );
+ else if (f_tx_reg[3])
+ `ASSERT(f_tx_reg[2:0] == f_tx_data[7:5] );
+ else if (f_tx_reg[2])
+ `ASSERT(f_tx_reg[1:0] == f_tx_data[7:6] );
+ else if (f_tx_reg[1])
+ `ASSERT(f_tx_reg[0] == f_tx_data[7]);
+ // Our counter since we start
+ initial f_tx_count = 0;
+ always @(posedge f_txclk)
+ if (!f_tx_busy)
+ f_tx_count <= 0;
+ else
+ f_tx_count <= f_tx_count + 1'b1;
+ always @(*)
+ if (f_tx_reg == 10'h0)
+ assume(i_uart_rx);
+ else
+ assume(i_uart_rx == f_tx_reg[0]);
+ //
+ // Make sure the absolute transmit clock timer matches our state
+ //
+ always @(posedge f_txclk)
+ if (!f_tx_busy)
+ begin
+ if ((!f_past_valid_tx)||(!$past(f_tx_busy)))
+ `ASSERT(f_tx_count == 0);
+ end else if (f_tx_reg[9])
+ `ASSERT(f_tx_count ==
+ CLOCKS_PER_BAUD -1 -f_tx_baud);
+ else if (f_tx_reg[8])
+ `ASSERT(f_tx_count ==
+ 2 * CLOCKS_PER_BAUD -1 -f_tx_baud);
+ else if (f_tx_reg[7])
+ `ASSERT(f_tx_count ==
+ 3 * CLOCKS_PER_BAUD -1 -f_tx_baud);
+ else if (f_tx_reg[6])
+ `ASSERT(f_tx_count ==
+ 4 * CLOCKS_PER_BAUD -1 -f_tx_baud);
+ else if (f_tx_reg[5])
+ `ASSERT(f_tx_count ==
+ 5 * CLOCKS_PER_BAUD -1 -f_tx_baud);
+ else if (f_tx_reg[4])
+ `ASSERT(f_tx_count ==
+ 6 * CLOCKS_PER_BAUD -1 -f_tx_baud);
+ else if (f_tx_reg[3])
+ `ASSERT(f_tx_count ==
+ 7 * CLOCKS_PER_BAUD -1 -f_tx_baud);
+ else if (f_tx_reg[2])
+ `ASSERT(f_tx_count ==
+ 8 * CLOCKS_PER_BAUD -1 -f_tx_baud);
+ else if (f_tx_reg[1])
+ `ASSERT(f_tx_count ==
+ 9 * CLOCKS_PER_BAUD -1 -f_tx_baud);
+ else if (f_tx_reg[0])
+ `ASSERT(f_tx_count ==
+ 10 * CLOCKS_PER_BAUD -1 -f_tx_baud);
+ else
+ `ASSERT(f_tx_count ==
+ 11 * CLOCKS_PER_BAUD -1 -f_tx_baud);
+ ///////////////////////////////////////
+ //
+ // Receiver
+ //
+ ///////////////////////////////////////
+ //
+ // Count RX clocks since the start of the first stop bit, measured in
+ // rx clocks
+ initial f_rx_count = 0;
+ always @(posedge i_clk)
+ if (state == `RXUL_IDLE)
+ f_rx_count = (!ck_uart) ? (chg_counter+2) : 0;
+ else
+ f_rx_count <= f_rx_count + 1'b1;
+ always @(posedge i_clk)
+ if (state == 0)
+ `ASSERT(f_rx_count
+ == half_baud + (CLOCKS_PER_BAUD-baud_counter));
+ else if (state == 1)
+ `ASSERT(f_rx_count == half_baud + 2 * CLOCKS_PER_BAUD
+ - baud_counter);
+ else if (state == 2)
+ `ASSERT(f_rx_count == half_baud + 3 * CLOCKS_PER_BAUD
+ - baud_counter);
+ else if (state == 3)
+ `ASSERT(f_rx_count == half_baud + 4 * CLOCKS_PER_BAUD
+ - baud_counter);
+ else if (state == 4)
+ `ASSERT(f_rx_count == half_baud + 5 * CLOCKS_PER_BAUD
+ - baud_counter);
+ else if (state == 5)
+ `ASSERT(f_rx_count == half_baud + 6 * CLOCKS_PER_BAUD
+ - baud_counter);
+ else if (state == 6)
+ `ASSERT(f_rx_count == half_baud + 7 * CLOCKS_PER_BAUD
+ - baud_counter);
+ else if (state == 7)
+ `ASSERT(f_rx_count == half_baud + 8 * CLOCKS_PER_BAUD
+ - baud_counter);
+ else if (state == 8)
+ `ASSERT((f_rx_count == half_baud + 9 * CLOCKS_PER_BAUD
+ - baud_counter)
+ ||(f_rx_count == half_baud + 10 * CLOCKS_PER_BAUD
+ - baud_counter));
+ always @(*)
+ `ASSERT( ((!zero_baud_counter)
+ &&(state == `RXUL_IDLE)
+ &&(baud_counter == 0))
+ ||((zero_baud_counter)&&(baud_counter == 0))
+ ||((!zero_baud_counter)&&(baud_counter != 0)));
+ always @(posedge i_clk)
+ if (!f_past_valid)
+ `ASSERT((state == `RXUL_IDLE)&&(baud_counter == 0)
+ &&(zero_baud_counter));
+ always @(*)
+ begin
+ `ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h2);
+ `ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h4);
+ `ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h5);
+ `ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h6);
+ `ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h9);
+ `ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'ha);
+ `ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'hb);
+ `ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'hd);
+ end
+ always @(posedge i_clk)
+ if ((f_past_valid)&&($past(state) >= `RXUL_WAIT)&&($past(ck_uart)))
+ `ASSERT(state == `RXUL_IDLE);
+ always @(posedge i_clk)
+ if ((f_past_valid)&&($past(state) >= `RXUL_WAIT)
+ &&(($past(state) != `RXUL_IDLE)||(state == `RXUL_IDLE)))
+ `ASSERT(zero_baud_counter);
+ // Calculate an absolute value of the difference between the two baud
+ // clocks
+ always @(posedge i_clk)
+ if ((f_past_valid)&&($past(state)==`RXUL_IDLE)&&(state == `RXUL_IDLE))
+ begin
+ `ASSERT(($past(ck_uart))
+ ||(chg_counter <=
+ { 1'b0, CLOCKS_PER_BAUD[(TB-1):1] }));
+ end
+ always @(posedge f_txclk)
+ if (!f_past_valid_tx)
+ `ASSERT((state == `RXUL_IDLE)&&(baud_counter == 0)
+ &&(zero_baud_counter)&&(!f_tx_busy));
+ wire [(TB+3):0] f_tx_count_two_clocks_ago;
+ assign f_tx_count_two_clocks_ago = f_tx_count - 2;
+ always @(*)
+ if (f_tx_count >= f_rx_count + 2)
+ f_baud_difference = f_tx_count_two_clocks_ago - f_rx_count;
+ else
+ f_baud_difference = f_rx_count - f_tx_count_two_clocks_ago;
+ localparam F_SYNC_DLY = 8;
+ reg [(TB+4+F_CKRES-1):0] f_sub_baud_difference;
+ reg [F_CKRES-1:0] ck_tx_clock;
+ reg [((F_SYNC_DLY-1)*F_CKRES)-1:0] q_tx_clock;
+ reg [TB+3:0] ck_tx_count;
+ reg [(F_SYNC_DLY-1)*(TB+4)-1:0] q_tx_count;
+ initial q_tx_count = 0;
+ initial ck_tx_count = 0;
+ initial q_tx_clock = 0;
+ initial ck_tx_clock = 0;
+ always @($global_clock)
+ { ck_tx_clock, q_tx_clock } <= { q_tx_clock, f_tx_clock };
+ always @($global_clock)
+ { ck_tx_count, q_tx_count } <= { q_tx_count, f_tx_count };
+ reg [TB+4+F_CKRES-1:0] f_ck_tx_time, f_rx_time;
+ always @(*)
+ f_ck_tx_time = { ck_tx_count, !ck_tx_clock[F_CKRES-1],
+ ck_tx_clock[F_CKRES-2:0] };
+ always @(*)
+ f_rx_time = { f_rx_count, !f_rx_clock[1], f_rx_clock[0],
+ {(F_CKRES-2){1'b0}} };
+ reg [TB+4+F_CKRES-1:0] f_signed_difference;
+ always @(*)
+ f_signed_difference = f_ck_tx_time - f_rx_time;
+ always @(*)
+ if (f_signed_difference[TB+4+F_CKRES-1])
+ f_sub_baud_difference = -f_signed_difference;
+ else
+ f_sub_baud_difference = f_signed_difference;
+ always @($global_clock)
+ if (state == `RXUL_WAIT)
+ `ASSERT((!f_tx_busy)||(f_tx_reg[9:1] == 0));
+ always @($global_clock)
+ if (state == `RXUL_IDLE)
+ begin
+ `ASSERT((!f_tx_busy)||(f_tx_reg[9])||(f_tx_reg[9:1]==0));
+ if (!ck_uart)
+ ;//`PHASE_TWO_ASSERT((f_rx_count < 4)||(f_sub_baud_difference <= ((CLOCKS_PER_BAUD< 6))
+ // assert(i_uart_rx == ck_uart);
+ // Make sure the data register matches
+ always @(posedge i_clk)
+ // if ((f_past_valid)&&(state != $past(state)))
+ begin
+ if (state == 4'h0)
+ `ASSERT(!data_reg[7]);
+ if (state == 4'h1)
+ `ASSERT((data_reg[7]
+ == $past(f_tx_data[0]))&&(!data_reg[6]));
+ if (state == 4'h2)
+ `ASSERT(data_reg[7:6]
+ == $past(f_tx_data[1:0]));
+ if (state == 4'h3)
+ `ASSERT(data_reg[7:5] == $past(f_tx_data[2:0]));
+ if (state == 4'h4)
+ `ASSERT(data_reg[7:4] == $past(f_tx_data[3:0]));
+ if (state == 4'h5)
+ `ASSERT(data_reg[7:3] == $past(f_tx_data[4:0]));
+ if (state == 4'h6)
+ `ASSERT(data_reg[7:2] == $past(f_tx_data[5:0]));
+ if (state == 4'h7)
+ `ASSERT(data_reg[7:1] == $past(f_tx_data[6:0]));
+ if (state == 4'h8)
+ `ASSERT(data_reg[7:0] == $past(f_tx_data[7:0]));
+ end
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Cover properties
+ //
+ ////////////////////////////////////////////////////////////////////////
+ //
+ always @(posedge i_clk)
+ cover(o_wr); // Step 626, takes about 20mins
+ always @(posedge i_clk)
+ begin
+ cover(!ck_uart);
+ cover((f_past_valid)&&($rose(ck_uart))); // 82
+ cover((zero_baud_counter)&&(state == `RXUL_BIT_ZERO)); // 110
+ cover((zero_baud_counter)&&(state == `RXUL_BIT_ONE)); // 174
+ cover((zero_baud_counter)&&(state == `RXUL_BIT_TWO)); // 238
+ cover((zero_baud_counter)&&(state == `RXUL_BIT_THREE));// 302
+ cover((zero_baud_counter)&&(state == `RXUL_BIT_FOUR)); // 366
+ cover((zero_baud_counter)&&(state == `RXUL_BIT_FIVE)); // 430
+ cover((zero_baud_counter)&&(state == `RXUL_BIT_SIX)); // 494
+ cover((zero_baud_counter)&&(state == `RXUL_BIT_SEVEN));// 558
+ cover((zero_baud_counter)&&(state == `RXUL_STOP)); // 622
+ cover((zero_baud_counter)&&(state == `RXUL_WAIT)); // 626
+ end
+`endif
+`ifdef FORMAL_VERILATOR
+ // FORMAL properties which can be tested via Verilator as well as
+ // Yosys FORMAL
+ always @(*)
+ assert((state == 4'hf)||(state <= `RXUL_WAIT));
+ always @(*)
+ assert(zero_baud_counter == (baud_counter == 0)? 1'b1:1'b0);
+ always @(*)
+ assert(baud_counter <= CLOCKS_PER_BAUD-1'b1);
+`endif
+endmodule
ADDED example2/tx.v
Index: example2/tx.v
==================================================================
--- /dev/null
+++ example2/tx.v
@@ -0,0 +1,434 @@
+
+////////////////////////////////////////////////////////////////////////////////
+//
+// Filename: txuartlite.v
+//
+// Project: wbuart32, a full featured UART with simulator
+//
+// Purpose: Transmit outputs over a single UART line. This particular UART
+// implementation has been extremely simplified: it does not handle
+// generating break conditions, nor does it handle anything other than the
+// 8N1 (8 data bits, no parity, 1 stop bit) UART sub-protocol.
+//
+// To interface with this module, connect it to your system clock, and
+// pass it the byte of data you wish to transmit. Strobe the i_wr line
+// high for one cycle, and your data will be off. Wait until the 'o_busy'
+// line is low before strobing the i_wr line again--this implementation
+// has NO BUFFER, so strobing i_wr while the core is busy will just
+// get ignored. The output will be placed on the o_txuart output line.
+//
+// (I often set both data and strobe on the same clock, and then just leave
+// them set until the busy line is low. Then I move on to the next piece
+// of data.)
+//
+// Creator: Dan Gisselquist, Ph.D.
+// Gisselquist Technology, LLC
+//
+////////////////////////////////////////////////////////////////////////////////
+//
+// Copyright (C) 2015-2020, Gisselquist Technology, LLC
+//
+// This program is free software (firmware): you can redistribute it and/or
+// modify it under the terms of the GNU General Public License as published
+// by the Free Software Foundation, either version 3 of the License, or (at
+// your option) any later version.
+//
+// This program is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
+// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
+// for more details.
+//
+// You should have received a copy of the GNU General Public License along
+// with this program. (It's in the $(ROOT)/doc directory. Run make with no
+// target there if the PDF file isn't present.) If not, see
+// for a copy.
+//
+// License: GPL, v3, as defined and found on www.gnu.org,
+// http://www.gnu.org/licenses/gpl.html
+//
+//
+////////////////////////////////////////////////////////////////////////////////
+//
+//
+`default_nettype none
+//
+`define TXUL_BIT_ZERO 4'h0
+`define TXUL_BIT_ONE 4'h1
+`define TXUL_BIT_TWO 4'h2
+`define TXUL_BIT_THREE 4'h3
+`define TXUL_BIT_FOUR 4'h4
+`define TXUL_BIT_FIVE 4'h5
+`define TXUL_BIT_SIX 4'h6
+`define TXUL_BIT_SEVEN 4'h7
+`define TXUL_STOP 4'h8
+`define TXUL_IDLE 4'hf
+//
+//
+module txuartlite(i_clk, i_wr, i_data, o_uart_tx, o_busy);
+ parameter [4:0] TIMING_BITS = 5'd24;
+ localparam TB = TIMING_BITS;
+ parameter [(TB-1):0] CLOCKS_PER_BAUD = 8; // 24'd868;
+ input wire i_clk;
+ input wire i_wr;
+ input wire [7:0] i_data;
+ // And the UART input line itself
+ output reg o_uart_tx;
+ // A line to tell others when we are ready to accept data. If
+ // (i_wr)&&(!o_busy) is ever true, then the core has accepted a byte
+ // for transmission.
+ output wire o_busy;
+
+ reg [(TB-1):0] baud_counter;
+ reg [3:0] state;
+ reg [7:0] lcl_data;
+ reg r_busy, zero_baud_counter;
+
+ // Big state machine controlling: r_busy, state
+ // {{{
+ //
+ initial r_busy = 1'b1;
+ initial state = `TXUL_IDLE;
+ always @(posedge i_clk)
+ begin
+ if (!zero_baud_counter)
+ // r_busy needs to be set coming into here
+ r_busy <= 1'b1;
+ else if (state > `TXUL_STOP) // STATE_IDLE
+ begin
+ state <= `TXUL_IDLE;
+ r_busy <= 1'b0;
+ if ((i_wr)&&(!r_busy))
+ begin // Immediately start us off with a start bit
+ r_busy <= 1'b1;
+ state <= `TXUL_BIT_ZERO;
+ end
+ end else begin
+ // One clock tick in each of these states ...
+ r_busy <= 1'b1;
+ if (state <=`TXUL_STOP) // start bit, 8-d bits, stop-b
+ state <= state + 1'b1;
+ else
+ state <= `TXUL_IDLE;
+ end
+ end
+ // }}}
+
+ // o_busy
+ // {{{
+ //
+ // This is a wire, designed to be true is we are ever busy above.
+ // originally, this was going to be true if we were ever not in the
+ // idle state. The logic has since become more complex, hence we have
+ // a register dedicated to this and just copy out that registers value.
+ assign o_busy = (r_busy);
+ // }}}
+
+
+ // lcl_data
+ // {{{
+ //
+ // This is our working copy of the i_data register which we use
+ // when transmitting. It is only of interest during transmit, and is
+ // allowed to be whatever at any other time. Hence, if r_busy isn't
+ // true, we can always set it. On the one clock where r_busy isn't
+ // true and i_wr is, we set it and r_busy is true thereafter.
+ // Then, on any zero_baud_counter (i.e. change between baud intervals)
+ // we simple logically shift the register right to grab the next bit.
+ initial lcl_data = 8'hff;
+ always @(posedge i_clk)
+ if ((i_wr)&&(!r_busy))
+ lcl_data <= i_data;
+ else if (zero_baud_counter)
+ lcl_data <= { 1'b1, lcl_data[7:1] };
+ // }}}
+
+ // o_uart_tx
+ // {{{
+ //
+ // This is the final result/output desired of this core. It's all
+ // centered about o_uart_tx. This is what finally needs to follow
+ // the UART protocol.
+ //
+ initial o_uart_tx = 1'b1;
+ always @(posedge i_clk)
+ if ((i_wr)&&(!r_busy))
+ o_uart_tx <= 1'b0; // Set the start bit on writes
+ else if (zero_baud_counter) // Set the data bit.
+ o_uart_tx <= lcl_data[0];
+ // }}}
+
+ // Baud counter
+ // {{{
+ // All of the above logic is driven by the baud counter. Bits must last
+ // CLOCKS_PER_BAUD in length, and this baud counter is what we use to
+ // make certain of that.
+ //
+ // The basic logic is this: at the beginning of a bit interval, start
+ // the baud counter and set it to count CLOCKS_PER_BAUD. When it gets
+ // to zero, restart it.
+ //
+ // However, comparing a 28'bit number to zero can be rather complex--
+ // especially if we wish to do anything else on that same clock. For
+ // that reason, we create "zero_baud_counter". zero_baud_counter is
+ // nothing more than a flag that is true anytime baud_counter is zero.
+ // It's true when the logic (above) needs to step to the next bit.
+ // Simple enough?
+ //
+ // I wish we could stop there, but there are some other (ugly)
+ // conditions to deal with that offer exceptions to this basic logic.
+ //
+ // 1. When the user has commanded a BREAK across the line, we need to
+ // wait several baud intervals following the break before we start
+ // transmitting, to give any receiver a chance to recognize that we are
+ // out of the break condition, and to know that the next bit will be
+ // a stop bit.
+ //
+ // 2. A reset is similar to a break condition--on both we wait several
+ // baud intervals before allowing a start bit.
+ //
+ // 3. In the idle state, we stop our counter--so that upon a request
+ // to transmit when idle we can start transmitting immediately, rather
+ // than waiting for the end of the next (fictitious and arbitrary) baud
+ // interval.
+ //
+ // When (i_wr)&&(!r_busy)&&(state == `TXUL_IDLE) then we're not only in
+ // the idle state, but we also just accepted a command to start writing
+ // the next word. At this point, the baud counter needs to be reset
+ // to the number of CLOCKS_PER_BAUD, and zero_baud_counter set to zero.
+ //
+ // The logic is a bit twisted here, in that it will only check for the
+ // above condition when zero_baud_counter is false--so as to make
+ // certain the STOP bit is complete.
+ initial zero_baud_counter = 1'b1;
+ initial baud_counter = 0;
+ always @(posedge i_clk)
+ begin
+ zero_baud_counter <= (baud_counter == 1);
+ if (state == `TXUL_IDLE)
+ begin
+ baud_counter <= 0;
+ zero_baud_counter <= 1'b1;
+ if ((i_wr)&&(!r_busy))
+ begin
+ baud_counter <= CLOCKS_PER_BAUD - 1'b1;
+ zero_baud_counter <= 1'b0;
+ end
+ end else if ((zero_baud_counter)&&(state == 4'h9))
+ begin
+ baud_counter <= 0;
+ zero_baud_counter <= 1'b1;
+ end else if (!zero_baud_counter)
+ baud_counter <= baud_counter - 1'b1;
+ else
+ baud_counter <= CLOCKS_PER_BAUD - 1'b1;
+ end
+ // }}}
+//
+//
+// FORMAL METHODS
+//
+//
+//
+`ifdef FORMAL
+
+`ifdef TXUARTLITE
+`define ASSUME assume
+`else
+`define ASSUME assert
+`endif
+
+ // Setup
+ // {{{
+ reg f_past_valid, f_last_clk;
+
+ initial f_past_valid = 1'b0;
+ always @(posedge i_clk)
+ f_past_valid <= 1'b1;
+
+ initial `ASSUME(!i_wr);
+ always @(posedge i_clk)
+ if ((f_past_valid)&&($past(i_wr))&&($past(o_busy)))
+ begin
+ `ASSUME(i_wr == $past(i_wr));
+ `ASSUME(i_data == $past(i_data));
+ end
+ // }}}
+
+ // Check the baud counter
+ // {{{
+ always @(posedge i_clk)
+ assert(zero_baud_counter == (baud_counter == 0));
+
+ always @(posedge i_clk)
+ if ((f_past_valid)&&($past(baud_counter != 0))&&($past(state != `TXUL_IDLE)))
+ assert(baud_counter == $past(baud_counter - 1'b1));
+
+ always @(posedge i_clk)
+ if ((f_past_valid)&&(!$past(zero_baud_counter))&&($past(state != `TXUL_IDLE)))
+ assert($stable(o_uart_tx));
+
+ reg [(TB-1):0] f_baud_count;
+ initial f_baud_count = 1'b0;
+ always @(posedge i_clk)
+ if (zero_baud_counter)
+ f_baud_count <= 0;
+ else
+ f_baud_count <= f_baud_count + 1'b1;
+
+ always @(posedge i_clk)
+ assert(f_baud_count < CLOCKS_PER_BAUD);
+
+ always @(posedge i_clk)
+ if (baud_counter != 0)
+ assert(o_busy);
+ // }}}
+
+ reg [9:0] f_txbits;
+ // {{{
+ initial f_txbits = 0;
+ always @(posedge i_clk)
+ if (zero_baud_counter)
+ f_txbits <= { o_uart_tx, f_txbits[9:1] };
+
+ always @(posedge i_clk)
+ if ((f_past_valid)&&(!$past(zero_baud_counter))
+ &&(!$past(state==`TXUL_IDLE)))
+ assert(state == $past(state));
+
+ reg [3:0] f_bitcount;
+ initial f_bitcount = 0;
+ always @(posedge i_clk)
+ if ((!f_past_valid)||(!$past(f_past_valid)))
+ f_bitcount <= 0;
+ else if ((state == `TXUL_IDLE)&&(zero_baud_counter))
+ f_bitcount <= 0;
+ else if (zero_baud_counter)
+ f_bitcount <= f_bitcount + 1'b1;
+
+ always @(posedge i_clk)
+ assert(f_bitcount <= 4'ha);
+
+ reg [7:0] f_request_tx_data;
+ always @(posedge i_clk)
+ if ((i_wr)&&(!o_busy))
+ f_request_tx_data <= i_data;
+
+ wire [3:0] subcount;
+ assign subcount = 10-f_bitcount;
+ always @(posedge i_clk)
+ if (f_bitcount > 0)
+ assert(!f_txbits[subcount]);
+
+ always @(posedge i_clk)
+ if (f_bitcount == 4'ha)
+ begin
+ assert(f_txbits[8:1] == f_request_tx_data);
+ assert( f_txbits[9]);
+ end
+
+ always @(posedge i_clk)
+ assert((state <= `TXUL_STOP + 1'b1)||(state == `TXUL_IDLE));
+
+ always @(posedge i_clk)
+ if ((f_past_valid)&&($past(f_past_valid))&&($past(o_busy)))
+ cover(!o_busy);
+ // }}}
+
+`endif // FORMAL
+`ifdef VERIFIC_SVA
+ reg [7:0] fsv_data;
+
+ //
+ // Grab a copy of the data any time we are sent a new byte to transmit
+ // We'll use this in a moment to compare the item transmitted against
+ // what is supposed to be transmitted
+ //
+ always @(posedge i_clk)
+ if ((i_wr)&&(!o_busy))
+ fsv_data <= i_data;
+
+ //
+ // One baud interval
+ // {{{
+ //
+ // 1. The UART output is constant at DAT
+ // 2. The internal state remains constant at ST
+ // 3. CKS = the number of clocks per bit.
+ //
+ // Everything stays constant during the CKS clocks with the exception
+ // of (zero_baud_counter), which is *only* raised on the last clock
+ // interval
+ sequence BAUD_INTERVAL(CKS, DAT, SR, ST);
+ ((o_uart_tx == DAT)&&(state == ST)
+ &&(lcl_data == SR)
+ &&(!zero_baud_counter))[*(CKS-1)]
+ ##1 (o_uart_tx == DAT)&&(state == ST)
+ &&(lcl_data == SR)
+ &&(zero_baud_counter);
+ endsequence
+ // }}}
+
+ //
+ // One byte transmitted
+ // {{{
+ //
+ // DATA = the byte that is sent
+ // CKS = the number of clocks per bit
+ //
+ sequence SEND(CKS, DATA);
+ BAUD_INTERVAL(CKS, 1'b0, DATA, 4'h0)
+ ##1 BAUD_INTERVAL(CKS, DATA[0], {{(1){1'b1}},DATA[7:1]}, 4'h1)
+ ##1 BAUD_INTERVAL(CKS, DATA[1], {{(2){1'b1}},DATA[7:2]}, 4'h2)
+ ##1 BAUD_INTERVAL(CKS, DATA[2], {{(3){1'b1}},DATA[7:3]}, 4'h3)
+ ##1 BAUD_INTERVAL(CKS, DATA[3], {{(4){1'b1}},DATA[7:4]}, 4'h4)
+ ##1 BAUD_INTERVAL(CKS, DATA[4], {{(5){1'b1}},DATA[7:5]}, 4'h5)
+ ##1 BAUD_INTERVAL(CKS, DATA[5], {{(6){1'b1}},DATA[7:6]}, 4'h6)
+ ##1 BAUD_INTERVAL(CKS, DATA[6], {{(7){1'b1}},DATA[7:7]}, 4'h7)
+ ##1 BAUD_INTERVAL(CKS, DATA[7], 8'hff, 4'h8)
+ ##1 BAUD_INTERVAL(CKS, 1'b1, 8'hff, 4'h9);
+ endsequence
+ // }}}
+
+ //
+ // Transmit one byte
+ // {{{
+ // Once the byte is transmitted, make certain we return to
+ // idle
+ //
+ assert property (
+ @(posedge i_clk)
+ (i_wr)&&(!o_busy)
+ |=> ((o_busy) throughout SEND(CLOCKS_PER_BAUD,fsv_data))
+ ##1 (!o_busy)&&(o_uart_tx)&&(zero_baud_counter));
+ // }}}
+
+ // {{{
+ assume property (
+ @(posedge i_clk)
+ (i_wr)&&(o_busy) |=>
+ (i_wr)&&(o_busy)&&($stable(i_data)));
+
+ //
+ // Make certain that o_busy is true any time zero_baud_counter is
+ // non-zero
+ //
+ always @(*)
+ assert((o_busy)||(zero_baud_counter) );
+
+ // If and only if zero_baud_counter is true, baud_counter must be zero
+ // Insist on that relationship here.
+ always @(*)
+ assert(zero_baud_counter == (baud_counter == 0));
+
+ // To make certain baud_counter stays below CLOCKS_PER_BAUD
+ always @(*)
+ assert(baud_counter < CLOCKS_PER_BAUD);
+
+ //
+ // Insist that we are only ever in a valid state
+ always @(*)
+ assert((state <= `TXUL_STOP+1'b1)||(state == `TXUL_IDLE));
+ // }}}
+
+`endif // Verific SVA
+endmodule