OpenCores
URL https://opencores.org/ocsvn/wbuart32/wbuart32/trunk

Subversion Repositories wbuart32

Compare Revisions

  • This comparison shows the changes necessary to convert path
    /wbuart32/trunk/rtl
    from Rev 21 to Rev 23
    Reverse comparison

Rev 21 → Rev 23

/rxuartlite.v
204,7 → 204,8
 
`ifdef FORMAL
 
// `define PHASE_TWO // SymbiYosys controls this definition
`define ASSUME assume
 
`define PHASE_ONE_ASSERT assert
`define PHASE_TWO_ASSERT assert
 
239,6 → 240,7
always @(posedge i_clk)
f_past_valid <= 1'b1;
 
`ifdef F_OPT_CLK2FFLOGIC
initial f_rx_clock = 3'h0;
always @($global_clock)
f_rx_clock <= f_rx_clock + 1'b1;
245,6 → 247,7
 
always @(*)
assume(i_clk == f_rx_clock[1]);
`endif
 
 
 
271,6 → 274,7
initial assert(F_MINSTEP <= F_MIDSTEP);
initial assert(F_MIDSTEP <= F_MAXSTEP);
 
`ifdef F_OPT_CLK2FFLOGIC
assign f_tx_step = $anyconst;
// assume((f_tx_step >= F_MINSTEP)&&(f_tx_step <= F_MAXSTEP));
//
284,7 → 288,9
f_tx_clock <= f_tx_clock + f_tx_step;
 
assign f_txclk = f_tx_clock[F_CKRES-1];
 
`else
assign f_tx_clk = i_clk;
`endif
//
initial f_past_valid_tx = 1'b0;
always @(posedge f_txclk)
/txuart.v
221,7 → 221,7
if (state == `TXU_BIT_SEVEN)
state <= (use_parity)?`TXU_PARITY:`TXU_STOP;
else
state <= state + 1;
state <= state + 1'b1;
end else if (state == `TXU_PARITY)
begin
state <= `TXU_STOP;
392,5 → 392,191
end else
baud_counter <= clocks_per_baud - 28'h01;
end
 
`ifdef FORMAL
reg fsv_parity;
reg [30:0] fsv_setup;
reg [7:0] fsv_data;
 
always @(posedge i_clk)
if ((i_wr)&&(!o_busy))
fsv_data <= i_data;
 
always @(posedge i_clk)
if ((i_wr)&&(!o_busy))
fsv_setup <= i_setup;
 
always @(posedge i_clk)
assert(zero_baud_counter == (baud_counter == 0));
 
always @(*)
assume(i_setup[21:0] >= 2);
always @(*)
assume(i_setup[21:0] <= 16);
 
// A single baud interval
sequence BAUD_INTERVAL(DAT, SR, ST);
((o_uart_tx == DAT)&&(state == ST)
&&(lcl_data == SR)
&&(baud_counter == fsv_setup[21:0]-1)
&&(!zero_baud_counter))
##1 ((o_uart_tx == DAT)&&(state == ST)
&&(lcl_data == SR)
&&(baud_counter == $past(baud_counter)-1)
&&(baud_counter > 0)
&&(baud_counter < fsv_setup[21:0])
&&(!zero_baud_counter))[*0:$]
##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 SEND5(DATA);
BAUD_INTERVAL(1'b0, DATA, 4'h3)
##1 BAUD_INTERVAL(DATA[0], {{(1){1'b1}},DATA[7:1]}, 4'h4)
##1 BAUD_INTERVAL(DATA[1], {{(2){1'b1}},DATA[7:2]}, 4'h5)
##1 BAUD_INTERVAL(DATA[2], {{(3){1'b1}},DATA[7:3]}, 4'h6)
##1 BAUD_INTERVAL(DATA[3], {{(4){1'b1}},DATA[7:4]}, 4'h7)
##1 BAUD_INTERVAL(DATA[4], {{(5){1'b1}},DATA[7:5]}, 4'h8);
endsequence
 
