Stucked at UART formal verification

[feiphung]

I have already added so many assert() at https://github.com/promach/UART/blob/development/rtl/test_UART.v , but during induction test, formal verification tool leads me straight to https://i.imgur.com/GNUAl7z.png which is the second last state during UART receiving mechanism at line 258 ?

Line 258 is about verifying the parity bit received against the parity value calculated from the received data, however, my coding failed this assert() test.

I am not sure what other assert() I should add before parity assertion. Could anyone advise ?

module test_UART(clk, reset, serial_out, enable, i_data, o_busy, received_data, data_is_valid, rx_error);

parameter INPUT_DATA_WIDTH = 8;
parameter PARITY_ENABLED = 1;
parameter PARITY_TYPE = 0;  // 0 = even parity, 1 = odd parity

input clk;
input reset;

// transmitter signals
input enable;
input [(INPUT_DATA_WIDTH-1):0] i_data;
output o_busy;
output serial_out;

`ifdef FORMAL
wire baud_clk;
wire [(INPUT_DATA_WIDTH+PARITY_ENABLED+1):0] shift_reg;  // Tx internal PISO
`endif

// receiver signals
wire serial_in;
output reg data_is_valid;
output reg rx_error;
output reg [(INPUT_DATA_WIDTH-1):0] received_data;

`ifdef FORMAL
localparam NUMBER_OF_BITS = INPUT_DATA_WIDTH + 3;   // 1 start bit, 8 data bits, 1 parity bit, 1 stop bit
wire [($clog2(NUMBER_OF_BITS)-1) : 0] state;  // for Rx
`endif

UART uart(.clk(clk), .reset(reset), .serial_out(serial_out), .enable(enable), .i_data(i_data), .o_busy(o_busy), .serial_in(serial_in), .received_data(received_data), .data_is_valid(data_is_valid), .rx_error(rx_error)
`ifdef FORMAL
	, .state(state), .baud_clk(baud_clk), .shift_reg(shift_reg)
`endif
);

assign serial_in = serial_out; // tx goes to rx, so that we know that our UART works at least in terms of logic-wise

