formal mux proof
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
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
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;
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
