From ac23e8a59913b565e79f1696152c5c0cc4c15957 Mon Sep 17 00:00:00 2001 From: Fischer Moseley <42497969+fischermoseley@users.noreply.github.com> Date: Mon, 17 Jul 2023 06:53:01 -0700 Subject: [PATCH] make functional sim run again --- .gitignore | 6 +- Makefile | 7 +- src/manta/uart_iface/__init__.py | 2 +- src/manta/uart_iface/bridge_rx.v | 37 ++- src/manta/uart_iface/bridge_tx.v | 12 +- .../uart_iface/uart_rx_bridge_rx_inst_templ.v | 2 +- test/functional_sim/bridge_tx_tb.sv | 31 +-- test/functional_sim/bus_fix_tb.sv | 221 ------------------ 8 files changed, 61 insertions(+), 257 deletions(-) delete mode 100644 test/functional_sim/bus_fix_tb.sv diff --git a/.gitignore b/.gitignore index a42d63d..8facbbb 100644 --- a/.gitignore +++ b/.gitignore @@ -26,4 +26,8 @@ dist/ __pycache__/ # Verilator outputs -obj_dir/ \ No newline at end of file +obj_dir/ + +# Formal outputs +test/formal_verification/*_basic +test/formal_verification/*_cover \ No newline at end of file diff --git a/Makefile b/Makefile index 153b796..b5ed0b4 100644 --- a/Makefile +++ b/Makefile @@ -26,6 +26,9 @@ clean: rm -f *.out *.vcd rm -rf dist/ rm -rf src/mantaray.egg-info + rm -rf test/formal_verification/*_basic + rm -rf test/formal_verification/*_cover + # API Generation Tests auto_gen: @@ -87,10 +90,6 @@ lut_mem_tb: 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/__init__.py b/src/manta/uart_iface/__init__.py index 6d3fca0..b4081c6 100644 --- a/src/manta/uart_iface/__init__.py +++ b/src/manta/uart_iface/__init__.py @@ -166,7 +166,7 @@ class UARTInterface: return ["input wire rx", "output reg tx"] def rx_hdl_def(self): - uart_rx_def = VerilogManipulator("uart_iface/rx_uart.v").get_hdl() + uart_rx_def = VerilogManipulator("uart_iface/uart_rx.v").get_hdl() bridge_rx_def = VerilogManipulator("uart_iface/bridge_rx.v").get_hdl() return uart_rx_def + '\n' + bridge_rx_def diff --git a/src/manta/uart_iface/bridge_rx.v b/src/manta/uart_iface/bridge_rx.v index 6f320dd..37d92d7 100644 --- a/src/manta/uart_iface/bridge_rx.v +++ b/src/manta/uart_iface/bridge_rx.v @@ -36,7 +36,7 @@ module bridge_rx ( else is_ascii_hex = 0; endfunction - reg [7:0][7:0] buffer = 0; // todo: see if sby will tolerate packed arrays? + reg [7:0] buffer [7:0]; // = 0; // todo: see if sby will tolerate packed arrays? localparam IDLE = 0; localparam READ = 1; @@ -120,8 +120,39 @@ module bridge_rx ( `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); + // covers + // find_any_write_transaction: cover(rw_o == 1); + // find_any_read_transaction: cover(rw_o == 0); + + // find_specific_write_transaction: + // cover(data_o == 16'h1234 && addr_o == 16'h5678 && rw_o == 1 && valid_o == 1); + + // find_specific_read_transaction: + // cover(addr_o == 16'h1234 && rw_o == 0 && valid_o == 1); + + // find_spacey_write_transaction: + // cover((rw_o == 1) && ($past(valid_i, 3) == 0)); + + // // asserts + // no_back_to_back_transactions: + // assert( ~(valid_o && $past(valid_o)) ); + + // no_invalid_states: + // assert(state == IDLE || state == READ || state == WRITE); + + // byte_counter_only_increases: + // assert(byte_num == $past(byte_num) || byte_num == $past(byte_num) + 1 || byte_num == 0); + + // only_r_triggers_reads: + // assert property ( (state == READ) |=> ($past(valid_i) ) ); + + + // state transitions + enter_read: + assert( ($past(state) == IDLE && state == READ) ) + + + end `endif // FORMAL endmodule diff --git a/src/manta/uart_iface/bridge_tx.v b/src/manta/uart_iface/bridge_tx.v index 109cd9e..ca7ede2 100644 --- a/src/manta/uart_iface/bridge_tx.v +++ b/src/manta/uart_iface/bridge_tx.v @@ -1,12 +1,6 @@ `default_nettype none `timescale 1ns/1ps -function [7:0] to_ascii_hex; - // convert a number from 0-15 into the corresponding ascii char - input [3:0] n; - to_ascii_hex = (n > 10) ? (n + 8'h30) : (n + 8'h41 - 'd10); -endfunction - module bridge_tx ( input wire clk, @@ -18,6 +12,12 @@ module bridge_tx ( output reg start_o, input wire done_i); + function [7:0] to_ascii_hex; + // convert a number from 0-15 into the corresponding ascii char + input [3:0] n; + to_ascii_hex = (n > 10) ? (n + 8'h30) : (n + 8'h41 - 'd10); + endfunction + localparam PREAMBLE = 8'h4D; localparam CR = 8'h0D; localparam LF = 8'h0A; diff --git a/src/manta/uart_iface/uart_rx_bridge_rx_inst_templ.v b/src/manta/uart_iface/uart_rx_bridge_rx_inst_templ.v index 62d1cd6..8ff8dec 100644 --- a/src/manta/uart_iface/uart_rx_bridge_rx_inst_templ.v +++ b/src/manta/uart_iface/uart_rx_bridge_rx_inst_templ.v @@ -15,6 +15,6 @@ bridge_rx brx ( .valid_i(urx_brx_valid), .addr_o(), - .wdata_o(), + .data_o(), .rw_o(), .valid_o()); \ No newline at end of file diff --git a/test/functional_sim/bridge_tx_tb.sv b/test/functional_sim/bridge_tx_tb.sv index 30d733d..2cfc32b 100644 --- a/test/functional_sim/bridge_tx_tb.sv +++ b/test/functional_sim/bridge_tx_tb.sv @@ -13,37 +13,32 @@ integer test_num; // tb -> bridge_tx signals logic [15:0] tb_btx_rdata; -logic res_ready; logic tb_btx_valid; -// uart_tx <--> bridge_tx signals -logic [7:0] btx_utx_data; -logic btx_utx_valid; -logic btx_utx_ready; - // uart_tx -> tb signals logic utx_tb_tx; bridge_tx btx ( .clk(clk), - .rdata_i(tb_btx_rdata), + .data_i(tb_btx_rdata), .rw_i(1'b1), .valid_i(tb_btx_valid), .data_o(btx_utx_data), - .ready_i(btx_utx_ready), - .valid_o(btx_utx_valid)); + .start_o(btx_utx_start), + .done_i(utx_btx_done)); -uart_tx #( - .CLOCKS_PER_BAUD(868)) - utx ( +reg [7:0] btx_utx_data; +reg btx_utx_start; +reg utx_btx_done; + +uart_tx #(.CLOCKS_PER_BAUD(/* CLOCKS_PER_BAUD */)) utx ( .clk(clk), - .data(btx_utx_data), - .valid(btx_utx_valid), - .busy(), - .ready(btx_utx_ready), + .data_i(btx_utx_data), + .start_i(btx_utx_start), + .done_o(utx_btx_done), .tx(utx_tb_tx)); @@ -71,7 +66,6 @@ initial begin tb_btx_valid = 1; #`CP; - assert(res_ready == 0) else $fatal(0, "invalid handshake: res_ready held high for more than one clock cycle"); tb_btx_valid = 0; #(100000*`CP); @@ -84,7 +78,6 @@ initial begin tb_btx_valid = 1; #`CP; - assert(res_ready == 0) else $fatal(0, "invalid handshake: res_ready held high for more than one clock cycle"); tb_btx_valid = 0; #(100000*`CP); @@ -97,7 +90,6 @@ initial begin tb_btx_valid = 1; #`CP; - assert(res_ready == 0) else $fatal(0, "invalid handshake: res_ready held high for more than one clock cycle"); tb_btx_valid = 0; #(100000*`CP); @@ -110,7 +102,6 @@ initial begin tb_btx_valid = 1; #`CP; - assert(res_ready == 0) else $fatal(0, "invalid handshake: res_ready held high for more than one clock cycle"); tb_btx_valid = 0; #(100000*`CP); diff --git a/test/functional_sim/bus_fix_tb.sv b/test/functional_sim/bus_fix_tb.sv deleted file mode 100644 index 54507f7..0000000 --- a/test/functional_sim/bus_fix_tb.sv +++ /dev/null @@ -1,221 +0,0 @@ -`default_nettype none -`timescale 1ns/1ps - -`define CP 10 -`define HCP 5 - -`define SEND_MSG_BITS(MSG) \ - for(int j=0; j < $size(msg); j++) begin \ - char = msg[j]; \ - for(int i=0; i < 10; i++) begin \ - if (i == 0) tb_urx_rxd = 0; \ - else if ((i > 0) & (i < 9)) tb_urx_rxd = char[i-1]; \ - else if (i == 9) tb_urx_rxd = 1; \ - #(868*`CP); \ - end \ - end \ - -module bus_fix_tb; - // https://www.youtube.com/watch?v=WCOAr-96bGc - - //boilerplate - logic clk; - logic rst; - integer test_num; - string msg; - logic [7:0] char; - - parameter CLOCKS_PER_BAUD = 10; - - // tb --> uart_rx signals - logic tb_urx_rxd; - rx_uart #(.CLOCKS_PER_BAUD(CLOCKS_PER_BAUD)) urx ( - .i_clk(clk), - .i_uart_rx(tb_urx_rxd), - .o_wr(urx_brx_axiv), - .o_data(urx_brx_axid)); - - // uart_rx --> bridge_rx signals - logic [7:0] urx_brx_axid; - logic urx_brx_axiv; - - bridge_rx brx ( - .clk(clk), - - .rx_data(urx_brx_axid), - .rx_valid(urx_brx_axiv), - - .addr_o(brx_mem_addr), - .wdata_o(brx_mem_wdata), - .rw_o(brx_mem_rw), - .valid_o(brx_mem_valid)); - - // bridge_rx --> mem signals - logic [15:0] brx_mem_addr; - logic [15:0] brx_mem_wdata; - logic brx_mem_rw; - logic brx_mem_valid; - - lut_mem #( - .DEPTH(32), - .BASE_ADDR(0) - ) ram ( - .clk(clk), - .addr_i(brx_mem_addr), - .wdata_i(brx_mem_wdata), - .rdata_i(16'h0), - .rw_i(brx_mem_rw), - .valid_i(brx_mem_valid), - - .addr_o(), - .wdata_o(), - .rdata_o(mem_btx_rdata), - .rw_o(mem_btx_rw), - .valid_o(mem_btx_valid)); - - // mem --> frizzle signals, it's frizzle because that's a bus you wanna get off of - logic [15:0] mem_btx_rdata; - logic mem_btx_rw; - logic mem_btx_valid; - - bridge_tx btx ( - .clk(clk), - - .rdata_i(mem_btx_rdata), - .rw_i(mem_btx_rw), - .valid_i(mem_btx_valid), - - .ready_i(utx_btx_ready), - .data_o(btx_utx_data), - .valid_o(btx_utx_valid)); - - logic utx_btx_ready; - logic btx_utx_valid; - logic [7:0] btx_utx_data; - - uart_tx #(.CLOCKS_PER_BAUD(CLOCKS_PER_BAUD)) utx ( - .clk(clk), - - .data(btx_utx_data), - .valid(btx_utx_valid), - .ready(utx_btx_ready), - - .tx(utx_tb_tx)); - - // utx --> tb signals - logic utx_tb_tx; - - // decoder for lolz - logic [7:0] tb_decoder_data; - logic [7:0] decoded_uart; - logic tb_decoder_valid; - - rx_uart #(.CLOCKS_PER_BAUD(CLOCKS_PER_BAUD)) decoder ( - .i_clk(clk), - - .i_uart_rx(utx_tb_tx), - .o_wr(tb_decoder_valid), - .o_data(tb_decoder_data)); - - always @(posedge clk) if (tb_decoder_valid) decoded_uart <= tb_decoder_data; - - always begin - #`HCP - clk = !clk; - end - - initial begin - $dumpfile("bus_fix.vcd"); - $dumpvars(0, bus_fix_tb); - - // setup and reset - clk = 0; - rst = 0; - tb_urx_rxd = 1; - test_num = 0; - #`CP - rst = 1; - #`CP - rst = 0; - #`HCP - - // throw some nonzero data in the memories just so we know that we're pulling from the right ones - - for(int i=0; i< 32; i++) mem.mem[i] = i; - - #(10*`CP); - - /* ==== Test 1 Begin ==== */ - $display("\n=== test 1: write 0x5678 to 0x1234 for baseline functionality ==="); - test_num = 1; - msg = {"M1234", 8'h0D, 8'h0A}; - `SEND_MSG_BITS(msg) - - #(10*`CP); - /* ==== Test 1 End ==== */ - - /* ==== Test 2 Begin ==== */ - $display("\n=== test 2: read from 0x0001 for baseline functionality ==="); - test_num = 2; - msg = {"M1234", 8'h0D, 8'h0A}; - `SEND_MSG_BITS(msg) - - #(1000*`CP); - /* ==== Test 2 End ==== */ - - /* ==== Test 3 Begin ==== */ - $display("\n=== test 3: 100 sequential reads, stress test ==="); - test_num = 3; - - for(int i=0; i<100; i++) begin - msg = {"M1234", 8'h0D, 8'h0A}; - `SEND_MSG_BITS(msg); - end - - - // big reads - // for(logic[15:0] j=0; j<10; j++) begin - // msg = {$sformatf("M%H", j), 8'h0D, 8'h0A}; - // `SEND_MSG_BITS(msg) - // end - - // for(logic[15:0] j=0; j<10; j++) begin - // msg = {$sformatf("M%H", j), 8'h0D, 8'h0A}; - // `SEND_MSG_BITS(msg) - // end - - - #(10*`CP); - /* ==== Test 3 End ==== */ - - /* ==== Test 4 Begin ==== */ - $display("\n=== test 4: 100 sequential writes, stress test ==="); - test_num = 4; - - for(int i=0; i<100; i++) begin - msg = {"M12345678", 8'h0D, 8'h0A}; - `SEND_MSG_BITS(msg); - end - - /* ==== Test 4 End ==== */ - - /* ==== Test 5 Begin ==== */ - $display("\n=== test 5: 100 sequential reads, stress test ==="); - test_num = 5; - - for(int i=0; i<100; i++) begin - msg = {"M1234", 8'h0D, 8'h0A}; - `SEND_MSG_BITS(msg); - end - - /* ==== Test 5 End ==== */ - - - - #(1000*`CP) - - $finish(); - end -endmodule - -`default_nettype wire \ No newline at end of file