`ifdef FORMAL

localparam Rx_IDLE       = 4'b0000;
localparam Rx_START_BIT  = 4'b0001;
localparam Rx_DATA_BIT_0 = 4'b0010;
localparam Rx_DATA_BIT_1 = 4'b0011;
localparam Rx_DATA_BIT_2 = 4'b0100;
localparam Rx_DATA_BIT_3 = 4'b0101;
localparam Rx_DATA_BIT_4 = 4'b0110;
localparam Rx_DATA_BIT_5 = 4'b0111;
localparam Rx_DATA_BIT_6 = 4'b1000;
localparam Rx_DATA_BIT_7 = 4'b1001;
localparam Rx_PARITY_BIT = 4'b1010;
localparam Rx_STOP_BIT   = 4'b1011;

localparam NUMBER_OF_RX_SYNCHRONIZERS = 3; // three FF synhronizers for clock domain crossing
localparam CLOCKS_PER_BIT = 8;

reg had_been_enabled;   // a signal to latch 'enable'
reg[($clog2(NUMBER_OF_BITS + NUMBER_OF_RX_SYNCHRONIZERS)-1) : 0] cnt;  // to track the number of clock cycles incurred between assertion of 'transmission_had_started' signal from Tx and assertion of 'data_is_valid' signal from Rx

reg transmission_had_started; 
reg had_just_reset;
reg first_clock_passed;

initial begin
	had_been_enabled = 0;  
	cnt = 0;
	transmission_had_started = 0;
	had_just_reset = 0;
	first_clock_passed = 0;
end

always @(posedge clk)
begin
	first_clock_passed <= 1;
end


wire [($clog2(NUMBER_OF_BITS-1)-1) : 0] stop_bit_location;
assign stop_bit_location = (cnt < NUMBER_OF_BITS) ? (NUMBER_OF_BITS - 1 - cnt) : 0;  // if not during UART transmission, set to zero as default for no specific reason

wire [($clog2(NUMBER_OF_BITS)-1) : 0] stop_bit_location_plus_one = stop_bit_location + 1;

always @(posedge clk)
begin
	assert(cnt < NUMBER_OF_BITS + NUMBER_OF_RX_SYNCHRONIZERS + 1);
	assert(stop_bit_location < NUMBER_OF_BITS);
	
	if(($past(first_clock_passed) == 0) && (first_clock_passed == 1)) begin
		assert($past(stop_bit_location) == (NUMBER_OF_BITS-1));
		assert($past(&shift_reg) == 1);
	end
end

always @(posedge clk)
begin
    if(reset) begin
        cnt <= 0;
    	had_been_enabled <= 0;
		transmission_had_started <= 0;
    end

	else if(baud_clk) begin
		if(transmission_had_started) begin
			cnt <= cnt + 1;
		end
		transmission_had_started <= had_been_enabled;  // Tx only operates at every rising edge of 'baud_clk' (Tx's clock)
	end    

    else begin
 
        if(enable && (!had_been_enabled)) begin
    	    cnt <= 0;
    	    assert(cnt == 0);            
    	    had_been_enabled <= 1;
    	    assert(state == Rx_IDLE);
    	    assert(data_is_valid == 0);
    	    
    	    if(had_just_reset) begin
    	    	assert(&shift_reg == 1);
    	    end
    	    
	    	assert(serial_out == 1);
	    	assert(o_busy == 0);
        end

    	else if(transmission_had_started) begin

			if(cnt == 0) begin // start of UART transmission
				assert(state < Rx_STOP_BIT);
				assert(data_is_valid == 0);
				assert(shift_reg == {1'b0, 1'b1, (^i_data), i_data});  // ^data is even parity bit
				assert(serial_out == 0);   // start bit
				assert(o_busy == 1);
			end
			
			else if((cnt > 0) && (cnt < (NUMBER_OF_BITS-1))) begin  // during UART transmission
				assert(state < Rx_STOP_BIT);
				assert(data_is_valid == 0);
				assert(shift_reg[stop_bit_location_plus_one] == 1'b0);
				assert(shift_reg[stop_bit_location] == 1'b1);
				assert(o_busy == 1);				
			end

			else if(cnt == (NUMBER_OF_BITS - 1)) begin // end of UART transmission
				assert(state < Rx_STOP_BIT);
				assert(data_is_valid == 0);
				assert(shift_reg == 0);
				assert(serial_out == 1);   // stop bit
				assert(o_busy == 1);
			end
			
			else begin // if(cnt > ((NUMBER_OF_BITS + 1)*CLOCKS_PER_BIT)) begin  // UART Rx internal states
				
				if(state == Rx_START_BIT) begin
					assert(data_is_valid == 0);
					assert(serial_in == 0);
					assert(o_busy == 1);
					assert(cnt == (NUMBER_OF_BITS + NUMBER_OF_RX_SYNCHRONIZERS + 1)*CLOCKS_PER_BIT);					
				end

				else if((state > Rx_START_BIT) && (state < Rx_PARITY_BIT)) begin // data bits
					assert(data_is_valid == 1);
					assert(o_busy == 1);
					assert(cnt == (NUMBER_OF_BITS + NUMBER_OF_RX_SYNCHRONIZERS + (state - Rx_START_BIT) +  1)*CLOCKS_PER_BIT);					
				end
	
				else if(state == Rx_PARITY_BIT) begin
					assert(data_is_valid == 0);
					assert(serial_in == ^i_data);
					assert(o_busy == 1);
					assert(cnt == (NUMBER_OF_BITS + NUMBER_OF_RX_SYNCHRONIZERS + state +  1)*CLOCKS_PER_BIT);					
				end
						
				else begin // if(state == Rx_STOP_BIT) begin  // end of one UART transaction (both transmitting and receiving)
					assert(state == Rx_STOP_BIT);
					assert(data_is_valid == 1);
					assert(serial_in == 1);
					assert(o_busy == 0);
					assert(cnt == (NUMBER_OF_BITS + NUMBER_OF_RX_SYNCHRONIZERS + 1)*CLOCKS_PER_BIT);
					cnt <= 0;
					had_been_enabled <= 0;
				end
				/*
				else begin
					assert(state == Rx_IDLE);
					assert(data_is_valid == 0);
					assert(serial_in == 1); 
				end*/
			end
    	end
    	    
    	else begin  // UART Tx and Rx are idling, still waiting for baud_clk
    	    cnt <= 0;
    	    assert(cnt == 0);
    	    assert(state == Rx_IDLE);
    	    assert(data_is_valid == 0);
    	    assert(serial_out == 1);
    	    
    	    if(!had_been_enabled) begin
    	    	assert(&shift_reg == 1);
    	    end
    	end
    end
end

always @(posedge clk)
begin
    if(reset) begin
    	had_just_reset <= 1;
		//assert();
    end

    else begin
    	had_just_reset <= 0;
    	
		if(!had_just_reset) begin
			if((had_been_enabled) && (!$past(had_been_enabled))) begin
				assert(!$past(o_busy));
				assert(o_busy);
			end

			else if((had_been_enabled) && ($past(had_been_enabled))) begin
				assert($past(o_busy));
				assert(o_busy);
			end

			else begin
			    assert(!$past(o_busy));
				
				if($past(enable)) begin
					assert(o_busy);
				end

				else begin
					assert(!o_busy);
				end

				assert(serial_out == 1);
			end
		end
    end
end

always @(posedge clk)
begin
    if(reset | o_busy) begin
        assume(enable == 0);
    end
	
	if(enable | had_been_enabled) begin
		assume($past(i_data) == i_data);
	end
end

always @(posedge clk)
begin
    assert(!rx_error);   // no parity error

    if(data_is_valid) begin   // state == Rx_STOP_BIT
        assert(received_data == i_data);
        assert(cnt < NUMBER_OF_BITS*CLOCKS_PER_BIT);
    end

	if((!had_just_reset) && (state <= Rx_STOP_BIT) && (first_clock_passed) && (transmission_had_started) && ($past(transmission_had_started)) && ($past(baud_clk))) begin
		assert(cnt - $past(cnt) == 1);
	end
end

`endif

