make functional sim run again

.gitignore

@@ -26,4 +26,8 @@ dist/
 __pycache__/
 
 # Verilator outputs
-obj_dir/
+obj_dir/
+
+# Formal outputs
+test/formal_verification/*_basic
+test/formal_verification/*_cover

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

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
 

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);
+            // covers
-            //cover(data_o == 16'h1234 && addr_o == 16'h5678 && rw_o == 1 && valid_o == 1);
+            // 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

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;

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());

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),
+    .start_o(btx_utx_start),
-    .valid_o(btx_utx_valid));
+    .done_i(utx_btx_done));
 
-uart_tx #(
+reg [7:0] btx_utx_data;
-    .CLOCKS_PER_BAUD(868))
+reg btx_utx_start;
-    utx (
+reg utx_btx_done;
+
+uart_tx #(.CLOCKS_PER_BAUD(/* CLOCKS_PER_BAUD */)) utx (
     .clk(clk),
 
-    .data(btx_utx_data),
+    .data_i(btx_utx_data),
-    .valid(btx_utx_valid),
+    .start_i(btx_utx_start),
-    .busy(),
+    .done_o(utx_btx_done),
-    .ready(btx_utx_ready),
 
     .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);

test/functional_sim/bus_fix_tb.sv

@@ -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