From f9ca386bda2fe89287b9bb65d3d28e0c150d8984 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 7 Oct 2021 13:43:16 +0100 Subject: Add initial files --- .../ExampleRun/output2/fuzz_1/actual_correct.v | 12 + .../ExampleRun/output2/fuzz_1/actual_wrong.v | 12 + .../output2/fuzz_1/equiv_identity_yosys/top.v | 8 + .../output2/fuzz_1/identity/syn_identity.v | 77 ++ .../output2/fuzz_1/identity/syn_identity_colour.v | 77 ++ .../output2/fuzz_1/identity/syn_identity_red1.v | 52 + .../fuzz_1/identity/syn_identity_red1_colour.v | 52 + .../output2/fuzz_1/identity/syn_identity_red2.v | 40 + .../fuzz_1/identity/syn_identity_red2_colour.v | 40 + .../fuzz_1/identity/syn_identity_red2_colour2.v | 40 + .../output2/fuzz_1/identity/syn_identity_red3.v | 35 + .../output2/fuzz_1/identity/syn_identity_red4.v | 27 + .../output2/fuzz_1/identity/syn_identity_red5.v | 15 + .../output2/fuzz_1/reduce_identity_yosys.v | 9 + .../ExampleRun/output2/fuzz_1/reduce_sim_yosys.v | 27 + .../ExampleRun/output2/fuzz_1/yosys/syn_yosys.v | 1441 ++++++++++++++++++++ presentation/Makefile | 4 + .../beamercolorthememetropolis-highcontrast.sty | 39 + presentation/beamercolorthememetropolis.sty | 138 ++ presentation/beamerfontthememetropolis.sty | 325 +++++ presentation/beamerinnerthememetropolis.sty | 297 ++++ presentation/beamerouterthememetropolis.sty | 137 ++ presentation/beamerthememetropolis.sty | 107 ++ presentation/paper-code.pdf | Bin 0 -> 2380 bytes presentation/presentation.tex | 1309 ++++++++++++++++++ presentation/verismith-github.pdf | Bin 0 -> 2380 bytes 26 files changed, 4320 insertions(+) create mode 100644 presentation/ExampleRun/output2/fuzz_1/actual_correct.v create mode 100644 presentation/ExampleRun/output2/fuzz_1/actual_wrong.v create mode 100644 presentation/ExampleRun/output2/fuzz_1/equiv_identity_yosys/top.v create mode 100644 presentation/ExampleRun/output2/fuzz_1/identity/syn_identity.v create mode 100644 presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_colour.v create mode 100644 presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red1.v create mode 100644 presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red1_colour.v create mode 100644 presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red2.v create mode 100644 presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red2_colour.v create mode 100644 presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red2_colour2.v create mode 100644 presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red3.v create mode 100644 presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red4.v create mode 100644 presentation/ExampleRun/output2/fuzz_1/identity/syn_identity_red5.v create mode 100644 presentation/ExampleRun/output2/fuzz_1/reduce_identity_yosys.v create mode 100644 presentation/ExampleRun/output2/fuzz_1/reduce_sim_yosys.v create mode 100644 presentation/ExampleRun/output2/fuzz_1/yosys/syn_yosys.v create mode 100644 presentation/Makefile create mode 100644 presentation/beamercolorthememetropolis-highcontrast.sty create mode 100644 presentation/beamercolorthememetropolis.sty create mode 100644 presentation/beamerfontthememetropolis.sty create mode 100644 presentation/beamerinnerthememetropolis.sty create mode 100644 presentation/beamerouterthememetropolis.sty create mode 100644 presentation/beamerthememetropolis.sty create mode 100644 presentation/paper-code.pdf create mode 100644 presentation/presentation.tex create mode 100644 presentation/verismith-github.pdf (limited to 'presentation') 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" $< +\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 +\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 Binary files /dev/null and b/presentation/paper-code.pdf differ 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 Binary files /dev/null and b/presentation/verismith-github.pdf differ -- cgit