endmodule

[ben2]

In reply to feiphung:
Your formal verification approach does not seem correct; specifically:

[list=1]
[] Your assertions do not reflect the black-box requirements of the UART. They are rather written at the low-level of the testbench.
[] Since the DUT is the UART, your assertions need to reflect the requirements of the UART. They are typically in a module or a checker bound to the DUT.
[] What you should provide to the formal verification tool is the UART and the assertions (that are in module or a checker bound to the DUT).
[] What you submitted to the formal verification tool is the verification of the testbench with a UART. Not quite what you really want!
[/litestbench
See Assertions Instead of FSMs/logic for Scoreboarding and Verification | Verification Horizons | Verification Academy
Also, see All test code and test results used in that paper at
http://systemverilog.us/uart4hz.tar

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

[feiphung]

In reply to ben@SystemVerilog.us:

If I treat my UART coding as blackbox, I would not be able to verify it formally.

Note: I am not using any UVM library. I am just using a free formal tool, yosys-smtbmc

[ben2]

In reply to feiphung:
That tool is more academic and “Yosys does not support SVA properties!”
Obviously, it is more practical to use SVA concurrent assertions with assumes to define the requirements and the restrictions. The definition you wrote is very hard to follow.
Commercial formal verification tools do use SVA and PSL.
Ben SystemVerilog.us

[feiphung]

In reply to ben@SystemVerilog.us:

@ben

I understand your concern regarding my UART testbench has more global assertions than local assertions.

However, it is due to the lack of FSM in UART transmitter

// Credit: Adapted from http://hamsterworks.co.nz/mediawiki/index.php/TinyTx or vhdl - UART HDL question - Electrical Engineering Stack Exchange

module TxUART(clk, reset, baud_clk, enable, i_data, o_busy, serial_out
`ifdef FORMAL
	, shift_reg
`endif
);

parameter INPUT_DATA_WIDTH = 8;
parameter PARITY_ENABLED = 1;

input clk, reset, baud_clk, enable;
input[(INPUT_DATA_WIDTH+PARITY_ENABLED-1):0] i_data;
output reg o_busy;      // busy signal for data source that Tx cannot accept data 
output reg serial_out;  // serialized data

`ifdef FORMAL
	output [(INPUT_DATA_WIDTH+PARITY_ENABLED+1):0] shift_reg;
`endif

reg [(INPUT_DATA_WIDTH+PARITY_ENABLED+1):0] shift_reg;  // PISO shift reg, start+data+parity+stop

initial 
begin
    o_busy = 0;
    serial_out = 1;
    shift_reg = ~0;
end

always @(posedge clk)   
begin
    if (reset) begin
        shift_reg <= ~0;  // set all bits to 1
    end

    else begin
        if (enable & !o_busy) begin
            shift_reg <= {1'b1, i_data, 1'b0};   // transmit LSB first: 1 = stop bit, 0 = start bit 
        end

        if (baud_clk) begin
            if (o_busy) begin
                shift_reg <= {1'b0, shift_reg[(INPUT_DATA_WIDTH+PARITY_ENABLED+1):1]};  // puts 0 for stop bit detection, see o_busy signal
            end
        end
    end
end 

always @(posedge clk) 
begin
    if(reset) begin 
    	serial_out <= 1;
    end

    else begin
        if (baud_clk) begin
            if (o_busy) begin
	            serial_out <= shift_reg[0]; 
            end	    
        end        
    end
end

always @(posedge clk) 
begin
    if(reset) begin 
    	o_busy <= 0;
    end

    else begin
		o_busy <= ((shift_reg != 0) && !(&shift_reg)) | enable;   // if not reset, ((Tx is busy transmitting when there is pending stop bit) AND (Tx does not just get reset)) OR (Tx is about to transmit)
    end
end


`ifdef FORMAL

reg first_clock_passed;
initial first_clock_passed = 0;

always @(posedge clk)
begin
	first_clock_passed <= 1;
end

always @(posedge clk) 
begin
	if(first_clock_passed && ($past(first_clock_passed) == 0)) begin    // for induction check purpose
		assert($past(o_busy) == 0);  // initially not busy
		assert(&($past(shift_reg)) == 1);  // initially all ones, transmitting ones
	end
end

`endif

endmodule

[feiphung]

In reply to feiphung:

@ben

I have finished UART formal verification (both bounded model check and k-induction) using SAME clocks for both Tx and Rx.

I am now planning for asynchronous clocks testing where the Tx and Rx clocks would be slightly different in frequency and phase.

How am I going to assert() when I have two different clocks ? this is really an headache

[ben2]

it has been decades since i designed a UART; however, if I recall it well, there is a 16x clock at the receiver. Thus, when you say “I am now planning for asynchronous clocks testing where the Tx and Rx clocks would be [b]slightly different in frequency and phase” I don’t really understand it. Typically, the tx 16x clock and rx 16x clock are of the same frequency, but not the same phase. Those frequencies can vary a bit and the 16x rate allows for some s=deviations between the rx and tx clock. Is this what you mean?

How am I going to assert() when I have two different clocks ?

You could simply have 2 counters, one for the tx and one for rx.
Let those clocks count for 100 or 1000 cycles, and then compare the values of the counts. From there you can assess the frequency differences. SVA would not do too well on this.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

See Paper: 1) VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy
2) http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf

[feiphung]

In reply to ben@SystemVerilog.us:

From there you can assess the frequency differences. SVA would not do too well on this.

See Formally Verifying Asynchronous Components for an asynchronous formal testing example.