Add initial filesHEADmaster

26 files changed, 4320 insertions, 0 deletions

diff --git a/presentation/ExampleRun/output2/fuzz_1/actual_correct.v b/presentation/ExampleRun/output2/fuzz_1/actual_correct.v
new file mode 100644
index 0000000..b82d0ac
--- /dev/null
+++ b/presentation/ExampleRun/output2/fuzz_1/actual_correct.v
@@ -0,0 +1,12 @@
+module top_1(y, clk, wire1);
+   input clk;
+   wire [1:0] reg4;
+   input wire1;
+   output [1:0] y;
+   reg reg4_reg[0]  = 1'b0;
+   always @(posedge clk)
+     reg4_reg[0]  <= wire1;
+   assign reg4[0] = reg4_reg[0] ;
+   assign reg4[1] = reg4[0];
+   assign y = { reg4[0], reg4[0] };
+endmodule
diff --git a/presentation/ExampleRun/output2/fuzz_1/actual_wrong.v b/presentation/ExampleRun/output2/fuzz_1/actual_wrong.v
new file mode 100644
index 0000000..31508e2
--- /dev/null
+++ b/presentation/ExampleRun/output2/fuzz_1/actual_wrong.v
@@ -0,0 +1,12 @@
+module top_1(y, clk, wire1);
+   input clk;
+   wire [1:0] reg4;
+   input wire1;
+   output [1:0] y;
+   reg reg4_reg[0]  = 1'hx;
+   always @(posedge clk)
+     reg4_reg[0]  <= wire1;
+   assign reg4[0] = reg4_reg[0] ;
+   assign reg4[1] = reg4[0];
+   assign y = { reg4[0], reg4[0] };
+endmodule
diff --git a/presentation/ExampleRun/output2/fuzz_1/equiv_identity_yosys/top.v b/presentation/ExampleRun/output2/fuzz_1/equiv_identity_yosys/top.v
new file mode 100644
index 0000000..0700c08
--- /dev/null
+++ b/presentation/ExampleRun/output2/fuzz_1/equiv_identity_yosys/top.v
@@ -0,0 +1,8 @@
+module top (y_1, y_2, clk, wire0, wire1, wire2, wire3);
+  top_gen top_gen (.y(y_1), .clk(clk), .wire0(wire0), .wire1(wire1), .wire2(wire2), .wire3(wire3));
+  top_syn top_syn (.y(y_2), .clk(clk), .wire0(wire0), .wire1(wire1), .wire2(wire2), .wire3(wire3));
+  always
+    @(posedge clk) begin
+      assert ((y_1 == y_2));
+    end
+endmodule
diff --git a/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity.v b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity.v
new file mode 100644
index 0000000..47c9bd6
--- /dev/null
+++ b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity.v
@@ -0,0 +1,77 @@
+// -*- mode: verilog -*-
+module top #(parameter param30 = (8'hbb)) (y, clk, wire0, wire1, wire2, wire3);
+  output [(32'hb7):(32'h0)] y;
+  input [(1'h0):(1'h0)] clk;
+  input signed [(5'h11):(1'h0)] wire0;
+  input signed [(4'ha):(1'h0)] wire1;
+  input [(4'hd):(1'h0)] wire2;
+  input [(4'h8):(1'h0)] wire3;
+  wire signed [(4'hb):(1'h0)] wire27;
+  wire [(5'h15):(1'h0)] wire26;
+  wire [(5'h10):(1'h0)] wire25;
+  wire [(5'h13):(1'h0)] wire24;
+  reg signed [(4'he):(1'h0)] reg4 = (1'h0);
+  reg [(2'h3):(1'h0)] reg5 = (1'h0);
+  reg [(5'h14):(1'h0)] reg6 = (1'h0);
+  reg signed [(5'h12):(1'h0)] reg7 = (1'h0);
+  reg [(4'hd):(1'h0)] reg8 = (1'h0);
+  wire [(4'hd):(1'h0)] wire9;
+  wire [(4'he):(1'h0)] wire10;
+  wire signed [(2'h2):(1'h0)] wire22;
+  assign y = {wire27, wire26, wire25, wire24, reg4, 
+              reg5, reg6, reg7, reg8, wire9, wire10, wire22};
+  always
+    @(posedge clk) begin
+      reg4 <=  wire1;
+      if ($unsigned((~&(8'hb2))))
+        begin
+          reg5 <=  reg4;
+          reg6 <=  wire1;
+        end
+      else
+        begin
+          reg5 <=  ($signed(reg7) ? wire2 : reg8[(4'h8):(2'h2)]);
+          reg6 <=  reg6;
+        end
+    end
+  always @* begin
+       reg7 = ((~|((wire0 & {wire3, reg4}) | $unsigned((reg4 != (8'h9d))))) <<< ((wire1[(2'h2):(2'h2)] + ((~(8'ha7)) ?
+                  wire3 : $signed(wire1))) ? $unsigned(((^wire0) + $unsigned(wire3))) : (((reg5 * wire3) ?
+                      wire1 : $unsigned(reg6)) ? {{reg4, wire2}} : (reg5[(1'h0):(1'h0)] ? $signed(reg4) : (~wire3)))));
+       reg8 = (~^$unsigned(reg6));
+  end
+  assign wire9 = (((8'ha2) ?
+                     wire3 : reg8[(4'h9):(4'h8)]) + $signed($signed(wire1)));
+  assign wire10 = $signed($signed($unsigned((~|(wire2 ? wire0 : wire0)))));
+  module11 modinst23 (.wire15(wire9), .wire16(wire3), .wire13(wire10), .wire12(wire1), .y(wire22), .wire14(wire0), .clk(clk));
+  assign wire24 = $signed((wire1 ?
+                      ((wire1 ? $unsigned(reg5) : ((8'hae) ? reg7 : wire9)) ?
+                          ($unsigned(wire0) && $signed(wire22)) : $unsigned(reg4[(2'h3):(2'h2)])) : $unsigned(wire0)));
+  assign wire25 = $unsigned($signed((~(|reg5))));
+  assign wire26 = reg4[(3'h5):(1'h0)];
+  assign wire27 = {(-wire0[(4'hd):(2'h2)]),
+                      $signed($signed(($signed(reg4) != $unsigned((7'h41)))))};
+endmodule
+
+module module11  (y, clk, wire16, wire15, wire14, wire13, wire12);
+  output wire  [(32'h40):(32'h0)] y;
+  input wire  [(1'h0):(1'h0)] clk;
+  input wire  [(2'h2):(1'h0)] wire16;
+  input wire signed [(3'h4):(1'h0)] wire15;
+  input wire signed [(5'h11):(1'h0)] wire14;
+  input wire signed [(4'he):(1'h0)] wire13;
+  input wire signed [(4'ha):(1'h0)] wire12;
+  wire signed [(4'hf):(1'h0)] wire21;
+  wire  [(4'hc):(1'h0)] wire20;
+  wire  [(3'h7):(1'h0)] wire19;
+  wire signed [(5'h11):(1'h0)] wire18;
+  wire signed [(4'hc):(1'h0)] wire17;
+  assign y = {wire21, wire20, wire19, wire18, wire17, (1'h0)};
+  assign wire17 = $unsigned(wire14[(1'h1):(1'h0)]);
+  assign wire18 = $unsigned(wire17);
+  assign wire19 = ($signed(((^wire18[(4'hb):(2'h3)]) ^ ((8'hb9) ?
+                          {(8'ha6), wire17} : $signed(wire16)))) ?
+                      wire12[(2'h3):(1'h0)] : (+(+wire15[(2'h3):(2'h2)])));
+  assign wire20 = (~|$signed(wire12));
+  assign wire21 = (|$unsigned($signed(((-wire19) | wire15))));
+endmodule
diff --git a/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_colour.v b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_colour.v
new file mode 100644
index 0000000..b2dcb5d
--- /dev/null
+++ b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_colour.v
@@ -0,0 +1,77 @@
+// -*- mode: verilog -*-
+module top #(parameter param30 = (8'hbb)) (y, clk, wire0, wire1, wire2, wire3);
+  output [(32'hb7):(32'h0)] y;
+  input [(1'h0):(1'h0)] clk;
+  input signed [(5'h11):(1'h0)] wire0;
+  input signed [(4'ha):(1'h0)] wire1;
+  input [(4'hd):(1'h0)] wire2;
+  input [(4'h8):(1'h0)] wire3;
+  wire signed [(4'hb):(1'h0)] wire27;
+  wire [(5'h15):(1'h0)] wire26;
+  wire [(5'h10):(1'h0)] wire25;
+  wire [(5'h13):(1'h0)] wire24;
+  reg signed [(4'he):(1'h0)] reg4 = (1'h0);
+  reg [(2'h3):(1'h0)] reg5 = (1'h0);
+  reg [(5'h14):(1'h0)] reg6 = (1'h0);
+  reg signed [(5'h12):(1'h0)] reg7 = (1'h0);
+  reg [(4'hd):(1'h0)] reg8 = (1'h0);
+  wire [(4'hd):(1'h0)] wire9;
+  wire [(4'he):(1'h0)] wire10;
+  wire signed [(2'h2):(1'h0)] wire22;
+  assign y = {wire27, wire26, wire25, wire24, reg4, 
+              reg5, reg6, reg7, reg8, wire9, wire10, ¬\colorbox{red!30}{wire22}¬};
+  always
+    @(posedge clk) begin
+      reg4 <=  wire1;
+      if ($unsigned((~&(8'hb2))))
+        begin
+          reg5 <=  reg4;
+          reg6 <=  wire1;
+        end
+      else
+        begin
+          reg5 <=  ($signed(reg7) ? wire2 : reg8[(4'h8):(2'h2)]);
+          reg6 <=  reg6;
+        end
+    end
+  always @* begin
+       reg7 = ((~|((wire0 & {wire3, reg4}) | $unsigned((reg4 != (8'h9d))))) <<< ((wire1[(2'h2):(2'h2)] + ((~(8'ha7)) ?
+                  wire3 : $signed(wire1))) ? $unsigned(((^wire0) + $unsigned(wire3))) : (((reg5 * wire3) ?
+                      wire1 : $unsigned(reg6)) ? {{reg4, wire2}} : (reg5[(1'h0):(1'h0)] ? $signed(reg4) : (~wire3)))));
+       reg8 = (~^$unsigned(reg6));
+  end
+  assign wire9 = (((8'ha2) ?
+                     wire3 : reg8[(4'h9):(4'h8)]) + $signed($signed(wire1)));
+  assign wire10 = $signed($signed($unsigned((~|(wire2 ? wire0 : wire0)))));
+  module11 modinst23 (.wire15(wire9), .wire16(wire3), .wire13(wire10), .wire12(wire1), .y(wire22), .wire14(wire0), .clk(clk));
+  assign wire24 = $signed((wire1 ?
+                      ((wire1 ? $unsigned(reg5) : ((8'hae) ? reg7 : wire9)) ?
+                          ($unsigned(wire0) && $signed(¬\colorbox{red!30}{wire22}¬)) : $unsigned(reg4[(2'h3):(2'h2)])) : $unsigned(wire0)));
+  assign wire25 = $unsigned($signed((~(|reg5))));
+  assign wire26 = reg4[(3'h5):(1'h0)];
+  assign wire27 = {(-wire0[(4'hd):(2'h2)]),
+                      $signed($signed(($signed(reg4) != $unsigned((7'h41)))))};
+endmodule
+
+module module11  (y, clk, wire16, wire15, wire14, wire13, wire12);
+  output wire  [(32'h40):(32'h0)] y;
+  input wire  [(1'h0):(1'h0)] clk;
+  input wire  [(2'h2):(1'h0)] wire16;
+  input wire signed [(3'h4):(1'h0)] wire15;
+  input wire signed [(5'h11):(1'h0)] wire14;
+  input wire signed [(4'he):(1'h0)] wire13;
+  input wire signed [(4'ha):(1'h0)] wire12;
+  wire signed [(4'hf):(1'h0)] wire21;
+  wire  [(4'hc):(1'h0)] wire20;
+  wire  [(3'h7):(1'h0)] wire19;
+  wire signed [(5'h11):(1'h0)] wire18;
+  wire signed [(4'hc):(1'h0)] wire17;
+  assign y = {wire21, wire20, wire19, wire18, wire17, (1'h0)};
+  assign wire17 = $unsigned(wire14[(1'h1):(1'h0)]);
+  assign wire18 = $unsigned(wire17);
+  assign wire19 = ($signed(((^wire18[(4'hb):(2'h3)]) ^ ((8'hb9) ?
+                          {(8'ha6), wire17} : $signed(wire16)))) ?
+                      wire12[(2'h3):(1'h0)] : (+(+wire15[(2'h3):(2'h2)])));
+  assign wire20 = (~|$signed(wire12));
+  assign wire21 = (|$unsigned($signed(((-wire19) | wire15))));
+endmodule
diff --git a/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red1.v b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red1.v
new file mode 100644
index 0000000..784ae4d
--- /dev/null
+++ b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red1.v
@@ -0,0 +1,52 @@
+// -*- mode: verilog -*-
+module top #(parameter param30 = (8'hbb)) (y, clk, wire0, wire1, wire2, wire3);
+  output [(32'hb7):(32'h0)] y;
+  input [(1'h0):(1'h0)] clk;
+  input signed [(5'h11):(1'h0)] wire0;
+  input signed [(4'ha):(1'h0)] wire1;
+  input [(4'hd):(1'h0)] wire2;
+  input [(4'h8):(1'h0)] wire3;
+  wire signed [(4'hb):(1'h0)] wire27;
+  wire [(5'h15):(1'h0)] wire26;
+  wire [(5'h10):(1'h0)] wire25;
+  wire [(5'h13):(1'h0)] wire24;
+  reg signed [(4'he):(1'h0)] reg4 = (1'h0);
+  reg [(2'h3):(1'h0)] reg5 = (1'h0);
+  reg [(5'h14):(1'h0)] reg6 = (1'h0);
+  reg signed [(5'h12):(1'h0)] reg7 = (1'h0);
+  reg [(4'hd):(1'h0)] reg8 = (1'h0);
+  wire [(4'hd):(1'h0)] wire9;
+  wire [(4'he):(1'h0)] wire10;
+  assign y = {wire27, wire26, wire25, wire24, reg4, 
+              reg5, reg6, reg7, reg8, wire9, wire10};
+  always
+    @(posedge clk) begin
+      reg4 <=  wire1;
+      if ($unsigned((~&(8'hb2))))
+        begin
+          reg5 <=  reg4;
+          reg6 <=  wire1;
+        end
+      else
+        begin
+          reg5 <=  ($signed(reg7) ? wire2 : reg8[(4'h8):(2'h2)]);
+          reg6 <=  reg6;
+        end
+    end
+  always @* begin
+       reg7 = ((~|((wire0 & {wire3, reg4}) | $unsigned((reg4 != (8'h9d))))) <<< ((wire1[(2'h2):(2'h2)] + ((~(8'ha7)) ?
+                  wire3 : $signed(wire1))) ? $unsigned(((^wire0) + $unsigned(wire3))) : (((reg5 * wire3) ?
+                      wire1 : $unsigned(reg6)) ? {{reg4, wire2}} : (reg5[(1'h0):(1'h0)] ? $signed(reg4) : (~wire3)))));
+       reg8 = (~^$unsigned(reg6));
+  end
+  assign wire9 = (((8'ha2) ?
+                     wire3 : reg8[(4'h9):(4'h8)]) + $signed($signed(wire1)));
+  assign wire10 = $signed($signed($unsigned((~|(wire2 ? wire0 : wire0)))));
+  assign wire24 = $signed((wire1 ?
+                      ((wire1 ? $unsigned(reg5) : ((8'hae) ? reg7 : wire9)) ?
+                          ($unsigned(wire0) && 1'b0) : $unsigned(reg4[(2'h3):(2'h2)])) : $unsigned(wire0)));
+  assign wire25 = $unsigned($signed((~(|reg5))));
+  assign wire26 = reg4[(3'h5):(1'h0)];
+  assign wire27 = {(-wire0[(4'hd):(2'h2)]),
+                      $signed($signed(($signed(reg4) != $unsigned((7'h41)))))};
+endmodule
diff --git a/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red1_colour.v b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red1_colour.v
new file mode 100644
index 0000000..5750a54
--- /dev/null
+++ b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red1_colour.v
@@ -0,0 +1,52 @@
+// -*- mode: verilog -*-
+module top #(parameter param30 = (8'hbb)) (y, clk, wire0, wire1, wire2, wire3);
+  output [(32'hb7):(32'h0)] y;
+  input [(1'h0):(1'h0)] clk;
+  input signed [(5'h11):(1'h0)] wire0;
+  input signed [(4'ha):(1'h0)] wire1;
+  input [(4'hd):(1'h0)] wire2;
+  input [(4'h8):(1'h0)] wire3;
+  wire signed [(4'hb):(1'h0)] wire27;
+  wire [(5'h15):(1'h0)] wire26;
+  wire [(5'h10):(1'h0)] wire25;
+  wire [(5'h13):(1'h0)] wire24;
+  reg signed [(4'he):(1'h0)] reg4 = (1'h0);
+  reg [(2'h3):(1'h0)] reg5 = (1'h0);
+  reg [(5'h14):(1'h0)] reg6 = (1'h0);
+  reg signed [(5'h12):(1'h0)] reg7 = (1'h0);
+  reg [(4'hd):(1'h0)] reg8 = (1'h0);
+  wire [(4'hd):(1'h0)] wire9;
+  wire [(4'he):(1'h0)] wire10;
+  assign y = {¬\colorbox{red!30}{wire27, wire26, wire25, wire24}¬, reg4, 
+              reg5, reg6, reg7, reg8, wire9, wire10};
+  always
+    @(posedge clk) begin
+      reg4 <=  wire1;
+      if ($unsigned((~&(8'hb2))))
+        begin
+          reg5 <=  reg4;
+          reg6 <=  wire1;
+        end
+      else
+        begin
+          reg5 <=  ($signed(reg7) ? wire2 : reg8[(4'h8):(2'h2)]);
+          reg6 <=  reg6;
+        end
+    end
+  always @* begin
+       reg7 = ((~|((wire0 & {wire3, reg4}) | $unsigned((reg4 != (8'h9d))))) <<< ((wire1[(2'h2):(2'h2)] + ((~(8'ha7)) ?
+                  wire3 : $signed(wire1))) ? $unsigned(((^wire0) + $unsigned(wire3))) : (((reg5 * wire3) ?
+                      wire1 : $unsigned(reg6)) ? {{reg4, wire2}} : (reg5[(1'h0):(1'h0)] ? $signed(reg4) : (~wire3)))));
+       reg8 = (~^$unsigned(reg6));
+  end
+  assign wire9 = (((8'ha2) ?
+                     wire3 : reg8[(4'h9):(4'h8)]) + $signed($signed(wire1)));
+  assign wire10 = $signed($signed($unsigned((~|(wire2 ? wire0 : wire0)))));
+  assign wire24 = $signed((wire1 ?
+                      ((wire1 ? $unsigned(reg5) : ((8'hae) ? reg7 : wire9)) ?
+                          ($unsigned(wire0) && 1'b0) : $unsigned(reg4[(2'h3):(2'h2)])) : $unsigned(wire0)));
+  assign wire25 = $unsigned($signed((~(|reg5))));
+  assign wire26 = reg4[(3'h5):(1'h0)];
+  assign wire27 = {(-wire0[(4'hd):(2'h2)]),
+                      $signed($signed(($signed(reg4) != $unsigned((7'h41)))))};
+endmodule
diff --git a/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red2.v b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red2.v
new file mode 100644
index 0000000..7cffea0
--- /dev/null
+++ b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red2.v
@@ -0,0 +1,40 @@
+// -*- mode: verilog -*-
+module top #(parameter param30 = (8'hbb)) (y, clk, wire0, wire1, wire2, wire3);
+  output [(32'hb7):(32'h0)] y;
+  input [(1'h0):(1'h0)] clk;
+  input signed [(5'h11):(1'h0)] wire0;
+  input signed [(4'ha):(1'h0)] wire1;
+  input [(4'hd):(1'h0)] wire2;
+  input [(4'h8):(1'h0)] wire3;
+  reg signed [(4'he):(1'h0)] reg4 = (1'h0);
+  reg [(2'h3):(1'h0)] reg5 = (1'h0);
+  reg [(5'h14):(1'h0)] reg6 = (1'h0);
+  reg signed [(5'h12):(1'h0)] reg7 = (1'h0);
+  reg [(4'hd):(1'h0)] reg8 = (1'h0);
+  wire [(4'hd):(1'h0)] wire9;
+  wire [(4'he):(1'h0)] wire10;
+  assign y = {reg4, reg5, reg6, reg7, reg8, wire9, wire10};
+  always
+    @(posedge clk) begin
+      reg4 <=  wire1;
+      if ($unsigned((~&(8'hb2))))
+        begin
+          reg5 <=  reg4;
+          reg6 <=  wire1;
+        end
+      else
+        begin
+          reg5 <=  ($signed(reg7) ? wire2 : reg8[(4'h8):(2'h2)]);
+          reg6 <=  reg6;
+        end
+    end
+  always @* begin
+       reg7 = ((~|((wire0 & {wire3, reg4}) | $unsigned((reg4 != (8'h9d))))) <<< ((wire1[(2'h2):(2'h2)] + ((~(8'ha7)) ?
+                  wire3 : $signed(wire1))) ? $unsigned(((^wire0) + $unsigned(wire3))) : (((reg5 * wire3) ?
+                      wire1 : $unsigned(reg6)) ? {{reg4, wire2}} : (reg5[(1'h0):(1'h0)] ? $signed(reg4) : (~wire3)))));
+       reg8 = (~^$unsigned(reg6));
+  end
+  assign wire9 = (((8'ha2) ?
+                     wire3 : reg8[(4'h9):(4'h8)]) + $signed($signed(wire1)));
+  assign wire10 = $signed($signed($unsigned((~|(wire2 ? wire0 : wire0)))));
+endmodule
diff --git a/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red2_colour.v b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red2_colour.v
new file mode 100644
index 0000000..f3904b4
--- /dev/null
+++ b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red2_colour.v
@@ -0,0 +1,40 @@
+// -*- mode: verilog -*-
+module top #(parameter param30 = (8'hbb)) (y, clk, wire0, wire1, wire2, wire3);
+  output [(32'hb7):(32'h0)] y;
+  input [(1'h0):(1'h0)] clk;
+  input signed [(5'h11):(1'h0)] wire0;
+  input signed [(4'ha):(1'h0)] wire1;
+  input [(4'hd):(1'h0)] wire2;
+  input [(4'h8):(1'h0)] wire3;
+  reg signed [(4'he):(1'h0)] reg4 = (1'h0);
+  reg [(2'h3):(1'h0)] reg5 = (1'h0);
+  reg [(5'h14):(1'h0)] reg6 = (1'h0);
+  reg signed [(5'h12):(1'h0)] reg7 = (1'h0);
+  reg [(4'hd):(1'h0)] reg8 = (1'h0);
+  wire [(4'hd):(1'h0)] wire9;
+  wire [(4'he):(1'h0)] wire10;
+  assign y = {¬\colorbox{green!30}{reg4, reg5, reg6, reg7, reg8}¬, wire9, wire10};
+  always
+    @(posedge clk) begin
+      reg4 <=  wire1;
+      if ($unsigned((~&(8'hb2))))
+        begin
+          reg5 <=  reg4;
+          reg6 <=  wire1;
+        end
+      else
+        begin
+          reg5 <=  ($signed(reg7) ? wire2 : reg8[(4'h8):(2'h2)]);
+          reg6 <=  reg6;
+        end
+    end
+  always @* begin
+       reg7 = ((~|((wire0 & {wire3, reg4}) | $unsigned((reg4 != (8'h9d))))) <<< ((wire1[(2'h2):(2'h2)] + ((~(8'ha7)) ?
+                  wire3 : $signed(wire1))) ? $unsigned(((^wire0) + $unsigned(wire3))) : (((reg5 * wire3) ?
+                      wire1 : $unsigned(reg6)) ? {{reg4, wire2}} : (reg5[(1'h0):(1'h0)] ? $signed(reg4) : (~wire3)))));
+       reg8 = (~^$unsigned(reg6));
+  end
+  assign wire9 = (((8'ha2) ?
+                     wire3 : ¬\colorbox{green!30}{reg8[(4'h9):(4'h8)]}¬) + $signed($signed(wire1)));
+  assign wire10 = $signed($signed($unsigned((~|(wire2 ? wire0 : wire0)))));
+endmodule
diff --git a/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red2_colour2.v b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red2_colour2.v
new file mode 100644
index 0000000..be8b21b
--- /dev/null
+++ b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red2_colour2.v
@@ -0,0 +1,40 @@
+// -*- mode: verilog -*-
+module top #(parameter param30 = (8'hbb)) (y, clk, wire0, wire1, wire2, wire3);
+  output [(32'hb7):(32'h0)] y;
+  input [(1'h0):(1'h0)] clk;
+  input signed [(5'h11):(1'h0)] wire0;
+  input signed [(4'ha):(1'h0)] wire1;
+  input [(4'hd):(1'h0)] wire2;
+  input [(4'h8):(1'h0)] wire3;
+  reg signed [(4'he):(1'h0)] reg4 = (1'h0);
+  reg [(2'h3):(1'h0)] reg5 = (1'h0);
+  reg [(5'h14):(1'h0)] reg6 = (1'h0);
+  reg signed [(5'h12):(1'h0)] reg7 = (1'h0);
+  reg [(4'hd):(1'h0)] reg8 = (1'h0);
+  wire [(4'hd):(1'h0)] wire9;
+  wire [(4'he):(1'h0)] wire10;
+  assign y = {reg4, reg5, reg6, reg7, reg8, ¬\colorbox{red!30}{wire9, wire10}¬};
+  always
+    @(posedge clk) begin
+      reg4 <=  wire1;
+      if ($unsigned((~&(8'hb2))))
+        begin
+          reg5 <=  reg4;
+          reg6 <=  wire1;
+        end
+      else
+        begin
+          reg5 <=  ($signed(reg7) ? wire2 : reg8[(4'h8):(2'h2)]);
+          reg6 <=  reg6;
+        end
+    end
+  always @* begin
+       reg7 = ((~|((wire0 & {wire3, reg4}) | $unsigned((reg4 != (8'h9d))))) <<< ((wire1[(2'h2):(2'h2)] + ((~(8'ha7)) ?
+                  wire3 : $signed(wire1))) ? $unsigned(((^wire0) + $unsigned(wire3))) : (((reg5 * wire3) ?
+                      wire1 : $unsigned(reg6)) ? {{reg4, wire2}} : (reg5[(1'h0):(1'h0)] ? $signed(reg4) : (~wire3)))));
+       reg8 = (~^$unsigned(reg6));
+  end
+  assign wire9 = (((8'ha2) ?
+                     wire3 : reg8[(4'h9):(4'h8)]) + $signed($signed(wire1)));
+  assign wire10 = $signed($signed($unsigned((~|(wire2 ? wire0 : wire0)))));
+endmodule
diff --git a/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red3.v b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red3.v
new file mode 100644
index 0000000..81b030d
--- /dev/null
+++ b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red3.v
@@ -0,0 +1,35 @@
+// -*- mode: verilog -*-
+module top #(parameter param30 = (8'hbb)) (y, clk, wire0, wire1, wire2, wire3);
+  output [(32'hb7):(32'h0)] y;
+  input [(1'h0):(1'h0)] clk;
+  input signed [(5'h11):(1'h0)] wire0;
+  input signed [(4'ha):(1'h0)] wire1;
+  input [(4'hd):(1'h0)] wire2;
+  input [(4'h8):(1'h0)] wire3;
+  reg signed [(4'he):(1'h0)] reg4 = (1'h0);
+  reg [(2'h3):(1'h0)] reg5 = (1'h0);
+  reg [(5'h14):(1'h0)] reg6 = (1'h0);
+  reg signed [(5'h12):(1'h0)] reg7 = (1'h0);
+  reg [(4'hd):(1'h0)] reg8 = (1'h0);
+  assign y = {reg4, reg5, reg6, reg7, reg8};
+  always
+    @(posedge clk) begin
+      reg4 <=  wire1;
+      if ($unsigned((~&(8'hb2))))
+        begin
+          reg5 <=  reg4;
+          reg6 <=  wire1;
+        end
+      else
+        begin
+          reg5 <=  ($signed(reg7) ? wire2 : reg8[(4'h8):(2'h2)]);
+          reg6 <=  reg6;
+        end
+    end
+  always @* begin
+       reg7 = ((~|((wire0 & {wire3, reg4}) | $unsigned((reg4 != (8'h9d))))) <<< ((wire1[(2'h2):(2'h2)] + ((~(8'ha7)) ?
+                  wire3 : $signed(wire1))) ? $unsigned(((^wire0) + $unsigned(wire3))) : (((reg5 * wire3) ?
+                      wire1 : $unsigned(reg6)) ? {{reg4, wire2}} : (reg5[(1'h0):(1'h0)] ? $signed(reg4) : (~wire3)))));
+       reg8 = (~^$unsigned(reg6));
+  end
+endmodule
diff --git a/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red4.v b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red4.v
new file mode 100644
index 0000000..fd3fd3c
--- /dev/null
+++ b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red4.v
@@ -0,0 +1,27 @@
+// -*- mode: verilog -*-
+module top #(parameter param30 = (8'hbb)) (y, clk, wire0, wire1, wire2, wire3);
+  output [(32'hb7):(32'h0)] y;
+  input [(1'h0):(1'h0)] clk;
+  input signed [(5'h11):(1'h0)] wire0;
+  input signed [(4'ha):(1'h0)] wire1;
+  input [(4'hd):(1'h0)] wire2;
+  input [(4'h8):(1'h0)] wire3;
+  reg signed [(4'he):(1'h0)] reg4 = (1'h0);
+  reg [(2'h3):(1'h0)] reg5 = (1'h0);
+  reg [(5'h14):(1'h0)] reg6 = (1'h0);
+  assign y = {reg4, reg5, reg6};
+  always
+    @(posedge clk) begin
+      reg4 <=  wire1;
+      if ($unsigned((~&(8'hb2))))
+        begin
+          reg5 <=  reg4;
+          reg6 <=  wire1;
+        end
+      else
+        begin
+          reg5 <=  ((1'b0) ? wire2 : (1'b0));
+          reg6 <=  reg6;
+        end
+    end
+endmodule
diff --git a/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red5.v b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red5.v
new file mode 100644
index 0000000..7f046e7
--- /dev/null
+++ b/presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red5.v
@@ -0,0 +1,15 @@
+// -*- mode: verilog -*-
+module top #(parameter param30 = (8'hbb)) (y, clk, wire0, wire1, wire2, wire3);
+  output [(32'hb7):(32'h0)] y;
+  input [(1'h0):(1'h0)] clk;
+  input signed [(5'h11):(1'h0)] wire0;
+  input signed [(4'ha):(1'h0)] wire1;
+  input [(4'hd):(1'h0)] wire2;
+  input [(4'h8):(1'h0)] wire3;
+  reg signed [(4'he):(1'h0)] reg4 = (1'h0);
+  assign y = {reg4};
+  always
+    @(posedge clk) begin
+      reg4 <=  wire1;
+    end
+endmodule
diff --git a/presentation/ExampleRun/output2/fuzz_1/reduce_identity_yosys.v b/presentation/ExampleRun/output2/fuzz_1/reduce_identity_yosys.v
new file mode 100644
index 0000000..3d5af91
--- /dev/null
+++ b/presentation/ExampleRun/output2/fuzz_1/reduce_identity_yosys.v
@@ -0,0 +1,9 @@
+module top (y, clk, wire1);
+   output wire [(32'hb7):(32'h0)] y;
+   input wire [(1'h0):(1'h0)] clk;
+   input wire signed [(4'ha):(1'h0)] wire1;
+   reg signed [(4'he):(1'h0)] reg4 = (1'h0);
+   assign y = {reg4};
+   always
+     @(posedge clk) reg4 <=  wire1;
+endmodule
diff --git a/presentation/ExampleRun/output2/fuzz_1/reduce_sim_yosys.v b/presentation/ExampleRun/output2/fuzz_1/reduce_sim_yosys.v
new file mode 100644
index 0000000..ea01016
--- /dev/null
+++ b/presentation/ExampleRun/output2/fuzz_1/reduce_sim_yosys.v
@@ -0,0 +1,27 @@
+// -*- mode: verilog -*-
+module top  (y, clk, wire0, wire1, wire2, wire3);
+  output wire  [(32'hb7):(32'h0)] y  ;
+  input wire  [(1'h0):(1'h0)] clk  ;
+  input wire signed [(5'h11):(1'h0)] wire0  ;
+  input wire signed [(4'ha):(1'h0)] wire1  ;
+  input wire  [(4'hd):(1'h0)] wire2  ;
+  input wire  [(4'h8):(1'h0)] wire3  ;
+   reg  [(2'h3):(1'h0)] reg5 = (1'h0) ;
+   reg  [(5'h14):(1'h0)] reg6 = (1'h0) ;
+   reg signed [(5'h12):(1'h0)] reg7 = (1'h0) ;
+   reg  [(4'hd):(1'h0)] reg8 = (1'h0) ;
+  assign y = {reg5, reg6, reg7, reg8} ;
+  always
+    @(posedge clk) begin
+      reg5 <=  (1'h0);
+      reg6 <=  wire1;
+      reg7 <=  ((~|((wire0 & {wire3,
+          (1'h0)}) | $unsigned(((1'h0) != (8'h9d))))) <<< ((wire1[(2'h2):(2'h2)] + ((~(8'ha7)) ?
+              wire3 : $signed(wire1))) ?
+          $unsigned(((^wire0) + $unsigned(wire3))) : (((reg5 * wire3) ?
+                  wire1 : $unsigned(reg6)) ?
+              {{(1'h0), wire2}} : (reg5[(1'h0):(1'h0)] ?
+                  $signed((1'h0)) : (~wire3)))));
+      reg8 <=  (~^$unsigned(reg6));
+    end
+endmodule
\ No newline at end of file
diff --git a/presentation/ExampleRun/output2/fuzz_1/yosys/syn_yosys.v b/presentation/ExampleRun/output2/fuzz_1/yosys/syn_yosys.v
new file mode 100644
index 0000000..d7ba555
--- /dev/null
+++ b/presentation/ExampleRun/output2/fuzz_1/yosys/syn_yosys.v
@@ -0,0 +1,1441 @@
+/* Generated by Yosys 0.8+415 (git sha1 3333e002, clang 9.0.0 -fPIC -Os) */
+
+module module11(y, clk, wire16, wire15, wire14, wire13, wire12);
+  wire _00_;
+  wire _01_;
+  wire _02_;
+  wire _03_;
+  wire _04_;
+  wire _05_;
+  wire _06_;
+  wire _07_;
+  wire _08_;
+  wire _09_;
+  wire _10_;
+  wire _11_;
+  wire _12_;
+  wire _13_;
+  wire _14_;
+  wire _15_;
+  wire _16_;
+  wire _17_;
+  wire _18_;
+  wire _19_;
+  wire _20_;
+  wire _21_;
+  wire _22_;
+  wire _23_;
+  wire _24_;
+  wire _25_;
+  input clk;
+  input [10:0] wire12;
+  input [14:0] wire13;
+  input [17:0] wire14;
+  input [4:0] wire15;
+  input [2:0] wire16;
+  wire [1:0] wire17;
+  wire [1:0] wire18;
+  wire [3:0] wire19;
+  wire wire20;
+  wire wire21;
+  output [64:0] y;
+  assign _00_ = wire12[2] | wire12[3];
+  assign _01_ = wire12[0] | wire12[1];
+  assign _02_ = _01_ | _00_;
+  assign _03_ = _02_ | wire15[4];
+  assign _04_ = _01_ | wire12[2];
+  assign _05_ = _04_ ^ wire12[3];
+  assign _06_ = _05_ | wire15[3];
+  assign _07_ = _01_ ^ wire12[2];
+  assign _08_ = _07_ | wire15[2];
+  assign _09_ = _08_ | _06_;
+  assign _10_ = wire12[0] ^ wire12[1];
+  assign _11_ = _10_ | wire15[1];
+  assign _12_ = wire15[0] | wire12[0];
+  assign _13_ = _12_ | _11_;
+  assign _14_ = _13_ | _09_;
+  assign wire21 = _14_ | _03_;
+  assign _15_ = ~(wire12[9] | wire12[10]);
+  assign _16_ = wire12[7] | wire12[8];
+  assign _17_ = _15_ & ~(_16_);
+  assign _18_ = wire12[5] | wire12[6];
+  assign _19_ = wire12[3] | wire12[4];
+  assign _20_ = _19_ | _18_;
+  assign _21_ = _17_ & ~(_20_);
+  assign _22_ = wire12[1] | wire12[2];
+  assign _23_ = _22_ | wire12[0];
+  assign wire20 = _21_ & ~(_23_);
+  assign _25_ = wire21;
+  assign _24_ = wire20;
+  assign wire17 = wire14[1:0];
+  assign wire18 = wire14[1:0];
+  assign wire19 = wire12[3:0];
+  assign y = { 11'h000, wire21, 12'h000, wire20, 4'h0, wire12[3:0], 16'h0000, wire14[1:0], 11'h000, wire14[1:0], 1'h0 };
+endmodule
+
+module top(y, clk, wire0, wire1, wire2, wire3);
+  wire [18:0] _0000_;
+  wire _0001_;
+  wire _0002_;
+  wire _0003_;
+  wire _0004_;
+  wire _0005_;
+  wire _0006_;
+  wire _0007_;
+  wire _0008_;
+  wire _0009_;
+  wire _0010_;
+  wire _0011_;
+  wire _0012_;
+  wire _0013_;
+  wire _0014_;
+  wire _0015_;
+  wire _0016_;
+  wire _0017_;
+  wire _0018_;
+  wire _0019_;
+  wire _0020_;
+  wire _0021_;
+  wire _0022_;
+  wire _0023_;
+  wire _0024_;
+  wire _0025_;
+  wire _0026_;
+  wire _0027_;
+  wire _0028_;
+  wire _0029_;
+  wire _0030_;
+  wire _0031_;
+  wire _0032_;
+  wire _0033_;
+  wire _0034_;
+  wire _0035_;
+  wire _0036_;
+  wire _0037_;
+  wire _0038_;
+  wire _0039_;
+  wire _0040_;
+  wire _0041_;
+  wire _0042_;
+  wire _0043_;
+  wire _0044_;
+  wire _0045_;
+  wire _0046_;
+  wire _0047_;
+  wire _0048_;
+  wire _0049_;
+  wire _0050_;
+  wire _0051_;
+  wire _0052_;
+  wire _0053_;
+  wire _0054_;
+  wire _0055_;
+  wire _0056_;
+  wire _0057_;
+  wire _0058_;
+  wire _0059_;
+  wire _0060_;
+  wire _0061_;
+  wire _0062_;
+  wire _0063_;
+  wire _0064_;
+  wire _0065_;
+  wire _0066_;
+  wire _0067_;
+  wire _0068_;
+  wire _0069_;
+  wire _0070_;
+  wire _0071_;
+  wire _0072_;
+  wire _0073_;
+  wire _0074_;
+  wire _0075_;
+  wire _0076_;
+  wire _0077_;
+  wire _0078_;
+  wire _0079_;
+  wire _0080_;
+  wire _0081_;
+  wire _0082_;
+  wire _0083_;
+  wire _0084_;
+  wire _0085_;
+  wire _0086_;
+  wire _0087_;
+  wire _0088_;
+  wire _0089_;
+  wire _0090_;
+  wire _0091_;
+  wire _0092_;
+  wire _0093_;
+  wire _0094_;
+  wire _0095_;
+  wire _0096_;
+  wire _0097_;
+  wire _0098_;
+  wire _0099_;
+  wire _0100_;
+  wire _0101_;
+  wire _0102_;
+  wire _0103_;
+  wire _0104_;
+  wire _0105_;
+  wire _0106_;
+  wire _0107_;
+  wire _0108_;
+  wire _0109_;
+  wire _0110_;
+  wire _0111_;
+  wire _0112_;
+  wire _0113_;
+  wire _0114_;
+  wire _0115_;
+  wire _0116_;
+  wire _0117_;
+  wire _0118_;
+  wire _0119_;
+  wire _0120_;
+  wire _0121_;
+  wire _0122_;
+  wire _0123_;
+  wire _0124_;
+  wire _0125_;
+  wire _0126_;
+  wire _0127_;
+  wire _0128_;
+  wire _0129_;
+  wire _0130_;
+  wire _0131_;
+  wire _0132_;
+  wire _0133_;
+  wire _0134_;
+  wire _0135_;
+  wire _0136_;
+  wire _0137_;
+  wire _0138_;
+  wire _0139_;
+  wire _0140_;
+  wire _0141_;
+  wire _0142_;
+  wire _0143_;
+  wire _0144_;
+  wire _0145_;
+  wire _0146_;
+  wire _0147_;
+  wire _0148_;
+  wire _0149_;
+  wire _0150_;
+  wire _0151_;
+  wire _0152_;
+  wire _0153_;
+  wire _0154_;
+  wire _0155_;
+  wire _0156_;
+  wire _0157_;
+  wire _0158_;
+  wire _0159_;
+  wire _0160_;
+  wire _0161_;
+  wire _0162_;
+  wire _0163_;
+  wire _0164_;
+  wire _0165_;
+  wire _0166_;
+  wire _0167_;
+  wire _0168_;
+  wire _0169_;
+  wire _0170_;
+  wire _0171_;
+  wire _0172_;
+  wire _0173_;
+  wire _0174_;
+  wire _0175_;
+  wire _0176_;
+  wire _0177_;
+  wire _0178_;
+  wire _0179_;
+  wire _0180_;
+  wire _0181_;
+  wire _0182_;
+  wire _0183_;
+  wire _0184_;
+  wire _0185_;
+  wire _0186_;
+  wire _0187_;
+  wire _0188_;
+  wire _0189_;
+  wire _0190_;
+  wire _0191_;
+  wire _0192_;
+  wire _0193_;
+  wire _0194_;
+  wire _0195_;
+  wire _0196_;
+  wire _0197_;
+  wire _0198_;
+  wire _0199_;
+  wire _0200_;
+  wire _0201_;
+  wire _0202_;
+  wire _0203_;
+  wire _0204_;
+  wire _0205_;
+  wire _0206_;
+  wire _0207_;
+  wire _0208_;
+  wire _0209_;
+  wire _0210_;
+  wire _0211_;
+  wire _0212_;
+  wire _0213_;
+  wire _0214_;
+  wire _0215_;
+  wire _0216_;
+  wire _0217_;
+  wire _0218_;
+  wire _0219_;
+  wire _0220_;
+  wire _0221_;
+  wire _0222_;
+  wire _0223_;
+  wire _0224_;
+  wire _0225_;
+  wire _0226_;
+  wire _0227_;
+  wire _0228_;
+  wire _0229_;
+  wire _0230_;
+  wire _0231_;
+  wire _0232_;
+  wire _0233_;
+  wire _0234_;
+  wire _0235_;
+  wire _0236_;
+  wire _0237_;
+  wire _0238_;
+  wire _0239_;
+  wire _0240_;
+  wire _0241_;
+  wire _0242_;
+  wire _0243_;
+  wire _0244_;
+  wire _0245_;
+  wire _0246_;
+  wire _0247_;
+  wire _0248_;
+  wire _0249_;
+  wire _0250_;
+  wire _0251_;
+  wire _0252_;
+  wire _0253_;
+  wire _0254_;
+  wire _0255_;
+  wire _0256_;
+  wire _0257_;
+  wire _0258_;
+  wire _0259_;
+  wire _0260_;
+  wire _0261_;
+  wire _0262_;
+  wire _0263_;
+  wire _0264_;
+  wire _0265_;
+  wire _0266_;
+  wire _0267_;
+  wire _0268_;
+  wire _0269_;
+  wire _0270_;
+  wire _0271_;
+  wire _0272_;
+  wire _0273_;
+  wire _0274_;
+  wire _0275_;
+  wire _0276_;
+  wire _0277_;
+  wire _0278_;
+  wire _0279_;
+  wire _0280_;
+  wire _0281_;
+  wire _0282_;
+  wire _0283_;
+  wire _0284_;
+  wire _0285_;
+  wire _0286_;
+  wire _0287_;
+  wire _0288_;
+  wire _0289_;
+  wire _0290_;
+  wire _0291_;
+  wire _0292_;
+  wire _0293_;
+  wire _0294_;
+  wire _0295_;
+  wire _0296_;
+  wire _0297_;
+  wire _0298_;
+  wire _0299_;
+  wire _0300_;
+  wire _0301_;
+  wire _0302_;
+  wire _0303_;
+  wire _0304_;
+  wire _0305_;
+  wire _0306_;
+  wire _0307_;
+  wire _0308_;
+  wire _0309_;
+  wire _0310_;
+  wire _0311_;
+  wire _0312_;
+  wire _0313_;
+  wire _0314_;
+  wire _0315_;
+  wire _0316_;
+  wire _0317_;
+  wire _0318_;
+  wire _0319_;
+  wire _0320_;
+  wire _0321_;
+  wire _0322_;
+  wire _0323_;
+  wire _0324_;
+  wire _0325_;
+  wire _0326_;
+  wire _0327_;
+  wire _0328_;
+  wire _0329_;
+  wire _0330_;
+  wire _0331_;
+  wire _0332_;
+  wire _0333_;
+  wire _0334_;
+  wire _0335_;
+  wire _0336_;
+  wire _0337_;
+  wire _0338_;
+  wire _0339_;
+  wire _0340_;
+  wire _0341_;
+  wire _0342_;
+  wire _0343_;
+  wire _0344_;
+  wire _0345_;
+  wire _0346_;
+  wire _0347_;
+  wire _0348_;
+  wire _0349_;
+  wire _0350_;
+  wire _0351_;
+  wire _0352_;
+  wire _0353_;
+  wire _0354_;
+  wire _0355_;
+  wire _0356_;
+  wire _0357_;
+  wire _0358_;
+  wire _0359_;
+  wire _0360_;
+  wire _0361_;
+  wire _0362_;
+  wire _0363_;
+  wire _0364_;
+  wire _0365_;
+  wire _0366_;
+  wire _0367_;
+  wire _0368_;
+  wire _0369_;
+  wire _0370_;
+  wire _0371_;
+  wire _0372_;
+  wire _0373_;
+  wire _0374_;
+  wire _0375_;
+  wire _0376_;
+  wire _0377_;
+  wire _0378_;
+  wire _0379_;
+  wire _0380_;
+  wire _0381_;
+  wire _0382_;
+  wire _0383_;
+  wire _0384_;
+  wire _0385_;
+  wire _0386_;
+  wire _0387_;
+  wire _0388_;
+  wire _0389_;
+  wire _0390_;
+  wire _0391_;
+  wire _0392_;
+  wire _0393_;
+  wire _0394_;
+  wire _0395_;
+  wire _0396_;
+  wire _0397_;
+  wire _0398_;
+  wire _0399_;
+  wire _0400_;
+  wire _0401_;
+  wire _0402_;
+  wire _0403_;
+  wire _0404_;
+  wire _0405_;
+  wire _0406_;
+  wire _0407_;
+  wire _0408_;
+  wire _0409_;
+  wire _0410_;
+  wire _0411_;
+  wire _0412_;
+  wire _0413_;
+  wire _0414_;
+  wire _0415_;
+  wire _0416_;
+  wire _0417_;
+  wire _0418_;
+  wire _0419_;
+  wire _0420_;
+  wire _0421_;
+  wire _0422_;
+  wire _0423_;
+  wire _0424_;
+  wire _0425_;
+  wire _0426_;
+  wire _0427_;
+  wire _0428_;
+  wire _0429_;
+  wire _0430_;
+  wire _0431_;
+  wire _0432_;
+  wire _0433_;
+  wire _0434_;
+  wire _0435_;
+  wire _0436_;
+  wire _0437_;
+  wire _0438_;
+  wire _0439_;
+  wire _0440_;
+  wire _0441_;
+  wire _0442_;
+  wire _0443_;
+  wire _0444_;
+  wire _0445_;
+  wire _0446_;
+  wire _0447_;
+  wire _0448_;
+  wire _0449_;
+  wire _0450_;
+  wire _0451_;
+  wire _0452_;
+  wire _0453_;
+  wire _0454_;
+  wire _0455_;
+  wire _0456_;
+  wire _0457_;
+  wire _0458_;
+  wire _0459_;
+  wire _0460_;
+  wire _0461_;
+  wire _0462_;
+  wire _0463_;
+  wire _0464_;
+  wire _0465_;
+  wire _0466_;
+  wire _0467_;
+  wire _0468_;
+  wire _0469_;
+  wire _0470_;
+  wire _0471_;
+  wire _0472_;
+  wire _0473_;
+  wire _0474_;
+  wire _0475_;
+  wire _0476_;
+  wire _0477_;
+  wire _0478_;
+  wire _0479_;
+  wire _0480_;
+  wire _0481_;
+  wire _0482_;
+  wire _0483_;
+  wire _0484_;
+  wire _0485_;
+  wire _0486_;
+  wire _0487_;
+  wire _0488_;
+  wire _0489_;
+  wire _0490_;
+  wire _0491_;
+  wire _0492_;
+  wire _0493_;
+  wire _0494_;
+  wire _0495_;
+  wire _0496_;
+  wire _0497_;
+  wire _0498_;
+  wire _0499_;
+  wire _0500_;
+  wire _0501_;
+  wire _0502_;
+  wire _0503_;
+  wire _0504_;
+  wire _0505_;
+  wire _0506_;
+  wire _0507_;
+  wire _0508_;
+  wire _0509_;
+  wire _0510_;
+  wire _0511_;
+  wire _0512_;
+  wire _0513_;
+  wire _0514_;
+  wire _0515_;
+  wire _0516_;
+  wire _0517_;
+  wire _0518_;
+  wire _0519_;
+  wire _0520_;
+  wire _0521_;
+  wire _0522_;
+  wire _0523_;
+  wire _0524_;
+  wire _0525_;
+  wire _0526_;
+  wire _0527_;
+  wire _0528_;
+  wire _0529_;
+  wire _0530_;
+  wire _0531_;
+  wire _0532_;
+  wire _0533_;
+  wire _0534_;
+  wire _0535_;
+  wire _0536_;
+  wire _0537_;
+  wire _0538_;
+  wire _0539_;
+  wire _0540_;
+  wire _0541_;
+  wire _0542_;
+  wire _0543_;
+  wire _0544_;
+  wire _0545_;
+  wire _0546_;
+  wire _0547_;
+  wire _0548_;
+  wire _0549_;
+  wire _0550_;
+  wire _0551_;
+  wire _0552_;
+  wire _0553_;
+  wire _0554_;
+  wire _0555_;
+  wire _0556_;
+  wire _0557_;
+  wire _0558_;
+  wire _0559_;
+  wire _0560_;
+  wire _0561_;
+  wire _0562_;
+  wire _0563_;
+  wire _0564_;
+  wire _0565_;
+  wire _0566_;
+  wire _0567_;
+  wire _0568_;
+  wire _0569_;
+  wire _0570_;
+  wire _0571_;
+  wire _0572_;
+  wire _0573_;
+  wire _0574_;
+  wire _0575_;
+  wire _0576_;
+  wire _0577_;
+  wire _0578_;
+  wire _0579_;
+  wire _0580_;
+  wire [11:0] _0581_;
+  wire [11:0] _0582_;
+  wire [61:0] _0583_;
+  wire [10:0] _0584_;
+  input clk;
+  wire [14:0] reg4;
+  reg [3:0] reg5 = 4'h0;
+  wire [20:0] reg6;
+  reg [18:0] reg7 = 19'h00000;
+  wire [13:0] reg8;
+  input [17:0] wire0;
+  input [10:0] wire1;
+  wire [14:0] wire10;
+  input [13:0] wire2;
+  wire [2:0] wire22;
+  wire [19:0] wire24;
+  wire wire25;
+  wire [5:0] wire26;
+  wire [11:0] wire27;
+  wire wire28;
+  wire [9:0] wire29;
+  input [8:0] wire3;
+  wire [11:0] wire9;
+  output [183:0] y;
+  assign _0022_ = reg4[1] | ~(reg4[0]);
+  assign _0023_ = reg4[3] | reg4[2];
+  assign _0024_ = _0023_ | _0022_;
+  assign _0025_ = reg4[5] | reg4[4];
+  assign _0026_ = reg4[7] | ~(reg4[6]);
+  assign _0027_ = _0026_ | _0025_;
+  assign _0028_ = _0027_ | _0024_;
+  assign _0029_ = reg4[9] | reg4[8];
+  assign _0030_ = _0029_ | reg4[10];
+  assign y[165] = _0030_ | _0028_;
+  assign _0031_ = reg5[1] ^ reg5[0];
+  assign _0032_ = ~(reg5[3] ^ reg5[2]);
+  assign wire28 = _0032_ ^ _0031_;
+  assign _0033_ = reg4[0] ^ reg4[1];
+  assign _0034_ = ~(reg4[3] ^ reg4[2]);
+  assign _0035_ = _0034_ ^ _0033_;
+  assign _0036_ = reg4[5] ^ reg4[4];
+  assign _0037_ = reg4[6] | ~(reg4[7]);
+  assign _0038_ = _0037_ & _0026_;
+  assign _0039_ = _0038_ ^ _0036_;
+  assign _0040_ = _0039_ ^ _0035_;
+  assign _0041_ = ~(reg4[9] ^ reg4[8]);
+  assign _0042_ = _0041_ ^ _0040_;
+  assign _0001_ = _0042_ ^ reg4[10];
+  assign _0043_ = ~(wire0[17] | wire0[16]);
+  assign _0044_ = wire0[15] | wire0[14];
+  assign _0045_ = _0043_ & ~(_0044_);
+  assign _0046_ = wire0[13] | wire0[12];
+  assign _0047_ = ~(wire0[11] | wire0[10]);
+  assign _0048_ = _0046_ | ~(_0047_);
+  assign _0049_ = _0048_ | ~(_0045_);
+  assign _0050_ = wire0[9] | wire0[8];
+  assign _0051_ = wire0[7] | wire0[6];
+  assign _0052_ = ~(_0051_ | _0050_);
+  assign _0053_ = ~(wire0[5] | wire0[4]);
+  assign _0054_ = ~(wire0[3] | wire0[2]);
+  assign _0055_ = _0054_ & _0053_;
+  assign _0056_ = _0055_ & _0052_;
+  assign _0057_ = _0056_ & ~(_0049_);
+  assign _0058_ = wire0[1] | wire0[0];
+  assign wire10[14] = _0057_ & ~(_0058_);
+  assign _0059_ = ~(wire1[1] | wire1[0]);
+  assign _0060_ = wire1[3] | wire1[2];
+  assign _0061_ = _0059_ & ~(_0060_);
+  assign _0062_ = wire1[5] | wire1[4];
+  assign _0063_ = wire1[7] | wire1[6];
+  assign _0064_ = _0063_ | _0062_;
+  assign _0065_ = _0061_ & ~(_0064_);
+  assign _0066_ = wire1[9] | wire1[8];
+  assign _0067_ = _0066_ | wire1[10];
+  assign _0068_ = _0065_ & ~(_0067_);
+  assign _0069_ = _0068_ ? reg7[0] : reg5[0];
+  assign _0070_ = _0068_ ? reg7[1] : reg5[1];
+  assign _0071_ = ~(_0070_ | _0069_);
+  assign _0072_ = _0068_ ? reg7[2] : reg5[2];
+  assign _0073_ = _0068_ ? reg7[3] : reg5[3];
+  assign _0074_ = _0073_ | _0072_;
+  assign _0075_ = _0071_ & ~(_0074_);
+  assign _0076_ = ~((reg7[5] | reg7[4]) & _0068_);
+  assign _0077_ = ~((reg7[7] | reg7[6]) & _0068_);
+  assign _0078_ = ~(_0077_ & _0076_);
+  assign _0079_ = _0075_ & ~(_0078_);
+  assign _0080_ = ~((reg7[9] | reg7[8]) & _0068_);
+  assign _0081_ = ~((reg7[11] | reg7[10]) & _0068_);
+  assign _0082_ = ~(_0081_ & _0080_);
+  assign _0083_ = ~((reg7[13] | reg7[12]) & _0068_);
+  assign _0084_ = ~((reg7[15] | reg7[14]) & _0068_);
+  assign _0085_ = ~(_0084_ & _0083_);
+  assign _0086_ = _0085_ | _0082_;
+  assign _0087_ = _0079_ & ~(_0086_);
+  assign _0088_ = ~((reg7[17] | reg7[16]) & _0068_);
+  assign _0089_ = ~(_0068_ & reg7[18]);
+  assign _0090_ = ~(_0089_ & _0088_);
+  assign _0091_ = _0087_ & ~(_0090_);
+  assign _0092_ = _0054_ & ~(_0058_);
+  assign _0093_ = _0051_ | ~(_0053_);
+  assign _0094_ = _0092_ & ~(_0093_);
+  assign _0095_ = _0050_ | ~(_0047_);
+  assign _0096_ = _0046_ | _0044_;
+  assign _0097_ = _0096_ | _0095_;
+  assign _0098_ = _0094_ & ~(_0097_);
+  assign _0099_ = ~(wire22[1] | wire22[0]);
+  assign _0100_ = _0099_ & ~(wire22[2]);
+  assign _0101_ = ~((_0098_ & _0043_) | _0100_);
+  assign _0102_ = _0091_ ? reg4[2] : _0101_;
+  assign y[106] = _0068_ ? wire0[0] : _0102_;
+  assign _0103_ = ~reg4[3];
+  assign _0104_ = _0091_ & ~(_0103_);
+  assign y[107] = _0068_ ? wire0[1] : _0104_;
+  assign y[108] = _0068_ & wire0[2];
+  assign y[109] = _0068_ & wire0[3];
+  assign _0105_ = ~wire0[4];
+  assign y[110] = _0068_ & ~(_0105_);
+  assign _0106_ = ~wire0[5];
+  assign y[111] = _0068_ & ~(_0106_);
+  assign _0107_ = ~wire0[6];
+  assign y[112] = _0068_ & ~(_0107_);
+  assign _0108_ = ~wire0[7];
+  assign y[113] = _0068_ & ~(_0108_);
+  assign _0109_ = ~wire0[8];
+  assign y[114] = _0068_ & ~(_0109_);
+  assign _0110_ = ~wire0[9];
+  assign y[115] = _0068_ & ~(_0110_);
+  assign _0111_ = ~wire0[10];
+  assign y[116] = _0068_ & ~(_0111_);
+  assign _0112_ = ~wire0[11];
+  assign y[117] = _0068_ & ~(_0112_);
+  assign _0113_ = ~wire0[12];
+  assign y[118] = _0068_ & ~(_0113_);
+  assign y[119] = _0068_ & wire0[13];
+  assign y[120] = _0068_ & wire0[14];
+  assign y[121] = _0068_ & wire0[15];
+  assign y[122] = _0068_ & wire0[16];
+  assign y[125] = _0068_ & wire0[17];
+  assign _0114_ = ~(reg5[3] | reg5[2]);
+  assign _0115_ = reg5[1] | reg5[0];
+  assign wire25 = _0114_ & ~(_0115_);
+  assign _0116_ = ~(wire0[3] ^ wire0[2]);
+  assign y[167] = ~_0116_;
+  assign y[168] = _0054_ ^ _0105_;
+  assign _0117_ = _0054_ & ~(wire0[4]);
+  assign y[169] = _0117_ ^ _0106_;
+  assign y[170] = _0055_ ^ _0107_;
+  assign _0118_ = _0055_ & ~(wire0[6]);
+  assign y[171] = _0118_ ^ _0108_;
+  assign _0119_ = _0055_ & ~(_0051_);
+  assign y[172] = _0119_ ^ _0109_;
+  assign _0120_ = _0119_ & ~(wire0[8]);
+  assign y[173] = _0120_ ^ _0110_;
+  assign y[174] = _0056_ ^ _0111_;
+  assign _0121_ = _0056_ & ~(wire0[10]);
+  assign y[175] = _0121_ ^ _0112_;
+  assign _0122_ = _0056_ & _0047_;
+  assign y[176] = _0122_ ^ _0113_;
+  assign _0123_ = ~(wire3[1] ^ wire1[1]);
+  assign _0124_ = wire3[0] & wire1[0];
+  assign wire9[1] = ~(_0124_ ^ _0123_);
+  assign _0125_ = ~(wire3[2] ^ wire1[2]);
+  assign _0126_ = _0124_ & ~(_0123_);
+  assign _0127_ = ~((wire3[1] & wire1[1]) | _0126_);
+  assign wire9[2] = _0127_ ^ _0125_;
+  assign _0128_ = ~(wire3[3] ^ wire1[3]);
+  assign _0129_ = wire3[2] & wire1[2];
+  assign _0130_ = ~_0129_;
+  assign _0131_ = ~((_0127_ | _0125_) & _0130_);
+  assign wire9[3] = ~(_0131_ ^ _0128_);
+  assign _0132_ = ~(wire3[4] ^ wire1[4]);
+  assign _0133_ = _0129_ & ~(_0128_);
+  assign _0134_ = ~((wire3[3] & wire1[3]) | _0133_);
+  assign _0135_ = ~(_0128_ | _0125_);
+  assign _0136_ = _0135_ & ~(_0127_);
+  assign _0137_ = _0134_ & ~(_0136_);
+  assign wire9[4] = _0137_ ^ _0132_;
+  assign _0138_ = ~(wire3[5] ^ wire1[5]);
+  assign _0139_ = wire3[4] & wire1[4];
+  assign _0140_ = ~_0139_;
+  assign _0141_ = ~((_0137_ | _0132_) & _0140_);
+  assign y[24] = ~(_0141_ ^ _0138_);
+  assign _0142_ = ~(wire3[6] ^ wire1[6]);
+  assign _0143_ = wire3[5] & wire1[5];
+  assign _0144_ = _0139_ & ~(_0138_);
+  assign _0145_ = ~(_0144_ | _0143_);
+  assign _0146_ = ~(_0138_ | _0132_);
+  assign _0147_ = _0146_ & ~(_0137_);
+  assign _0148_ = _0145_ & ~(_0147_);
+  assign y[25] = _0148_ ^ _0142_;
+  assign _0149_ = ~(wire3[7] ^ wire1[7]);
+  assign _0150_ = wire3[6] & wire1[6];
+  assign _0151_ = ~_0150_;
+  assign _0152_ = ~((_0148_ | _0142_) & _0151_);
+  assign y[26] = ~(_0152_ ^ _0149_);
+  assign _0153_ = ~(wire3[8] ^ wire1[8]);
+  assign _0154_ = _0150_ & ~(_0149_);
+  assign _0155_ = ~((wire3[7] & wire1[7]) | _0154_);
+  assign _0156_ = ~(_0149_ | _0142_);
+  assign _0157_ = ~_0156_;
+  assign _0158_ = ~((_0157_ | _0145_) & _0155_);
+  assign _0159_ = _0156_ & _0146_;
+  assign _0160_ = _0159_ & ~(_0137_);
+  assign _0161_ = ~(_0160_ | _0158_);
+  assign y[27] = _0161_ ^ _0153_;
+  assign _0162_ = wire3[8] & wire1[8];
+  assign _0163_ = _0161_ | _0153_;
+  assign _0164_ = _0163_ & ~(_0162_);
+  assign y[28] = ~(_0164_ ^ wire1[9]);
+  assign _0165_ = wire1[9] & ~(_0153_);
+  assign _0166_ = _0165_ & ~(_0161_);
+  assign _0167_ = ~((_0162_ & wire1[9]) | _0166_);
+  assign y[29] = ~(_0167_ ^ wire1[10]);
+  assign wire9[0] = wire3[0] ^ wire1[0];
+  assign y[30] = wire1[10] & ~(_0167_);
+  assign _0168_ = ~((wire3[2] & wire0[17]) | (wire3[1] & wire0[16]));
+  assign _0169_ = ~((wire3[0] & wire0[15]) | (wire0[14] & reg4[10]));
+  assign _0170_ = ~(_0169_ & _0168_);
+  assign _0171_ = ~((wire0[13] | wire0[12]) & reg4[10]);
+  assign _0172_ = ~((wire0[11] | wire0[10]) & reg4[10]);
+  assign _0173_ = ~(_0172_ & _0171_);
+  assign _0174_ = _0173_ | _0170_;
+  assign _0175_ = ~((wire0[9] & reg4[9]) | (wire0[8] & reg4[8]));
+  assign _0176_ = ~((wire0[7] & reg4[7]) | (wire0[6] & reg4[6]));
+  assign _0177_ = ~(_0176_ & _0175_);
+  assign _0178_ = ~((wire0[5] & reg4[5]) | (wire0[4] & reg4[4]));
+  assign _0179_ = ~((wire0[3] & reg4[3]) | (wire0[2] & reg4[2]));
+  assign _0180_ = ~(_0179_ & _0178_);
+  assign _0181_ = _0180_ | _0177_;
+  assign _0182_ = _0181_ | _0174_;
+  assign _0183_ = ~(wire0[1] & reg4[1]);
+  assign _0184_ = ~(reg4[3] & reg4[2]);
+  assign _0185_ = _0184_ | _0022_;
+  assign _0186_ = reg4[5] | ~(reg4[4]);
+  assign _0187_ = _0037_ | _0186_;
+  assign _0188_ = _0187_ | _0185_;
+  assign _0189_ = _0188_ | _0030_;
+  assign _0190_ = ~((reg4[0] & wire0[0]) | _0189_);
+  assign _0191_ = ~(_0190_ & _0183_);
+  assign _0192_ = _0191_ | _0182_;
+  assign _0193_ = ~wire3[6];
+  assign _0194_ = reg5[0] ? reg4[6] : _0193_;
+  assign _0195_ = ~reg4[10];
+  assign _0196_ = ~(wire3[1] & reg5[0]);
+  assign _0197_ = ~(wire3[0] & reg5[1]);
+  assign _0198_ = _0197_ ^ _0196_;
+  assign _0199_ = ~((wire3[0] & reg5[0]) | _0198_);
+  assign _0200_ = ~(wire3[2] & reg5[0]);
+  assign _0201_ = ~(wire3[1] & reg5[1]);
+  assign _0202_ = _0201_ ^ _0200_;
+  assign _0203_ = _0197_ | _0196_;
+  assign _0204_ = ~(_0203_ ^ _0202_);
+  assign _0205_ = wire3[0] & reg5[2];
+  assign _0206_ = _0205_ ^ _0204_;
+  assign _0207_ = wire3[0] & reg5[3];
+  assign _0208_ = wire3[3] & reg5[0];
+  assign _0209_ = _0208_ ^ _0207_;
+  assign _0210_ = wire3[2] & reg5[1];
+  assign _0211_ = _0210_ ^ _0209_;
+  assign _0212_ = ~(_0201_ | _0200_);
+  assign _0213_ = _0212_ ^ _0211_;
+  assign _0214_ = wire3[1] & reg5[2];
+  assign _0215_ = ~(_0214_ ^ _0213_);
+  assign _0216_ = _0202_ & ~(_0203_);
+  assign _0217_ = ~((_0205_ & _0204_) | _0216_);
+  assign _0218_ = _0217_ ^ _0215_;
+  assign _0219_ = _0218_ | _0206_;
+  assign _0220_ = _0199_ & ~(_0219_);
+  assign _0221_ = wire3[1] & reg5[3];
+  assign _0222_ = wire3[4] & reg5[0];
+  assign _0223_ = _0222_ ^ _0221_;
+  assign _0224_ = wire3[3] & reg5[1];
+  assign _0225_ = _0224_ ^ _0223_;
+  assign _0226_ = _0208_ & _0207_;
+  assign _0227_ = ~((_0210_ & _0209_) | _0226_);
+  assign _0228_ = ~(_0227_ ^ _0225_);
+  assign _0229_ = wire3[2] & reg5[2];
+  assign _0230_ = _0229_ ^ _0228_;
+  assign _0231_ = _0212_ & _0211_;
+  assign _0232_ = ~((_0214_ & _0213_) | _0231_);
+  assign _0233_ = ~(_0232_ ^ _0230_);
+  assign _0234_ = _0217_ | _0215_;
+  assign _0235_ = ~(_0234_ ^ _0233_);
+  assign _0236_ = wire3[2] & reg5[3];
+  assign _0237_ = wire3[5] & reg5[0];
+  assign _0238_ = _0237_ ^ _0236_;
+  assign _0239_ = wire3[4] & reg5[1];
+  assign _0240_ = _0239_ ^ _0238_;
+  assign _0241_ = _0222_ & _0221_;
+  assign _0242_ = ~((_0224_ & _0223_) | _0241_);
+  assign _0243_ = ~(_0242_ ^ _0240_);
+  assign _0244_ = wire3[3] & reg5[2];
+  assign _0245_ = _0244_ ^ _0243_;
+  assign _0246_ = _0225_ & ~(_0227_);
+  assign _0247_ = ~((_0229_ & _0228_) | _0246_);
+  assign _0248_ = ~(_0247_ ^ _0245_);
+  assign _0249_ = ~_0234_;
+  assign _0250_ = _0230_ & ~(_0232_);
+  assign _0251_ = ~((_0249_ & _0233_) | _0250_);
+  assign _0252_ = ~(_0251_ ^ _0248_);
+  assign _0253_ = _0252_ | _0235_;
+  assign _0254_ = wire3[3] & reg5[3];
+  assign _0255_ = wire3[6] & reg5[0];
+  assign _0256_ = _0255_ ^ _0254_;
+  assign _0257_ = wire3[5] & reg5[1];
+  assign _0258_ = _0257_ ^ _0256_;
+  assign _0259_ = _0237_ & _0236_;
+  assign _0260_ = ~((_0239_ & _0238_) | _0259_);
+  assign _0261_ = ~(_0260_ ^ _0258_);
+  assign _0262_ = wire3[4] & reg5[2];
+  assign _0263_ = _0262_ ^ _0261_;
+  assign _0264_ = _0240_ & ~(_0242_);
+  assign _0265_ = ~((_0244_ & _0243_) | _0264_);
+  assign _0266_ = ~(_0265_ ^ _0263_);
+  assign _0267_ = _0245_ & ~(_0247_);
+  assign _0268_ = ~((_0250_ & _0248_) | _0267_);
+  assign _0269_ = ~(_0248_ & _0233_);
+  assign _0270_ = ~((_0269_ | _0234_) & _0268_);
+  assign _0271_ = _0270_ ^ _0266_;
+  assign _0272_ = wire3[4] & reg5[3];
+  assign _0273_ = wire3[7] & reg5[0];
+  assign _0274_ = _0273_ ^ _0272_;
+  assign _0275_ = wire3[6] & reg5[1];
+  assign _0276_ = _0275_ ^ _0274_;
+  assign _0277_ = _0255_ & _0254_;
+  assign _0278_ = ~((_0257_ & _0256_) | _0277_);
+  assign _0279_ = ~(_0278_ ^ _0276_);
+  assign _0280_ = wire3[5] & reg5[2];
+  assign _0281_ = _0280_ ^ _0279_;
+  assign _0282_ = _0258_ & ~(_0260_);
+  assign _0283_ = ~((_0262_ & _0261_) | _0282_);
+  assign _0284_ = _0283_ ^ _0281_;
+  assign _0285_ = _0263_ & ~(_0265_);
+  assign _0286_ = ~((_0270_ & _0266_) | _0285_);
+  assign _0287_ = _0286_ ^ _0284_;
+  assign _0288_ = _0287_ | _0271_;
+  assign _0289_ = _0288_ | _0253_;
+  assign _0290_ = _0220_ & ~(_0289_);
+  assign _0291_ = ~(wire3[5] & reg5[3]);
+  assign _0292_ = wire3[8] & reg5[0];
+  assign _0293_ = _0292_ ^ _0291_;
+  assign _0294_ = wire3[7] & reg5[1];
+  assign _0295_ = _0294_ ^ _0293_;
+  assign _0296_ = _0273_ & _0272_;
+  assign _0297_ = ~((_0275_ & _0274_) | _0296_);
+  assign _0298_ = _0297_ ^ _0295_;
+  assign _0299_ = wire3[6] & reg5[2];
+  assign _0300_ = _0299_ ^ _0298_;
+  assign _0301_ = _0276_ & ~(_0278_);
+  assign _0302_ = ~((_0280_ & _0279_) | _0301_);
+  assign _0303_ = _0302_ ^ _0300_;
+  assign _0304_ = _0283_ | ~(_0281_);
+  assign _0305_ = _0285_ & ~(_0284_);
+  assign _0306_ = _0304_ & ~(_0305_);
+  assign _0307_ = _0284_ | ~(_0266_);
+  assign _0308_ = ~((_0307_ | _0268_) & _0306_);
+  assign _0309_ = ~(_0307_ | _0269_);
+  assign _0310_ = ~((_0309_ & _0249_) | _0308_);
+  assign _0311_ = _0310_ ^ _0303_;
+  assign _0312_ = _0290_ & ~(_0311_);
+  assign _0313_ = _0312_ & ~(_0195_);
+  assign _0314_ = _0312_ ? reg4[0] : wire1[0];
+  assign _0315_ = _0312_ ? reg4[1] : wire1[1];
+  assign _0316_ = _0315_ | _0314_;
+  assign _0317_ = _0312_ ? reg4[2] : wire1[2];
+  assign _0318_ = _0312_ ? reg4[3] : wire1[3];
+  assign _0319_ = _0318_ | _0317_;
+  assign _0320_ = _0319_ | _0316_;
+  assign _0321_ = _0312_ ? reg4[4] : wire1[4];
+  assign _0322_ = _0312_ ? reg4[5] : wire1[5];
+  assign _0323_ = _0322_ | _0321_;
+  assign _0324_ = _0312_ ? reg4[6] : wire1[6];
+  assign _0325_ = _0312_ ? reg4[7] : wire1[7];
+  assign _0326_ = _0325_ | _0324_;
+  assign _0327_ = _0326_ | _0323_;
+  assign _0328_ = _0327_ | _0320_;
+  assign _0329_ = _0312_ ? reg4[8] : wire1[8];
+  assign _0330_ = _0312_ ? reg4[9] : wire1[9];
+  assign _0331_ = _0330_ | _0329_;
+  assign _0332_ = _0312_ ? reg4[10] : wire1[10];
+  assign _0333_ = _0332_ | _0331_;
+  assign _0334_ = _0333_ | _0313_;
+  assign _0335_ = _0334_ | _0328_;
+  assign _0336_ = _0335_ | _0313_;
+  assign _0337_ = _0336_ ? wire2[6] : _0194_;
+  assign _0338_ = ~(wire3[0] ^ wire1[2]);
+  assign _0339_ = wire3[0] & wire1[2];
+  assign _0340_ = _0339_ ^ wire3[1];
+  assign _0341_ = _0338_ & ~(_0340_);
+  assign _0342_ = ~wire3[1];
+  assign _0343_ = _0339_ & ~(_0342_);
+  assign _0344_ = _0343_ ^ wire3[2];
+  assign _0345_ = ~wire3[2];
+  assign _0346_ = _0343_ & ~(_0345_);
+  assign _0347_ = _0346_ ^ wire3[3];
+  assign _0348_ = _0347_ | _0344_;
+  assign _0349_ = _0341_ & ~(_0348_);
+  assign _0350_ = ~(wire3[3] & wire3[2]);
+  assign _0351_ = _0343_ & ~(_0350_);
+  assign _0352_ = _0351_ ^ wire3[4];
+  assign _0353_ = ~wire3[4];
+  assign _0354_ = _0351_ & ~(_0353_);
+  assign _0355_ = _0354_ ^ wire3[5];
+  assign _0356_ = _0355_ | _0352_;
+  assign _0357_ = ~(wire3[5] & wire3[4]);
+  assign _0358_ = _0351_ & ~(_0357_);
+  assign _0359_ = _0358_ ^ wire3[6];
+  assign _0360_ = _0358_ & ~(_0193_);
+  assign _0361_ = _0360_ ^ wire3[7];
+  assign _0362_ = _0361_ | _0359_;
+  assign _0363_ = _0362_ | _0356_;
+  assign _0364_ = _0349_ & ~(_0363_);
+  assign _0365_ = ~(wire3[7] & wire3[6]);
+  assign _0366_ = ~(_0365_ | _0357_);
+  assign _0367_ = _0366_ & _0351_;
+  assign _0368_ = _0367_ | wire3[8];
+  assign _0369_ = _0364_ & ~(_0368_);
+  assign _0370_ = ~(wire0[1] ^ wire0[0]);
+  assign _0371_ = _0370_ ^ _0116_;
+  assign _0372_ = wire0[5] ^ wire0[4];
+  assign _0373_ = ~(wire0[7] ^ wire0[6]);
+  assign _0374_ = _0373_ ^ _0372_;
+  assign _0375_ = _0374_ ^ _0371_;
+  assign _0376_ = ~(wire0[9] ^ wire0[8]);
+  assign _0377_ = ~(wire0[11] ^ wire0[10]);
+  assign _0378_ = _0377_ ^ _0376_;
+  assign _0379_ = wire0[13] ^ wire0[12];
+  assign _0380_ = ~(wire0[15] ^ wire0[14]);
+  assign _0381_ = _0380_ ^ _0379_;
+  assign _0382_ = _0381_ ^ _0378_;
+  assign _0383_ = _0382_ ^ _0375_;
+  assign _0384_ = ~(wire0[17] ^ wire0[16]);
+  assign _0385_ = _0384_ ^ _0383_;
+  assign _0386_ = wire3[0] & ~(_0385_);
+  assign _0387_ = _0386_ & ~(_0342_);
+  assign _0388_ = _0387_ & ~(_0350_);
+  assign _0389_ = _0388_ & ~(_0357_);
+  assign _0390_ = _0389_ ^ wire3[6];
+  assign _0391_ = _0369_ ? _0337_ : _0390_;
+  assign _0392_ = ~wire3[7];
+  assign _0393_ = reg5[0] ? reg4[7] : _0392_;
+  assign _0394_ = _0336_ ? wire2[7] : _0393_;
+  assign _0395_ = _0389_ & ~(_0193_);
+  assign _0396_ = _0395_ ^ wire3[7];
+  assign _0397_ = _0369_ ? _0394_ : _0396_;
+  assign _0398_ = _0397_ | _0391_;
+  assign _0399_ = ~_0369_;
+  assign _0400_ = ~wire2[8];
+  assign _0401_ = ~reg4[8];
+  assign _0402_ = reg5[0] ? _0401_ : wire3[8];
+  assign _0403_ = _0336_ ? _0400_ : _0402_;
+  assign _0404_ = ~(_0388_ & _0366_);
+  assign _0405_ = _0404_ ^ wire3[8];
+  assign _0406_ = _0369_ ? _0403_ : _0405_;
+  assign _0407_ = ~wire2[9];
+  assign _0408_ = reg5[0] & ~(reg4[9]);
+  assign _0409_ = _0336_ ? _0407_ : _0408_;
+  assign _0410_ = ~((_0409_ | _0399_) & _0406_);
+  assign _0411_ = _0410_ | _0398_;
+  assign _0412_ = ~wire2[10];
+  assign _0413_ = reg5[0] & ~(reg4[10]);
+  assign _0414_ = _0336_ ? _0412_ : _0413_;
+  assign _0415_ = ~wire2[11];
+  assign _0416_ = _0336_ ? _0415_ : _0413_;
+  assign _0417_ = ~((_0416_ & _0414_) | _0399_);
+  assign _0418_ = ~wire2[12];
+  assign _0419_ = _0336_ ? _0418_ : _0413_;
+  assign _0420_ = ~wire2[13];
+  assign _0421_ = _0336_ ? _0420_ : _0413_;
+  assign _0422_ = ~((_0421_ & _0419_) | _0399_);
+  assign _0423_ = _0422_ | _0417_;
+  assign _0424_ = _0423_ | _0411_;
+  assign _0425_ = ~reg4[0];
+  assign _0426_ = _0336_ ? _0425_ : _0413_;
+  assign _0427_ = ~reg4[1];
+  assign _0428_ = _0336_ ? _0427_ : reg5[0];
+  assign _0429_ = ~((_0428_ & _0426_) | _0399_);
+  assign _0430_ = ~reg4[2];
+  assign _0431_ = _0336_ ? _0430_ : reg5[0];
+  assign _0432_ = _0336_ ? _0103_ : reg5[0];
+  assign _0433_ = ~((_0432_ & _0431_) | _0399_);
+  assign _0434_ = _0433_ | _0429_;
+  assign _0435_ = ~reg4[4];
+  assign _0436_ = _0336_ ? _0435_ : reg5[0];
+  assign _0437_ = ~reg4[5];
+  assign _0438_ = _0336_ ? _0437_ : reg5[0];
+  assign _0439_ = ~((_0438_ & _0436_) | _0399_);
+  assign _0440_ = ~reg4[6];
+  assign _0441_ = _0336_ ? _0440_ : reg5[0];
+  assign _0442_ = ~reg4[7];
+  assign _0443_ = _0336_ ? _0442_ : reg5[0];
+  assign _0444_ = ~((_0443_ & _0441_) | _0399_);
+  assign _0445_ = _0444_ | _0439_;
+  assign _0446_ = _0445_ | _0434_;
+  assign _0447_ = _0446_ | _0424_;
+  assign _0448_ = _0336_ ? _0195_ : reg5[0];
+  assign _0449_ = _0369_ & ~(_0448_);
+  assign _0450_ = _0336_ ? _0401_ : reg5[0];
+  assign _0451_ = ~reg4[9];
+  assign _0452_ = _0336_ ? _0451_ : reg5[0];
+  assign _0453_ = ~((_0452_ & _0450_) | _0399_);
+  assign _0454_ = _0453_ | _0449_;
+  assign _0455_ = _0454_ | _0447_;
+  assign _0456_ = _0455_ | _0192_;
+  assign _0457_ = ~wire3[0];
+  assign _0458_ = reg5[0] ? reg4[0] : _0457_;
+  assign _0459_ = _0336_ ? wire2[0] : _0458_;
+  assign _0460_ = _0385_ ^ _0457_;
+  assign _0461_ = _0369_ ? _0459_ : _0460_;
+  assign _0462_ = _0461_ | _0456_;
+  assign _0463_ = reg5[0] ? reg4[1] : _0342_;
+  assign _0464_ = _0336_ ? wire2[1] : _0463_;
+  assign _0465_ = _0386_ ^ wire3[1];
+  assign _0466_ = _0369_ ? _0464_ : _0465_;
+  assign _0467_ = _0466_ | _0462_;
+  assign _0468_ = reg5[0] ? reg4[2] : _0345_;
+  assign _0469_ = _0336_ ? wire2[2] : _0468_;
+  assign _0470_ = _0387_ ^ wire3[2];
+  assign _0471_ = _0369_ ? _0469_ : _0470_;
+  assign _0472_ = _0471_ | _0467_;
+  assign _0473_ = ~wire3[3];
+  assign _0474_ = reg5[0] ? reg4[3] : _0473_;
+  assign _0475_ = _0336_ ? wire2[3] : _0474_;
+  assign _0476_ = _0387_ & ~(_0345_);
+  assign _0477_ = _0476_ ^ wire3[3];
+  assign _0478_ = _0369_ ? _0475_ : _0477_;
+  assign _0479_ = ~(_0478_ | _0472_);
+  assign _0480_ = reg5[0] ? reg4[4] : _0353_;
+  assign _0481_ = _0336_ ? wire2[4] : _0480_;
+  assign _0482_ = _0388_ ^ wire3[4];
+  assign _0483_ = _0369_ ? _0481_ : _0482_;
+  assign _0484_ = _0479_ & ~(_0483_);
+  assign _0485_ = ~wire2[5];
+  assign _0486_ = reg5[0] ? _0437_ : wire3[5];
+  assign _0487_ = _0336_ ? _0485_ : _0486_;
+  assign _0488_ = ~(_0388_ & wire3[4]);
+  assign _0489_ = _0488_ ^ wire3[5];
+  assign _0490_ = _0369_ ? _0487_ : _0489_;
+  assign _0000_[0] = _0490_ & _0484_;
+  assign _0491_ = _0456_ | ~(_0461_);
+  assign _0492_ = _0491_ | _0466_;
+  assign _0493_ = _0492_ | _0471_;
+  assign _0494_ = _0493_ | _0478_;
+  assign _0495_ = _0494_ | _0483_;
+  assign _0000_[1] = _0490_ & ~(_0495_);
+  assign _0496_ = _0462_ | ~(_0466_);
+  assign _0497_ = _0496_ | _0471_;
+  assign _0498_ = _0497_ | _0478_;
+  assign _0499_ = _0498_ | _0483_;
+  assign _0000_[2] = _0490_ & ~(_0499_);
+  assign _0500_ = _0491_ | ~(_0466_);
+  assign _0501_ = _0500_ | _0471_;
+  assign _0502_ = _0501_ | _0478_;
+  assign _0503_ = _0502_ | _0483_;
+  assign _0000_[3] = _0490_ & ~(_0503_);
+  assign _0504_ = _0467_ | ~(_0471_);
+  assign _0505_ = _0504_ | _0478_;
+  assign _0506_ = _0505_ | _0483_;
+  assign _0000_[4] = _0490_ & ~(_0506_);
+  assign _0507_ = _0492_ | ~(_0471_);
+  assign _0508_ = _0507_ | _0478_;
+  assign _0509_ = _0508_ | _0483_;
+  assign _0000_[5] = _0490_ & ~(_0509_);
+  assign _0510_ = _0496_ | ~(_0471_);
+  assign _0511_ = _0510_ | _0478_;
+  assign _0512_ = _0511_ | _0483_;
+  assign _0000_[6] = _0490_ & ~(_0512_);
+  assign _0513_ = _0500_ | ~(_0471_);
+  assign _0514_ = _0513_ | _0478_;
+  assign _0515_ = _0514_ | _0483_;
+  assign _0000_[7] = _0490_ & ~(_0515_);
+  assign _0516_ = _0472_ | ~(_0478_);
+  assign _0517_ = _0516_ | _0483_;
+  assign _0000_[8] = _0490_ & ~(_0517_);
+  assign _0518_ = _0493_ | ~(_0478_);
+  assign _0519_ = _0518_ | _0483_;
+  assign _0000_[9] = _0490_ & ~(_0519_);
+  assign _0520_ = _0497_ | ~(_0478_);
+  assign _0521_ = _0520_ | _0483_;
+  assign _0000_[10] = _0490_ & ~(_0521_);
+  assign _0522_ = _0501_ | ~(_0478_);
+  assign _0523_ = _0522_ | _0483_;
+  assign _0000_[11] = _0490_ & ~(_0523_);
+  assign _0524_ = _0504_ | ~(_0478_);
+  assign _0525_ = _0524_ | _0483_;
+  assign _0000_[12] = _0490_ & ~(_0525_);
+  assign _0526_ = _0507_ | ~(_0478_);
+  assign _0527_ = _0526_ | _0483_;
+  assign _0000_[13] = _0490_ & ~(_0527_);
+  assign _0528_ = _0510_ | ~(_0478_);
+  assign _0529_ = _0528_ | _0483_;
+  assign _0000_[14] = _0490_ & ~(_0529_);
+  assign _0530_ = _0513_ | ~(_0478_);
+  assign _0531_ = _0530_ | _0483_;
+  assign _0000_[15] = _0490_ & ~(_0531_);
+  assign _0532_ = ~(_0483_ & _0479_);
+  assign _0000_[16] = _0490_ & ~(_0532_);
+  assign _0533_ = _0494_ | ~(_0483_);
+  assign _0000_[17] = _0490_ & ~(_0533_);
+  assign _0534_ = _0498_ | ~(_0483_);
+  assign _0000_[18] = _0490_ & ~(_0534_);
+  reg \reg4_reg[0]  = 1'h0;
+  always @(posedge clk)
+      \reg4_reg[0]  <= wire1[0];
+  assign reg4[0] = \reg4_reg[0] ;
+  reg \reg4_reg[1]  = 1'h0;
+  always @(posedge clk)
+      \reg4_reg[1]  <= wire1[1];
+  assign reg4[1] = \reg4_reg[1] ;
+  reg \reg4_reg[2]  = 1'h0;
+  always @(posedge clk)
+      \reg4_reg[2]  <= wire1[2];
+  assign reg4[2] = \reg4_reg[2] ;
+  reg \reg4_reg[3]  = 1'h0;
+  always @(posedge clk)
+      \reg4_reg[3]  <= wire1[3];
+  assign reg4[3] = \reg4_reg[3] ;
+  reg \reg4_reg[4]  = 1'h0;
+  always @(posedge clk)
+      \reg4_reg[4]  <= wire1[4];
+  assign reg4[4] = \reg4_reg[4] ;
+  reg \reg4_reg[5]  = 1'h0;
+  always @(posedge clk)
+      \reg4_reg[5]  <= wire1[5];
+  assign reg4[5] = \reg4_reg[5] ;
+  reg \reg4_reg[6]  = 1'h0;
+  always @(posedge clk)
+      \reg4_reg[6]  <= wire1[6];
+  assign reg4[6] = \reg4_reg[6] ;
+  reg \reg4_reg[7]  = 1'h0;
+  always @(posedge clk)
+      \reg4_reg[7]  <= wire1[7];
+  assign reg4[7] = \reg4_reg[7] ;
+  reg \reg4_reg[8]  = 1'h0;
+  always @(posedge clk)
+      \reg4_reg[8]  <= wire1[8];
+  assign reg4[8] = \reg4_reg[8] ;
+  reg \reg4_reg[9]  = 1'h0;
+  always @(posedge clk)
+      \reg4_reg[9]  <= wire1[9];
+  assign reg4[9] = \reg4_reg[9] ;
+  reg \reg4_reg[10]  = 1'hx;
+  always @(posedge clk)
+      \reg4_reg[10]  <= wire1[10];
+  assign reg4[10] = \reg4_reg[10] ;
+  reg \reg8_reg[0]  = 1'h0;
+  always @(posedge clk)
+      \reg8_reg[0]  <= _0001_;
+  assign reg8[0] = \reg8_reg[0] ;
+  always @(posedge clk)
+      reg7[0] <= _0000_[0];
+  always @(posedge clk)
+      reg7[1] <= _0000_[1];
+  always @(posedge clk)
+      reg7[2] <= _0000_[2];
+  always @(posedge clk)
+      reg7[3] <= _0000_[3];
+  always @(posedge clk)
+      reg7[4] <= _0000_[4];
+  always @(posedge clk)
+      reg7[5] <= _0000_[5];
+  always @(posedge clk)
+      reg7[6] <= _0000_[6];
+  always @(posedge clk)
+      reg7[7] <= _0000_[7];
+  always @(posedge clk)
+      reg7[8] <= _0000_[8];
+  always @(posedge clk)
+      reg7[9] <= _0000_[9];
+  always @(posedge clk)
+      reg7[10] <= _0000_[10];
+  always @(posedge clk)
+      reg7[11] <= _0000_[11];
+  always @(posedge clk)
+      reg7[12] <= _0000_[12];
+  always @(posedge clk)
+      reg7[13] <= _0000_[13];
+  always @(posedge clk)
+      reg7[14] <= _0000_[14];
+  always @(posedge clk)
+      reg7[15] <= _0000_[15];
+  always @(posedge clk)
+      reg7[16] <= _0000_[16];
+  always @(posedge clk)
+      reg7[17] <= _0000_[17];
+  always @(posedge clk)
+      reg7[18] <= _0000_[18];
+  always @(posedge clk)
+      reg5[0] <= reg4[0];
+  always @(posedge clk)
+      reg5[1] <= reg4[1];
+  always @(posedge clk)
+      reg5[2] <= reg4[2];
+  always @(posedge clk)
+      reg5[3] <= reg4[3];
+  module11 modinst23 (
+    .clk(clk),
+    .wire12(wire1),
+    .wire13({ wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14] }),
+    .wire14(wire0),
+    .wire15(wire9[4:0]),
+    .wire16(wire3[2:0]),
+    .y({ _0583_, wire22 })
+  );
+  assign _0535_ = wire0[2];
+  assign _0562_ = y[165];
+  assign _0538_ = wire28;
+  assign _0021_ = _0001_;
+  assign _0536_ = wire10[14];
+  assign _0544_ = y[106];
+  assign _0545_ = y[107];
+  assign _0546_ = y[108];
+  assign _0547_ = y[109];
+  assign _0548_ = y[110];
+  assign _0549_ = y[111];
+  assign _0550_ = y[112];
+  assign _0551_ = y[113];
+  assign _0552_ = y[114];
+  assign _0553_ = y[115];
+  assign _0554_ = y[116];
+  assign _0555_ = y[117];
+  assign _0556_ = y[118];
+  assign _0557_ = y[119];
+  assign _0558_ = y[120];
+  assign _0559_ = y[121];
+  assign _0560_ = y[122];
+  assign _0561_ = y[125];
+  assign _0537_ = wire25;
+  assign _0563_ = wire0[2];
+  assign _0564_ = y[167];
+  assign _0565_ = y[168];
+  assign _0566_ = y[169];
+  assign _0567_ = y[170];
+  assign _0568_ = y[171];
+  assign _0569_ = y[172];
+  assign _0570_ = y[173];
+  assign _0571_ = y[174];
+  assign _0572_ = y[175];
+  assign _0573_ = y[176];
+  assign _0540_ = wire9[1];
+  assign _0541_ = wire9[2];
+  assign _0542_ = wire9[3];
+  assign _0543_ = wire9[4];
+  assign _0574_ = y[24];
+  assign _0575_ = y[25];
+  assign _0576_ = y[26];
+  assign _0577_ = y[27];
+  assign _0578_ = y[28];
+  assign _0579_ = y[29];
+  assign _0539_ = wire9[0];
+  assign _0580_ = y[30];
+  assign _0002_ = _0000_[0];
+  assign _0012_ = _0000_[1];
+  assign _0013_ = _0000_[2];
+  assign _0014_ = _0000_[3];
+  assign _0015_ = _0000_[4];
+  assign _0016_ = _0000_[5];
+  assign _0017_ = _0000_[6];
+  assign _0018_ = _0000_[7];
+  assign _0019_ = _0000_[8];
+  assign _0020_ = _0000_[9];
+  assign _0003_ = _0000_[10];
+  assign _0004_ = _0000_[11];
+  assign _0005_ = _0000_[12];
+  assign _0006_ = _0000_[13];
+  assign _0007_ = _0000_[14];
+  assign _0008_ = _0000_[15];
+  assign _0009_ = _0000_[16];
+  assign _0010_ = _0000_[17];
+  assign _0011_ = _0000_[18];
+  assign _0581_[11:10] = { 1'h0, y[30] };
+  assign { _0582_[11:9], _0582_[0] } = { 1'h0, wire1[10:9], wire9[0] };
+  assign { _0584_[10:8], _0584_[6:5], _0584_[1] } = { reg4[10:8], reg4[6:5], reg4[1] };
+  assign reg4[14:11] = { reg4[10], reg4[10], reg4[10], reg4[10] };
+  assign reg6 = { reg4[10], reg4[10], reg4[10], reg4[10], reg4[10], reg4[10], reg4[10], reg4[10], reg4[10], reg4[10], reg4[10:0] };
+  assign reg8[13:1] = 13'h0000;
+  assign wire10[13:0] = { wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14] };
+  assign wire24 = { y[125], y[125], y[125], y[122:106] };
+  assign wire26 = reg4[5:0];
+  assign wire27 = { y[176:167], wire0[2], y[165] };
+  assign wire29 = 10'b0000000xxx;
+  assign wire9[11:5] = y[30:24];
+  assign { y[183:177], y[166], y[164:126], y[124:123], y[105:31], y[23:0] } = { 6'h00, wire28, wire0[2], 16'h0000, reg4[5:0], 16'h0000, wire25, y[125], y[125], reg4[10], reg4[10], reg4[10], reg4[10], reg4[10:0], reg5, reg4[10], reg4[10], reg4[10], reg4[10], reg4[10], reg4[10], reg4[10], reg4[10], reg4[10], reg4[10], reg4[10:0], reg7, 13'h0000, reg8[0], 2'h0, wire9[4:0], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire10[14], wire22, 1'h0 };
+endmodule
diff --git a/presentation/Makefile b/presentation/Makefile
new file mode 100644
index 0000000..7ac8ecc
--- /dev/null
+++ b/presentation/Makefile
@@ -0,0 +1,4 @@
+all: presentation.pdf
+
+%.pdf: %.tex
+	latexmk -pdf -pdflatex="lualatex -shell-escape" $< </dev/null
diff --git a/presentation/beamercolorthememetropolis-highcontrast.sty b/presentation/beamercolorthememetropolis-highcontrast.sty
new file mode 100644
index 0000000..85665dc
--- /dev/null
+++ b/presentation/beamercolorthememetropolis-highcontrast.sty
@@ -0,0 +1,39 @@
+%%
+%% This is file `beamercolorthememetropolis-highcontrast.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% beamercolorthememetropolis-highcontrast.dtx  (with options: `package')
+%% ---------------------------------------------------------------------------
+%% Copyright 2015 Matthias Vogelgesang and the LaTeX community. A full list of
+%% contributors can be found at
+%% 
+%%     https://github.com/matze/mtheme/graphs/contributors
+%% 
+%% and the original template was based on the HSRM theme by Benjamin Weiss.
+%% 
+%% This work is licensed under a Creative Commons Attribution-ShareAlike 4.0
+%% International License (https://creativecommons.org/licenses/by-sa/4.0/).
+%% ---------------------------------------------------------------------------
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{beamercolorthememetropolis-highcontrast}[2017/01/23 Metropolis color theme]
+\usecolortheme{metropolis}
+
+\definecolor{mAlert}{HTML}{AD003D}
+\definecolor{mExample}{HTML}{005580}
+
+\setbeamercolor{normal text}{%
+  fg=black,
+  bg=white
+}
+\setbeamercolor{alerted text}{%
+  fg=mAlert,
+}
+\setbeamercolor{example text}{%
+  fg=mExample,
+}
+\mode<all>
+\endinput
+%%
+%% End of file `beamercolorthememetropolis-highcontrast.sty'.
diff --git a/presentation/beamercolorthememetropolis.sty b/presentation/beamercolorthememetropolis.sty
new file mode 100644
index 0000000..cdc497a
--- /dev/null
+++ b/presentation/beamercolorthememetropolis.sty
@@ -0,0 +1,138 @@
+%%
+%% This is file `beamercolorthememetropolis.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% beamercolorthememetropolis.dtx  (with options: `package')
+%% ---------------------------------------------------------------------------
+%% Copyright 2015 Matthias Vogelgesang and the LaTeX community. A full list of
+%% contributors can be found at
+%% 
+%%     https://github.com/matze/mtheme/graphs/contributors
+%% 
+%% and the original template was based on the HSRM theme by Benjamin Weiss.
+%% 
+%% This work is licensed under a Creative Commons Attribution-ShareAlike 4.0
+%% International License (https://creativecommons.org/licenses/by-sa/4.0/).
+%% ---------------------------------------------------------------------------
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{beamercolorthememetropolis}[2017/01/23 Metropolis color theme]
+\RequirePackage{pgfopts}
+\pgfkeys{
+  /metropolis/color/block/.cd,
+    .is choice,
+    transparent/.code=\metropolis@block@transparent,
+    fill/.code=\metropolis@block@fill,
+}
+\pgfkeys{
+  /metropolis/color/background/.cd,
+    .is choice,
+    dark/.code=\metropolis@colors@dark,
+    light/.code=\metropolis@colors@light,
+}
+\newcommand{\metropolis@color@setdefaults}{
+  \pgfkeys{/metropolis/color/.cd,
+    background=light,
+    block=transparent,
+  }
+}
+\definecolor{mDarkBrown}{HTML}{604c38}
+\definecolor{mDarkTeal}{HTML}{23373b}
+\definecolor{mLightBrown}{HTML}{EB811B}
+\definecolor{mLightGreen}{HTML}{14B03D}
+\newcommand{\metropolis@colors@dark}{
+  \setbeamercolor{normal text}{%
+    fg=black!2,
+    bg=mDarkTeal
+  }
+  \usebeamercolor[fg]{normal text}
+}
+\newcommand{\metropolis@colors@light}{
+  \setbeamercolor{normal text}{%
+    fg=mDarkTeal,
+    bg=black!2
+  }
+}
+\setbeamercolor{alerted text}{%
+  fg=mLightBrown
+}
+\setbeamercolor{example text}{%
+  fg=mLightGreen
+}
+\setbeamercolor{titlelike}{use=normal text, parent=normal text}
+\setbeamercolor{author}{use=normal text, parent=normal text}
+\setbeamercolor{date}{use=normal text, parent=normal text}
+\setbeamercolor{institute}{use=normal text, parent=normal text}
+\setbeamercolor{structure}{use=normal text, fg=normal text.fg}
+\setbeamercolor{palette primary}{%
+  use=normal text,
+  fg=normal text.bg,
+  bg=normal text.fg
+}
+\setbeamercolor{frametitle}{%
+  use=palette primary,
+  parent=palette primary
+}
+\setbeamercolor{progress bar}{%
+  use=alerted text,
+  fg=alerted text.fg,
+  bg=alerted text.fg!50!black!30
+}
+\setbeamercolor{title separator}{
+  use=progress bar,
+  parent=progress bar
+}
+\setbeamercolor{progress bar in head/foot}{%
+  use=progress bar,
+  parent=progress bar
+}
+\setbeamercolor{progress bar in section page}{
+  use=progress bar,
+  parent=progress bar
+}
+\newcommand{\metropolis@block@transparent}{
+  \setbeamercolor{block title}{%
+    use=normal text,
+    fg=normal text.fg,
+    bg=
+  }
+  \setbeamercolor{block body}{
+    bg=
+  }
+}
+\newcommand{\metropolis@block@fill}{
+  \setbeamercolor{block title}{%
+    use=normal text,
+    fg=normal text.fg,
+    bg=normal text.bg!80!fg
+  }
+  \setbeamercolor{block body}{
+    use={block title, normal text},
+    bg=block title.bg!50!normal text.bg
+  }
+}
+\setbeamercolor{block title alerted}{%
+    use={block title, alerted text},
+    bg=block title.bg,
+    fg=alerted text.fg
+}
+\setbeamercolor{block title example}{%
+    use={block title, example text},
+    bg=block title.bg,
+    fg=example text.fg
+}
+\setbeamercolor{block body alerted}{use=block body, parent=block body}
+\setbeamercolor{block body example}{use=block body, parent=block body}
+\setbeamercolor{footnote}{fg=normal text.fg!90}
+\setbeamercolor{footnote mark}{fg=.}
+\setbeamercolor{bibliography entry author}{fg=, bg=}
+\setbeamercolor{bibliography entry title}{fg=, bg=}
+\setbeamercolor{bibliography entry location}{fg=, bg=}
+\setbeamercolor{bibliography entry note}{fg=, bg=}
+\metropolis@color@setdefaults
+\ProcessPgfPackageOptions{/metropolis/color}
+\mode<all>
+\endinput
+%%
+%% End of file `beamercolorthememetropolis.sty'.
diff --git a/presentation/beamerfontthememetropolis.sty b/presentation/beamerfontthememetropolis.sty
new file mode 100644
index 0000000..15cced3
--- /dev/null
+++ b/presentation/beamerfontthememetropolis.sty
@@ -0,0 +1,325 @@
+%%
+%% This is file `beamerfontthememetropolis.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% beamerfontthememetropolis.dtx  (with options: `package')
+%% ---------------------------------------------------------------------------
+%% Copyright 2015 Matthias Vogelgesang and the LaTeX community. A full list of
+%% contributors can be found at
+%% 
+%%     https://github.com/matze/mtheme/graphs/contributors
+%% 
+%% and the original template was based on the HSRM theme by Benjamin Weiss.
+%% 
+%% This work is licensed under a Creative Commons Attribution-ShareAlike 4.0
+%% International License (https://creativecommons.org/licenses/by-sa/4.0/).
+%% ---------------------------------------------------------------------------
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{beamerfontthememetropolis}[2017/01/23 Metropolis font theme]
+\RequirePackage{etoolbox}
+\RequirePackage{ifxetex}
+\RequirePackage{ifluatex}
+\RequirePackage{pgfopts}
+\ifboolexpr{bool {xetex} or bool {luatex}}{
+  \@ifpackageloaded{fontspec}{
+    \PassOptionsToPackage{no-math}{fontspec}
+  }{
+    \RequirePackage[no-math]{fontspec}
+  }
+  \newcounter{fontsnotfound}
+  \newcommand{\checkfont}[1]{%
+    \suppressfontnotfounderror=1%
+    \font\x = "#1" at 10pt
+    \selectfont
+    \ifx\x\nullfont%
+      \stepcounter{fontsnotfound}%
+    \fi%
+    \suppressfontnotfounderror=0%
+  }
+
+  \newcommand{\iffontsavailable}[3]{%
+    \setcounter{fontsnotfound}{0}%
+    \expandafter\forcsvlist\expandafter%
+    \checkfont\expandafter{#1}%
+    \ifnum\value{fontsnotfound}=0%
+      #2%
+    \else%
+      #3%
+    \fi%
+  }
+  \iffontsavailable{Fira Sans Light,%
+                    Fira Sans Light Italic,%
+                    Fira Sans,%
+                    Fira Sans Italic}%
+  {%
+    \setsansfont[ItalicFont={Fira Sans Light Italic},%
+                 BoldFont={Fira Sans},%
+                 BoldItalicFont={Fira Sans Italic}]%
+                {Fira Sans Light}%
+  }{%
+    \iffontsavailable{Fira Sans Light OT,%
+                      Fira Sans Light Italic OT,%
+                      Fira Sans OT,%
+                      Fira Sans Italic OT}%
+    {%
+      \setsansfont[ItalicFont={Fira Sans Light Italic OT},%
+                   BoldFont={Fira Sans OT},%
+                   BoldItalicFont={Fira Sans Italic OT}]%
+                  {Fira Sans Light OT}%
+    }{%
+      \PackageWarning{beamerthememetropolis}{%
+        Could not find Fira Sans fonts%
+      }
+    }
+  }
+  \iffontsavailable{Fira Mono, Fira Mono Bold}{%
+    \setmonofont[BoldFont={Fira Mono Medium}]{Fira Mono}%
+  }{%
+    \iffontsavailable{Fira Mono OT, Fira Mono Bold OT}{%
+      \setmonofont[BoldFont={Fira Mono Medium OT}]{Fira Mono OT}%
+    }{%
+      \PackageWarning{beamerthememetropolis}{%
+        Could not find Fira Mono fonts%
+      }
+    }
+  }
+  \AtBeginEnvironment{tabular}{%
+    \addfontfeature{Numbers={Monospaced}}%
+  }
+}{%
+  \PackageWarning{beamerthememetropolis}{%
+    You need to compile with XeLaTeX or LuaLaTeX to use the Fira fonts%
+  }
+}
+\setbeamerfont{title}{size=\Large,%
+                      series=\bfseries}
+\setbeamerfont{author}{size=\small}
+\setbeamerfont{date}{size=\small}
+\setbeamerfont{section title}{size=\Large,%
+                              series=\bfseries}
+\setbeamerfont{block title}{size=\normalsize,%
+                            series=\bfseries}
+\setbeamerfont{block title alerted}{size=\normalsize,%
+                                    series=\bfseries}
+\setbeamerfont*{subtitle}{size=\large}
+\setbeamerfont{frametitle}{size=\large,%
+                           series=\bfseries}
+\setbeamerfont{caption}{size=\small}
+\setbeamerfont{caption name}{series=\bfseries}
+\setbeamerfont{description item}{series=\bfseries}
+\setbeamerfont{page number in head/foot}{size=\scriptsize}
+\setbeamerfont{bibliography entry author}{size=\normalsize,%
+                                          series=\normalfont}
+\setbeamerfont{bibliography entry title}{size=\normalsize,%
+                                         series=\bfseries}
+\setbeamerfont{bibliography entry location}{size=\normalsize,%
+                                            series=\normalfont}
+\setbeamerfont{bibliography entry note}{size=\small,%
+                                        series=\normalfont}
+\setbeamerfont{standout}{size=\Large,%
+                         series=\bfseries}
+\pgfkeys{
+  /metropolis/font/titleformat title/.cd,
+    .is choice,
+    regular/.code={%
+      \let\metropolis@titleformat\@empty%
+      \setbeamerfont{title}{shape=\normalfont}%
+    },
+    smallcaps/.code={%
+      \let\metropolis@titleformat\@empty%
+      \setbeamerfont{title}{shape=\scshape}%
+    },
+    allsmallcaps/.code={%
+      \let\metropolis@titleformat\lowercase%
+      \setbeamerfont{title}{shape=\scshape}%
+      \PackageWarning{beamerthememetropolis}{%
+        Be aware that titleformat title=allsmallcaps can lead to problems%
+      }
+    },
+    allcaps/.code={%
+      \let\metropolis@titleformat\uppercase%
+      \setbeamerfont{title}{shape=\normalfont}
+      \PackageWarning{beamerthememetropolis}{%
+        Be aware that titleformat title=allcaps can lead to problems%
+      }
+    },
+}
+\pgfkeys{
+  /metropolis/font/titleformat subtitle/.cd,
+    .is choice,
+    regular/.code={%
+      \let\metropolis@subtitleformat\@empty%
+      \setbeamerfont{subtitle}{shape=\normalfont}%
+    },
+    smallcaps/.code={%
+      \let\metropolis@subtitleformat\@empty%
+      \setbeamerfont{subtitle}{shape=\scshape}%
+    },
+    allsmallcaps/.code={%
+      \let\metropolis@subtitleformat\lowercase%
+      \setbeamerfont{subtitle}{shape=\scshape}%
+      \PackageWarning{beamerthememetropolis}{%
+        Be aware that titleformat subtitle=allsmallcaps can lead to problems%
+      }
+    },
+    allcaps/.code={%
+      \let\metropolis@subtitleformat\uppercase%
+      \setbeamerfont{subtitle}{shape=\normalfont}%
+      \PackageWarning{beamerthememetropolis}{%
+        Be aware that titleformat subtitle=allcaps can lead to problems%
+      }
+    },
+}
+\pgfkeys{
+  /metropolis/font/titleformat section/.cd,
+    .is choice,
+    regular/.code={%
+      \let\metropolis@sectiontitleformat\@empty%
+      \setbeamerfont{section title}{shape=\normalfont}%
+    },
+    smallcaps/.code={%
+      \let\metropolis@sectiontitleformat\@empty%
+      \setbeamerfont{section title}{shape=\scshape}%
+    },
+    allsmallcaps/.code={%
+      \let\metropolis@sectiontitleformat\MakeLowercase%
+      \setbeamerfont{section title}{shape=\scshape}%
+      \PackageWarning{beamerthememetropolis}{%
+        Be aware that titleformat section=allsmallcaps can lead to problems%
+      }
+    },
+    allcaps/.code={%
+      \let\metropolis@sectiontitleformat\MakeUppercase%
+      \setbeamerfont{section title}{shape=\normalfont}%
+      \PackageWarning{beamerthememetropolis}{%
+        Be aware that titleformat section=allcaps can lead to problems%
+      }
+    },
+}
+\pgfkeys{
+  /metropolis/font/titleformat frame/.cd,
+    .is choice,
+    regular/.code={%
+      \let\metropolis@frametitleformat\@empty%
+      \setbeamerfont{frametitle}{shape=\normalfont}%
+    },
+    smallcaps/.code={%
+      \let\metropolis@frametitleformat\@empty%
+      \setbeamerfont{frametitle}{shape=\scshape}%
+    },
+    allsmallcaps/.code={%
+      \let\metropolis@frametitleformat\MakeLowercase%
+      \setbeamerfont{frametitle}{shape=\scshape}%
+      \PackageWarning{beamerthememetropolis}{%
+        Be aware that titleformat frame=allsmallcaps can lead to problems%
+      }
+    },
+    allcaps/.code={%
+      \let\metropolis@frametitleformat\MakeUppercase%
+      \setbeamerfont{frametitle}{shape=\normalfont}
+      \PackageWarning{beamerthememetropolis}{%
+        Be aware that titleformat frame=allcaps can lead to problems%
+      }
+    },
+}
+\pgfkeys{
+  /metropolis/font/.cd,
+  titleformattitle/.code=\pgfkeysalso{titleformat title=#1},
+  titleformatsubtitle/.code=\pgfkeysalso{titleformat subtitle=#1},
+  titleformatsection/.code=\pgfkeysalso{titleformat section=#1},
+  titleformatframe/.code=\pgfkeysalso{titleformat frame=#1},
+}
+\newcommand{\metropolis@font@setdefaults}{
+  \pgfkeys{/metropolis/font/.cd,
+    titleformat title=regular,
+    titleformat subtitle=regular,
+    titleformat section=regular,
+    titleformat frame=regular,
+  }
+}
+\def\metropolis@titleformat#1{#1}
+\def\metropolis@subtitleformat#1{#1}
+\def\metropolis@sectiontitleformat#1{#1}
+\def\metropolis@frametitleformat#1{#1}
+\patchcmd{\beamer@title}%
+  {\def\inserttitle{#2}}%
+  {\def\inserttitle{\metropolis@titleformat{#2}}}%
+  {}%
+  {\PackageError{beamerfontthememetropolis}{Patching title failed}\@ehc}
+\patchcmd{\beamer@subtitle}%
+  {\def\insertsubtitle{#2}}%
+  {\def\insertsubtitle{\metropolis@subtitleformat{#2}}}%
+  {}%
+  {\PackageError{beamerfontthememetropolis}{Patching subtitle failed}\@ehc}
+\patchcmd{\sectionentry}
+  {\def\insertsectionhead{#2}}
+  {\def\insertsectionhead{\metropolis@sectiontitleformat{#2}}}
+  {}
+  {\PackageError{beamerfontthememetropolis}{Patching section title failed}\@ehc}
+\@tempswafalse
+\patchcmd{\beamer@section}
+  {\edef\insertsectionhead{\noexpand\hyperlink{Navigation\the\c@page}{\unexpanded{#1}}}}
+  {\edef\insertsectionhead{\noexpand\hyperlink{Navigation\the\c@page}{%
+    \noexpand\metropolis@sectiontitleformat{\unexpanded{#1}}}}}
+  {\@tempswatrue}
+  {}
+\patchcmd{\beamer@section}
+  {\def\insertsectionhead{\hyperlink{Navigation\the\c@page}{#1}}}
+  {\def\insertsectionhead{\hyperlink{Navigation\the\c@page}{%
+    \metropolis@sectiontitleformat{#1}}}}
+  {\@tempswatrue}
+  {}
+\patchcmd{\beamer@section}
+  {\protected@edef\insertsectionhead{\noexpand\hyperlink{Navigation\the\c@page}{#1}}}
+  {\protected@edef\insertsectionhead{\noexpand\hyperlink{Navigation\the\c@page}{%
+    \noexpand\metropolis@sectiontitleformat{#1}}}}
+  {\@tempswatrue}
+  {}
+\if@tempswa\else
+  \PackageError{beamerfontthememetropolis}{Patching section title failed}\@ehc
+\fi
+\@tempswafalse
+\patchcmd{\beamer@subsection}
+  {\edef\insertsubsectionhead{\noexpand\hyperlink{Navigation\the\c@page}{\unexpanded{#1}}}}
+  {\edef\insertsubsectionhead{\noexpand\hyperlink{Navigation\the\c@page}{%
+    \noexpand\metropolis@sectiontitleformat{\unexpanded{#1}}}}}
+  {\@tempswatrue}
+  {}
+\patchcmd{\beamer@subsection}
+  {\def\insertsubsectionhead{\hyperlink{Navigation\the\c@page}{#1}}}
+  {\def\insertsubsectionhead{\hyperlink{Navigation\the\c@page}{%
+    \metropolis@sectiontitleformat{#1}}}}
+  {\@tempswatrue}
+  {}
+\patchcmd{\beamer@subsection}
+  {\protected@edef\insertsubsectionhead{\noexpand\hyperlink{Navigation\the\c@page}{#1}}}
+  {\protected@edef\insertsubsectionhead{\noexpand\hyperlink{Navigation\the\c@page}{%
+    \noexpand\metropolis@sectiontitleformat{#1}}}}
+  {\@tempswatrue}
+  {}
+\if@tempswa\else
+  \PackageError{beamerfontthememetropolis}{Patching section title failed}\@ehc
+\fi
+\patchcmd{\beamer@@frametitle}
+  {{%
+      \gdef\insertframetitle{{#2\ifnum\beamer@autobreakcount>0\relax{}\space%
+      \usebeamertemplate*{frametitle continuation}\fi}}%
+    \gdef\beamer@frametitle{#2}%
+    \gdef\beamer@shortframetitle{#1}%
+    }}
+  {{%
+      \gdef\insertframetitle{{\metropolis@frametitleformat{#2}\ifnum%
+      \beamer@autobreakcount>0\relax{}\space%
+      \usebeamertemplate*{frametitle continuation}\fi}}%
+    \gdef\beamer@frametitle{#2}%
+    \gdef\beamer@shortframetitle{#1}%
+    }}
+  {}
+  {\PackageError{beamerfontthememetropolis}{Patching frame title failed}\@ehc}
+\metropolis@font@setdefaults
+\ProcessPgfPackageOptions{/metropolis/font}
+\endinput
+%%
+%% End of file `beamerfontthememetropolis.sty'.
diff --git a/presentation/beamerinnerthememetropolis.sty b/presentation/beamerinnerthememetropolis.sty
new file mode 100644
index 0000000..415b46f
--- /dev/null
+++ b/presentation/beamerinnerthememetropolis.sty
@@ -0,0 +1,297 @@
+%%
+%% This is file `beamerinnerthememetropolis.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% beamerinnerthememetropolis.dtx  (with options: `package')
+%% ---------------------------------------------------------------------------
+%% Copyright 2015 Matthias Vogelgesang and the LaTeX community. A full list of
+%% contributors can be found at
+%% 
+%%     https://github.com/matze/mtheme/graphs/contributors
+%% 
+%% and the original template was based on the HSRM theme by Benjamin Weiss.
+%% 
+%% This work is licensed under a Creative Commons Attribution-ShareAlike 4.0
+%% International License (https://creativecommons.org/licenses/by-sa/4.0/).
+%% ---------------------------------------------------------------------------
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{beamerinnerthememetropolis}[2017/01/23 Metropolis inner theme]
+\RequirePackage{etoolbox}
+\RequirePackage{keyval}
+\RequirePackage{calc}
+\RequirePackage{pgfopts}
+\RequirePackage{tikz}
+\pgfkeys{
+  /metropolis/inner/sectionpage/.cd,
+    .is choice,
+    none/.code=\metropolis@disablesectionpage,
+    simple/.code={\metropolis@enablesectionpage
+                  \setbeamertemplate{section page}[simple]},
+    progressbar/.code={\metropolis@enablesectionpage
+                       \setbeamertemplate{section page}[progressbar]},
+}
+\pgfkeys{
+  /metropolis/inner/subsectionpage/.cd,
+    .is choice,
+    none/.code=\metropolis@disablesubsectionpage,
+    simple/.code={\metropolis@enablesubsectionpage
+                  \setbeamertemplate{section page}[simple]},
+    progressbar/.code={\metropolis@enablesubsectionpage
+                       \setbeamertemplate{section page}[progressbar]},
+}
+\newcommand{\metropolis@inner@setdefaults}{
+  \pgfkeys{/metropolis/inner/.cd,
+    sectionpage=progressbar,
+    subsectionpage=none
+  }
+}
+\setbeamertemplate{title page}{
+  \begin{minipage}[b][\paperheight]{\textwidth}
+    \ifx\inserttitlegraphic\@empty\else\usebeamertemplate*{title graphic}\fi
+    \vfill%
+    \ifx\inserttitle\@empty\else\usebeamertemplate*{title}\fi
+    \ifx\insertsubtitle\@empty\else\usebeamertemplate*{subtitle}\fi
+    \usebeamertemplate*{title separator}
+    \ifx\beamer@shortauthor\@empty\else\usebeamertemplate*{author}\fi
+    \ifx\insertdate\@empty\else\usebeamertemplate*{date}\fi
+    \ifx\insertinstitute\@empty\else\usebeamertemplate*{institute}\fi
+    \vfill
+    \vspace*{1mm}
+  \end{minipage}
+}
+\def\maketitle{%
+  \ifbeamer@inframe
+    \titlepage
+  \else
+    \frame[plain,noframenumbering]{\titlepage}
+  \fi
+}
+\def\titlepage{%
+  \usebeamertemplate{title page}
+}
+\setbeamertemplate{title graphic}{
+  \vbox to 0pt {
+    \vspace*{2em}
+    \inserttitlegraphic%
+  }%
+  \nointerlineskip%
+}
+\setbeamertemplate{title}{
+  \raggedright%
+  \linespread{1.0}%
+  \inserttitle%
+  \par%
+  \vspace*{0.5em}
+}
+\setbeamertemplate{subtitle}{
+  \raggedright%
+  \insertsubtitle%
+  \par%
+  \vspace*{0.5em}
+}
+\newlength{\metropolis@titleseparator@linewidth}
+\setlength{\metropolis@titleseparator@linewidth}{0.4pt}
+\setbeamertemplate{title separator}{
+  \tikzexternaldisable%
+  \begin{tikzpicture}
+    \fill[fg] (0,0) rectangle (\textwidth, \metropolis@titleseparator@linewidth);
+  \end{tikzpicture}%
+  \tikzexternalenable%
+  \par%
+}
+\setbeamertemplate{author}{
+  \vspace*{2em}
+  \insertauthor%
+  \par%
+  \vspace*{0.25em}
+}
+\setbeamertemplate{date}{
+  \insertdate%
+  \par%
+}
+\setbeamertemplate{institute}{
+  \vspace*{3mm}
+  \insertinstitute%
+  \par%
+}
+\defbeamertemplate{section page}{simple}{
+  \begin{center}
+    \usebeamercolor[fg]{section title}
+    \usebeamerfont{section title}
+    \insertsectionhead\par
+    \ifx\insertsubsectionhead\@empty\else
+      \usebeamercolor[fg]{subsection title}
+      \usebeamerfont{subsection title}
+      \insertsubsectionhead
+    \fi
+  \end{center}
+}
+\defbeamertemplate{section page}{progressbar}{
+  \centering
+  \begin{minipage}{22em}
+    \raggedright
+    \usebeamercolor[fg]{section title}
+    \usebeamerfont{section title}
+    \insertsectionhead\\[-1ex]
+    \usebeamertemplate*{progress bar in section page}
+    \par
+    \ifx\insertsubsectionhead\@empty\else%
+      \usebeamercolor[fg]{subsection title}%
+      \usebeamerfont{subsection title}%
+      \insertsubsectionhead
+    \fi
+  \end{minipage}
+  \par
+  \vspace{\baselineskip}
+}
+\newcommand{\metropolis@disablesectionpage}{
+  \AtBeginSection{
+    % intentionally empty
+  }
+}
+\newcommand{\metropolis@enablesectionpage}{
+  \AtBeginSection{
+    \ifbeamer@inframe
+      \sectionpage
+    \else
+      \frame[plain,c,noframenumbering]{\sectionpage}
+    \fi
+  }
+}
+\setbeamertemplate{subsection page}{%
+  \usebeamertemplate*{section page}
+}
+\newcommand{\metropolis@disablesubsectionpage}{
+  \AtBeginSubsection{
+    % intentionally empty
+  }
+}
+\newcommand{\metropolis@enablesubsectionpage}{
+  \AtBeginSubsection{
+    \ifbeamer@inframe
+      \subsectionpage
+    \else
+      \frame[plain,c,noframenumbering]{\subsectionpage}
+    \fi
+  }
+}
+\newlength{\metropolis@progressonsectionpage}
+\newlength{\metropolis@progressonsectionpage@linewidth}
+\setlength{\metropolis@progressonsectionpage@linewidth}{0.4pt}
+\setbeamertemplate{progress bar in section page}{
+  \setlength{\metropolis@progressonsectionpage}{%
+    \textwidth * \ratio{\insertframenumber pt}{\inserttotalframenumber pt}%
+  }%
+  \tikzexternaldisable%
+  \begin{tikzpicture}
+    \fill[bg] (0,0) rectangle (\textwidth, \metropolis@progressonsectionpage@linewidth);
+    \fill[fg] (0,0) rectangle (\metropolis@progressonsectionpage, \metropolis@progressonsectionpage@linewidth);
+  \end{tikzpicture}%
+  \tikzexternalenable%
+}
+\def\inserttotalframenumber{100}
+\newlength{\metropolis@blocksep}
+\newlength{\metropolis@blockadjust}
+\setlength{\metropolis@blocksep}{0.75ex}
+\setlength{\metropolis@blockadjust}{0.25ex}
+\providecommand{\metropolis@strut}{%
+  \vphantom{ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz()}%
+}
+\newcommand{\metropolis@block}[1]{
+  \par\vskip\medskipamount%
+  \setlength{\parskip}{0pt}
+  \ifbeamercolorempty[bg]{block title#1}{%
+    \begin{beamercolorbox}[rightskip=0pt plus 4em]{block title#1}}{%
+  \ifbeamercolorempty[bg]{block title}{%
+    \begin{beamercolorbox}[rightskip=0pt plus 4em]{block title#1}%
+  }%
+  {%
+    \begin{beamercolorbox}[
+      sep=\dimexpr\metropolis@blocksep-\metropolis@blockadjust\relax,
+      leftskip=\metropolis@blockadjust,
+      rightskip=\dimexpr\metropolis@blockadjust plus 4em\relax
+    ]{block title#1}%
+  }}%
+      \usebeamerfont*{block title#1}%
+      \metropolis@strut%
+      \insertblocktitle%
+      \metropolis@strut%
+  \end{beamercolorbox}%
+  \nointerlineskip%
+  \ifbeamercolorempty[bg]{block body#1}{%
+    \begin{beamercolorbox}[vmode]{block body#1}}{
+  \ifbeamercolorempty[bg]{block body}{%
+    \begin{beamercolorbox}[vmode]{block body#1}%
+  }{%
+    \begin{beamercolorbox}[sep=\metropolis@blocksep, vmode]{block body#1}%
+    \vspace{-\metropolis@parskip}
+  }}%
+      \usebeamerfont{block body#1}%
+      \setlength{\parskip}{\metropolis@parskip}%
+}
+\setbeamertemplate{block begin}{\metropolis@block{}}
+\setbeamertemplate{block alerted begin}{\metropolis@block{ alerted}}
+\setbeamertemplate{block example begin}{\metropolis@block{ example}}
+\setbeamertemplate{block end}{\end{beamercolorbox}\vspace*{0.2ex}}
+\setbeamertemplate{block alerted end}{\end{beamercolorbox}\vspace*{0.2ex}}
+\setbeamertemplate{block example end}{\end{beamercolorbox}\vspace*{0.2ex}}
+\setbeamertemplate{itemize items}{\textbullet}
+\setbeamertemplate{caption label separator}{: }
+\setbeamertemplate{caption}[numbered]
+\setbeamertemplate{footnote}{%
+  \parindent 0em\noindent%
+  \raggedright
+  \usebeamercolor{footnote}\hbox to 0.8em{\hfil\insertfootnotemark}\insertfootnotetext\par%
+}
+\newlength{\metropolis@parskip}
+\setlength{\metropolis@parskip}{0.5em}
+\setlength{\parskip}{\metropolis@parskip}
+\linespread{1.15}
+\define@key{beamerframe}{c}[true]{% centered
+  \beamer@frametopskip=0pt plus 1fill\relax%
+  \beamer@framebottomskip=0pt plus 1fill\relax%
+  \beamer@frametopskipautobreak=0pt plus .4\paperheight\relax%
+  \beamer@framebottomskipautobreak=0pt plus .6\paperheight\relax%
+  \def\beamer@initfirstlineunskip{}%
+}
+\providebool{metropolis@standout}
+\define@key{beamerframe}{standout}[true]{%
+  \booltrue{metropolis@standout}
+  \begingroup
+    \setkeys{beamerframe}{c}
+    \setkeys{beamerframe}{noframenumbering}
+    \ifbeamercolorempty[bg]{palette primary}{
+      \setbeamercolor{background canvas}{
+        use=palette primary,
+        bg=-palette primary.fg
+      }
+    }{
+      \setbeamercolor{background canvas}{
+        use=palette primary,
+        bg=palette primary.bg
+      }
+    }
+    \setbeamercolor{local structure}{
+      fg=palette primary.fg
+    }
+    \usebeamercolor[fg]{palette primary}
+}
+  \pretocmd{\beamer@reseteecodes}{%
+    \ifbool{metropolis@standout}{
+      \endgroup
+      \boolfalse{metropolis@standout}
+    }{}
+  }{}{}
+  \AtBeginEnvironment{beamer@frameslide}{
+    \ifbool{metropolis@standout}{
+      \centering
+      \usebeamerfont{standout}
+    }{}
+  }
+\metropolis@inner@setdefaults
+\ProcessPgfPackageOptions{/metropolis/inner}
+\endinput
+%%
+%% End of file `beamerinnerthememetropolis.sty'.
diff --git a/presentation/beamerouterthememetropolis.sty b/presentation/beamerouterthememetropolis.sty
new file mode 100644
index 0000000..928a122
--- /dev/null
+++ b/presentation/beamerouterthememetropolis.sty
@@ -0,0 +1,137 @@
+%%
+%% This is file `beamerouterthememetropolis.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% beamerouterthememetropolis.dtx  (with options: `package')
+%% ---------------------------------------------------------------------------
+%% Copyright 2015 Matthias Vogelgesang and the LaTeX community. A full list of
+%% contributors can be found at
+%% 
+%%     https://github.com/matze/mtheme/graphs/contributors
+%% 
+%% and the original template was based on the HSRM theme by Benjamin Weiss.
+%% 
+%% This work is licensed under a Creative Commons Attribution-ShareAlike 4.0
+%% International License (https://creativecommons.org/licenses/by-sa/4.0/).
+%% ---------------------------------------------------------------------------
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{beamerouterthememetropolis}[2017/01/23 Metropolis outer theme]
+\RequirePackage{etoolbox}
+\RequirePackage{calc}
+\RequirePackage{pgfopts}
+\pgfkeys{
+  /metropolis/outer/numbering/.cd,
+    .is choice,
+    none/.code=\setbeamertemplate{frame numbering}[none],
+    counter/.code=\setbeamertemplate{frame numbering}[counter],
+    fraction/.code=\setbeamertemplate{frame numbering}[fraction],
+}
+\pgfkeys{
+  /metropolis/outer/progressbar/.cd,
+    .is choice,
+    none/.code={%
+      \setbeamertemplate{headline}[plain]
+      \setbeamertemplate{frametitle}[plain]
+      \setbeamertemplate{footline}[plain]
+    },
+    head/.code={\pgfkeys{/metropolis/outer/progressbar=none}
+      \addtobeamertemplate{headline}{}{%
+        \usebeamertemplate*{progress bar in head/foot}
+      }
+    },
+    frametitle/.code={\pgfkeys{/metropolis/outer/progressbar=none}
+      \addtobeamertemplate{frametitle}{}{%
+        \usebeamertemplate*{progress bar in head/foot}
+      }
+    },
+    foot/.code={\pgfkeys{/metropolis/outer/progressbar=none}
+      \addtobeamertemplate{footline}{}{%
+        \usebeamertemplate*{progress bar in head/foot}%
+      }
+    },
+}
+\newcommand{\metropolis@outer@setdefaults}{
+  \pgfkeys{/metropolis/outer/.cd,
+    numbering=counter,
+    progressbar=none,
+  }
+}
+\setbeamertemplate{navigation symbols}{}
+\defbeamertemplate{frame footer}{none}{}
+\defbeamertemplate{frame footer}{custom}[1]{ #1 }
+\defbeamertemplate{frame numbering}{none}{}
+\defbeamertemplate{frame numbering}{counter}{\insertframenumber}
+\defbeamertemplate{frame numbering}{fraction}{
+  \insertframenumber/\inserttotalframenumber
+}
+\defbeamertemplate{headline}{plain}{}
+\defbeamertemplate{footline}{plain}{%
+  \begin{beamercolorbox}[wd=\textwidth, sep=3ex]{footline}%
+    \usebeamerfont{page number in head/foot}%
+    \usebeamertemplate*{frame footer}
+    \hfill%
+    \usebeamertemplate*{frame numbering}
+  \end{beamercolorbox}%
+}
+\newlength{\metropolis@frametitle@padding}
+\setlength{\metropolis@frametitle@padding}{2.2ex}
+\newcommand{\metropolis@frametitlestrut@start}{
+  \rule{0pt}{\metropolis@frametitle@padding +%
+    \totalheightof{%
+      \ifcsdef{metropolis@frametitleformat}{\metropolis@frametitleformat X}{X}%
+    }%
+  }%
+}
+\newcommand{\metropolis@frametitlestrut@end}{
+  \rule[-\metropolis@frametitle@padding]{0pt}{\metropolis@frametitle@padding}
+}
+\defbeamertemplate{frametitle}{plain}{%
+  \nointerlineskip%
+  \begin{beamercolorbox}[%
+      wd=\paperwidth,%
+      sep=0pt,%
+      leftskip=\metropolis@frametitle@padding,%
+      rightskip=\metropolis@frametitle@padding,%
+    ]{frametitle}%
+  \metropolis@frametitlestrut@start%
+  \insertframetitle%
+  \nolinebreak%
+  \metropolis@frametitlestrut@end%
+  \end{beamercolorbox}%
+}
+\setbeamertemplate{frametitle continuation}{%
+  \usebeamerfont{frametitle}
+  \romannumeral \insertcontinuationcount
+}
+\newlength{\metropolis@progressinheadfoot}
+\newlength{\metropolis@progressinheadfoot@linewidth}
+\setlength{\metropolis@progressinheadfoot@linewidth}{0.4pt}
+\setbeamertemplate{progress bar in head/foot}{
+  \nointerlineskip
+  \setlength{\metropolis@progressinheadfoot}{%
+    \paperwidth * \ratio{\insertframenumber pt}{\inserttotalframenumber pt}%
+  }%
+  \begin{beamercolorbox}[wd=\paperwidth]{progress bar in head/foot}
+    \tikzexternaldisable%
+    \begin{tikzpicture}
+      \fill[bg] (0,0) rectangle (\paperwidth, \metropolis@progressinheadfoot@linewidth);
+      \fill[fg] (0,0) rectangle (\metropolis@progressinheadfoot, \metropolis@progressinheadfoot@linewidth);
+    \end{tikzpicture}%
+    \tikzexternalenable%
+  \end{beamercolorbox}
+}
+\AtBeginDocument{%
+  \apptocmd{\appendix}{%
+    \pgfkeys{%
+      /metropolis/outer/.cd,
+      numbering=none,
+      progressbar=none}
+    }{}{}
+}
+\metropolis@outer@setdefaults
+\ProcessPgfPackageOptions{/metropolis/outer}
+\endinput
+%%
+%% End of file `beamerouterthememetropolis.sty'.
diff --git a/presentation/beamerthememetropolis.sty b/presentation/beamerthememetropolis.sty
new file mode 100644
index 0000000..9fbe86e
--- /dev/null
+++ b/presentation/beamerthememetropolis.sty
@@ -0,0 +1,107 @@
+%%
+%% This is file `beamerthememetropolis.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% beamerthememetropolis.dtx  (with options: `package')
+%% ---------------------------------------------------------------------------
+%% Copyright 2015 Matthias Vogelgesang and the LaTeX community. A full list of
+%% contributors can be found at
+%% 
+%%     https://github.com/matze/mtheme/graphs/contributors
+%% 
+%% and the original template was based on the HSRM theme by Benjamin Weiss.
+%% 
+%% This work is licensed under a Creative Commons Attribution-ShareAlike 4.0
+%% International License (https://creativecommons.org/licenses/by-sa/4.0/).
+%% ---------------------------------------------------------------------------
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{beamerthememetropolis}
+  [2017/01/23 v1.2 Metropolis Beamer theme]
+\RequirePackage{etoolbox}
+\RequirePackage{pgfopts}
+\pgfkeys{/metropolis/.cd,
+  .search also={
+    /metropolis/inner,
+    /metropolis/outer,
+    /metropolis/color,
+    /metropolis/font,
+  }
+}
+\pgfkeys{
+  /metropolis/titleformat plain/.cd,
+    .is choice,
+    regular/.code={%
+      \let\metropolis@plaintitleformat\@empty%
+      \setbeamerfont{standout}{shape=\normalfont}%
+    },
+    smallcaps/.code={%
+      \let\metropolis@plaintitleformat\@empty%
+      \setbeamerfont{standout}{shape=\scshape}%
+    },
+    allsmallcaps/.code={%
+      \let\metropolis@plaintitleformat\MakeLowercase%
+      \setbeamerfont{standout}{shape=\scshape}%
+      \PackageWarning{beamerthememetropolis}{%
+        Be aware that titleformat plain=allsmallcaps can lead to problems%
+      }
+    },
+    allcaps/.code={%
+      \let\metropolis@plaintitleformat\MakeUppercase%
+      \setbeamerfont{standout}{shape=\normalfont}%
+      \PackageWarning{beamerthememetropolis}{%
+        Be aware that titleformat plain=allcaps can lead to problems%
+      }
+    },
+}
+\pgfkeys{
+  /metropolis/titleformat/.code=\pgfkeysalso{
+      font/titleformat title=#1,
+      font/titleformat subtitle=#1,
+      font/titleformat section=#1,
+      font/titleformat frame=#1,
+      titleformat plain=#1,
+    }
+}
+\pgfkeys{/metropolis/.cd,
+  usetitleprogressbar/.code=\pgfkeysalso{outer/progressbar=frametitle},
+  noslidenumbers/.code=\pgfkeysalso{outer/numbering=none},
+  usetotalslideindicator/.code=\pgfkeysalso{outer/numbering=fraction},
+  nosectionslide/.code=\pgfkeysalso{inner/sectionpage=none},
+  darkcolors/.code=\pgfkeysalso{color/background=dark},
+  blockbg/.code=\pgfkeysalso{color/block=fill, inner/block=fill},
+}
+\newcommand{\metropolis@setdefaults}{
+  \pgfkeys{/metropolis/.cd,
+    titleformat plain=regular,
+  }
+}
+\providecommand{\tikzexternalenable}{}
+\providecommand{\tikzexternaldisable}{}
+\useinnertheme{metropolis}
+\useoutertheme{metropolis}
+\usecolortheme{metropolis}
+\usefonttheme{metropolis}
+\AtEndPreamble{%
+  \@ifpackageloaded{pgfplots}{%
+    \RequirePackage{pgfplotsthemetol}
+  }{}
+}
+\newcommand{\metroset}[1]{\pgfkeys{/metropolis/.cd,#1}}
+\def\metropolis@plaintitleformat#1{#1}
+\newcommand{\plain}[2][]{%
+  \PackageWarning{beamerthememetropolis}{%
+    The syntax `\plain' may be deprecated in a future version of Metropolis.
+    Please use a frame with [standout] instead.
+  }
+  \begin{frame}[standout]{#1}
+    \metropolis@plaintitleformat{#2}
+  \end{frame}
+}
+\newcommand{\mreducelistspacing}{\vspace{-\topsep}}
+\metropolis@setdefaults
+\ProcessPgfOptions{/metropolis}
+\endinput
+%%
+%% End of file `beamerthememetropolis.sty'.
diff --git a/presentation/paper-code.pdf b/presentation/paper-code.pdf
new file mode 100644
index 0000000..0deb974
--- /dev/null
+++ b/presentation/paper-code.pdf
diff --git a/presentation/presentation.tex b/presentation/presentation.tex
new file mode 100644
index 0000000..e1500e0
--- /dev/null
+++ b/presentation/presentation.tex
@@ -0,0 +1,1309 @@
+\documentclass[10pt,aspectratio=169,table]{beamer}
+
+\def\ymhgistrue{1}
+\def\ymhgextended{0}
+
+\usepackage{minted}
+\usepackage{tikz}
+\usepackage{pgfplots}
+\usepackage{booktabs}
+\usepackage{multicol}
+\usepackage{multirow}
+\usepackage{graphicx}
+
+% \usepackage{pgfpages}
+% \setbeameroption{show notes}
+% \setbeameroption{show notes on second screen=right}
+
+% Ideas for xilinx
+% - Explain XORed circuit
+% - Go over difficulties that were encountered when fuzzing tools
+% - Explain SMT in detail and how the equivalence check is done
+% -
+
+\usetheme{metropolis}
+
+\usetikzlibrary{calc,arrows.meta}
+\usetikzlibrary{decorations,patterns,arrows,decorations.pathmorphing}
+\usetikzlibrary{circuits.logic.US,calc}
+% \usetikzlibrary{external}
+% \usepgfplotslibrary{external}
+
+\pgfplotsset{every x tick label/.append style={font=\footnotesize, yshift=0.5ex}}
+
+% \definecolor{imperialbg}{HTML}{002147}
+
+% \setbeamercolor{palette primary}{bg=imperialbg,fg=black!2}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%%% Declarations                                                        %%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+\newsavebox{\codebox}
+\newsavebox{\codeboxbody}
+\newsavebox{\codeboxassign}
+\newsavebox{\codeboxinit}
+\newsavebox{\codeboxtoplevel}
+\newsavebox{\codeboxextra}
+\newsavebox{\codeboxsynthesised}
+\newsavebox{\codeboxreduction}
+\newsavebox{\background}
+\newsavebox{\codeboxresult}
+\newsavebox{\motivationa}
+\newsavebox{\motivationb}
+\newsavebox{\motivationc}
+\newsavebox{\motivationd}
+\newsavebox{\motivatione}
+\newsavebox{\motivationf}
+
+\definecolor{palette1}{HTML}{f5793a}
+\definecolor{palette2}{HTML}{a95aa1}
+\definecolor{palette3}{HTML}{85c0f9}
+\definecolor{palette4}{HTML}{0f2080}
+
+\definecolor{ribbon1}{HTML}{66c2a5}
+\definecolor{ribbon2}{HTML}{fc8d62}
+\definecolor{ribbon3}{HTML}{8da0cb}
+\definecolor{ribbon4}{HTML}{e78ac3}
+\definecolor{ribbon5}{HTML}{a6d854}
+\definecolor{ribbon6}{HTML}{ffd92f}
+
+\definecolor{diag1}{HTML}{ccebc5}
+\definecolor{diag2}{HTML}{b3cde3}
+\definecolor{diagerr}{HTML}{fbb4ae}
+\definecolor{rred}{HTML}{c0504d}
+
+\definecolor{distr1}{HTML}{1b9e77}
+\definecolor{distr2}{HTML}{d95f02}
+\definecolor{distr3}{HTML}{7570b3}
+\definecolor{distr4}{HTML}{e7298a}
+\definecolor{distr5}{HTML}{66a61e}
+\definecolor{distr6}{HTML}{e6ab02}
+\definecolor{distr7}{HTML}{a6761d}
+\definecolor{distr8}{HTML}{666666}
+
+\definecolor{pltblue}{HTML}{1f77b4}
+
+\colorlet{mintedhlcolor}{palette4!20}
+\colorlet{presentationbg}{black!2}
+
+\definecolor{verireduce}{HTML}{e66101}
+\definecolor{creduce}{HTML}{5e3c99}
+
+\pgfplotsset{
+  verismith missynth/.style={verireduce, draw=verireduce, mark=*},
+  creduce missynth/.style={creduce, draw=creduce, mark=triangle*},
+  verismith crash/.style={verireduce, draw=verireduce, mark=o},
+  creduce crash/.style={creduce, draw=creduce, mark=triangle}
+}
+
+\setminted{fontsize=\small,breaklines,highlightcolor=mintedhlcolor}
+
+\setlength{\fboxsep}{2pt}
+
+\newcommand{\tool}[2][]{%
+  \ifx\hfuzz#1\hfuzz #2%
+  \else #2 #1%
+  \fi}%
+\newcommand{\xilinx}[1][]{\tool[#1]{Xilinx}}%
+\newcommand{\intel}[1][]{\tool[#1]{Intel}}%
+\newcommand{\quartus}[1][]{\tool[#1]{Quartus Prime}}%
+\newcommand{\quartuslite}[1][]{\tool[#1]{Quartus Prime Lite}}%
+\newcommand{\yosys}[1][]{\tool[#1]{Yosys}}%
+\newcommand{\xst}[1][]{\tool[#1]{XST}}%
+\newcommand{\vivado}[1][]{\tool[#1]{Vivado}}%
+\newcommand{\verismith}[1][]{\tool[#1]{Verismith}}%
+\newcommand{\iverilog}[1][]{\tool[#1]{Icarus Verilog}}%
+
+\newcommand{\ymhgifextend}{\ifx\ymhgistrue\ymhgextended}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%%% TIKZ EXTERNALIZE                                                    %%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+% 
+% \makeatletter
+% \newcommand*{\overlaynumber}{\number\beamer@slideinframe}
+% \tikzset{
+%   beamer externalizing/.style={%
+%     execute at end picture={%
+%       \tikzifexternalizing{%
+%         \ifbeamer@anotherslide
+%         \pgfexternalstorecommand{\string\global\string\beamer@anotherslidetrue}%
+%         \fi
+%       }{}%
+%     }%
+%   },
+%   external/optimize=false
+% }
+% \let\orig@tikzsetnextfilename=\tikzsetnextfilename
+% \renewcommand\tikzsetnextfilename[1]{\orig@tikzsetnextfilename{#1-\overlaynumber}}
+% \makeatother
+% 
+% \tikzset{every picture/.style={beamer externalizing}}
+% 
+% \tikzexternalize
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%%% Row colours                                                         %%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+\makeatletter
+\def\rowcolor{\noalign{\ifnum0=`}\fi\bmr@rowcolor}
+\newcommand<>{\bmr@rowcolor}{%
+  \alt#1%
+  {\global\let\CT@do@color\CT@@do@color\@ifnextchar[\CT@rowa\CT@rowb}%
+  {\ifnum0=`{\fi}\@gooble@rowcolor}%
+}
+
+\newcommand{\@gooble@rowcolor}[2][]{\@gooble@rowcolor@}
+\newcommand{\@gooble@rowcolor@}[1][]{\@gooble@rowcolor@@}
+\newcommand{\@gooble@rowcolor@@}[1][]{\ignorespaces}
+\makeatother
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%%% Content                                                             %%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+\title{Finding and Understanding Bugs in FPGA Synthesis Tools}
+\subtitle{Verismith: FPGA Synthesis Tool Fuzzer}
+
+\author{\underline{Yann Herklotz}, John Wickerson}
+\institute{Imperial College London}
+
+\begin{document}
+
+\maketitle
+
+\note{Trust synthesis tool (Can we and should we?). They have a privileged position and we have to trust them. There is an effective bug finding method that can be used (fuzzing), which is effective at finding bugs.}
+
+\begin{frame}
+  \frametitle{Why find bugs?}
+  \large
+  \visible<1->{
+    \begin{itemize}
+    \item Designers have to trust the synthesis tool to do the right job
+    \item Bugs that generate wrong code can be hard to debug
+    \item Bugs that crash the tool can affect tool flows
+    \end{itemize}
+  }
+  \visible<2>{
+    \vspace{2em}
+
+    \begin{itemize}
+    \item Use \textbf{Verismith} to improve reliability of synthesis tools
+    \end{itemize}
+  }
+\end{frame}
+
+\note[itemize]{%
+\item We often assume correctness of Synthesis tools
+\item If our netlist does not work correctly, we assume there must be a mistake in the design.
+\item Find bugs in C programs, fuzzing was effective.
+}
+
+\begin{frame}
+  \frametitle{Verismith}
+  \begin{center}
+    \begin{tikzpicture}
+      \only<1>{\node[draw,fill=palette3!50,text width=2cm,align=center] (verilog) at (0,0)
+        {Verilog generation};}
+      \only<2->{\node[draw,fill=palette1!50,text width=2cm,align=center] (verilog) at (0,0)
+        {Verilog generation};}
+      \node[draw,fill=palette2!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+      (verdes) at (2.5,0) {\small Verilog design};
+      \node[draw,fill=palette2!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+      (vernet) at (6.5,0) {\small Verilog netlist};
+      \node[draw,fill=palette2!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+      (vertest) at (0,-2) {\footnotesize Reduced test case};
+      \node[draw,fill=palette3!50,minimum height=1cm] (synth) at (4.5,0) {Synthesis};
+      \node[draw,fill=palette3!50,minimum height=1cm,text width=2cm,align=center]
+      (equiv) at (6,-2) {Equivalence check};
+      \only<1>{\node[draw,fill=palette3!50,minimum height=1cm,text width=2cm,align=center]
+        (reduce) at (2.5,-2) {Reduction};}
+      \only<2->{\node[draw,fill=palette1!50,minimum height=1cm,text width=2cm,align=center]
+        (reduce) at (2.5,-2) {Reduction};}
+      \node at (4.3,-2.4) {{\color{rred} \small fail}};
+      \node at (3.8,-1.2) {{\color{rred} \small crash}};
+      \draw[very thick,->] (verilog) -- (verdes);
+      \draw[very thick,->] (verdes) -- (synth);
+      \draw[very thick,->] (synth) -- (vernet);
+      \draw[->] (verdes) -- ($ (equiv.north) + (-0.5,0) $);
+      \draw[very thick,->] (vernet) -- ($ (equiv.north) + (0.5,0) $);
+      \draw[rred,very thick,dashed,->] (synth.south) to [out=270,in=0] ($ (reduce.east) + (0,0.25) $);
+      \draw[->] (verdes) -- ($ (reduce.north) $);
+      \draw[rred,very thick,dashed,->] (equiv) to [out=180,in=0] ($ (reduce.east) + (0,-0.25) $);
+      \draw[very thick,->] (reduce) -- (vertest);
+    \end{tikzpicture}
+  \end{center}
+
+  \vspace{1em}
+  \large
+  \begin{columns}
+    \begin{column}{0.6\textwidth}
+      \textbf{Main contributions}
+      \begin{itemize}
+      \item Synthesis tool fuzzing framework
+      \item<2-> Behavioural and deterministic Verilog generation
+      \item<2-> Efficient Verilog Reduction
+      \end{itemize}
+    \end{column}
+    \begin{column}{0.4\textwidth}
+      \visible<3>{%
+        \textbf{Synthesis tools tested}
+        \begin{itemize}
+        \item[] Quartus \hspace{2em} Vivado
+        \item[] XST \hspace{4em} Yosys
+        \end{itemize}
+        \vspace{2.5em}
+      }
+    \end{column}
+  \end{columns}
+\end{frame}
+
+\begin{lrbox}{\background}
+  \begin{tikzpicture}
+    \node (chosen) at (0,1) {\textbf{Chosen}};
+    \node (subset) at (0,0.6) {\textbf{subset}};
+    \node (deterministic) at (3,1) {\textbf{Deterministic}};
+    \node (synthesisable) at (-3,1) {\textbf{Synthesisable}};
+    \node (semantic) at (0,3.5) {\textbf{Semantically correct}};
+    \node (syntactic) at (0,2) [draw,very thick,minimum width=12cm,minimum height=7.5cm] {};
+    \node (text) at (-3,5) {\textbf{Syntactically correct}};
+    \draw[very thick]
+    (0,0.8) ellipse (1cm and 0.7cm)
+    (-1.5,1) ellipse (3cm and 2cm)
+    (1.5,1) ellipse (3cm and 2cm)
+    (0,1.5) ellipse (5cm and 3cm)
+    ;
+  \end{tikzpicture}
+\end{lrbox}
+
+\begin{frame}
+  \frametitle{Background}
+  \large
+  \begin{columns}
+    \begin{column}{0.3\textwidth}
+      \textbf{Verilog 2005 standards}
+
+      \begin{itemize}
+      \item Verilog for simulation
+      \item Synthesisable Verilog
+      \end{itemize}
+
+    \end{column}%
+    \begin{column}{0.7\textwidth}
+      \scalebox{0.8}{\usebox{\background}}
+    \end{column}
+  \end{columns}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Background}
+  \large
+
+
+  \textbf{What is deterministic Verilog?}
+  \begin{itemize}
+  \item Only one interpretation of the design
+  \item Nondeterminism example:
+
+    Any undefined values can be 1 or 0
+  \end{itemize}
+
+  \vspace{2em}
+
+  \visible<2>{%
+    \textbf{What is a bug?}
+    \begin{itemize}
+    \item Synthesis tool crashes
+    \item Synthesis tool outputs the wrong netlist
+    \end{itemize}
+  }
+\end{frame}
+
+\note[itemize]{%
+\item Determinism in terms of the spec
+\item Code will only be generated that does not give any ambiguity about its value
+}
+
+\begin{frame}[fragile]
+  \frametitle{Motivating Bug: Yosys}
+  \large
+  \begin{lrbox}{\motivationa}
+    \begin{minipage}{.8\textwidth}
+\begin{minted}[fontsize=\large]{verilog}
+module top (output y, input [2:0] w);
+  assign y = 1'b1 >> (w * (3'b110));
+endmodule
+\end{minted}
+    \end{minipage}
+  \end{lrbox}
+  \begin{lrbox}{\motivationb}
+    \begin{minipage}{.8\textwidth}
+\begin{minted}[fontsize=\large]{verilog}
+module top (output y, input [2:0] w);
+  assign y = 1'b1 >> (3'b100 * (3'b110));
+endmodule
+\end{minted}
+    \end{minipage}
+  \end{lrbox}
+  \begin{lrbox}{\motivationc}
+    \begin{minipage}{.8\textwidth}
+\begin{minted}[escapeinside=||,fontsize=\large]{verilog}
+module top (output y, input [2:0] w);
+  assign y = 1'b1 >> |\colorbox{red!20}{6'b110000}|;
+endmodule
+\end{minted}
+    \end{minipage}
+  \end{lrbox}
+  \begin{lrbox}{\motivationd}
+    \begin{minipage}{.8\textwidth}
+\begin{minted}[escapeinside=||,fontsize=\large]{verilog}
+module top (output y, input [2:0] w);
+  assign y = |\colorbox{red!20}{1'b0}|;
+endmodule
+\end{minted}
+    \end{minipage}
+  \end{lrbox}
+  \begin{lrbox}{\motivatione}
+    \begin{minipage}{.8\textwidth}
+\begin{minted}[fontsize=\large]{verilog}
+module top (output y, input [2:0] w);
+  assign y = 1'b1 >> 3'b000;
+endmodule
+\end{minted}
+    \end{minipage}
+  \end{lrbox}
+  \begin{lrbox}{\motivationf}
+    \begin{minipage}{.8\textwidth}
+\begin{minted}[fontsize=\large]{verilog}
+module top (output y, input [2:0] w);
+  assign y = 1'b1;
+endmodule
+\end{minted}
+    \end{minipage}
+  \end{lrbox}
+  \begin{center}%
+    \only<1>{\usebox{\motivationa}}%
+    \only<2>{\usebox{\motivationb}}%
+    \only<3>{\usebox{\motivationc}}%
+    \only<4>{\usebox{\motivationd}}%
+    \only<5>{\usebox{\motivatione}}%
+    \only<6>{\usebox{\motivationf}}%
+  \end{center}
+
+  \vspace{3em}
+
+  \begin{itemize}
+  \item Bug in a development version of Yosys\footnotemark
+  \item Result not truncated properly, which results in an unwanted shift
+  \end{itemize}
+  \footnotetext{\url{https://github.com/YosysHQ/yosys/issues/1047}}
+\end{frame}
+
+\note[itemize]{%
+\item Bug found in dev version of Yosys between 0.8 and 0.9.
+\item Multiplication not truncated which results in shifts that should not occur.
+}
+
+\section{Example Verismith Run}
+
+\begin{frame}
+  \frametitle{Run Outline: Verilog Generation}
+  \begin{center}
+    \scalebox{1.3}{
+      \begin{tikzpicture}
+        \draw[palette1,fill=palette1,draw opacity=0,fill opacity=0.3,very thick] (0.9,0) ellipse (2.5cm and 1.2cm);
+        \node[draw,fill=palette1!50,text width=2cm,align=center] (verilog) at (0,0)
+        {Verilog generation};
+        \node[draw,fill=palette1!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (verdes) at (2.5,0) {\small Verilog design};
+        \node[draw,fill=palette2!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (vernet) at (6.5,0) {\small Verilog netlist};
+        \node[draw,fill=palette2!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (vertest) at (0,-2) {\footnotesize Reduced test case};
+        \node[draw,fill=palette3!50,minimum height=1cm] (synth) at (4.5,0) {Synthesis};
+        \node[draw,fill=palette3!50,minimum height=1cm,text width=2cm,align=center]
+        (equiv) at (6,-2) {Equivalence check};
+        \node[draw,fill=palette3!50,minimum height=1cm,text width=2cm,align=center]
+        (reduce) at (2.5,-2) {Reduction};
+        \node at (4.3,-2.4) {{\color{rred} \small fail}};
+        \node at (3.8,-1.2) {{\color{rred} \small crash}};
+        \draw[palette1,very thick,->] (verilog) -- (verdes);
+        \draw[very thick,->] (verdes) -- (synth);
+        \draw[very thick,->] (synth) -- (vernet);
+        \draw[->] (verdes) -- ($ (equiv.north) + (-0.5,0) $);
+        \draw[very thick,->] (vernet) -- ($ (equiv.north) + (0.5,0) $);
+        \draw[rred,very thick,dashed,->] (synth.south) to [out=270,in=0] ($ (reduce.east) + (0,0.25) $);
+        \draw[->] (verdes) -- ($ (reduce.north) $);
+        \draw[rred,very thick,dashed,->] (equiv) to [out=180,in=0] ($ (reduce.east) + (0,-0.25) $);
+        \draw[very thick,->] (reduce) -- (vertest);
+      \end{tikzpicture}
+    }
+  \end{center}
+\end{frame}
+
+\begin{lrbox}{\codebox}
+  \begin{minipage}{2\textwidth}
+    \vspace{4em}
+    \inputminted{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity.v}
+  \end{minipage}
+\end{lrbox}
+
+\begin{frame}[fragile]
+  \frametitle{Verilog generation}
+  \large
+  \begin{columns}
+    \begin{column}{0.4\textwidth}
+      \scalebox{0.2}{\usebox{\codebox}}
+      % \tikzset{external/export next=false}
+      \begin{tikzpicture}[overlay]
+        \begin{scope}[shift={(0,0.05)}]
+          \only<4->{%
+            \draw[fill=palette1,fill opacity=0.5,thick] (0,5.05) rectangle (5,6.65);
+            \draw[fill=palette1,fill opacity=0.5,thick] (0,0.8) rectangle (5,1.85);
+          }
+          \only<3->{%
+            \draw[fill=palette2,fill opacity=0.5,thick] (0,4.85) rectangle (5,5.05);
+            \draw[fill=palette2,fill opacity=0.5,thick] (0,0.7) rectangle (5,0.8);
+          }
+          \only<2->{%
+            \draw[fill=palette3,fill opacity=0.5,thick] (0,2.1) rectangle (5,4.85);
+            \draw[fill=palette3,fill opacity=0.5,thick] (0,0.05) rectangle (5,0.7);
+          }
+        \end{scope}
+      \end{tikzpicture}
+    \end{column}%
+    \begin{column}{0.6\textwidth}
+      Example of generated Verilog by Verismith
+      \begin{itemize}
+      \item Bug of uninitialised variable in Yosys 0.8
+      \end{itemize}
+
+      \vspace{2em}
+
+      \begin{itemize}
+      \item<2-> Random module items in the body
+      \item<3-> Assignment of the internal state to the output
+      \item<4-> Definition of nets and initialisation of variables
+      \end{itemize}
+    \end{column}
+  \end{columns}
+\end{frame}
+
+\note[itemize]{%
+\item Bug found in Yosys 0.8.
+\item There are 3 main sections in the Verilog code: initialisation, assignment to output and random Verilog section.
+\item There can also be multiple modules in the Verilog code.
+}
+
+\begin{lrbox}{\codeboxbody}%
+  \begin{minipage}{0.9\textwidth}%
+    \vspace{2em}%
+    \inputminted[firstline=23,lastline=42]{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity.v}
+  \end{minipage}%
+\end{lrbox}%
+
+{
+  \setbeamercolor{frametitle}{%
+    fg=black!90,
+    bg=palette3!80%
+  }
+  \begin{frame}
+    \frametitle{Generation of the body}
+    \large
+    \begin{columns}
+      \begin{column}{0.6\textwidth}
+        \scalebox{0.6}{\usebox{\codeboxbody}}
+      \end{column}%
+      \begin{column}{0.4\textwidth}
+        \only<1>{%
+          Generate Verilog node-by-node to:
+
+          \begin{itemize}
+          \item Ensure determinism
+          \item Generate behavioural constructs
+          \item Avoid logic loops
+          \end{itemize}
+        }%
+        \only<2>{%
+          Unsupported constructs:
+          \begin{itemize}
+          \item function definitions
+          \item alternate ranges (\texttt{+:}, \texttt{-:})
+          \end{itemize}
+        }
+      \end{column}
+    \end{columns}
+  \end{frame}
+}
+
+{
+  \setbeamercolor{frametitle}{%
+    fg=black!90,
+    bg=palette2!80%
+  }
+  \begin{frame}
+    \frametitle{Internal State Assignment}
+    \inputminted[firstline=21,lastline=22]{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity.v}
+    \vspace{2em}
+    Need to assign all the internal state to the output \texttt{y}.
+
+    \begin{itemize}
+    \item As all the wires and variables are assigned a value, this concatenation can never be undefined.
+    \item Any changes in the internal state are reflected in \texttt{y}.
+    \end{itemize}
+  \end{frame}
+}
+
+{
+  \setbeamercolor{frametitle}{%
+    fg=black!90,
+    bg=palette1!80%
+  }
+  \begin{frame}
+    \frametitle{Initialisation}
+    \large
+    \only<2>{
+      \setminted{highlightlines={3-8}}
+    }
+    \only<3>{
+      \setminted{highlightlines={9-12,18-20}}
+    }
+    \only<4>{
+      \setminted{highlightlines={13-17}}
+    }
+    \begin{lrbox}{\codeboxinit}
+      \begin{minipage}{0.6\textwidth}
+        \vspace{2em}
+        \inputminted[firstline=3,lastline=20]{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity.v}
+      \end{minipage}
+    \end{lrbox}
+    \begin{columns}
+      \begin{column}{0.45\textwidth}
+        \scalebox{0.8}{\usebox{\codeboxinit}}
+      \end{column}
+      \begin{column}{0.55\textwidth}
+        \begin{itemize}
+        \item<2-> Define the inputs and outputs of the module with random sizes.
+        \item<3-> Define nets that get assigned in the module.
+        \item<4-> Define and initialise variables to 0.
+        \end{itemize}
+      \end{column}
+    \end{columns}
+  \end{frame}
+
+  \note[itemize]{%
+  \item The verilog has to be correct meaning we have to correctly initialise the inputs and outputs.
+  \item We also declare the wires with random sizes.
+  }
+}
+
+\begin{frame}
+  \frametitle{Run Outline: Synthesis}
+  \begin{center}
+    \scalebox{1.3}{
+      \begin{tikzpicture}
+        \draw[palette1,fill=palette1,draw opacity=0,fill opacity=0.3,very thick] (4.5,0) ellipse (3cm and 1.2cm);
+        \node[draw,fill=palette3!50,text width=2cm,align=center] (verilog) at (0,0)
+        {Verilog generation};
+        \node[draw,fill=palette1!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (verdes) at (2.5,0) {\small Verilog design};
+        \node[draw,fill=palette1!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (vernet) at (6.5,0) {\small Verilog netlist};
+        \node[draw,fill=palette2!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (vertest) at (0,-2) {\footnotesize Reduced test case};
+        \node[draw,fill=palette1!50,minimum height=1cm] (synth) at (4.5,0) {Synthesis};
+        \node[draw,fill=palette3!50,minimum height=1cm,text width=2cm,align=center]
+        (equiv) at (6,-2) {Equivalence check};
+        \node[draw,fill=palette3!50,minimum height=1cm,text width=2cm,align=center]
+        (reduce) at (2.5,-2) {Reduction};
+        \node at (4.3,-2.4) {{\color{rred} \small fail}};
+        \node at (3.8,-1.2) {{\color{rred} \small crash}};
+        \draw[very thick,->] (verilog) -- (verdes);
+        \draw[palette1,very thick,->] (verdes) -- (synth);
+        \draw[palette1,very thick,->] (synth) -- (vernet);
+        \draw[->] (verdes) -- ($ (equiv.north) + (-0.5,0) $);
+        \draw[very thick,->] (vernet) -- ($ (equiv.north) + (0.5,0) $);
+        \draw[rred,very thick,dashed,->] (synth.south) to [out=270,in=0] ($ (reduce.east) + (0,0.25) $);
+        \draw[->] (verdes) -- ($ (reduce.north) $);
+        \draw[rred,very thick,dashed,->] (equiv) to [out=180,in=0] ($ (reduce.east) + (0,-0.25) $);
+        \draw[very thick,->] (reduce) -- (vertest);
+      \end{tikzpicture}
+    }
+  \end{center}
+\end{frame}
+
+\begin{lrbox}{\codeboxsynthesised}
+  \begin{minipage}{\textwidth}
+    \vspace{3em}
+    \inputminted[firstline=800,lastline=820]{verilog}{ExampleRun/output2/fuzz_1/yosys/syn_yosys.v}
+  \end{minipage}
+\end{lrbox}
+
+\begin{frame}
+  \frametitle{Yosys Synthesis}
+  \large
+  \begin{columns}
+    \begin{column}{0.65\textwidth}
+      \scalebox{0.6}{\usebox{\codeboxbody}}
+    \end{column}
+    \begin{column}{0.35\textwidth}
+      \begin{center}
+        \scalebox{0.6}{\usebox{\codeboxsynthesised}}
+      \end{center}
+    \end{column}
+  \end{columns}
+  \scalebox{0.7}{
+    % \tikzset{external/export next=false}
+    \begin{tikzpicture}[overlay]
+      \begin{scope}[shift={(10,4.5)}]
+        \draw[draw,rounded corners,very thick] (0,0) -- (2,0) -- (3,0.5) -- (2,1) -- (0,1) -- (0.5,0.5) -- cycle;
+        \node at (1.5,0.5) {Synthesis};
+      \end{scope}
+    \end{tikzpicture}
+  }
+\end{frame}
+
+\begin{frame}
+  \frametitle{Run Outline: Equivalence Check}
+  \begin{center}
+    \scalebox{1.3}{
+      \begin{tikzpicture}
+        \draw[palette1,fill=palette1,draw opacity=0,fill opacity=0.3,very thick] (6,-2) ellipse (1.5cm and 1cm);
+        \node[draw,fill=palette3!50,text width=2cm,align=center] (verilog) at (0,0)
+        {Verilog generation};
+        \node[draw,fill=palette1!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (verdes) at (2.5,0) {\small Verilog design};
+        \node[draw,fill=palette1!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (vernet) at (6.5,0) {\small Verilog netlist};
+        \node[draw,fill=palette2!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (vertest) at (0,-2) {\footnotesize Reduced test case};
+        \node[draw,fill=palette3!50,minimum height=1cm] (synth) at (4.5,0) {Synthesis};
+        \node[draw,fill=palette1!50,minimum height=1cm,text width=2cm,align=center]
+        (equiv) at (6,-2) {Equivalence check};
+        \node[draw,fill=palette3!50,minimum height=1cm,text width=2cm,align=center]
+        (reduce) at (2.5,-2) {Reduction};
+        \node at (4.3,-2.4) {{\color{rred} \small fail}};
+        \node at (3.8,-1.2) {{\color{rred} \small crash}};
+        \draw[very thick,->] (verilog) -- (verdes);
+        \draw[very thick,->] (verdes) -- (synth);
+        \draw[very thick,->] (synth) -- (vernet);
+        \draw[palette1,->] (verdes) -- ($ (equiv.north) + (-0.5,0) $);
+        \draw[palette1,very thick,->] (vernet) -- ($ (equiv.north) + (0.5,0) $);
+        \draw[rred,very thick,dashed,->] (synth.south) to [out=270,in=0] ($ (reduce.east) + (0,0.25) $);
+        \draw[->] (verdes) -- ($ (reduce.north) $);
+        \draw[rred,very thick,dashed,->] (equiv) to [out=180,in=0] ($ (reduce.east) + (0,-0.25) $);
+        \draw[very thick,->] (reduce) -- (vertest);
+      \end{tikzpicture}
+    }
+  \end{center}
+\end{frame}
+
+\ymhgifextend%
+\begin{frame}
+  \frametitle{Equivalence check: What is an SMT solver?}
+  \large
+
+\end{frame}
+
+\begin{frame}
+  \frametitle{Equivalence check: What is ABC?}
+  \large
+\end{frame}
+\fi
+
+\begin{frame}
+  \frametitle{Equivalence check}
+  \large
+  \begin{lrbox}{\codeboxtoplevel}
+    \begin{minipage}{0.8\textwidth}
+      \vspace{2em}
+      \only<1>{\inputminted{verilog}{ExampleRun/output2/fuzz_1/equiv_identity_yosys/top.v}}
+      \only<2>{\inputminted[highlightlines={2}]{verilog}{ExampleRun/output2/fuzz_1/equiv_identity_yosys/top.v}}
+      \only<3>{\inputminted[highlightlines={3}]{verilog}{ExampleRun/output2/fuzz_1/equiv_identity_yosys/top.v}}
+      \only<4>{\inputminted[highlightlines={6}]{verilog}{ExampleRun/output2/fuzz_1/equiv_identity_yosys/top.v}}
+    \end{minipage}
+  \end{lrbox}
+  \begin{columns}
+    \begin{column}{0.6\textwidth}
+      \begin{tikzpicture}[circuit logic US]
+        \node[xor gate,scale=2] (comp) at (4.7,-0.5) {};
+        \node[or gate] (comb) at (6.5,-0.5) {};
+        
+        \draw (0,0) rectangle (3,2);
+        \node at (1.5,1) {Design};
+        \foreach \i in {0,...,3} {
+          \node at (0.4,0.8+0.3*\i) {\tiny wire\i};}
+        \draw (0,0.2) -- (0.1,0.3) -- (0,0.4);
+        \node at (2.8,0.3) {\tiny y};
+
+        \draw (0,-3) rectangle (3,-1);
+        \node at (1.5,-2) {Netlist};
+        \foreach \i in {0,...,3} {
+          \node at (0.4,0.8+0.3*\i-3) {\tiny wire\i};}
+        \draw (0,0.2-3) -- (0.1,0.3-3) -- (0,0.4-3);
+        \node at (2.8,-1.3) {\tiny y};
+
+        \draw[very thick] (3,-1.3) -- (3.5,-1.3) |- (comp.input 2);
+        \draw (3.2,-1.5) -- (3.3,-1.1);
+        \node at (3.25,-0.9) {\footnotesize N};
+        \draw[very thick] (3,0.3) -- (3.5,0.3) |- (comp.input 1);
+        \draw (3.2,0.1) -- (3.3,0.5);
+        \node at (3.25,0.7) {\footnotesize N};
+        \draw[very thick] (comp.output) -- (comb.west);
+        \draw (comb.output) -- ($(comb.output) + (0.2,0)$);
+        \draw ($(comp.output) + (0.3,0.2)$) -- ($(comp.output) + (0.2,-0.2)$);
+        \node at ($(comp.output) + (0.25,0.4)$) {\footnotesize N};
+
+        \foreach \i in {0,...,3} {
+          \draw[very thick] (-1,-1+\i*0.3) -| (-0.5+0.1*\i,-1+\i*0.3) |- (0,0.8+0.3*\i);
+          \draw[very thick] (-0.5+0.1*\i,-1+\i*0.3) |- (0,0.8+0.3*\i-3);
+          \draw (-0.9,-1+\i*0.3-0.2) -- (-0.8,-1+\i*0.3+0.2);
+          \node at (-1.5,-1+\i*0.3) {\tiny wire\i};}
+
+        \draw (-1,-1.3) -| (-0.6,-1.3) |- (0,0.3);
+        \draw (-0.6,-1.3) |- (0,0.3-3);
+        \node at (-1.4,-1.3) {\tiny clk};
+      \end{tikzpicture}
+    \end{column}%
+    \begin{column}{0.4\textwidth}
+      Equivalence check done using an SMT solver (Z3) through Yosys
+      \begin{itemize}
+      \item<2-> Instantiate generated design with output \texttt{y\_1}
+      \item<3-> Instantiate synthesised netlist with output \texttt{y\_2}
+      \item<4-> Should be equal at every clock edge
+      \end{itemize}
+    \end{column}
+  \end{columns}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Run Outline: Reduction}
+  \begin{center}
+    \scalebox{1.3}{
+      \begin{tikzpicture}
+        \draw[palette1,fill=palette1,draw opacity=0,fill opacity=0.3,very thick] (1.5,-2) ellipse (2.7cm and 1.2cm);
+        \node[draw,fill=palette3!50,text width=2cm,align=center] (verilog) at (0,0)
+        {Verilog generation};
+        \node[draw,fill=palette1!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (verdes) at (2.5,0) {\small Verilog design};
+        \node[draw,fill=palette2!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (vernet) at (6.5,0) {\small Verilog netlist};
+        \node[draw,fill=palette1!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (vertest) at (0,-2) {\footnotesize Reduced test case};
+        \node[draw,fill=palette3!50,minimum height=1cm] (synth) at (4.5,0) {Synthesis};
+        \node[draw,fill=palette3!50,minimum height=1cm,text width=2cm,align=center]
+        (equiv) at (6,-2) {Equivalence check};
+        \node[draw,fill=palette1!50,minimum height=1cm,text width=2cm,align=center]
+        (reduce) at (2.5,-2) {Reduction};
+        \node at (4.3,-2.4) {{\color{rred} \small fail}};
+        \node at (3.8,-1.2) {{\color{rred} \small crash}};
+        \draw[very thick,->] (verilog) -- (verdes);
+        \draw[very thick,->] (verdes) -- (synth);
+        \draw[very thick,->] (synth) -- (vernet);
+        \draw[->] (verdes) -- ($ (equiv.north) + (-0.5,0) $);
+        \draw[very thick,->] (vernet) -- ($ (equiv.north) + (0.5,0) $);
+        \draw[rred,very thick,dashed,->] (synth.south) to [out=270,in=0] ($ (reduce.east) + (0,0.25) $);
+        \draw[palette1,->] (verdes) -- ($ (reduce.north) $);
+        \draw[rred,very thick,dashed,->] (equiv) to [out=180,in=0] ($ (reduce.east) + (0,-0.25) $);
+        \draw[palette1,very thick,->] (reduce) -- (vertest);
+      \end{tikzpicture}
+    }
+  \end{center}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Reduction}
+  \large
+  \begin{lrbox}{\codeboxreduction}
+    \begin{minipage}{1.2\textwidth}
+      \vspace{2em}
+      \only<1>{\inputminted{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity.v}}
+      \only<2>{\inputminted[escapeinside=¬¬,highlightlines={20,46,56-77},highlightcolor=red!30]{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_colour.v}}
+      \only<3>{\inputminted{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_red1.v}}
+      \only<4>{\inputminted[escapeinside=¬¬,highlightlines={9-12,45-51},highlightcolor=red!30]{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_red1_colour.v}}
+      % \only<5>{\inputminted{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_red2.v}}
+      % \only<6>{\inputminted[escapeinside=¬¬,highlightlines={9-12,17-36},highlightcolor=green!30]{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_red2_colour.v}}
+      % \only<7>{\inputminted[escapeinside=¬¬,highlightlines={14-15,37-39},highlightcolor=red!30]{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_red2_colour2.v}}
+      % \only<8>{\inputminted{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_red3.v}}
+      % \only<9>{\inputminted{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_red4.v}}
+      % \only<10>{\inputminted{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_red5.v}}
+      \only<5->{\inputminted{verilog}{ExampleRun/output2/fuzz_1/reduce_identity_yosys.v}}
+    \end{minipage}
+  \end{lrbox}
+  \begin{lrbox}{\codeboxresult}
+    \begin{minipage}{0.55\textwidth}
+      \vspace{3em}
+      \only<6>{\inputminted[highlightcolor=red!30,highlightlines={6}]{verilog}{ExampleRun/output2/fuzz_1/actual_wrong.v}}
+      \only<7>{\inputminted{verilog}{ExampleRun/output2/fuzz_1/actual_correct.v}}
+    \end{minipage}
+  \end{lrbox}
+  \only<1-5>{
+    \begin{columns}
+      \begin{column}{0.35\textwidth}
+        \only<1-2>{\scalebox{0.2}{\usebox{\codeboxreduction}}}
+        \only<3-4>{\scalebox{0.3}{\usebox{\codeboxreduction}}}
+        \only<5>{\scalebox{0.8}{\usebox{\codeboxreduction}}}
+        % \only<9-10>{\scalebox{0.4}{\usebox{\codeboxreduction}}}
+      \end{column}%
+      \begin{column}{0.65\textwidth}
+        \only<1-2>{%
+          \begin{itemize}
+          \item Verilog has to be reduced to a minimal representation to identify the bug.
+          \item Perform binary search on \textbf{syntax tree}.
+          \item Traditional methods perform search on source code.
+          \end{itemize}%
+        }%
+        \only<3-4>{%
+          Search is performed on different levels of granularity:
+          \begin{itemize}
+          \item Modules
+          \item Module items
+          \item Statements inside always blocks
+          \item Expressions
+          \end{itemize}
+        }%
+        \only<5>{%
+          \hspace{5em} We then get a minimal testcase
+        }
+      \end{column}
+    \end{columns}
+  }
+  \only<6->{
+    \begin{columns}
+      \begin{column}{0.5\textwidth}
+        \begin{center}
+          \textbf{\Large Input design}
+        \end{center}
+      \end{column}
+      \begin{column}{0.5\textwidth}
+        \begin{center}
+          \textbf{\Large Yosys netlist}
+        \end{center}
+      \end{column}
+    \end{columns}
+    \begin{columns}
+      \begin{column}{0.5\textwidth}
+        \begin{center}
+          \scalebox{0.8}{\usebox{\codeboxreduction}}
+        \end{center}
+      \end{column}
+      \begin{column}{0.5\textwidth}
+        \begin{center}
+          \scalebox{0.8}{\usebox{\codeboxresult}}
+        \end{center}
+      \end{column}
+    \end{columns}
+  }
+\end{frame}
+
+\section{Experiments and Results}
+
+\begin{frame}
+  \frametitle{Bugs found}
+  \large
+  \scalebox{0.7}{
+    \rowcolors{1}{}{lightgray!20}
+    \begin{tabular}{lrp{5mm}rrrr}
+      \toprule
+      \textbf{Tool} & \multicolumn{1}{p{2cm}}{\centering \textbf{Total test cases}} & \multicolumn{3}{r}{\textbf{Failing test cases}} & \multicolumn{1}{p{3cm}}{\centering \textbf{Distinct failing test cases}} & \multicolumn{1}{p{2cm}}{\centering \textbf{Bug reports}} \\
+      \midrule
+      \rowcolor<4>{palette1!30} \yosys{ 0.8}                                            & 26400 & & 7164 & (27.1\%) & $\ge 1$ & 0 \\
+      \rowcolor<5>{palette1!30} \yosys{ 3333e00}                                        & 51000 & & 7224 & (14.2\%) & $\ge 4$ & 3 \\
+      \rowcolor<5>{palette2!30} \yosys{ 70d0f38} (crash)                                        & 11 & & 1 & (9.09\%) & 1 & 1 \\
+      \rowcolor<4>{palette1!30} \yosys{ 0.9}                                            & 26400 & & 611  & (2.31\%) & $\ge 1$ & 1 \\
+      \rowcolor<3>{palette1!30} \vivado{ 2018.2}                                          & 47992 & & 1134 & (2.36\%) & $\ge 5$ & 3 \\
+      \rowcolor<3>{palette2!30} \vivado{ 2018.2} (crash)                                & 47992 & & 566  & (1.18\%) & 5       & 2 \\
+      \rowcolor<3>{palette1!30} \xst{ 14.7}                                             & 47992 & & 539  & (1.12\%) & $\ge 2$ & 0 \\
+      \rowcolor<2>{palette1!30} \quartus{ 19.2}                                         & 80300 & & 0    & (0\%)    & 0       & 0 \\
+      \rowcolor<2>{palette1!30} \quartuslite{ 19.1}                                    & 43    & & 17   & (39.5\%) & 1       & 0 \\
+      \rowcolor<2>{palette1!30} \quartuslite{ 19.1} (No \texttt{\$signed})             & 137   & & 0    & (0\%)    & 0       & 0 \\
+      \midrule
+      \rowcolor<6>{palette1!30} \iverilog{ 10.3}                                        & 26400 & & 616  & (2.33\%) & $\ge 1$  & 1 \\
+      \bottomrule
+    \end{tabular}
+  }
+
+  \vspace{1em}
+
+  \only<1>{%
+    \begin{itemize}
+    \item Summary of all the tests run over 18000 CPU hours
+    \end{itemize}
+    \vspace{1.5em}
+  }
+  \only<2>{%
+    \begin{itemize}
+    \item Quartus Prime Light failing because of the handling of \texttt{\$signed}
+    \item No crashes or failures found in Quartus Prime
+    \end{itemize}
+  }
+  \only<3>{%
+    \begin{itemize}
+    \item Vivado was the only stable tool that crashed
+    \end{itemize}
+    \vspace{1.5em}
+  }
+  \only<4>{%
+    \begin{itemize}
+    \item Yosys improved quite a lot between versions
+    \item Yosys 0.9 contains all the bug fixes that were submitted
+    \end{itemize}
+  }
+  \only<5>{%
+    \begin{itemize}
+    \item Yosys development versions also tested to aid development
+    \end{itemize}
+    \vspace{1.5em}
+  }
+  \only<6>{%
+    \begin{itemize}
+    \item Truncation bug in Icarus Verilog found while checking SMT counter examples
+    \end{itemize}
+    \vspace{1.5em}
+  }
+\end{frame}
+
+\begin{frame}
+  \frametitle{Efficiency at different Verilog sizes}
+  \begin{columns}
+    \begin{column}{0.5\textwidth}
+      \begin{tikzpicture}
+        \begin{semilogxaxis}[width=\linewidth,
+          major x tick style=transparent,
+          xlabel=Lines of code in generated programs,
+          legend style={at={(0.5,-0.15)},anchor=north,legend columns=-1},
+          ylabel=Number of test cases,
+          legend pos=north east,
+          legend style={font=\scriptsize},
+          xmin=50,
+          xmax=8800,
+          ybar=-3.6pt,
+          bar width=3.6pt,
+          ymin=0
+          % nodes near coords,
+          % nodes near coords align={vertical}
+          ]
+          \addplot[style={distr1,fill=distr1,mark=none,fill opacity=0.5,draw opacity=0}] coordinates {
+            (50.0,36) (55.2273245010972,42) (61.0011474309897,113) (67.3786032822108,210) (74.422799757947,341) (82.2034422502463,458) (90.7975236052311,501) (100.290086000843,507) (110.77506247623,353) (122.356206440081,241) (135.148118355792,115) (149.27737976296,39) (164.88380585685,11) (182.121829020643,3) (201.162027001128,0) (222.192810849795,0) (245.422289332251,0) (271.080328255088,0) (299.420825088154,0) (330.724221390595,0) (365.300277902221,0) (403.491139760939,0) (445.674722177899,0) (492.268450073103,0) (543.733388676789,0) (600.578805970684,0) (663.36721211649,0) (732.71992573891,0) (809.323222144053,0) (893.935124312463,0) (987.392903866661,0) (1090.6213662385,0) (1204.64200202167,0) (1330.58309506604,0) (1469.69088733773,0) (1623.34191102612,0) (1793.05660992942,0) (1980.51438490818,0) (2187.5702122883,0) (2416.2729996596,0) (2668.88586070881,0) (2947.90850971511,0) (3256.10199731164,0) (3596.51603228401,0) (3972.51915976695,0) (4387.83209446551,0) (4846.56453874751,0) (5353.25584993839,0) (5912.91995923888,0) (6531.09498675799,0) (7213.89804362345,0) (7968.08576346046,0) (8801.12116222408,0)
+          };
+          \addplot[style={distr2,fill=distr2,mark=none,fill opacity=0.5,draw opacity=0}] coordinates {
+            (50.0,0) (55.2273245010972,0) (61.0011474309897,1) (67.3786032822108,2) (74.422799757947,1) (82.2034422502463,6) (90.7975236052311,12) (100.290086000843,29) (110.77506247623,52) (122.356206440081,99) (135.148118355792,128) (149.27737976296,191) (164.88380585685,219) (182.121829020643,323) (201.162027001128,355) (222.192810849795,294) (245.422289332251,209) (271.080328255088,137) (299.420825088154,71) (330.724221390595,28) (365.300277902221,14) (403.491139760939,2) (445.674722177899,1) (492.268450073103,0) (543.733388676789,0) (600.578805970684,0) (663.36721211649,0) (732.71992573891,0) (809.323222144053,0) (893.935124312463,0) (987.392903866661,0) (1090.6213662385,0) (1204.64200202167,0) (1330.58309506604,0) (1469.69088733773,0) (1623.34191102612,0) (1793.05660992942,0) (1980.51438490818,0) (2187.5702122883,0) (2416.2729996596,0) (2668.88586070881,0) (2947.90850971511,0) (3256.10199731164,0) (3596.51603228401,0) (3972.51915976695,0) (4387.83209446551,0) (4846.56453874751,0) (5353.25584993839,0) (5912.91995923888,0) (6531.09498675799,0) (7213.89804362345,0) (7968.08576346046,0) (8801.12116222408,0)
+          };
+          \addplot[style={distr3,fill=distr3,mark=none,fill opacity=0.5,draw opacity=0}] coordinates {
+            (50.0,0) (55.2273245010972,0) (61.0011474309897,0) (67.3786032822108,0) (74.422799757947,0) (82.2034422502463,0) (90.7975236052311,0) (100.290086000843,0) (110.77506247623,0) (122.356206440081,0) (135.148118355792,0) (149.27737976296,0) (164.88380585685,0) (182.121829020643,0) (201.162027001128,0) (222.192810849795,1) (245.422289332251,0) (271.080328255088,3) (299.420825088154,7) (330.724221390595,9) (365.300277902221,12) (403.491139760939,32) (445.674722177899,46) (492.268450073103,74) (543.733388676789,93) (600.578805970684,129) (663.36721211649,166) (732.71992573891,186) (809.323222144053,171) (893.935124312463,116) (987.392903866661,58) (1090.6213662385,43) (1204.64200202167,16) (1330.58309506604,2) (1469.69088733773,1) (1623.34191102612,0) (1793.05660992942,0) (1980.51438490818,0) (2187.5702122883,0) (2416.2729996596,0) (2668.88586070881,0) (2947.90850971511,0) (3256.10199731164,0) (3596.51603228401,0) (3972.51915976695,0) (4387.83209446551,0) (4846.56453874751,0) (5353.25584993839,0) (5912.91995923888,0) (6531.09498675799,0) (7213.89804362345,0) (7968.08576346046,0) (8801.12116222408,0)
+          };
+          \addplot[style={distr4,fill=distr4,mark=none,fill opacity=0.5,draw opacity=0}] coordinates {
+            (50.0,0) (55.2273245010972,0) (61.0011474309897,0) (67.3786032822108,0) (74.422799757947,0) (82.2034422502463,0) (90.7975236052311,0) (100.290086000843,0) (110.77506247623,0) (122.356206440081,0) (135.148118355792,0) (149.27737976296,0) (164.88380585685,0) (182.121829020643,0) (201.162027001128,0) (222.192810849795,0) (245.422289332251,0) (271.080328255088,0) (299.420825088154,0) (330.724221390595,0) (365.300277902221,0) (403.491139760939,0) (445.674722177899,0) (492.268450073103,2) (543.733388676789,2) (600.578805970684,6) (663.36721211649,12) (732.71992573891,14) (809.323222144053,30) (893.935124312463,56) (987.392903866661,65) (1090.6213662385,84) (1204.64200202167,103) (1330.58309506604,123) (1469.69088733773,109) (1623.34191102612,66) (1793.05660992942,45) (1980.51438490818,18) (2187.5702122883,10) (2416.2729996596,1) (2668.88586070881,0) (2947.90850971511,0) (3256.10199731164,0) (3596.51603228401,0) (3972.51915976695,0) (4387.83209446551,0) (4846.56453874751,0) (5353.25584993839,0) (5912.91995923888,0) (6531.09498675799,0) (7213.89804362345,0) (7968.08576346046,0) (8801.12116222408,0)
+          };
+          \addplot[style={distr5,fill=distr5,mark=none,fill opacity=0.5,draw opacity=0}] coordinates {
+            (50.0,0) (55.2273245010972,0) (61.0011474309897,0) (67.3786032822108,0) (74.422799757947,0) (82.2034422502463,0) (90.7975236052311,0) (100.290086000843,0) (110.77506247623,0) (122.356206440081,0) (135.148118355792,0) (149.27737976296,0) (164.88380585685,0) (182.121829020643,0) (201.162027001128,0) (222.192810849795,0) (245.422289332251,0) (271.080328255088,0) (299.420825088154,0) (330.724221390595,0) (365.300277902221,0) (403.491139760939,0) (445.674722177899,0) (492.268450073103,0) (543.733388676789,0) (600.578805970684,0) (663.36721211649,2) (732.71992573891,0) (809.323222144053,2) (893.935124312463,14) (987.392903866661,16) (1090.6213662385,29) (1204.64200202167,50) (1330.58309506604,76) (1469.69088733773,83) (1623.34191102612,99) (1793.05660992942,99) (1980.51438490818,81) (2187.5702122883,49) (2416.2729996596,35) (2668.88586070881,16) (2947.90850971511,3) (3256.10199731164,2) (3596.51603228401,1) (3972.51915976695,1) (4387.83209446551,0) (4846.56453874751,0) (5353.25584993839,0) (5912.91995923888,0) (6531.09498675799,0) (7213.89804362345,0) (7968.08576346046,0) (8801.12116222408,0)
+          };
+          \addplot[style={distr6,fill=distr6,mark=none,fill opacity=0.5,draw opacity=0}] coordinates {
+            (50.0,0) (55.2273245010972,0) (61.0011474309897,0) (67.3786032822108,0) (74.422799757947,0) (82.2034422502463,0) (90.7975236052311,0) (100.290086000843,0) (110.77506247623,0) (122.356206440081,0) (135.148118355792,0) (149.27737976296,0) (164.88380585685,0) (182.121829020643,0) (201.162027001128,0) (222.192810849795,0) (245.422289332251,0) (271.080328255088,0) (299.420825088154,0) (330.724221390595,0) (365.300277902221,0) (403.491139760939,0) (445.674722177899,0) (492.268450073103,0) (543.733388676789,0) (600.578805970684,0) (663.36721211649,0) (732.71992573891,0) (809.323222144053,0) (893.935124312463,0) (987.392903866661,0) (1090.6213662385,2) (1204.64200202167,2) (1330.58309506604,1) (1469.69088733773,2) (1623.34191102612,4) (1793.05660992942,15) (1980.51438490818,16) (2187.5702122883,28) (2416.2729996596,49) (2668.88586070881,58) (2947.90850971511,66) (3256.10199731164,50) (3596.51603228401,59) (3972.51915976695,37) (4387.83209446551,15) (4846.56453874751,7) (5353.25584993839,1) (5912.91995923888,0) (6531.09498675799,0) (7213.89804362345,0) (7968.08576346046,0) (8801.12116222408,0)
+          };
+          \addplot[style={distr7,fill=distr7,mark=none,fill opacity=0.5,draw opacity=0}] coordinates {
+            (50.0,0) (55.2273245010972,0) (61.0011474309897,0) (67.3786032822108,0) (74.422799757947,0) (82.2034422502463,0) (90.7975236052311,0) (100.290086000843,0) (110.77506247623,0) (122.356206440081,0) (135.148118355792,0) (149.27737976296,0) (164.88380585685,0) (182.121829020643,0) (201.162027001128,0) (222.192810849795,0) (245.422289332251,0) (271.080328255088,0) (299.420825088154,0) (330.724221390595,0) (365.300277902221,0) (403.491139760939,0) (445.674722177899,0) (492.268450073103,0) (543.733388676789,0) (600.578805970684,0) (663.36721211649,0) (732.71992573891,0) (809.323222144053,0) (893.935124312463,0) (987.392903866661,1) (1090.6213662385,0) (1204.64200202167,0) (1330.58309506604,0) (1469.69088733773,0) (1623.34191102612,4) (1793.05660992942,4) (1980.51438490818,7) (2187.5702122883,12) (2416.2729996596,23) (2668.88586070881,41) (2947.90850971511,36) (3256.10199731164,51) (3596.51603228401,65) (3972.51915976695,43) (4387.83209446551,37) (4846.56453874751,24) (5353.25584993839,10) (5912.91995923888,3) (6531.09498675799,0) (7213.89804362345,0) (7968.08576346046,0) (8801.12116222408,0)
+          };
+          \addplot[style={distr8,fill=distr8,mark=none,fill opacity=0.5,draw opacity=0}] coordinates {
+            (50.0,0) (55.2273245010972,0) (61.0011474309897,0) (67.3786032822108,0) (74.422799757947,0) (82.2034422502463,0) (90.7975236052311,0) (100.290086000843,0) (110.77506247623,0) (122.356206440081,0) (135.148118355792,0) (149.27737976296,0) (164.88380585685,0) (182.121829020643,0) (201.162027001128,0) (222.192810849795,0) (245.422289332251,0) (271.080328255088,0) (299.420825088154,0) (330.724221390595,0) (365.300277902221,0) (403.491139760939,0) (445.674722177899,0) (492.268450073103,0) (543.733388676789,0) (600.578805970684,0) (663.36721211649,0) (732.71992573891,0) (809.323222144053,0) (893.935124312463,0) (987.392903866661,0) (1090.6213662385,0) (1204.64200202167,0) (1330.58309506604,0) (1469.69088733773,0) (1623.34191102612,0) (1793.05660992942,1) (1980.51438490818,4) (2187.5702122883,0) (2416.2729996596,2) (2668.88586070881,5) (2947.90850971511,8) (3256.10199731164,16) (3596.51603228401,24) (3972.51915976695,24) (4387.83209446551,28) (4846.56453874751,32) (5353.25584993839,25) (5912.91995923888,24) (6531.09498675799,8) (7213.89804362345,2) (7968.08576346046,1) (8801.12116222408,0)
+          };
+          \node at (axis cs: 100,530) {\footnotesize 10};
+          \node at (axis cs: 200,380) {\footnotesize 15};
+          \node at (axis cs: 750,210) {\footnotesize 20};
+          \node at (axis cs:1300,150) {\footnotesize 21};
+          \node at (axis cs:2000,125) {\footnotesize 26};
+          \node at (axis cs:2800, 90) {\footnotesize 27};
+          \node at (axis cs:4300, 85) {\footnotesize 30};
+          \node at (axis cs:6000, 50) {\footnotesize 35};
+        \end{semilogxaxis}
+      \end{tikzpicture}
+    \end{column}
+    \begin{column}{0.5\textwidth}
+      \visible<2>{%
+        \begin{tikzpicture}
+          \begin{axis}[width=\linewidth,
+            major x tick style=transparent,
+            symbolic x coords={91,181,438,792,929,1700,2110,4230},
+            xlabel=Average lines of code in generated programs,
+            ylabel=Number of test cases,
+            clip=false,
+            legend pos=north east,
+            legend style={font=\scriptsize},
+            xtick=data,
+            every axis x label/.style={at={($(ticklabel cs:0.6) + (0,-0.02)$)},anchor=near ticklabel,},
+            ybar=0,
+            bar width=8pt,
+            ymin=0,
+            % nodes near coords,
+            % nodes near coords align={vertical}
+            ]
+            \fill[distr1!50] (axis cs:91,-15) circle (3pt);
+            \fill[distr2!50] (axis cs:181,-15) circle (3pt);
+            \fill[distr3!50] (axis cs:438,-15) circle (3pt);
+            \fill[distr4!50] (axis cs:792,-15) circle (3pt);
+            \fill[distr5!50] (axis cs:929,-15) circle (3pt);
+            \fill[distr6!50] (axis cs:1700,-15) circle (3pt);
+            \fill[distr7!50] (axis cs:2110,-15) circle (3pt);
+            \fill[distr8!50] (axis cs:4230,-15) circle (3pt);
+            \addplot[style={black,fill=black!70,mark=none}] coordinates {
+              (91,122) (181,87) (438,63) (792,56) (929,43)
+              (1700,14) (2110,10) (4230,7)
+            };
+            \addplot[style={red!50,fill=red!50,mark=none}] coordinates {
+              (91,0) (181,2) (438,4) (792,12) (929,10)
+              (1700,8) (2110,12) (4230,17)
+            };
+            \legend{Bugs found,Crashes found};
+          \end{axis}
+        \end{tikzpicture}}
+    \end{column}
+  \end{columns}
+
+  \vspace{1em}
+  \large
+  \begin{itemize}
+  \item Each experiment was run over 3 days with Yosys, Vivado and XST
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Bugs found in Vivado over different versions}
+  \large
+  \begin{columns}
+    \begin{column}{0.65\textwidth}
+      \begin{tikzpicture}
+        \foreach \i in {-1,...,5}
+        {
+          \draw (-1,0.767441860465*\i+0.37) -- (8,0.767441860465*\i+0.37);
+        }
+        \only<2->{
+          \fill[fill=ribbon1] (-0.5,4.2) -- (7,4.2) -- (7.5,3.6) -- (7,3) -- (-0.5,3) --
+          (-0.2,3.6) -- cycle;
+          \node at (1.1,3.6) {15};
+          \fill[fill=ribbon5] (-0.5,3) -- (4.6,3) to [out=0,in=180] (6.6,0.5) --
+          (7,0.5) -- (7.1,0.45) -- (7,0.4) -- (6.6,0.4) to [out=180,in=0] (4.6,2.9) --
+          (-0.5,2.9) -- (-0.4,2.95) -- cycle;
+          \fill[fill=ribbon3] (-0.5,2.9) -- (2.4,2.9) to [out=0,in=180] (6.6,0.4) --
+          (7,0.4) -- (7.3,0.2) -- (7,0) -- (6.6,0) to [out=180,in=0] (2.4,2.5) --
+          (-0.5,2.5) -- (-0.2,2.7) -- cycle;
+          \node at (1.1,2.7) {6};
+          \fill[fill=ribbon2] (-0.5,2.2) -- (2.4,2.2) to [out=0,in=180] (4.4,2.9) --
+          (4.6,2.9) to [out=0,in=180] (6.6,3) -- (7,3) -- (7.4,2.55) -- (7,2.1) --
+          (6.6,2.1) to [out=180,in=0] (4.6,2) -- (4.4,2) to [out=180,in=0] (2.4,1.3) --
+          (-0.5,1.3) -- (-0.2,1.75) -- cycle;
+          \node at (1.1,1.75) {11};
+          \fill[fill=ribbon6] (-0.5,1.3) -- (2.4,1.3) to [out=0,in=180] (4.4,2) -- (4.6,2) to
+          [out=0,in=180] (6.6,0) -- (7,0) -- (7.1,-0.05) -- (7,-0.1) -- (6.6,-0.1) to
+          [out=180,in=0] (4.6,1.9) -- (4.4,1.9) to [out=180,in=0] (2.4,1.2) --
+          (-0.5,1.2) -- (-0.5,1.25) -- cycle;
+          \fill[fill=ribbon4] (-0.5,1.2) -- (3,1.2) to [out=0,in=180] (6.6,2.1)
+          -- (7,2.1) -- (7.5,1.5) -- (7,0.9)
+          -- (6.6,0.9) to [out=180,in=0] (3,0) -- (-0.5,0) -- (-0.1,0.6) -- cycle;
+          \node at (1.1,0.6) {17};
+        }
+        \filldraw[fill] (-0.1,2.5) rectangle (0.3,4.2);
+        \filldraw[fill] (2.1,2.5) rectangle (2.5,4.2);
+        \filldraw[fill] (4.3,1.9) rectangle (4.7,4.2);
+        \filldraw[fill] (6.5,0.9) rectangle (6.9,4.2);
+        \node at (0.1,4.6) {2016.1};
+        \node at (2.3,4.6) {2016.2};
+        \node at (4.5,4.6) {2017.4};
+        \node at (6.7,4.6) {2018.2};
+        \node at (0.1,2.7) {\color{presentationbg}{22}};
+        \node at (2.3,2.7) {\color{presentationbg}{22}};
+        \node at (4.5,2.1) {\color{presentationbg}{28}};
+        \node at (6.7,1.1) {\color{presentationbg}{43}};
+        \node at (3.4,5.3) {Vivado version};
+      \end{tikzpicture}
+    \end{column}%
+    \begin{column}{0.35\textwidth}
+      \begin{itemize}
+      \item Total number of bugs increase with versions
+      \item This does not mean there are more bugs, just that they were more commonly found
+      \end{itemize}
+    \end{column}
+  \end{columns}
+\end{frame}
+
+\note{One can see from the arrows that there are at least 3 different bugs in Vivado 2018.2, however, we identified 5 different ones in total.}
+
+\ymhgifextend%
+\begin{frame}
+  \frametitle{Reduction efficiency}
+  \large
+  \begin{center}
+    \begin{tikzpicture}
+      \begin{loglogaxis}[
+        width=0.65\linewidth,
+        legend style={nodes={scale=0.7, transform shape}},
+        legend pos=south east,
+        xlabel=Final size of reduced test case (lines of code),
+        ylabel=Time taken for reduction (s),
+        xticklabel style={
+          /pgf/number format/fixed,
+          /pgf/number format/precision=2
+        },
+        scaled x ticks=false,
+        grid=major,
+        major grid style={line width=.2pt,draw=black!20},
+        legend columns=2,
+        legend cell align=left,
+        ymin=0.4
+        ]
+        \addplot[only marks, verismith missynth]
+        coordinates {
+          (8,24.228676396) (12,48.020800025) (9,239.19471845) (19,78.85903502) (11,73.373059156) (265,396.931663908) (9,28.596337771) (9,121.520180855) (56,392.16407163) (12,9.194543707) (443,1106.024588047) (9,88.786871352) (9,166.899571358) (120,142.222511227) (9,73.07548465) (9,71.661578111) (26,47.691798645) (87,153.32273806) (9,89.500623124)
+        };
+        \addplot[only marks, creduce missynth]
+        coordinates {
+          (23,546.138) (40,549.916) (63,2954.062) (66,2565.887) (65,4355.297) (59,1695.4) (32,2355.947) (60,5091.577) (64,1611.466) (15,89.294) (137,6825.607) (74,13896.513) (64,9126.388) (90,4550.126) (43,5553.653) (27,1096.045) (16,340.533) (68,2814.821) (85,10592.831)
+        };
+        \addplot[only marks, verismith crash]
+        coordinates {
+          (462,31.025951033) (405,32.882851417) (75,49.630976912) (49,4.096207305) (234,10.081659552) (191,23.921349163) (99,10.894472949) (115,16.908927877) (32,18.313146602) (12,1.4856776) (230,30.366253517)
+        };
+        \addplot[only marks, creduce crash]
+        coordinates {
+          (30,225.177) (69,289.044) (33,136.239) (33,194.167) (52,352.996) (60,313.808) (54,285.255) (63,221.02) (60,137.885) (34,223.37) (54,213.942)
+        };
+        \legend{\verismith{}: mis-synthesis,C-Reduce: mis-synthesis,\verismith{}: crash,C-Reduce: crash}
+      \end{loglogaxis}
+    \end{tikzpicture}
+  \end{center}
+\end{frame}
+\fi
+
+\begin{frame}
+  \frametitle{Summary}
+  \large
+  Verismith can find hard-to-find bugs in synthesis tools by:
+
+  \begin{itemize}
+  \item Generating behavioural and deterministic Verilog.
+  \item Reducing it to a minimal representation if it is not.
+  \end{itemize}
+
+  In total 11 unique bugs were found, reported and fixed by tool vendors.
+
+  \vspace{2em}
+
+  Future work could be by supporting:
+  \begin{itemize}
+  \item A larger subset of Verilog
+  \item Controlled nondeterminism
+  \end{itemize}
+\end{frame}
+
+{
+  \setbeamercolor{footnote}{%
+    fg=black!2,
+    bg=mDarkTeal%
+  }
+  \begin{frame}[standout]
+    \Large
+    Finding and Understanding Bugs in FPGA Synthesis Tools
+
+    \vspace{1.5em}
+
+    \begin{columns}
+      \begin{column}{0.35\textwidth}
+        \begin{center}
+          Verismith Github\footnotemark
+
+          \vspace{1em}
+
+          \scalebox{0.5}{\includegraphics{verismith-github.pdf}}
+        \end{center}
+      \end{column}
+      \begin{column}{0.35\textwidth}
+        \begin{center}
+          Link to paper\footnotemark
+
+          \vspace{1em}
+
+          \scalebox{0.5}{\includegraphics{paper-code.pdf}}
+        \end{center}
+      \end{column}
+    \end{columns}
+    \addtocounter{footnote}{-1}
+    \footnotetext{\url{https://github.com/ymherklotz/verismith}}
+    \stepcounter{footnote}\footnotetext{\url{https://yannherklotz.com/papers/fubfst_fpga2020.pdf}}
+  \end{frame}
+}
+
+\begin{frame}[fragile]
+  \frametitle{Motivating Bug 2: Vivado}
+  \begin{columns}
+    \begin{column}{0.5\textwidth}
+      \definecolor{minline1}{named}{presentationbg}
+      \definecolor{minline2}{named}{presentationbg}
+      \definecolor{minline3}{named}{presentationbg}
+      \setminted{highlightlines={}}
+      \only<2>{
+        \definecolor{minline2}{named}{mintedhlcolor}
+        \definecolor{minline3}{named}{mintedhlcolor}
+      }
+      \only<3>{\setminted{highlightlines={4-5}}}
+      \only<4>{\setminted{highlightlines={8,11}}}
+      \only<5>{
+        \setminted{highlightlines={9-10}}
+        \definecolor{minline1}{named}{mintedhlcolor}
+        \definecolor{minline3}{named}{mintedhlcolor}
+      }
+      \only<6>{
+        \definecolor{minline1}{named}{mintedhlcolor}
+        \definecolor{minline3}{named}{mintedhlcolor}
+      }
+\begin{minted}[escapeinside=||]{verilog}
+module top (output [1:0] y,
+            input clk,
+            input [1:0] |\colorbox{minline2}{w0}|);
+   reg [1:0] r0 = 2'b0;
+   reg [2:0] r1 = 3'b0;
+   assign y = r1;
+   always @(posedge clk) begin
+      r0 <= 1'b1;
+      if (r0)
+        |\colorbox{minline1}{r1}| <= r0 ? |\colorbox{minline1}{\colorbox{minline3}{w0}[0:0]}| : 1'b0;
+      else r1 <= 3'b1;
+   end
+endmodule
+\end{minted}
+    \end{column}%
+    \begin{column}{0.5\textwidth}
+      Bug found in Vivado 2019.1.\footnotemark
+      \begin{itemize}
+      \item<2-> Assume \texttt{w0 = 2'b10},
+      \item<3-> initialise \texttt{r0 = 2'b0},
+
+        \texttt{r1 = 3'b0},
+      \item<4-> first \texttt{clk} edge sets \texttt{r0 = 1'b1},
+
+        \texttt{r1 = 3'b1},
+      \item<5-> next \texttt{clk} edge enters the \texttt{if} statement,
+      \item<6-> sets \texttt{r1 = w0[0:0] = 3'b0}
+
+        Vivado returns \texttt{r1 = w0[0:0] = 3'b010}
+      \end{itemize}
+    \end{column}
+  \end{columns}
+  \footnotetext{\tiny\url{https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Bit-selection-synthesis-mismatch/td-p/982419}}
+\end{frame}
+
+\note[itemize]{%
+\item Assume that \texttt{w0 = 2'b10}.
+\item Everything else is initialised to \texttt{1'b0}.
+\item First edge sets \texttt{r0 = 2'b1}
+\item Therefore it should enter the if statement on the next iteration and assign \texttt{r1 = 3'b0} as that is the LSB of w0.
+\item However, \texttt{3'b010} is assigned instead which results in an output of \texttt{2'b10} instead of \texttt{2'b00}
+}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% ymhg/TeX-expand-shell-escape: t
+%%% End:
diff --git a/presentation/verismith-github.pdf b/presentation/verismith-github.pdf
new file mode 100644
index 0000000..9e96d56
--- /dev/null
+++ b/presentation/verismith-github.pdf