From 2b483b1beb119ba6fb08f57068c9deb4a6c198c5 Mon Sep 17 00:00:00 2001
From: Fischer Moseley <42497969+fischermoseley@users.noreply.github.com>
Date: Mon, 17 Jul 2023 07:41:29 -0700
Subject: [PATCH] add bridge_rx formal to makefile

---
 Makefile                         |  1 +
 src/manta/uart_iface/bridge_rx.v | 41 ++++++++++++--------------------
 2 files changed, 16 insertions(+), 26 deletions(-)

diff --git a/Makefile b/Makefile
index c6c4127..1767f28 100644
--- a/Makefile
+++ b/Makefile
@@ -95,6 +95,7 @@ lut_mem_tb:
 # Formal Verification
 formal:
 	sby -f test/formal_verification/uart_rx.sby
+	sby -f test/formal_verification/bridge_rx.sby
 
 # Build Examples
 nexys_a7: nexys_a7_video_sprite_uart nexys_a7_io_core nexys_a7_ps2_logic_analyzer nexys_a7_lut_mem
diff --git a/src/manta/uart_iface/bridge_rx.v b/src/manta/uart_iface/bridge_rx.v
index 37d92d7..995b1ab 100644
--- a/src/manta/uart_iface/bridge_rx.v
+++ b/src/manta/uart_iface/bridge_rx.v
@@ -121,38 +121,27 @@ module bridge_rx (
 `ifdef FORMAL
         always @(posedge clk) begin
             // covers
-            // find_any_write_transaction: cover(rw_o == 1);
-            // find_any_read_transaction: cover(rw_o == 0);
+            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_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_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) )
+            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);
         end
 `endif // FORMAL
 endmodule