From 1a536080f1990f587ddcd7ee0b46a5b67f987382 Mon Sep 17 00:00:00 2001 From: Fischer Moseley <42497969+fischermoseley@users.noreply.github.com> Date: Fri, 14 Jul 2023 06:30:05 -0700 Subject: [PATCH] rewrite bridge_rx and add basic formal --- Makefile | 8 + src/manta/uart_iface/bridge_rx.v | 208 +++++++++++++------------ src/manta/uart_iface/bridge_tx.v | 12 +- test/formal_verification/bridge_rx.sby | 29 ++++ test/formal_verification/uart_rx.sby | 29 ++++ 5 files changed, 178 insertions(+), 108 deletions(-) create mode 100644 test/formal_verification/bridge_rx.sby create mode 100644 test/formal_verification/uart_rx.sby diff --git a/Makefile b/Makefile index 2397732..153b796 100644 --- a/Makefile +++ b/Makefile @@ -83,6 +83,14 @@ lut_mem_tb: vvp sim.out rm sim.out +# Formal Verification +formal: + sby test/formal_verification/uart_rx.sby + +formal_clean: + rm -rf test/formal_verification/*_basic + rm -rf test/formal_verification/*_cover + # Build Examples examples: icestick nexys_a7 diff --git a/src/manta/uart_iface/bridge_rx.v b/src/manta/uart_iface/bridge_rx.v index 32082cc..dd29380 100644 --- a/src/manta/uart_iface/bridge_rx.v +++ b/src/manta/uart_iface/bridge_rx.v @@ -1,6 +1,25 @@ `default_nettype none `timescale 1ns/1ps +function [3:0] from_ascii_hex; + // convert an ascii char encoding a hex value to + // the corresponding hex value + input [7:0] c; + + if ((c >= 8'h30) && (c <= 8'h39)) from_ascii_hex = c - 8'h30; + else if ((c >= 8'h41) && (c <= 8'h46)) from_ascii_hex = c - 8'h41 + 'd1; + else from_ascii_hex = 0; +endfunction + +function is_ascii_hex; + // checks if a byte is an ascii char encoding a hex digit + input [7:0] c; + + if ((c >= 8'h30) && (c <= 8'h39)) is_ascii_hex = 1; // 0-9 + else if ((c >= 8'h41) && (c <= 8'h46)) is_ascii_hex = 1; // A-F + else is_ascii_hex = 0; +endfunction + module bridge_rx ( input wire clk, @@ -8,123 +27,108 @@ module bridge_rx ( input wire valid_i, output reg [15:0] addr_o, - output reg [15:0] wdata_o, + output reg [15:0] data_o, output reg rw_o, output reg valid_o); - // this is a hack, the FSM needs to be updated - // but this will bypass it for now - parameter ready_i = 1; + initial addr_o = 0; + initial data_o = 0; + initial rw_o = 0; + initial valid_o = 0; - parameter ADDR_WIDTH = 0; - parameter DATA_WIDTH = 0; - - localparam PREAMBLE = 8'h4D; - localparam CR = 8'h0D; - localparam LF = 8'h0A; - - localparam ACQUIRE = 0; - localparam TRANSMIT = 1; - localparam ERROR = 2; - - reg [1:0] state; - reg [3:0] bytes_received; - - // no global resets! - initial begin - addr_o = 0; - wdata_o = 0; - rw_o = 0; - valid_o = 0; - bytes_received = 0; - state = ACQUIRE; - end - - reg [3:0] data_i_decoded; - reg data_i_is_0_thru_9; - reg data_i_is_A_thru_F; - - always @(*) begin - data_i_is_0_thru_9 = (data_i >= 8'h30) & (data_i <= 8'h39); - data_i_is_A_thru_F = (data_i >= 8'h41) & (data_i <= 8'h46); - - if (data_i_is_0_thru_9) data_i_decoded = data_i - 8'h30; - else if (data_i_is_A_thru_F) data_i_decoded = data_i - 8'h41 + 'd10; - else data_i_decoded = 0; - end + reg [7:0] buffer [7:0]; // todo: see if sby will tolerate packed arrays? + localparam IDLE = 0; + localparam READ = 1; + localparam WRITE = 2; + reg [1:0] state = 0; + reg [3:0] byte_num = 0; always @(posedge clk) begin - if (state == ACQUIRE) begin - if(valid_i) begin + addr_o <= 0; + data_o <= 0; + rw_o <= 0; + valid_o <= 0; - if (bytes_received == 0) begin - if(data_i == PREAMBLE) bytes_received <= 1; - end - - else if( (bytes_received >= 1) & (bytes_received <= 4) ) begin - // only advance if byte is valid hex digit - if(data_i_is_0_thru_9 | data_i_is_A_thru_F) begin - addr_o <= (addr_o << 4) | data_i_decoded; - bytes_received <= bytes_received + 1; - end - - else state <= ERROR; - end - - else if( bytes_received == 5) begin - if( (data_i == CR) | (data_i == LF)) begin - valid_o <= 1; - rw_o <= 0; - bytes_received <= 0; - state <= TRANSMIT; - end - - else if (data_i_is_0_thru_9 | data_i_is_A_thru_F) begin - bytes_received <= bytes_received + 1; - wdata_o <= (wdata_o << 4) | data_i_decoded; - end - - else state <= ERROR; - end - - else if ( (bytes_received >= 6) & (bytes_received <= 8) ) begin - - if (data_i_is_0_thru_9 | data_i_is_A_thru_F) begin - wdata_o <= (wdata_o << 4) | data_i_decoded; - bytes_received <= bytes_received + 1; - end - - else state <= ERROR; - end - - else if (bytes_received == 9) begin - bytes_received <= 0; - if( (data_i == CR) | (data_i == LF)) begin - valid_o <= 1; - rw_o <= 1; - state <= TRANSMIT; - end - - else state <= ERROR; - end - end + if (state == IDLE) begin + byte_num <= 0; + if (valid_i) begin + if (data_i == "R") state <= READ; + if (data_i == "W") state <= WRITE; + end end + else begin + if (valid_i) begin + // buffer bytes regardless of if they're good + byte_num <= byte_num + 1; + buffer[byte_num] <= data_i; - else if (state == TRANSMIT) begin - if(ready_i) begin - valid_o <= 0; - state <= ACQUIRE; - end + // current transaction specifies a read operation + if(state == READ) begin - if(valid_i) begin - if ( (data_i != CR) & (data_i != LF)) begin - valid_o <= 0; - state <= ERROR; + // go to idle if anything doesn't make sense + if(byte_num <= 3) + if(!is_ascii_hex(data_i)) state <= IDLE; + + else if(byte_num == 4) + if(data_i != CR) state <= IDLE; + + else if(byte_num == 5) begin + state <= IDLE; + + // put data on the bus if the last byte looks good + if(data_i == LF) begin + addr_o <= (from_ascii_hex(buffer[0]) << 12) | + (from_ascii_hex(buffer[1]) << 8) | + (from_ascii_hex(buffer[2]) << 4) | + (from_ascii_hex(buffer[3])); + data_o <= 0; + rw_o <= 0; + valid_o <= 1; + end + end + end + + // current transaction specifies a write transaction + if(state == WRITE) begin + + // go to idle if anything doesn't make sense + if(byte_num <= 3) + if(!is_ascii_hex(data_i)) state <= IDLE; + + else if(byte_num == 4) + if(data_i != CR) state <= IDLE; + + else if(byte_num == 5) begin + state <= IDLE; + + // put data on the bus if the last byte looks good + if(data_i == LF) begin + addr_o <= (from_ascii_hex(buffer[0]) << 12) | + (from_ascii_hex(buffer[1]) << 8) | + (from_ascii_hex(buffer[2]) << 4) | + (from_ascii_hex(buffer[3])); + data_o <= (from_ascii_hex(buffer[4]) << 12) | + (from_ascii_hex(buffer[5]) << 8) | + (from_ascii_hex(buffer[6]) << 4) | + (from_ascii_hex(buffer[7])); + rw_o <= 1; + valid_o <= 1; + end + end end end end end + +`ifdef FORMAL + always @(posedge clk) begin + cover(data_o == 16'h1234); + //cover(data_o == 16'h1234 && addr_o == 16'h5678 && rw_o == 1 && valid_o == 1); + end +`endif // FORMAL endmodule + + `default_nettype wire \ No newline at end of file diff --git a/src/manta/uart_iface/bridge_tx.v b/src/manta/uart_iface/bridge_tx.v index 9baa70c..109cd9e 100644 --- a/src/manta/uart_iface/bridge_tx.v +++ b/src/manta/uart_iface/bridge_tx.v @@ -1,10 +1,10 @@ `default_nettype none `timescale 1ns/1ps -function [7:0] ascii_hex; +function [7:0] to_ascii_hex; // convert a number from 0-15 into the corresponding ascii char input [3:0] n; - ascii_hex = (n > 10) ? (n + 8'h30) : (n + 8'h41 - 'd10); + to_ascii_hex = (n > 10) ? (n + 8'h30) : (n + 8'h41 - 'd10); endfunction module bridge_tx ( @@ -57,10 +57,10 @@ module bridge_tx ( always @(*) begin case (count) 0: data_o = PREAMBLE; - 1: data_o = ascii_hex(buffer[15:12]); - 2: data_o = ascii_hex(buffer[11:8]); - 3: data_o = ascii_hex(buffer[7:4]); - 4: data_o = ascii_hex(buffer[3:0]); + 1: data_o = to_ascii_hex(buffer[15:12]); + 2: data_o = to_ascii_hex(buffer[11:8]); + 3: data_o = to_ascii_hex(buffer[7:4]); + 4: data_o = to_ascii_hex(buffer[3:0]); 5: data_o = CR; 6: data_o = LF; default: data_o = 0; diff --git a/test/formal_verification/bridge_rx.sby b/test/formal_verification/bridge_rx.sby new file mode 100644 index 0000000..93a9ed9 --- /dev/null +++ b/test/formal_verification/bridge_rx.sby @@ -0,0 +1,29 @@ +[tasks] +basic bmc +nofullskip prove +cover +noverific cover +basic cover : default + +[options] +cover: +mode cover +-- +prove: +mode prove +-- +bmc: +mode bmc +-- + +[engines] +smtbmc boolector + +[script] +nofullskip: read -define NO_FULL_SKIP=1 +noverific: read -noverific +read -formal bridge_rx.v +prep -top bridge_rx + +[files] +src/manta/uart_iface/bridge_rx.v \ No newline at end of file diff --git a/test/formal_verification/uart_rx.sby b/test/formal_verification/uart_rx.sby new file mode 100644 index 0000000..6b05f3c --- /dev/null +++ b/test/formal_verification/uart_rx.sby @@ -0,0 +1,29 @@ +[tasks] +basic bmc +nofullskip prove +cover +noverific cover +basic cover : default + +[options] +cover: +mode cover +-- +prove: +mode prove +-- +bmc: +mode bmc +-- + +[engines] +smtbmc boolector + +[script] +nofullskip: read -define NO_FULL_SKIP=1 +noverific: read -noverific +read -formal uart_rx.v +prep -top uart_rx + +[files] +src/manta/uart_iface/uart_rx.v \ No newline at end of file