formal mux proof

verilog/rtl/scan_controller/Makefile

diff --git a/verilog/rtl/scan_controller/Makefile b/verilog/rtl/scan_controller/Makefile
new file mode 100644
index 0000000..408fcf6
--- /dev/null
+++ b/verilog/rtl/scan_controller/Makefile
@@ -0,0 +1,2 @@
+prove_mux:
+	sby -f scan_mux.sby

verilog/rtl/scan_controller/properties.v

diff --git a/verilog/rtl/scan_controller/properties.v b/verilog/rtl/scan_controller/properties.v
new file mode 100644
index 0000000..c104f6a
--- /dev/null
+++ b/verilog/rtl/scan_controller/properties.v
@@ -0,0 +1,23 @@
+always @(*) begin
+    if(driver_sel == 2'b00) begin // external driver
+        assert(outputs[0]    == scan_data_in);
+        assert(scan_clk      == ext_scan_clk);
+        assert(scan_data_out == inputs[1]);
+        assert(scan_select   == inputs[2]);
+        assert(scan_latch_en == inputs[3]);
+    end else
+    if(driver_sel == 2'b10) begin // external driver
+        assert(la_scan_data_out == scan_data_in);
+        assert(scan_clk      == la_scan_clk);
+        assert(scan_data_out == la_scan_data_in);
+        assert(scan_select   == la_scan_select);
+        assert(scan_latch_en == la_scan_latch_en);
+    end else
+    if(driver_sel == 2'b01) begin // internal driver
+        assert(int_scan_data_out == scan_data_out);
+        assert(scan_clk      == int_scan_clk);
+        assert(scan_data_in  == int_scan_data_in);
+        assert(scan_select   == int_scan_select);
+        assert(scan_latch_en == int_scan_latch_en);
+    end
+end

verilog/rtl/scan_controller/scan_controller.v

diff --git a/verilog/rtl/scan_controller/scan_controller.v b/verilog/rtl/scan_controller/scan_controller.v
index 60b366b..d9f8f96 100644
--- a/verilog/rtl/scan_controller/scan_controller.v
+++ b/verilog/rtl/scan_controller/scan_controller.v
@@ -11,14 +11,14 @@
     output wire ready,                  // debug output that goes high once per refresh
     output wire slow_clk,               // debug clock divider output
 
-    output wire scan_clk,               // scan chain interface for the tiny designs
+    output wire scan_clk,               // scan chain interface for the tiny designs, from perspective of this module
     output wire scan_data_out,          // see diagrams below for how the scan chain works
     input  wire scan_data_in,           // will be driven by internal driver, external gpio pins, or Caravel logic analyser
     output wire scan_select,            // external scan chain driver muxes with ins/outs, eg microcontroller outside the ASIC
     output wire scan_latch_en,
 
     input  wire la_scan_clk,            // logic analyser scan chain driver, driven by firmware running on Caravel's VexRisc 
-    input  wire la_scan_data_in,
+    input  wire la_scan_data_in,        // signal names from perspective of this module
     output wire la_scan_data_out,
     input  wire la_scan_select,
     input  wire la_scan_latch_en,
@@ -40,18 +40,25 @@
     localparam LATCH = 4;
                     
     // scan chain muxing
-    wire ext_scan_clk;
-    wire ext_scan_data_out;
-    wire ext_scan_data_in;
-    wire ext_scan_select;
-    wire ext_scan_latch_en;
+    // signal names in perspective of this module
+    wire ext_scan_clk       = inputs[0];
+    wire ext_scan_data_in   = inputs[1];
+    wire ext_scan_data_out  = scan_data_in;
+    wire ext_scan_select    = inputs[2];   
+    wire ext_scan_latch_en  = inputs[3];
 
     assign scan_clk         = driver_sel == 2'b00 ? ext_scan_clk      : driver_sel == 2'b01 ? int_scan_clk      : la_scan_clk;
-    assign scan_data_out    = driver_sel == 2'b00 ? ext_scan_data_out : driver_sel == 2'b01 ? int_scan_data_out : la_scan_data_out;
+    assign scan_data_out    = driver_sel == 2'b00 ? ext_scan_data_in  : driver_sel == 2'b01 ? int_scan_data_out : la_scan_data_in;
     assign scan_select      = driver_sel == 2'b00 ? ext_scan_select   : driver_sel == 2'b01 ? int_scan_select   : la_scan_select;
     assign scan_latch_en    = driver_sel == 2'b00 ? ext_scan_latch_en : driver_sel == 2'b01 ? int_scan_latch_en : la_scan_latch_en;
 
-    wire   int_scan_data_in = scan_data_in;
+    wire int_scan_data_in   = scan_data_in;
+    wire la_scan_data_out   = scan_data_in;
+    assign outputs          = driver_sel == 2'b01 ? outputs_r : {7'b0, ext_scan_data_out};
+
+    `ifdef FORMAL
+        `include "properties.v"
+    `endif
 
     // reg
     reg [8:0] current_design;
@@ -65,7 +72,6 @@
     reg [7:0] output_buf;
 
     // wires
-    assign outputs = outputs_r;
     wire [8:0] active_select_rev = NUM_DESIGNS - 1 - active_select;
     assign ready = state == START;
     wire int_scan_latch_en = state == LATCH;
@@ -114,7 +120,7 @@
 
     */
 
-    // FSM
+    // FSM, only run it if driver_sel is set to internal
     always @(posedge clk) begin
         if(reset) begin
             current_design <= 0;
@@ -124,7 +130,7 @@
             scan_clk_r <= 0;
             num_io <= 0;
             output_buf <= 0;
-        end else begin
+        end else if (driver_sel == 2'b01) begin
             case(state)
                 START: begin
                     state <= LOAD;

verilog/rtl/scan_controller/scan_mux.sby

diff --git a/verilog/rtl/scan_controller/scan_mux.sby b/verilog/rtl/scan_controller/scan_mux.sby
new file mode 100644
index 0000000..57fe264
--- /dev/null
+++ b/verilog/rtl/scan_controller/scan_mux.sby
@@ -0,0 +1,13 @@
+[options]
+mode prove
+
+[engines]
+smtbmc
+
+[script]
+read -formal -DMPRJ_IO_PADS=38 scan_controller.v
+prep -top scan_controller
+
+[files]
+scan_controller.v
+properties.v