sequence SEND6(DATA);
BAUD_INTERVAL(1'b0, DATA, 4'h2)
##1 BAUD_INTERVAL(DATA[0], {{(1){1'b1}},DATA[7:1]}, 4'h3)
##1 BAUD_INTERVAL(DATA[1], {{(2){1'b1}},DATA[7:2]}, 4'h4)
##1 BAUD_INTERVAL(DATA[2], {{(3){1'b1}},DATA[7:3]}, 4'h5)
##1 BAUD_INTERVAL(DATA[3], {{(4){1'b1}},DATA[7:4]}, 4'h6)
##1 BAUD_INTERVAL(DATA[4], {{(5){1'b1}},DATA[7:5]}, 4'h7)
##1 BAUD_INTERVAL(DATA[5], {{(6){1'b1}},DATA[7:6]}, 4'h8);
endsequence
 
sequence SEND7(DATA);
BAUD_INTERVAL(1'b0, DATA, 4'h1)
##1 BAUD_INTERVAL(DATA[0], {{(1){1'b1}},DATA[7:1]}, 4'h2)
##1 BAUD_INTERVAL(DATA[1], {{(2){1'b1}},DATA[7:2]}, 4'h3)
##1 BAUD_INTERVAL(DATA[2], {{(3){1'b1}},DATA[7:3]}, 4'h4)
##1 BAUD_INTERVAL(DATA[3], {{(4){1'b1}},DATA[7:4]}, 4'h5)
##1 BAUD_INTERVAL(DATA[4], {{(5){1'b1}},DATA[7:5]}, 4'h6)
##1 BAUD_INTERVAL(DATA[5], {{(6){1'b1}},DATA[7:6]}, 4'h7)
##1 BAUD_INTERVAL(DATA[6], {{(7){1'b1}},DATA[7:7]}, 4'h8);
endsequence
 
sequence SEND8(DATA);
BAUD_INTERVAL(1'b0, DATA, 4'h0)
##1 BAUD_INTERVAL(DATA[0], {{(1){1'b1}},DATA[7:1]}, 4'h1)
##1 BAUD_INTERVAL(DATA[1], {{(2){1'b1}},DATA[7:2]}, 4'h2)
##1 BAUD_INTERVAL(DATA[2], {{(3){1'b1}},DATA[7:3]}, 4'h3)
##1 BAUD_INTERVAL(DATA[3], {{(4){1'b1}},DATA[7:4]}, 4'h4)
##1 BAUD_INTERVAL(DATA[4], {{(5){1'b1}},DATA[7:5]}, 4'h5)
##1 BAUD_INTERVAL(DATA[5], {{(6){1'b1}},DATA[7:6]}, 4'h6)
##1 BAUD_INTERVAL(DATA[6], {{(7){1'b1}},DATA[7:7]}, 4'h7)
##1 BAUD_INTERVAL(DATA[7], 8'hff, 4'h8);
endsequence
 
always @(posedge i_clk)
if (fsv_setup[25])
fsv_parity <= fsv_setup[24];
else
case(fsv_setup[29:28])
2'b00: fsv_parity <= (^fsv_data[4:0]) ^ fsv_setup[24];
2'b01: fsv_parity <= (^fsv_data[5:0]) ^ fsv_setup[24];
2'b10: fsv_parity <= (^fsv_data[6:0]) ^ fsv_setup[24];
2'b11: fsv_parity <= (^fsv_data[7:0]) ^ fsv_setup[24];
endcase
 
assert property( @(posedge i_clk)
(o_busy)[*2] |=> $stable(fsv_parity));
 
assert property( @(posedge i_clk)
(o_busy) |=> $stable(fsv_data));
 
assert property( @(posedge i_clk)
(o_busy) |=> $stable(fsv_setup));
 
