enable tribuf and fix loopback issue

Author: mattvenn

formal/README.md

@@ -12,3 +12,8 @@ To make a proof that the ins, outs and bidirectionals are all connected correctl
 * tt_top_formal.v instantiates tt_top.v and loops back the outputs and inputs
 * tt_um_formal.v is a user project that asserts that when its enabled, the inputs are driven by the outputs
 * p_wrapper.v is a replacement for p00, p01, p02, p03_wrapper.v that just instantiates tt_um_formal for each design
+
+## Limitations
+
+As the proof is made from the outside of the chip, we don't know the state of the bidirectional enables 
+(without changing the RTL). To work around this, the user modules always set the bottom 4 bidir pins as output.

formal/config.sby

@@ -12,7 +12,7 @@ read -noverific
 read -sv sg13g2_io.v tt_top.v basic_mux.v counter.v p_wrappers.v tt_um_formal.v tt_top_formal.v
 
 # convert tribuf to logic
-prep -top tt_top_formal; flatten #; tribuf -logic
+prep -top tt_top_formal; flatten ; tribuf -formal
 
 [files]
 ../IHP-Open-PDK/ihp-sg13g2/libs.ref/sg13g2_io/verilog/sg13g2_io.v

formal/tt_top_formal.v

@@ -1,3 +1,4 @@
+`default_nettype none
 
 module tt_top_formal ();
 
@@ -29,8 +30,8 @@ tt_top tt_top(
 
     // loopback the output to the input
     assign ui_in = uo_out;
-    // loopback the bidirectionals, if they're set as output
-    assign tt_top.uio_in = tt_top.uio_out & tt_top.uio_oe;
+    // bidirectionals loop top half to bottom half
+    assign uio[7:4] = uio[3:0];
 
     // only useful for cover
     initial assume(rst_n == 0);

formal/tt_um_formal.v

@@ -22,21 +22,23 @@ module tt_um_formal (
     // let solver drive the outputs
     rand reg [7:0] anyseq1; assign uo_out   = anyseq1;
     // bidirectional outputs
-    rand reg [7:0] anyseq2; assign uio_out  = anyseq2;
-    // bidirectional enables
-    rand reg [7:0] anyseq3; assign uio_oe   = anyseq3;
+    rand reg [3:0] anyseq2; assign uio_out[3:0]  = anyseq2;
+    // bidirectional enables - hard code bottom 4 are outputs
+    assign uio_oe[7:0] = 8'b00001111;
 
     always @(*) begin
         if(ena) begin
             // if design is enabled, looped back inputs must = outputs
-            assert(ui_in == uo_out);
-            // bidirectional outputs, only should match if oe is set
-            assert(uio_in == (uio_out & uio_oe));
+            ui_loop: assert(ui_in == uo_out);
+            // bidirectional outputs
+            bidir: assert(uio_in[7:4] == uio_out[3:0]);
+            // some covers
             cover(ui_in == 8'hAA);
             cover(uio_in == 8'hAA);
         end else begin
             // otherwise inputs must be 0
             assert(ui_in == 0);
+            assert(uio_in == 0);
             // design is in reset 
             assert(rst_n == 0);
             // no clock