sequence SENDPARITY(SETUP);
((o_uart_tx == fsv_parity)&&(state == `TXU_PARITY)
&&(SETUP[26])
&&(baud_counter == SETUP[21:0]-1)
&&(!zero_baud_counter))
##1 ((o_uart_tx == fsv_parity)&&(state == `TXU_PARITY)
&&(SETUP[26])
&&(baud_counter < SETUP[21:0])
&&(baud_counter > 0)
&&(baud_counter == $past(baud_counter)-1)
&&(!zero_baud_counter))[*0:$]
##1 (o_uart_tx == fsv_parity)&&(state == `TXU_PARITY)
&&(SETUP[26])
&&(zero_baud_counter);
endsequence
 
sequence SENDSINGLESTOP(CKS,ST);
((o_uart_tx == 1'b1)&&(state == ST)
&&(baud_counter == CKS-1)
&&(!zero_baud_counter))
##1 ((o_uart_tx == 1'b1)&&(state == ST)
&&(baud_counter > 0)
&&(baud_counter == $past(baud_counter)-1)
&&(!zero_baud_counter))[*0:$]
##1 (o_uart_tx == 1'b1)&&(state == ST)
&&(zero_baud_counter);
endsequence
 
sequence SENDFULLSTOP(SETUP);
((!SETUP[27]) throughout SENDSINGLESTOP(SETUP[21:0],`TXU_STOP))
or (SETUP[27]) throughout
SENDSINGLESTOP(SETUP[21:0],`TXU_STOP)
##1 SENDSINGLESTOP(SETUP[21:0],`TXU_SECOND_STOP);
endsequence
 
sequence UART_IDLE;
(!o_busy)&&(o_uart_tx)&&(zero_baud_counter);
endsequence
 
assert property ( @(posedge i_clk) (!o_busy) |-> UART_IDLE);
 
 
assert property ( @(posedge i_clk)
(i_wr)&&(!o_busy)&&(i_setup[29:28]==2'b00) |=>
((o_busy) throughout
SEND5(fsv_data)
##1 SENDPARITY(fsv_setup)
##1 SENDFULLSTOP(fsv_setup)
)
##1 UART_IDLE);
 
assert property ( @(posedge i_clk)
(i_wr)&&(!o_busy)&&(i_setup[29:28]==2'b01) |=>
((o_busy) throughout
SEND6(fsv_data)
##1 SENDPARITY(fsv_setup)
##1 SENDFULLSTOP(fsv_setup)
)
##1 UART_IDLE);
 
assert property ( @(posedge i_clk)
(i_wr)&&(!o_busy)&&(i_setup[29:28]==2'b10) |=>
((o_busy) throughout
SEND7(fsv_data)
##1 SENDPARITY(fsv_setup)
##1 SENDFULLSTOP(fsv_setup)
)
##1 UART_IDLE);
 
assert property ( @(posedge i_clk)
(i_wr)&&(!o_busy)&&(i_setup[29:28]==2'b11) |=>
((o_busy) throughout
SEND8(fsv_data)
##1 SENDPARITY(fsv_setup)
##1 SENDFULLSTOP(fsv_setup)
)
##1 UART_IDLE);
 
`endif // FORMAL
endmodule
 
/ufifo.v
374,5 → 374,19
end
end
 
always @(posedge i_clk)
if (RXFIFO)
begin
assert(o_status[0] == (f_fill != 0));
assert(o_status[1] == (f_fill[LGFLEN-1]));
end
 
always @(posedge i_clk)
if (!RXFIFO) // Transmit FIFO interrupt flags
begin
assert(o_status[0] != (!w_full_n));
assert(o_status[1] == (!f_fill[LGFLEN-1]));
end
 
`endif
endmodule

powered by: WebSVN 2.1.0

© copyright 1999-2024 OpenCores.org, equivalent to Oliscience, all rights reserved. OpenCores®, registered trademark.