verismith 0.4.0.1 → 0.5.0.0

raw patch · 24 files changed

+1757/−704 lines, 24 filesdep +mtlPVP ok

version bump matches the API change (PVP)

Dependencies added: mtl

API changes (from Hackage documentation)

Files

• README.md +12/−6
• data/cells_cyclone_v.v +474/−30
• scripts/reducer.sh +65/−0
• src/Verismith.hs +49/−267
• src/Verismith/Config.hs +19/−11
• src/Verismith/CounterEg.hs +112/−0
• src/Verismith/Fuzz.hs +224/−151
• src/Verismith/Generate.hs +32/−38
• src/Verismith/OptParser.hs +299/−0
• src/Verismith/Reduce.hs +65/−20
• src/Verismith/Report.hs +52/−36
• src/Verismith/Result.hs +10/−0
• src/Verismith/Tool.hs +4/−0
• src/Verismith/Tool/Icarus.hs +66/−43
• src/Verismith/Tool/Internal.hs +12/−3
• src/Verismith/Tool/Quartus.hs +12/−11
• src/Verismith/Tool/QuartusLight.hs +78/−0
• src/Verismith/Tool/Template.hs +66/−16
• src/Verismith/Tool/Yosys.hs +23/−19
• src/Verismith/Verilog/AST.hs +6/−0
• src/Verismith/Verilog/Mutate.hs +2/−2
• test/Parser.hs +9/−10
• test/Reduce.hs +31/−8
• verismith.cabal +35/−33

@@ -29,7 +29,7 @@  ## Reported bugs -9 bugs have been reported and confirmed to be bugs by the vendors, out of which 4 have been fixed.+9 bugs have been reported and confirmed to be bugs by the vendors, out of which 4 have been fixed. 1 bug has also been found in the Icarus Verilog simulator as a side effect of using it to verify equivalence check results.  ### Yosys @@ -44,11 +44,17 @@  | Type          | Issue                                                                                                                               | Confirmed | Fixed | |---------------|-------------------------------------------------------------------------------------------------------------------------------------|-----------|-------|-| Crash         | [Forum 981787](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Verilog-If-statement-nesting-crash/td-p/981787)                 | ✓         | 𐄂     |-| Crash         | [Forum 981136](https://forums.xilinx.com/t5/Synthesis/Vivado-2018-3-synthesis-crash/td-p/981136)                                    | ✓         | 𐄂     |-| Mis-synthesis | [Forum 981789](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Unsigned-bit-extension-in-if-statement/td-p/981789)             | ✓         | 𐄂     |-| Mis-synthesis | [Forum 982518](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Signed-with-shift-in-condition-synthesis-mistmatch/td-p/982518) | ✓         | 𐄂     |-| Mis-synthesis | [Forum 982419](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Bit-selection-synthesis-mismatch/td-p/982419)                   | ✓         | 𐄂     |+| Crash         | [Forum 981787](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Verilog-If-statement-nesting-crash/td-p/981787)                 | ✓         | ✗     |+| Crash         | [Forum 981136](https://forums.xilinx.com/t5/Synthesis/Vivado-2018-3-synthesis-crash/td-p/981136)                                    | ✓         | ✗     |+| Mis-synthesis | [Forum 981789](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Unsigned-bit-extension-in-if-statement/td-p/981789)             | ✓         | ✗     |+| Mis-synthesis | [Forum 982518](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Signed-with-shift-in-condition-synthesis-mistmatch/td-p/982518) | ✓         | ✗     |+| Mis-synthesis | [Forum 982419](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Bit-selection-synthesis-mismatch/td-p/982419)                   | ✓         | ✗     |++### Icarus Verilog++| Type           | Issue                                                           | Confirmed | Fixed |+|----------------|-----------------------------------------------------------------|-----------|-------|+| Mis-simulation | [Issue 283](https://github.com/steveicarus/iverilog/issues/283) | ✓         | ✓     |  ## Install the Fuzzer 

@@ -2,6 +2,46 @@  // ========================================================================================== +module dffeas (d, clk, ena, clrn, prn, aload, asdata, sclr, sload, devclrn, devpor, q );+   // GLOBAL PARAMETER DECLARATION+   parameter power_up = "DONT_CARE";+   parameter is_wysiwyg = "false";+   parameter dont_touch = "false";+++   parameter x_on_violation = "on";+   parameter lpm_type = "dffeas";++   input d;+   input clk;+   input ena;+   input clrn;+   input prn;+   input aload; +   input asdata;  +   input sclr; +   input sload; +   input devclrn; +   input devpor; ++   output reg q = 0;++   always @(posedge clk) begin+      if (ena == 1'b1) begin+         if (sclr == 1'b1)+           q <= 0;+         else if (aload == 1'b1)+           q <= asdata;+         else if (sload == 1'b1)+           q <= asdata;+         else+           q <= d;+      end+   end++endmodule++ module cyclonev_lcell_comb ( 	                        dataa, datab, datac, datad, datae, dataf, datag, cin, sharein, 	                        combout, sumout, cout, shareout@@ -155,6 +195,32 @@  endmodule +module cyclonev_clkena    (+                           inclk,+                           ena,+                           enaout,+                           outclk);++   // leda G_521_3_B off+   parameter    clock_type    =    "auto";+   parameter    ena_register_mode    =    "always enabled";+   parameter    lpm_type    =    "cyclonev_clkena";+   parameter    ena_register_power_up    =    "high";+   parameter    disable_mode    =    "low";+   parameter    test_syn    =    "high";+   // leda G_521_3_B on++   input    inclk;+   input    ena;+   output   enaout;+   output   outclk;++   assign outclk = ena ? inclk : 1'b0;+   assign enaout = ena;++endmodule //cyclonev_clkena++ // ==========================================================================================  module cyclonev_io_ibuf (i, ibar, dynamicterminationcontrol, o);@@ -196,42 +262,201 @@  endmodule -module dffeas (d, clk, ena, clrn, prn, aload, asdata, sclr, sload, devclrn, devpor, q );-   // GLOBAL PARAMETER DECLARATION-   parameter power_up = "DONT_CARE";-   parameter is_wysiwyg = "false";-   parameter dont_touch = "false";+module cyclone10lp_lcell_comb (+	                        dataa, datab, datac, datad, datae, dataf, datag, cin, sharein,+	                        combout, sumout, cout, shareout+                            ); +   input dataa, datab, datac, datad, datae, dataf, datag, cin, sharein;+   output reg combout = 0, sumout = 0, cout = 0, shareout = 0; -   parameter x_on_violation = "on";-   parameter lpm_type = "dffeas";+   parameter lut_mask = 64'hFFFFFFFFFFFFFFFF;+   parameter shared_arith = "off";+   parameter extended_lut = "off";+   parameter dont_touch = "off";+   parameter lpm_type = "cyclone10lp_lcell_comb"; -   input d;-   input clk;-   input ena;-   input clrn;-   input prn;-   input aload; -   input asdata;  -   input sclr; -   input sload; -   input devclrn; -   input devpor; +   localparam ishared_arith = shared_arith == "on";+   localparam iextended_lut = extended_lut == "on"; -   output reg q = 0;+   localparam [15:0] f0_mask = lut_mask[15:0];+   localparam [15:0] f1_mask = lut_mask[31:16];+   localparam [15:0] f2_mask = lut_mask[47:32];+   localparam [15:0] f3_mask = lut_mask[63:48]; -   always @(posedge clk or posedge aload) begin-      if (aload == 1'b1)-        q <= asdata;-      else if (sload == 1'b1)-        q <= asdata;-      else-        q <= d;-   end+   reg        f0_out, f1_out, f2_out, f3_out;+   reg        g0_out, g1_out;+   reg        f2_input3, f2_f;+   reg        adder_input2; +   // 4-input LUT function+   function lut4;+      input [15:0] mask;+      input        dataa;+      input        datab;+      input        datac;+      input        datad;+      begin+         lut4 = datad ? ( datac ? ( datab ? ( dataa ? mask[15] : mask[14])+                                    : ( dataa ? mask[13] : mask[12]))+                          : ( datab ? ( dataa ? mask[11] : mask[10])+                              : ( dataa ? mask[ 9] : mask[ 8])))+           : ( datac ? ( datab ? ( dataa ? mask[ 7] : mask[ 6])+                         : ( dataa ? mask[ 5] : mask[ 4]))+               : ( datab ? ( dataa ? mask[ 3] : mask[ 2])+                   : ( dataa ? mask[ 1] : mask[ 0])));+      end+   endfunction++   // 5-input LUT function+   function lut5;+      input [31:0] mask;+      input        dataa;+      input        datab;+      input        datac;+      input        datad;+      input        datae;+      reg          e0_lut;+      reg          e1_lut;+      reg [15:0]   e0_mask;+      reg [31:16]  e1_mask;+      begin+         e0_mask = mask[15:0];+         e1_mask = mask[31:16];+         e0_lut = lut4(e0_mask, dataa, datab, datac, datad);+         e1_lut = lut4(e1_mask, dataa, datab, datac, datad);+      end+   endfunction++   // 6-input LUT function+   function lut6;+      input [63:0] mask;+      input        dataa;+      input        datab;+      input        datac;+      input        datad;+      input        datae;+      input        dataf;+      reg          f0_lut;+      reg          f1_lut;+      reg [31:0]   f0_mask;+      reg [63:32]  f1_mask ;+      begin+         f0_mask = mask[31:0];+         f1_mask = mask[63:32];+         lut6 = mask[{dataf, datae, datad, datac, datab, dataa}];+      end+   endfunction++   always @(datag or dataf or datae or datad or datac or+            datab or dataa or cin or sharein)+     begin+        // check for extended LUT mode+        if (iextended_lut == 1)+          f2_input3 = datag;+        else+          f2_input3 = datac;++        f0_out = lut4(f0_mask, dataa, datab, datac, datad);+        f1_out = lut4(f1_mask, dataa, datab, f2_input3, datad);+        f2_out = lut4(f2_mask, dataa, datab, datac, datad);+        f3_out = lut4(f3_mask, dataa, datab, f2_input3, datad);++        // combout is the 6-input LUT+        if (iextended_lut == 1)+          begin+             if (datae == 1'b0)+               begin+                  g0_out = f0_out;+                  g1_out = f2_out;+               end+             else if (datae == 1'b1)+               begin+                  g0_out = f1_out;+                  g1_out = f3_out;+               end+             else+               begin+                  if (f0_out == f1_out)+                    g0_out = f0_out;+                  else+                    g0_out = 1'bX;++                  if (f2_out == f3_out)+                    g1_out = f2_out;+                  else+                    g1_out = 1'bX;+               end++             if (dataf == 1'b0)+               combout = g0_out;+             else if ((dataf == 1'b1) || (g0_out == g1_out))+               combout = g1_out;+             else+               combout = 1'bX;+          end+        else+          combout = lut6(lut_mask, dataa, datab, datac, datad, datae, dataf);++        // check for shareed arithmetic mode+        if (ishared_arith == 1)+          adder_input2 = sharein;+        else+          begin+             f2_f = lut4(f2_mask, dataa, datab, datac, dataf);+             adder_input2 = !f2_f;+          end++        // sumout & cout+        sumout = cin ^ f0_out ^ adder_input2;+        cout = (cin & f0_out) | (cin & adder_input2) | (f0_out & adder_input2);+        shareout = f2_out;+     end+ endmodule -module cyclonev_clkena    (+// ==========================================================================================++module cyclone10lp_io_ibuf (i, ibar, dynamicterminationcontrol, o);++   parameter differential_mode = 0;+   parameter bus_hold = 0;+   parameter simulate_z_as = 0;+   parameter lpm_type = 0;++   input i;+   input ibar;+   input dynamicterminationcontrol;+   output o;++   assign o = i;++endmodule++// ==========================================================================================++module cyclone10lp_io_obuf (i, oe, dynamicterminationcontrol, seriesterminationcontrol, parallelterminationcontrol, devoe, o, obar);++   parameter open_drain_output = 0;+   parameter bus_hold = 0;+   parameter shift_series_termination_control = 0;+   parameter sim_dynamic_termination_control_is_connected = 0;+   parameter lpm_type = 0;++   input i;+   input oe;+   input devoe;+   input dynamicterminationcontrol;+   input [15:0] seriesterminationcontrol;+   input [15:0] parallelterminationcontrol;+   output       o;+   output       obar;++   assign o = i, obar = ~i;++endmodule++module cyclone10lp_clkena    (                            inclk,                            ena,                            enaout,@@ -240,7 +465,7 @@    // leda G_521_3_B off    parameter    clock_type    =    "auto";    parameter    ena_register_mode    =    "always enabled";-   parameter    lpm_type    =    "cyclonev_clkena";+   parameter    lpm_type    =    "cyclone10lp_clkena";    parameter    ena_register_power_up    =    "high";    parameter    disable_mode    =    "low";    parameter    test_syn    =    "high";@@ -254,4 +479,223 @@    assign outclk = ena ? inclk : 1'b0;    assign enaout = ena; -endmodule //cyclonev_clkena+endmodule //cyclone10lp_clkena++module cyclone10gx_lcell_comb (+	                        dataa, datab, datac, datad, datae, dataf, datag, cin, sharein,+	                        combout, sumout, cout, shareout+                            );++   input dataa, datab, datac, datad, datae, dataf, datag, cin, sharein;+   output reg combout = 0, sumout = 0, cout = 0, shareout = 0;++   parameter lut_mask = 64'hFFFFFFFFFFFFFFFF;+   parameter shared_arith = "off";+   parameter extended_lut = "off";+   parameter dont_touch = "off";+   parameter lpm_type = "cyclone10gx_lcell_comb";++   localparam ishared_arith = shared_arith == "on";+   localparam iextended_lut = extended_lut == "on";++   localparam [15:0] f0_mask = lut_mask[15:0];+   localparam [15:0] f1_mask = lut_mask[31:16];+   localparam [15:0] f2_mask = lut_mask[47:32];+   localparam [15:0] f3_mask = lut_mask[63:48];++   reg        f0_out, f1_out, f2_out, f3_out;+   reg        g0_out, g1_out;+   reg        f2_input3, f2_f;+   reg        adder_input2;++   // 4-input LUT function+   function lut4;+      input [15:0] mask;+      input        dataa;+      input        datab;+      input        datac;+      input        datad;+      begin+         lut4 = datad ? ( datac ? ( datab ? ( dataa ? mask[15] : mask[14])+                                    : ( dataa ? mask[13] : mask[12]))+                          : ( datab ? ( dataa ? mask[11] : mask[10])+                              : ( dataa ? mask[ 9] : mask[ 8])))+           : ( datac ? ( datab ? ( dataa ? mask[ 7] : mask[ 6])+                         : ( dataa ? mask[ 5] : mask[ 4]))+               : ( datab ? ( dataa ? mask[ 3] : mask[ 2])+                   : ( dataa ? mask[ 1] : mask[ 0])));+      end+   endfunction++   // 5-input LUT function+   function lut5;+      input [31:0] mask;+      input        dataa;+      input        datab;+      input        datac;+      input        datad;+      input        datae;+      reg          e0_lut;+      reg          e1_lut;+      reg [15:0]   e0_mask;+      reg [31:16]  e1_mask;+      begin+         e0_mask = mask[15:0];+         e1_mask = mask[31:16];+         e0_lut = lut4(e0_mask, dataa, datab, datac, datad);+         e1_lut = lut4(e1_mask, dataa, datab, datac, datad);+      end+   endfunction++   // 6-input LUT function+   function lut6;+      input [63:0] mask;+      input        dataa;+      input        datab;+      input        datac;+      input        datad;+      input        datae;+      input        dataf;+      reg          f0_lut;+      reg          f1_lut;+      reg [31:0]   f0_mask;+      reg [63:32]  f1_mask ;+      begin+         f0_mask = mask[31:0];+         f1_mask = mask[63:32];+         lut6 = mask[{dataf, datae, datad, datac, datab, dataa}];+      end+   endfunction++   always @(datag or dataf or datae or datad or datac or+            datab or dataa or cin or sharein)+     begin+        // check for extended LUT mode+        if (iextended_lut == 1)+          f2_input3 = datag;+        else+          f2_input3 = datac;++        f0_out = lut4(f0_mask, dataa, datab, datac, datad);+        f1_out = lut4(f1_mask, dataa, datab, f2_input3, datad);+        f2_out = lut4(f2_mask, dataa, datab, datac, datad);+        f3_out = lut4(f3_mask, dataa, datab, f2_input3, datad);++        // combout is the 6-input LUT+        if (iextended_lut == 1)+          begin+             if (datae == 1'b0)+               begin+                  g0_out = f0_out;+                  g1_out = f2_out;+               end+             else if (datae == 1'b1)+               begin+                  g0_out = f1_out;+                  g1_out = f3_out;+               end+             else+               begin+                  if (f0_out == f1_out)+                    g0_out = f0_out;+                  else+                    g0_out = 1'bX;++                  if (f2_out == f3_out)+                    g1_out = f2_out;+                  else+                    g1_out = 1'bX;+               end++             if (dataf == 1'b0)+               combout = g0_out;+             else if ((dataf == 1'b1) || (g0_out == g1_out))+               combout = g1_out;+             else+               combout = 1'bX;+          end+        else+          combout = lut6(lut_mask, dataa, datab, datac, datad, datae, dataf);++        // check for shareed arithmetic mode+        if (ishared_arith == 1)+          adder_input2 = sharein;+        else+          begin+             f2_f = lut4(f2_mask, dataa, datab, datac, dataf);+             adder_input2 = !f2_f;+          end++        // sumout & cout+        sumout = cin ^ f0_out ^ adder_input2;+        cout = (cin & f0_out) | (cin & adder_input2) | (f0_out & adder_input2);+        shareout = f2_out;+     end++endmodule++// ==========================================================================================++module cyclone10gx_io_ibuf (i, ibar, dynamicterminationcontrol, o);++   parameter differential_mode = 0;+   parameter bus_hold = 0;+   parameter simulate_z_as = 0;+   parameter lpm_type = 0;++   input i;+   input ibar;+   input dynamicterminationcontrol;+   output o;++   assign o = i;++endmodule++// ==========================================================================================++module cyclone10gx_io_obuf (i, oe, dynamicterminationcontrol, seriesterminationcontrol, parallelterminationcontrol, devoe, o, obar);++   parameter open_drain_output = 0;+   parameter bus_hold = 0;+   parameter shift_series_termination_control = 0;+   parameter sim_dynamic_termination_control_is_connected = 0;+   parameter lpm_type = 0;++   input i;+   input oe;+   input devoe;+   input dynamicterminationcontrol;+   input [15:0] seriesterminationcontrol;+   input [15:0] parallelterminationcontrol;+   output       o;+   output       obar;++   assign o = i, obar = ~i;++endmodule++module cyclone10gx_clkena    (+                           inclk,+                           ena,+                           enaout,+                           outclk);++   // leda G_521_3_B off+   parameter    clock_type    =    "auto";+   parameter    ena_register_mode    =    "always enabled";+   parameter    lpm_type    =    "cyclone10gx_clkena";+   parameter    ena_register_power_up    =    "high";+   parameter    disable_mode    =    "low";+   parameter    test_syn    =    "high";+   // leda G_521_3_B on++   input    inclk;+   input    ena;+   output   enaout;+   output   outclk;++   assign outclk = ena ? inclk : 1'b0;+   assign enaout = ena;++endmodule //cyclone10gx_clkena

@@ -0,0 +1,65 @@+#!/usr/bin/env bash++for i in $(seq 0 100); do+  echo "INFO: Run ${i}"+  dir="$(dirname "$(find /mnt/data/projects/verismith/runs/yosys_0.8/run_5 -name 'reduce*' -type f | shuf | head -1)")"+  dest="$(pwd)/run_${i}"+  interesting="${dest}/creduce/interesting.sh"+  vfile="${dest}/creduce/rtl.v"+  orig="$(pwd)"++  echo "INFO: Picked ${dir}"++  cp -r $dir $dest+  mkdir -p "${dest}/creduce"++  if [[ -f "${dest}/reduce_yosys.v" ]]; then+    echo "INFO: Detected crash"+    cat >$interesting <<EOF+/mnt/data/tools/yosys/constant/bin/yosys -q -p "read_verilog rtl.v; synth; write_verilog -noattr syn_yosys.v" >yosys.log 2>&1+grep "vector::_M_range_check:" yosys.log++exit \$?+EOF+  elif [[ -f "${dest}/reduce_identity_yosys.v" ]]; then+    echo "INFO: Detected mis-synthesis"+    cat >$interesting <<EOF+#!/usr/bin/env bash++grep -v -E '^[[:space:]]*reg[[:space:]].*=.*0.*;' rtl.v | grep '^[[:space:]]*reg[[:space:]].*[^,+-]*;'+if [[ \$? -eq 0 ]]; then exit 1; fi++cp "${dest}/equiv_identity_yosys/top.v" .+cp "${dest}/equiv_identity_yosys/proof.sby" .++sed -i 's:/home/vagrant/.cabal/store/ghc-8.6.5/verismith-0.4.0.1-[a-f0-9]*/share:/home/ymherklotz/projects/verismith:' proof.sby++/mnt/data/tools/yosys/constant/bin/yosys -q -p "read_verilog rtl.v; synth; write_verilog -noattr syn_yosys.v" >yosys1.log 2>&1 || exit 1++grep -v "Warning: Resizing cell port" yosys1.log >yosys.log++grep "Warning" yosys.log+greturn=\$?+if [[ \$greturn -eq 0 ]]; then exit 1; fi++sed -i -E 's/((module[0-9]+)|top)/\1_2/' syn_yosys.v+sed -E 's/((module[0-9]+)|top)/\1_1/' rtl.v >syn_identity.v++sby -f proof.sby >symbiyosys.log 2>&1++grep "FAIL" symbiyosys.log >/dev/null 2>&1 || exit 1++exit 0+EOF+  else+    echo "WARNING: No original reduction found"+    continue+  fi++  cp "${dest}/identity/syn_identity.v" "$vfile"+  chmod +x "$interesting"+  cd "${dest}/creduce"+  time creduce --abs-timing --no-c ./interesting.sh rtl.v >creduce.log+  cd "${orig}"+  echo "INFO: Done"+done

@@ -54,6 +54,7 @@ import qualified Hedgehog.Gen             as Hog import           Hedgehog.Internal.Seed   (Seed) import           Options.Applicative+import           Paths_verismith          (getDataDir) import           Prelude                  hiding (FilePath) import           Shelly                   hiding (command) import           Shelly.Lifted            (liftSh)@@ -62,6 +63,7 @@ import           Verismith.Config import           Verismith.Fuzz import           Verismith.Generate+import           Verismith.OptParser import           Verismith.Reduce import           Verismith.Report import           Verismith.Result@@ -70,36 +72,21 @@ import           Verismith.Verilog import           Verismith.Verilog.Parser (parseSourceInfoFile) -data OptTool = TYosys-          | TXST-          | TIcarus+-- | Generate a specific number of random bytestrings of size 256.+randomByteString :: C.CtrDRBG -> Int -> [ByteString] -> [ByteString]+randomByteString gen n bytes+    | n == 0    = ranBytes : bytes+    | otherwise = randomByteString newGen (n - 1) $ ranBytes : bytes+    where Right (ranBytes, newGen) = C.genBytes 32 gen -instance Show OptTool where-  show TYosys  = "yosys"-  show TXST    = "xst"-  show TIcarus = "icarus"+-- | generates the specific number of bytestring with a random seed.+generateByteString :: Int -> IO [ByteString]+generateByteString n = do+    gen <- C.newGenIO :: IO C.CtrDRBG+    return $ randomByteString gen n [] -data Opts = Fuzz { fuzzOutput :: {-# UNPACK #-} !Text-                 , configFile :: !(Maybe FilePath)-                 , forced     :: !Bool-                 , keepAll    :: !Bool-                 , num        :: {-# UNPACK #-} !Int-                 }-          | Generate { mFileName  :: !(Maybe FilePath)-                     , configFile :: !(Maybe FilePath)-                     }-          | Parse { fileName :: {-# UNPACK #-} !FilePath-                  }-          | Reduce { fileName        :: {-# UNPACK #-} !FilePath-                   , top             :: {-# UNPACK #-} !Text-                   , reduceScript    :: !(Maybe FilePath)-                   , synthesiserDesc :: ![SynthDescription]-                   , rerun           :: Bool-                   }-          | ConfigOpt { writeConfig :: !(Maybe FilePath)-                      , configFile  :: !(Maybe FilePath)-                      , doRandomise :: !Bool-                      }+toFP :: String -> FilePath+toFP = fromText . T.pack  myForkIO :: IO () -> IO (MVar ()) myForkIO io = do@@ -107,221 +94,15 @@     _    <- forkFinally io (\_ -> putMVar mvar ())     return mvar -textOption :: Mod OptionFields String -> Parser Text-textOption = fmap T.pack . strOption--optReader :: (String -> Maybe a) -> ReadM a-optReader f = eitherReader $ \arg -> case f arg of-    Just a  -> Right a-    Nothing -> Left $ "Cannot parse option: " <> arg--parseSynth :: String -> Maybe OptTool-parseSynth val | val == "yosys" = Just TYosys-               | val == "xst"   = Just TXST-               | otherwise      = Nothing--parseSynthDesc :: String -> Maybe SynthDescription-parseSynthDesc val-    | val == "yosys" = Just $ SynthDescription "yosys" Nothing Nothing Nothing-    | val == "vivado" = Just $ SynthDescription "vivado" Nothing Nothing Nothing-    | val == "xst" = Just $ SynthDescription "xst" Nothing Nothing Nothing-    | val == "quartus" = Just-    $ SynthDescription "quartus" Nothing Nothing Nothing-    | val == "identity" = Just-    $ SynthDescription "identity" Nothing Nothing Nothing-    | otherwise = Nothing--parseSim :: String -> Maybe OptTool-parseSim val | val == "icarus" = Just TIcarus-             | otherwise       = Nothing--fuzzOpts :: Parser Opts-fuzzOpts =-    Fuzz-        <$> textOption-                (  long "output"-                <> short 'o'-                <> metavar "DIR"-                <> help "Output directory that the fuzz run takes place in."-                <> showDefault-                <> value "output"-                )-        <*> (  optional-            .  strOption-            $  long "config"-            <> short 'c'-            <> metavar "FILE"-            <> help "Config file for the current fuzz run."-            )-        <*> (switch $ long "force" <> short 'f' <> help-                "Overwrite the specified directory."-            )-        <*> (switch $ long "keep" <> short 'k' <> help-                "Keep all the directories."-            )-        <*> (  option auto-            $  long "num"-            <> short 'n'-            <> help "The number of fuzz runs that should be performed."-            <> showDefault-            <> value 1-            <> metavar "INT"-            )--genOpts :: Parser Opts-genOpts =-    Generate-        <$> (  optional-            .  strOption-            $  long "output"-            <> short 'o'-            <> metavar "FILE"-            <> help "Output to a verilog file instead."-            )-        <*> (  optional-            .  strOption-            $  long "config"-            <> short 'c'-            <> metavar "FILE"-            <> help "Config file for the generation run."-            )--parseOpts :: Parser Opts-parseOpts = Parse . fromText . T.pack <$> strArgument-    (metavar "FILE" <> help "Verilog input file.")--reduceOpts :: Parser Opts-reduceOpts =-    Reduce-        .   fromText-        .   T.pack-        <$> strArgument (metavar "FILE" <> help "Verilog input file.")-        <*> textOption-                (  short 't'-                <> long "top"-                <> metavar "TOP"-                <> help "Name of top level module."-                <> showDefault-                <> value "top"-                )-        <*> (  optional-            .  strOption-            $  long "script"-            <> metavar "SCRIPT"-            <> help-                   "Script that determines if the current file is interesting, which is determined by the script returning 0."-            )-        <*> (  many-            .  option (optReader parseSynthDesc)-            $  short 's'-            <> long "synth"-            <> metavar "SYNTH"-            <> help "Specify synthesiser to use."-            )-        <*> (  switch-            $  short 'r'-            <> long "rerun"-            <> help-                   "Only rerun the current synthesis file with all the synthesisers."-            )--configOpts :: Parser Opts-configOpts =-    ConfigOpt-        <$> (  optional-            .  strOption-            $  long "output"-            <> short 'o'-            <> metavar "FILE"-            <> help "Output to a TOML Config file."-            )-        <*> (  optional-            .  strOption-            $  long "config"-            <> short 'c'-            <> metavar "FILE"-            <> help "Config file for the current fuzz run."-            )-        <*> (  switch-            $  long "randomise"-            <> short 'r'-            <> help-                   "Randomise the given default config, or the default config by randomly switchin on and off options."-            )--argparse :: Parser Opts-argparse =-    hsubparser-            (  command-                    "fuzz"-                    (info-                        fuzzOpts-                        (progDesc-                            "Run fuzzing on the specified simulators and synthesisers."-                        )-                    )-            <> metavar "fuzz"-            )-        <|> hsubparser-                (  command-                        "generate"-                        (info-                            genOpts-                            (progDesc "Generate a random Verilog program.")-                        )-                <> metavar "generate"-                )-        <|> hsubparser-                (  command-                        "parse"-                        (info-                            parseOpts-                            (progDesc-                                "Parse a verilog file and output a pretty printed version."-                            )-                        )-                <> metavar "parse"-                )-        <|> hsubparser-                (  command-                        "reduce"-                        (info-                            reduceOpts-                            (progDesc-                                "Reduce a Verilog file by rerunning the fuzzer on the file."-                            )-                        )-                <> metavar "reduce"-                )-        <|> hsubparser-                (  command-                        "config"-                        (info-                            configOpts-                            (progDesc-                                "Print the current configuration of the fuzzer."-                            )-                        )-                <> metavar "config"-                )--version :: Parser (a -> a)-version = infoOption versionInfo $ mconcat-    [long "version", short 'v', help "Show version information.", hidden]--opts :: ParserInfo Opts-opts = info-    (argparse <**> helper <**> version)-    (  fullDesc-    <> progDesc "Fuzz different simulators and synthesisers."-    <> header-           "Verismith - A hardware simulator and synthesiser Verilog fuzzer."-    )- getConfig :: Maybe FilePath -> IO Config getConfig s =     maybe (return defaultConfig) parseConfigFile $ T.unpack . toTextIgnore <$> s +getGenerator :: Config -> Text -> Maybe FilePath -> IO (Gen SourceInfo)+getGenerator config top s =+    maybe (return $ proceduralSrc top config) (fmap return . parseSourceInfoFile top)+    $ toTextIgnore <$> s+ -- | Randomly remove an option by setting it to 0. randDelete :: Int -> IO Int randDelete i = do@@ -363,12 +144,15 @@     ce = config ^. configProbability . probExpr  handleOpts :: Opts -> IO ()-handleOpts (Fuzz o configF _ k n) = do+handleOpts (Fuzz o configF f k n nosim noequiv noreduction file top cc) = do     config <- getConfig configF+    gen <- getGenerator config top file+    datadir <- getDataDir     _      <- runFuzz-        config+        (FuzzOpts (Just $ fromText o)+         f k n nosim noequiv noreduction config (toFP datadir) cc)         defaultYosys-        (fuzzMultiple n k (Just $ fromText o) (proceduralSrc "top" config))+        (fuzzMultiple gen)     return () handleOpts (Generate f c) = do     config <- getConfig c@@ -377,21 +161,29 @@         $   T.unpack         .   toTextIgnore         <$> f-handleOpts (Parse f) = do+handleOpts (Parse f t o rc) = do     verilogSrc <- T.readFile file     case parseVerilog (T.pack file) verilogSrc of         Left  l -> print l-        Right v -> print $ GenVerilog v-    where file = T.unpack . toTextIgnore $ f+        Right v ->+            case (o, GenVerilog+                     . mapply rc (takeReplace . removeConstInConcat)+                     $ SourceInfo t v) of+            (Nothing, a) -> print a+            (Just o', a) -> writeFile (T.unpack $ toTextIgnore o') $ show a+  where+    file = T.unpack . toTextIgnore $ f+    mapply i f = if i then f else id handleOpts (Reduce f t _ ls' False) = do     src <- parseSourceInfoFile t (toTextIgnore f)+    datadir <- getDataDir     case descriptionToSynth <$> ls' of         a : b : _ -> do             putStrLn "Reduce with equivalence check"             shelly $ do                 make dir                 pop dir $ do-                    src' <- reduceSynth a b src+                    src' <- reduceSynth (toFP datadir) a b src                     writefile (fromText ".." </> dir <.> "v") $ genSource src'         a : _ -> do             putStrLn "Reduce with synthesis failure"@@ -406,6 +198,7 @@     where dir = fromText "reduce" handleOpts (Reduce f t _ ls' True) = do     src <- parseSourceInfoFile t (toTextIgnore f)+    datadir <- getDataDir     case descriptionToSynth <$> ls' of         a : b : _ -> do             putStrLn "Starting equivalence check"@@ -414,12 +207,12 @@                 pop dir $ do                     runSynth a src                     runSynth b src-                    runEquiv a b src+                    runEquiv (toFP datadir) a b src             case res of-                Pass _            -> putStrLn "Equivalence check passed"-                Fail EquivFail    -> putStrLn "Equivalence check failed"-                Fail TimeoutError -> putStrLn "Equivalence check timed out"-                Fail _            -> putStrLn "Equivalence check error"+                Pass _             -> putStrLn "Equivalence check passed"+                Fail (EquivFail _) -> putStrLn "Equivalence check failed"+                Fail TimeoutError  -> putStrLn "Equivalence check timed out"+                Fail _             -> putStrLn "Equivalence check error"             return ()         as -> do             putStrLn "Synthesis check"@@ -438,19 +231,6 @@     optsparsed <- execParser opts     handleOpts optsparsed --- | Generate a specific number of random bytestrings of size 256.-randomByteString :: C.CtrDRBG -> Int -> [ByteString] -> [ByteString]-randomByteString gen n bytes-    | n == 0    = ranBytes : bytes-    | otherwise = randomByteString newGen (n - 1) $ ranBytes : bytes-    where Right (ranBytes, newGen) = C.genBytes 32 gen---- | generates the specific number of bytestring with a random seed.-generateByteString :: Int -> IO [ByteString]-generateByteString n = do-    gen <- C.newGenIO :: IO C.CtrDRBG-    return $ randomByteString gen n []- makeSrcInfo :: ModDecl -> SourceInfo makeSrcInfo m = SourceInfo (getIdentifier $ m ^. modId) (Verilog [m]) @@ -504,10 +284,11 @@ checkEquivalence src dir = shellyFailDir $ do     mkdir_p (fromText dir)     curr <- toTextIgnore <$> pwd+    datadir <- liftIO getDataDir     setenv "VERISMITH_ROOT" curr     cd (fromText dir)     catch_sh-        ((runResultT $ runEquiv defaultYosys defaultVivado src) >> return True)+        ((runResultT $ runEquiv (toFP datadir) defaultYosys defaultVivado src) >> return True)         ((\_ -> return False) :: RunFailed -> Sh Bool)  -- | Run a fuzz run and check if all of the simulators passed by checking if the@@ -524,6 +305,7 @@     (_, m) <- shelly $ sampleSeed seed gm     let srcInfo = SourceInfo "top" m     rand <- generateByteString 20+    datadir <- getDataDir     shellyFailDir $ do         mkdir_p (fromText d </> fromText n)         curr <- toTextIgnore <$> pwd@@ -532,7 +314,7 @@         _ <-             catch_sh                     (  runResultT-                    $  runEquiv defaultYosys defaultVivado srcInfo+                    $  runEquiv (toFP datadir) defaultYosys defaultVivado srcInfo                     >> liftSh (logger "Test OK")                     )                 $ onFailure n@@ -550,4 +332,4 @@  runReduce :: SourceInfo -> IO SourceInfo runReduce s =-    shelly $ reduce (\s' -> not <$> liftIO (checkEquivalence s' "reduce")) s+    shelly $ reduce "reduce.v" (\s' -> not <$> liftIO (checkEquivalence s' "reduce")) s

@@ -36,6 +36,7 @@     , fromYosys     , fromVivado     , fromQuartus+    , fromQuartusLight     , configProbability     , configProperty     , configSimulators@@ -79,20 +80,21 @@     ) where -import           Control.Applicative    (Alternative)-import           Control.Lens           hiding ((.=))-import           Data.List.NonEmpty     (NonEmpty (..))-import           Data.Maybe             (fromMaybe)-import           Data.Text              (Text, pack)-import qualified Data.Text.IO           as T-import           Data.Version           (showVersion)+import           Control.Applicative         (Alternative)+import           Control.Lens                hiding ((.=))+import           Data.List.NonEmpty          (NonEmpty (..))+import           Data.Maybe                  (fromMaybe)+import           Data.Text                   (Text, pack)+import qualified Data.Text.IO                as T+import           Data.Version                (showVersion) import           Development.GitRev-import           Hedgehog.Internal.Seed (Seed)-import           Paths_verismith        (version)-import           Shelly                 (toTextIgnore)-import           Toml                   (TomlCodec, (.=))+import           Hedgehog.Internal.Seed      (Seed)+import           Paths_verismith             (version)+import           Shelly                      (toTextIgnore)+import           Toml                        (TomlCodec, (.=)) import qualified Toml import           Verismith.Tool.Quartus+import           Verismith.Tool.QuartusLight import           Verismith.Tool.Vivado import           Verismith.Tool.XST import           Verismith.Tool.Yosys@@ -283,6 +285,12 @@  fromQuartus :: Quartus -> SynthDescription fromQuartus (Quartus a b c) = SynthDescription "quartus"+                                               (toTextIgnore <$> a)+                                               (Just b)+                                               (Just $ toTextIgnore c)++fromQuartusLight :: QuartusLight -> SynthDescription+fromQuartusLight (QuartusLight a b c) = SynthDescription "quartuslight"                                                (toTextIgnore <$> a)                                                (Just b)                                                (Just $ toTextIgnore c)

@@ -0,0 +1,112 @@+{-|+Module      : Verismith.CounterEg+Description : Counter example parser to load the counter example+Copyright   : (c) 2019, Yann Herklotz+License     : BSD-3+Maintainer  : yann [at] yannherklotz [dot] com+Stability   : experimental+Portability : POSIX+-}++module Verismith.CounterEg+    ( CounterEg(..)+    , parseCounterEg+    )+where++import           Control.Applicative  ((<|>))+import           Data.Bifunctor       (bimap)+import           Data.Binary          (encode)+import           Data.Bits            (shiftL, (.|.))+import           Data.ByteString      (ByteString)+import qualified Data.ByteString      as B+import qualified Data.ByteString.Lazy as L+import           Data.Char            (digitToInt)+import           Data.Functor         (($>))+import           Data.Maybe           (listToMaybe)+import           Data.Text            (Text)+import qualified Data.Text            as T+import           Numeric              (readInt)+import qualified Text.Parsec          as P++data CounterEg = CounterEg { _counterEgInitial :: ![(Text, Text)]+                           , _counterEgStates  :: ![[(Text, Text)]]+                           }+               deriving (Eq, Show)++instance Semigroup CounterEg where+    CounterEg a b <> CounterEg c d = CounterEg (a <> c) (b <> d)++instance Monoid CounterEg where+    mempty = CounterEg mempty mempty++type Parser = P.Parsec String ()++-- fromBytes :: ByteString -> Int+-- fromBytes = B.foldl' f 0 where f a b = a `shiftL` 8 .|. fromIntegral b++-- convert :: String -> ByteString+-- convert =+--     L.toStrict+--         . (encode :: Integer -> L.ByteString)+--         . maybe 0 fst+--         . listToMaybe+--         . readInt 2 (`elem` ("01" :: String)) digitToInt++-- convertBinary :: String -> Int+-- convertBinary = fromBytes . convert++lexme :: Parser a -> Parser a+lexme f = do { a <- f; _ <- P.spaces; return a }++nameChar :: Parser Char+nameChar = P.alphaNum+           <|> P.oneOf "$.:_"++parens :: Parser a -> Parser a+parens = lexme . P.between (P.char '(') (P.char ')')++brackets :: Parser a -> Parser a+brackets = lexme . P.between (P.char '[') (P.char ']')++trueOrFalse :: Parser String+trueOrFalse = lexme $ (P.string "true" $> "1") <|> (P.string "false" $> "0")++assumeBody :: Parser (String, String)+assumeBody = lexme $ do+    name <- P.char '=' *> P.spaces *> brackets (P.many1 nameChar)+    num <- P.spaces *> ((P.string "#b" *> P.many1 P.digit) <|> trueOrFalse)+    return (name, num)++parseAssume :: Parser (String, String)+parseAssume = lexme $ P.string "assume" *> P.spaces *> parens assumeBody++parseInitial :: Parser [(String, String)]+parseInitial = lexme $ do+    _ <- lexme $ P.string "initial"+    P.many parseAssume++parseState :: Parser (String, [(String, String)])+parseState = lexme $ do+    n <- lexme $ P.string "state" *> P.spaces *> P.many1 P.digit+    assumes <- P.many parseAssume+    return (n, assumes)++parseCE :: Parser [[(String, String)]]+parseCE = lexme $ do+    i <- parseInitial+    other <- fmap snd <$> P.many parseState+    return (i : other)++cEtoCounterEg :: [[(String, String)]] -> CounterEg+cEtoCounterEg [] = mempty+cEtoCounterEg (i : is) = CounterEg (bimap T.pack T.pack <$> i)+                         (fmap (bimap T.pack T.pack) <$> is)++parseCounterEg' :: Parser CounterEg+parseCounterEg' = lexme $ do+    _ <- P.spaces+    cEtoCounterEg <$> parseCE++parseCounterEg :: Text -> Either String CounterEg+parseCounterEg = bimap show id . P.parse parseCounterEg' "" . T.unpack

@@ -15,7 +15,8 @@ {-# LANGUAGE TemplateHaskell  #-}  module Verismith.Fuzz-    ( Fuzz+    ( Fuzz (..)+    , FuzzOpts (..)     , fuzz     , fuzzInDir     , fuzzMultiple@@ -27,34 +28,33 @@     ) where -import           Control.DeepSeq                  (force)-import           Control.Exception.Lifted         (finally)-import           Control.Lens                     hiding ((<.>))-import           Control.Monad                    (forM, replicateM)+import           Control.DeepSeq             (force)+import           Control.Exception.Lifted    (finally)+import           Control.Lens                hiding ((<.>))+import           Control.Monad               (forM, replicateM) import           Control.Monad.IO.Class-import           Control.Monad.Trans.Class        (lift)-import           Control.Monad.Trans.Control      (MonadBaseControl)-import           Control.Monad.Trans.Maybe        (runMaybeT)-import           Control.Monad.Trans.Reader       hiding (local)-import           Control.Monad.Trans.State.Strict-import qualified Crypto.Random.DRBG               as C-import           Data.ByteString                  (ByteString)-import           Data.List                        (nubBy, sort)-import           Data.Maybe                       (isNothing)-import           Data.Text                        (Text)-import qualified Data.Text                        as T+import           Control.Monad.Reader+import           Control.Monad.State.Strict+import           Control.Monad.Trans.Control (MonadBaseControl)+import qualified Crypto.Random.DRBG          as C+import           Data.ByteString             (ByteString)+import           Data.List                   (nubBy, sort)+import           Data.Maybe                  (catMaybes, fromMaybe, isNothing)+import           Data.Text                   (Text)+import qualified Data.Text                   as T import           Data.Time-import           Data.Tuple                       (swap)-import           Hedgehog                         (Gen)-import qualified Hedgehog.Internal.Gen            as Hog-import           Hedgehog.Internal.Seed           (Seed)-import qualified Hedgehog.Internal.Seed           as Hog-import qualified Hedgehog.Internal.Tree           as Hog-import           Prelude                          hiding (FilePath)-import           Shelly                           hiding (get)-import           Shelly.Lifted                    (MonadSh, liftSh)-import           System.FilePath.Posix            (takeBaseName)+import           Data.Tuple                  (swap)+import           Hedgehog                    (Gen)+import qualified Hedgehog.Internal.Gen       as Hog+import           Hedgehog.Internal.Seed      (Seed)+import qualified Hedgehog.Internal.Seed      as Hog+import qualified Hedgehog.Internal.Tree      as Hog+import           Prelude                     hiding (FilePath)+import           Shelly                      hiding (get)+import           Shelly.Lifted               (MonadSh, liftSh)+import           System.FilePath.Posix       (takeBaseName) import           Verismith.Config+import           Verismith.CounterEg         (CounterEg (..)) import           Verismith.Internal import           Verismith.Reduce import           Verismith.Report@@ -65,12 +65,43 @@ import           Verismith.Verilog.AST import           Verismith.Verilog.CodeGen -data FuzzEnv = FuzzEnv { getSynthesisers :: ![SynthTool]-                       , getSimulators   :: ![SimTool]-                       , yosysInstance   :: {-# UNPACK #-} !Yosys+data FuzzOpts = FuzzOpts { _fuzzOptsOutput      :: !(Maybe FilePath)+                         , _fuzzOptsForced      :: !Bool+                         , _fuzzOptsKeepAll     :: !Bool+                         , _fuzzOptsIterations  :: {-# UNPACK #-} !Int+                         , _fuzzOptsNoSim       :: !Bool+                         , _fuzzOptsNoEquiv     :: !Bool+                         , _fuzzOptsNoReduction :: !Bool+                         , _fuzzOptsConfig      :: {-# UNPACK #-} !Config+                         , _fuzzDataDir         :: {-# UNPACK #-} !FilePath+                         , _fuzzOptsCrossCheck  :: !Bool+                         }+              deriving (Show, Eq)++$(makeLenses ''FuzzOpts)++defaultFuzzOpts :: FuzzOpts+defaultFuzzOpts = FuzzOpts { _fuzzOptsOutput      = Nothing+                           , _fuzzOptsForced      = False+                           , _fuzzOptsKeepAll     = False+                           , _fuzzOptsIterations  = 1+                           , _fuzzOptsNoSim       = False+                           , _fuzzOptsNoEquiv     = False+                           , _fuzzOptsNoReduction = False+                           , _fuzzOptsConfig      = defaultConfig+                           , _fuzzDataDir = fromText "."+                           , _fuzzOptsCrossCheck = False+                           }++data FuzzEnv = FuzzEnv { _getSynthesisers :: ![SynthTool]+                       , _getSimulators   :: ![SimTool]+                       , _yosysInstance   :: {-# UNPACK #-} !Yosys+                       , _fuzzEnvOpts     :: {-# UNPACK #-} !FuzzOpts                        }                deriving (Eq, Show) +$(makeLenses ''FuzzEnv)+ data FuzzState = FuzzState { _fuzzSynthResults :: ![SynthResult]                            , _fuzzSimResults   :: ![SimResult]                            , _fuzzSynthStatus  :: ![SynthStatus]@@ -87,29 +118,80 @@  type MonadFuzz m = (MonadBaseControl IO m, MonadIO m, MonadSh m) -runFuzz :: MonadIO m => Config -> Yosys -> (Config -> Fuzz Sh a) -> m a-runFuzz conf yos m = shelly $ runFuzz' conf yos m+runFuzz :: MonadIO m => FuzzOpts -> Yosys -> Fuzz Sh a -> m a+runFuzz fo yos m = shelly $ runFuzz' fo yos m -runFuzz' :: Monad m => Config -> Yosys -> (Config -> Fuzz m b) -> m b-runFuzz' conf yos m = runReaderT-    (evalStateT (m conf) (FuzzState [] [] []))-    (FuzzEnv-        ( force-        $ defaultIdentitySynth-        : (descriptionToSynth <$> conf ^. configSynthesisers)-        )-        (force $ descriptionToSim <$> conf ^. configSimulators)-        yos+runFuzz' :: Monad m => FuzzOpts -> Yosys -> Fuzz m b -> m b+runFuzz' fo yos m = runReaderT+    (evalStateT m (FuzzState [] [] []))+    (FuzzEnv { _getSynthesisers = ( force+                                   $ defaultIdentitySynth+                                   : (descriptionToSynth <$> conf ^. configSynthesisers)+                                 )+             , _getSimulators = (force $ descriptionToSim <$> conf ^. configSimulators)+             , _yosysInstance = yos+             , _fuzzEnvOpts   = fo+             }     )+  where+    conf = _fuzzOptsConfig fo +askConfig :: Monad m => Fuzz m Config+askConfig = asks (_fuzzOptsConfig . _fuzzEnvOpts)++askOpts :: Monad m => Fuzz m FuzzOpts+askOpts = asks _fuzzEnvOpts++genMethod conf seed gen =+    case T.toLower $ conf ^. configProperty . propSampleMethod of+        "hat" -> do+            logT "Using the hat function"+            sv hatFreqs+        "mean" -> do+            logT "Using the mean function"+            sv meanFreqs+        "median" -> do+            logT "Using the median function"+            sv medianFreqs+        _ -> do+            logT "Using first seed"+            sampleSeed seed gen+  where+    sv a = sampleVerilog a (conf ^. configProperty . propSampleSize) seed gen++relativeFuzzReport :: (MonadSh m) => FuzzReport -> m FuzzReport+relativeFuzzReport fr@(FuzzReport dir _ _ _ _ _ _ _) = liftSh $ do+    newPath <- relPath dir+    return $ (fuzzDir .~ newPath) fr++filterSynth :: SynthResult -> Bool+filterSynth (SynthResult _ _ (Pass _) _) = True+filterSynth _                            = False++filterSim :: SimResult -> Bool+filterSim (SimResult _ _ _ (Pass _) _) = True+filterSim _                            = False++filterSynthStat :: SynthStatus -> Bool+filterSynthStat (SynthStatus _ (Pass _) _) = True+filterSynthStat _                          = False++passedFuzz :: FuzzReport -> Bool+passedFuzz (FuzzReport _ synth sim synthstat _ _ _ _) =+    (passedSynth + passedSim + passedSynthStat) == 0+  where+    passedSynth = length $ filter (not . filterSynth) synth+    passedSim = length $ filter (not . filterSim) sim+    passedSynthStat = length $ filter (not . filterSynthStat) synthstat+ synthesisers :: Monad m => Fuzz m [SynthTool]-synthesisers = lift $ asks getSynthesisers+synthesisers = lift $ asks _getSynthesisers  --simulators :: (Monad m) => Fuzz () m [SimTool] --simulators = lift $ asks getSimulators ---combinations :: [a] -> [b] -> [(a, b)]---combinations l1 l2 = [ (x, y) | x <- l1, y <- l2 ]+combinations :: [a] -> [b] -> [(a, b)]+combinations l1 l2 = [ (x, y) | x <- l1, y <- l2 ]  logT :: MonadSh m => Text -> m () logT = liftSh . logger@@ -148,9 +230,7 @@     toSynth (SynthStatus s _ _) = s  make :: MonadSh m => FilePath -> m ()-make f = liftSh $ do-    mkdir_p f-    cp_r "data" $ f </> fromText "data"+make f = liftSh $ mkdir_p f  pop :: (MonadBaseControl IO m, MonadSh m) => FilePath -> m a -> m a pop f a = do@@ -163,35 +243,43 @@ applyLots :: (a -> b -> c -> d -> e) -> [(a, b)] -> [(c, d)] -> [e] applyLots func a b = applyList (uncurry . uncurry func <$> a) b -toSynthResult-    :: [(SynthTool, SynthTool)]-    -> [(NominalDiffTime, Result Failed ())]-    -> [SynthResult]+toSynthResult :: [(SynthTool, SynthTool)]+              -> [(NominalDiffTime, Result Failed ())]+              -> [SynthResult] toSynthResult a b = applyLots SynthResult a $ fmap swap b -toolRun :: (MonadIO m, MonadSh m) => Text -> m a -> m (NominalDiffTime, a)+toSimResult :: SimTool+            -> [ByteString]+            -> [SynthTool]+            -> [(NominalDiffTime, Result Failed ByteString)]+            -> [SimResult]+toSimResult sima bs as b =+    applyList (applyList (repeat uncurry)+               (applyList (applyList (SimResult <$> as) (repeat sima)) (repeat bs)))+    $ fmap swap b++toolRun :: (MonadIO m, MonadSh m, Show a) => Text -> m a -> m (NominalDiffTime, a) toolRun t m = do     logT $ "Running " <> t-    (diff, res) <- timeit m-    logT $ "Finished " <> t <> " (" <> showT diff <> ")"-    return (diff, res)+    s <- timeit m+    logT $ "Finished " <> t <> " " <> showT s+    return s  equivalence :: (MonadBaseControl IO m, MonadSh m) => SourceInfo -> Fuzz m () equivalence src = do+    doCrossCheck <- fmap _fuzzOptsCrossCheck askOpts+    datadir <- fmap _fuzzDataDir askOpts     synth <- passedSynthesis---    let synthComb =---            nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth     let synthComb =-            nubBy tupEq-                .   filter (uncurry (/=))-                $   (,) defaultIdentitySynth-                <$> synth-    resTimes <- liftSh $ mapM (uncurry equiv) synthComb+            if doCrossCheck+            then nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth+            else nubBy tupEq . filter (uncurry (/=)) $ (,) defaultIdentitySynth <$> synth+    resTimes <- liftSh $ mapM (uncurry (equiv datadir)) synthComb     fuzzSynthResults .= toSynthResult synthComb resTimes     liftSh $ inspect resTimes   where     tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a')-    equiv a b =+    equiv datadir a b =         toolRun ("equivalence check for " <> toText a <> " and " <> toText b)             . runResultT             $ do make dir@@ -206,30 +294,42 @@                               </> synthOutput b                             ) $ synthOutput b                          writefile "rtl.v" $ genSource src-                     runEquiv a b src+                     runEquiv datadir a b src         where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b  simulation :: (MonadIO m, MonadSh m) => SourceInfo -> Fuzz m () simulation src = do-    synth    <- passEquiv+    datadir <- fmap _fuzzDataDir askOpts+    synth    <- passedSynthesis+    counterEgs <- failEquivWithIdentityCE     vals     <- liftIO $ generateByteString 20-    ident    <- liftSh $ equiv vals defaultIdentitySynth-    resTimes <- liftSh $ mapM (equiv vals) $ conv <$> synth+    ident    <- liftSh $ sim datadir vals Nothing defaultIdentitySynth+    resTimes <- liftSh $ mapM (sim datadir vals (justPass $ snd ident)) synth+    resTimes2 <- liftSh $ mapM (simCounterEg datadir) counterEgs+    fuzzSimResults .= toSimResult defaultIcarusSim vals synth resTimes     liftSh         .   inspect         $   (\(_, r) -> bimap show (T.unpack . T.take 10 . showBS) r)         <$> (ident : resTimes)   where-    conv (SynthResult _ a _ _) = a-    equiv b a = toolRun ("simulation for " <> toText a) . runResultT $ do+    sim datadir b i a = toolRun ("simulation for " <> toText a) . runResultT $ do         make dir         pop dir $ do             liftSh $ do                 cp (fromText ".." </> fromText (toText a) </> synthOutput a)                     $ synthOutput a                 writefile "rtl.v" $ genSource src-            runSimIc defaultIcarus a src b+            runSimIc datadir defaultIcarus a src b i         where dir = fromText $ "simulation_" <> toText a+    simCounterEg datadir (a, b) = toolRun ("counter-example simulation for " <> toText a) . runResultT $ do+        make dir+        pop dir $ do+            liftSh $ do+                cp (fromText ".." </> fromText (toText a) </> synthOutput a) $ synthOutput a+                writefile "syn_identity.v" $ genSource src+            ident <- runSimIcEC datadir defaultIcarus defaultIdentitySynth src b Nothing+            runSimIcEC datadir defaultIcarus a src b (Just ident)+      where dir = fromText $ "countereg_sim_" <> toText a  -- | Generate a specific number of random bytestrings of size 256. randomByteString :: C.CtrDRBG -> Int -> [ByteString] -> [ByteString]@@ -247,10 +347,23 @@ failEquivWithIdentity :: (MonadSh m) => Fuzz m [SynthResult] failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get   where-    withIdentity (SynthResult (IdentitySynth _) _ (Fail EquivFail) _) = True-    withIdentity (SynthResult _ (IdentitySynth _) (Fail EquivFail) _) = True+    withIdentity (SynthResult (IdentitySynth _) _ (Fail (EquivFail _)) _) = True+    withIdentity (SynthResult _ (IdentitySynth _) (Fail (EquivFail _)) _) = True     withIdentity _                                                    = False +failEquivWithIdentityCE :: (MonadSh m) => Fuzz m [(SynthTool, CounterEg)]+failEquivWithIdentityCE = catMaybes . fmap withIdentity . _fuzzSynthResults <$> get+  where+    withIdentity (SynthResult (IdentitySynth _) s (Fail (EquivFail c)) _) = Just (s, c)+    withIdentity (SynthResult s (IdentitySynth _) (Fail (EquivFail c)) _) = Just (s, c)+    withIdentity _                                                        = Nothing++failedSimulations :: (MonadSh m) => Fuzz m [SimResult]+failedSimulations = filter failedSim . _fuzzSimResults <$> get+  where+    failedSim (SimResult _ _ _ (Fail (SimFail _)) _) = True+    failedSim _                                      = False+ passEquiv :: (MonadSh m) => Fuzz m [SynthResult] passEquiv = filter withIdentity . _fuzzSynthResults <$> get   where@@ -260,26 +373,18 @@ -- | Always reduces with respect to 'Identity'. reduction :: (MonadSh m) => SourceInfo -> Fuzz m () reduction src = do+    datadir <- fmap _fuzzDataDir askOpts     fails      <- failEquivWithIdentity     synthFails <- failedSynthesis-    _          <- liftSh $ mapM red fails+    simFails <- failedSimulations+    _          <- liftSh $ mapM (red datadir) fails     _          <- liftSh $ mapM redSynth synthFails+    _ <- liftSh $ mapM (redSim datadir) simFails     return ()   where-    red (SynthResult a b _ _) = do-        make dir-        pop dir $ do-            s <- reduceSynth a b src-            writefile (fromText ".." </> dir <.> "v") $ genSource s-            return s-        where dir = fromText $ "reduce_" <> toText a <> "_" <> toText b-    redSynth a = do-        make dir-        pop dir $ do-            s <- reduceSynthesis a src-            writefile (fromText ".." </> dir <.> "v") $ genSource s-            return s-        where dir = fromText $ "reduce_" <> toText a+    red datadir (SynthResult a b _ _) = reduceSynth datadir a b src+    redSynth a = reduceSynthesis a src+    redSim datadir (SimResult t _ bs _ _) = reduceSimIc datadir bs t src  titleRun     :: (MonadIO m, MonadSh m) => Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a)@@ -346,9 +451,12 @@     hat = set_ <$> [1 .. length l]     set_ n = if n == h then 1 else 0 -fuzz :: MonadFuzz m => Gen SourceInfo -> Config -> Fuzz m FuzzReport-fuzz gen conf = do-    (seed', src) <- generateSample genMethod+fuzz :: MonadFuzz m => Gen SourceInfo -> Fuzz m FuzzReport+fuzz gen = do+    conf <- askConfig+    opts <- askOpts+    let seed = conf ^. configProperty . propSeed+    (seed', src) <- generateSample $ genMethod conf seed gen     let size = length . lines . T.unpack $ genSource src     liftSh         .  writefile "config.toml"@@ -358,12 +466,18 @@         .  propSeed         ?~ seed'     (tsynth, _) <- titleRun "Synthesis" $ synthesis src-    (tequiv, _) <- titleRun "Equivalence Check" $ equivalence src-    (_     , _) <- titleRun "Simulation" $ simulation src+    (tequiv, _) <- if (_fuzzOptsNoEquiv opts)+        then return (0, mempty)+        else titleRun "Equivalence Check" $ equivalence src+    (_     , _) <- if (_fuzzOptsNoSim opts)+        then return (0, mempty)+        else titleRun "Simulation" $ simulation src     fails       <- failEquivWithIdentity+    failedSim <- failedSimulations     synthFails  <- failedSynthesis     redResult   <--        whenMaybe (not $ null fails && null synthFails)+        whenMaybe (not (null failedSim && null fails && null synthFails)+                   && not (_fuzzOptsNoReduction opts))         . titleRun "Reduction"         $ reduction src     state_  <- get@@ -378,70 +492,28 @@                             tequiv                             (getTime redResult)     return report-  where-    seed      = conf ^. configProperty . propSeed-    genMethod = case T.toLower $ conf ^. configProperty . propSampleMethod of-        "hat" -> do-            logT "Using the hat function"-            sv hatFreqs-        "mean" -> do-            logT "Using the mean function"-            sv meanFreqs-        "median" -> do-            logT "Using the median function"-            sv medianFreqs-        _ -> do-            logT "Using first seed"-            sampleSeed seed gen-    sv a = sampleVerilog a (conf ^. configProperty . propSampleSize) seed gen -relativeFuzzReport :: (MonadSh m) => FuzzReport -> m FuzzReport-relativeFuzzReport fr@(FuzzReport dir _ _ _ _ _ _ _) = liftSh $ do-    newPath <- relPath dir-    return $ (fuzzDir .~ newPath) fr--filterSynth :: SynthResult -> Bool-filterSynth (SynthResult _ _ (Pass _) _) = True-filterSynth _                            = False--filterSim :: SimResult -> Bool-filterSim (SimResult _ _ (Pass _) _) = True-filterSim _                          = False--filterSynthStat :: SynthStatus -> Bool-filterSynthStat (SynthStatus _ (Pass _) _) = True-filterSynthStat _                          = False--passedFuzz :: FuzzReport -> Bool-passedFuzz (FuzzReport _ synth sim synthstat _ _ _ _) =-    (passedSynth + passedSim + passedSynthStat) == 0-  where-    passedSynth = length $ filter (not . filterSynth) synth-    passedSim = length $ filter (not . filterSim) sim-    passedSynthStat = length $ filter (not . filterSynthStat) synthstat--fuzzInDir-    :: MonadFuzz m => Bool -> FilePath -> Gen SourceInfo -> Config -> Fuzz m FuzzReport-fuzzInDir k fp src conf = do+fuzzInDir :: MonadFuzz m => Gen SourceInfo -> Fuzz m FuzzReport+fuzzInDir src = do+    fuzzOpts <- askOpts+    let fp = fromMaybe "fuzz" $ _fuzzOptsOutput fuzzOpts     make fp-    res <- pop fp $ fuzz src conf+    res <- pop fp $ fuzz src     liftSh $ do         writefile (fp <.> "html") $ printResultReport (bname fp) res-        when (passedFuzz res && not k) $ rm_rf fp+        when (passedFuzz res && not (_fuzzOptsKeepAll fuzzOpts)) $ rm_rf fp     relativeFuzzReport res   where     bname = T.pack . takeBaseName . T.unpack . toTextIgnore  fuzzMultiple     :: MonadFuzz m-    => Int-    -> Bool-    -> Maybe FilePath-    -> Gen SourceInfo-    -> Config+    => Gen SourceInfo     -> Fuzz m [FuzzReport]-fuzzMultiple n k fp src conf = do-    x <- case fp of+fuzzMultiple src = do+    fuzzOpts <- askOpts+    let seed = (_fuzzOptsConfig fuzzOpts) ^. configProperty . propSeed+    x <- case _fuzzOptsOutput fuzzOpts of         Nothing -> do             ct <- liftIO getZonedTime             return@@ -453,21 +525,22 @@     make x     pop x $ do         results <- if isNothing seed-            then forM [1 .. n] fuzzDir'+            then forM [1 .. (_fuzzOptsIterations fuzzOpts)] fuzzDir'             else (: []) <$> fuzzDir' (1 :: Int)         liftSh . writefile (fromText "index" <.> "html") $ printSummary             "Fuzz Summary"             results         return results   where-    fuzzDir' n' = fuzzInDir k (fromText $ "fuzz_" <> showT n') src conf-    seed = conf ^. configProperty . propSeed+    fuzzDir' :: (Show a, MonadFuzz m) => a -> Fuzz m FuzzReport+    fuzzDir' n' = local (fuzzEnvOpts . fuzzOptsOutput .~+                         (Just . fromText $ "fuzz_" <> showT n'))+                  $ fuzzInDir src  sampleSeed :: MonadSh m => Maybe Seed -> Gen a -> m (Seed, a) sampleSeed s gen =     liftSh-        $ let-              loop n = if n <= 0+        $ let loop n = if n <= 0                   then                       error                           "Hedgehog.Gen.sample: too many discards, could not generate a sample"

@@ -10,7 +10,8 @@ Various useful generators. -} -{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TemplateHaskell  #-} {-# OPTIONS_GHC -Wno-unused-imports #-}  module Verismith.Generate@@ -60,19 +61,18 @@     ) where -import           Control.Lens                     hiding (Context)-import           Control.Monad                    (replicateM)-import           Control.Monad.Trans.Class        (lift)-import           Control.Monad.Trans.Reader       hiding (local)-import           Control.Monad.Trans.State.Strict-import           Data.Foldable                    (fold)-import           Data.Functor.Foldable            (cata)-import           Data.List                        (foldl', partition)-import qualified Data.Text                        as T-import           Hedgehog                         (Gen, GenT, MonadGen)-import qualified Hedgehog                         as Hog-import qualified Hedgehog.Gen                     as Hog-import qualified Hedgehog.Range                   as Hog+import           Control.Lens               hiding (Context)+import           Control.Monad              (replicateM)+import           Control.Monad.Reader+import           Control.Monad.State.Strict+import           Data.Foldable              (fold)+import           Data.Functor.Foldable      (cata)+import           Data.List                  (foldl', partition)+import qualified Data.Text                  as T+import           Hedgehog                   (Gen, GenT, MonadGen)+import qualified Hedgehog                   as Hog+import qualified Hedgehog.Gen               as Hog+import qualified Hedgehog.Range             as Hog import           Verismith.Config import           Verismith.Internal import           Verismith.Verilog.AST@@ -149,12 +149,6 @@ askProbability :: StateGen Probability askProbability = asks probability -rask :: StateGen Config-rask = ask--lget :: StateGen Context-lget = lift . lift $ get- -- | Generates a random large number, which can also be negative. largeNum :: (MonadGen m) => m Int largeNum = Hog.int $ Hog.linear (-100) 100@@ -314,7 +308,7 @@ -- is then increased so that the label is unique. makeIdentifier :: T.Text -> StateGen Identifier makeIdentifier prefix = do-    context <- lget+    context <- get     let ident = Identifier $ prefix <> showT (context ^. nameCounter)     nameCounter += 1     return ident@@ -332,7 +326,7 @@ -- the generation is currently in the other branch of an if-statement. nextPort :: PortType -> StateGen Port nextPort pt = do-    context <- lget+    context <- get     ident   <- makeIdentifier . T.toLower $ showT pt     getPort' pt ident (_variables context) @@ -347,7 +341,7 @@ -- | Generates an expression from variables that are currently in scope. scopedExpr :: StateGen Expr scopedExpr = do-    context <- lget+    context <- get     prob    <- askProbability     Hog.sized         . exprWithContext (_probExpr prob) (_parameters context)@@ -383,12 +377,12 @@ conditional :: StateGen Statement conditional = do     expr  <- scopedExpr-    nc    <- _nameCounter <$> lget+    nc    <- _nameCounter <$> get     tstat <- seqBlock-    nc'   <- _nameCounter <$> lget+    nc'   <- _nameCounter <$> get     nameCounter .= nc     fstat <- seqBlock-    nc''  <- _nameCounter <$> lget+    nc''  <- _nameCounter <$> get     nameCounter .= max nc' nc''     return $ CondStmnt expr (Just tstat) (Just fstat) @@ -408,7 +402,7 @@ statement :: StateGen Statement statement = do     prob <- askProbability-    cont <- lget+    cont <- get     let defProb i = prob ^. probStmnt . i     Hog.frequency         [ (defProb probStmntBlock              , BlockAssign <$> assignment)@@ -442,13 +436,13 @@ -- representation for the clock. instantiate :: ModDecl -> StateGen ModItem instantiate (ModDecl i outP inP _ _) = do-    context <- lget+    context <- get     outs    <- replicateM (length outP) (nextPort Wire)     ins <- take (length inpFixed) <$> Hog.shuffle (context ^. variables)     insLit <- replicateM (length inpFixed - length ins) (Number <$> genBitVec)     mapM_ (uncurry process) . zip (ins ^.. traverse . portName) $ inpFixed ^.. traverse . portSize     ident <- makeIdentifier "modinst"-    vs <- view variables <$> lget+    vs <- view variables <$> get     Hog.choice         [ return . ModInst i ident $ ModConn <$> (toE (outs <> clkPort <> ins) <> insLit)         , ModInst i ident <$> Hog.shuffle@@ -462,7 +456,7 @@             | n == "clk" = False             | otherwise = True         process p r = do-            params <- view parameters <$> lget+            params <- view parameters <$> get             variables %= resizePort params p r  -- | Generates a module instance by also generating a new module if there are@@ -486,8 +480,8 @@ -- a module from a context or generating a new one. modInst :: StateGen ModItem modInst = do-    prob    <- rask-    context <- lget+    prob    <- ask+    context <- get     let maxMods = prob ^. configProperty . propMaxModules     if length (context ^. modules) < maxMods         then do@@ -499,7 +493,7 @@             parameters .= []             modDepth -= 1             chosenMod <- moduleDef Nothing-            ncont     <- lget+            ncont     <- get             let genMods = ncont ^. modules             modDepth += 1             parameters .= params@@ -511,9 +505,9 @@ -- | Generate a random module item. modItem :: StateGen ModItem modItem = do-    conf    <- rask+    conf    <- ask     let prob = conf ^. configProbability-    context <- lget+    context <- get     let defProb i = prob ^. probModItem . i     det <- Hog.frequency [ (conf ^. configProperty . propDeterminism, return True)                          , (conf ^. configProperty . propNonDeterminism, return False) ]@@ -535,7 +529,7 @@ constExpr :: StateGen ConstExpr constExpr = do     prob    <- askProbability-    context <- lget+    context <- get     Hog.sized $ constExprWithContext (context ^. parameters)                                            (prob ^. probExpr) @@ -576,8 +570,8 @@     portList <- Hog.list (Hog.linear 4 10) $ nextPort Wire     mi       <- Hog.list (Hog.linear 4 100) modItem     ps       <- Hog.list (Hog.linear 0 10) parameter-    context  <- lget-    config   <- rask+    context  <- get+    config   <- ask     let (newPorts, local) = partition (`identElem` portList) $ _variables context     let          size =

@@ -0,0 +1,299 @@+module Verismith.OptParser+    ( OptTool (..)+    , Opts (..)+    , opts+    )+where++import           Control.Applicative ((<|>))+import           Data.Text           (Text)+import qualified Data.Text           as T+import           Options.Applicative (Mod (..), OptionFields (..), Parser (..),+                                      ParserInfo (..), ReadM (..), (<**>))+import qualified Options.Applicative as Opt+import           Prelude             hiding (FilePath (..))+import           Shelly              (FilePath (..), fromText)+import           Verismith.Config    (SynthDescription (..), versionInfo)++data OptTool = TYosys+             | TXST+             | TIcarus++instance Show OptTool where+  show TYosys  = "yosys"+  show TXST    = "xst"+  show TIcarus = "icarus"++data Opts = Fuzz { fuzzOutput          :: {-# UNPACK #-} !Text+                 , fuzzConfigFile      :: !(Maybe FilePath)+                 , fuzzForced          :: !Bool+                 , fuzzKeepAll         :: !Bool+                 , fuzzNum             :: {-# UNPACK #-} !Int+                 , fuzzNoSim           :: !Bool+                 , fuzzNoEquiv         :: !Bool+                 , fuzzNoReduction     :: !Bool+                 , fuzzExistingFile    :: !(Maybe FilePath)+                 , fuzzExistingFileTop :: !Text+                 , fuzzCrossCheck      :: !Bool+                 }+          | Generate { generateFilename   :: !(Maybe FilePath)+                     , generateConfigFile :: !(Maybe FilePath)+                     }+          | Parse { parseFilename            :: {-# UNPACK #-} !FilePath+                  , parseTop                 :: {-# UNPACK #-} !Text+                  , parseOutput              :: !(Maybe FilePath)+                  , parseRemoveConstInConcat :: !Bool+                  }+          | Reduce { reduceFilename        :: {-# UNPACK #-} !FilePath+                   , reduceTop             :: {-# UNPACK #-} !Text+                   , reduceScript          :: !(Maybe FilePath)+                   , reduceSynthesiserDesc :: ![SynthDescription]+                   , reduceRerun           :: !Bool+                   }+          | ConfigOpt { configOptWriteConfig :: !(Maybe FilePath)+                      , configOptConfigFile  :: !(Maybe FilePath)+                      , configOptDoRandomise :: !Bool+                      }++textOption :: Mod OptionFields String -> Parser Text+textOption = fmap T.pack . Opt.strOption++optReader :: (String -> Maybe a) -> ReadM a+optReader f = Opt.eitherReader $ \arg -> case f arg of+    Just a  -> Right a+    Nothing -> Left $ "Cannot parse option: " <> arg++parseSynth :: String -> Maybe OptTool+parseSynth val | val == "yosys" = Just TYosys+               | val == "xst"   = Just TXST+               | otherwise      = Nothing++parseSynthDesc :: String -> Maybe SynthDescription+parseSynthDesc val+    | val == "yosys" = Just $ SynthDescription "yosys" Nothing Nothing Nothing+    | val == "vivado" = Just $ SynthDescription "vivado" Nothing Nothing Nothing+    | val == "xst" = Just $ SynthDescription "xst" Nothing Nothing Nothing+    | val == "quartus" = Just+    $ SynthDescription "quartus" Nothing Nothing Nothing+    | val == "identity" = Just+    $ SynthDescription "identity" Nothing Nothing Nothing+    | otherwise = Nothing++parseSim :: String -> Maybe OptTool+parseSim val | val == "icarus" = Just TIcarus+             | otherwise       = Nothing++fuzzOpts :: Parser Opts+fuzzOpts =+    Fuzz+        <$> textOption+                (  Opt.long "output"+                <> Opt.short 'o'+                <> Opt.metavar "DIR"+                <> Opt.help "Output directory that the fuzz run takes place in."+                <> Opt.showDefault+                <> Opt.value "output")+        <*> (  Opt.optional+            .  Opt.strOption+            $  Opt.long "config"+            <> Opt.short 'c'+            <> Opt.metavar "FILE"+            <> Opt.help "Config file for the current fuzz run.")+        <*> (Opt.switch $ Opt.long "force" <> Opt.short 'f' <> Opt.help+                "Overwrite the specified directory.")+        <*> (Opt.switch $ Opt.long "keep" <> Opt.short 'k' <> Opt.help+                "Keep all the directories.")+        <*> (  Opt.option Opt.auto+            $  Opt.long "num"+            <> Opt.short 'n'+            <> Opt.help "The number of fuzz runs that should be performed."+            <> Opt.showDefault+            <> Opt.value 1+            <> Opt.metavar "INT")+        <*> (Opt.switch $ Opt.long "no-sim" <> Opt.help+                "Do not run simulation on the output netlist.")+        <*> (Opt.switch $ Opt.long "no-equiv" <> Opt.help+                "Do not run an equivalence check on the output netlist.")+        <*> (Opt.switch $ Opt.long "no-reduction" <> Opt.help+                "Do not run reduction on a failed testcase.")+        <*> (  Opt.optional+            .  Opt.strOption+            $  Opt.long "source"+            <> Opt.short 's'+            <> Opt.metavar "FILE"+            <> Opt.help "Name of the top module.")+        <*> textOption+                (  Opt.long "source-top"+                <> Opt.short 't'+                <> Opt.metavar "TOP"+                <> Opt.help "Define the top module for the source file."+                <> Opt.showDefault+                <> Opt.value "top")+        <*> (Opt.switch $ Opt.long "crosscheck" <> Opt.help+                "Do not only compare against the original design, but also against other netlists.")++genOpts :: Parser Opts+genOpts =+    Generate+        <$> (  Opt.optional+            .  Opt.strOption+            $  Opt.long "output"+            <> Opt.short 'o'+            <> Opt.metavar "FILE"+            <> Opt.help "Output to a verilog file instead."+            )+        <*> (  Opt.optional+            .  Opt.strOption+            $  Opt.long "config"+            <> Opt.short 'c'+            <> Opt.metavar "FILE"+            <> Opt.help "Config file for the generation run."+            )++parseOpts :: Parser Opts+parseOpts = Parse+    <$> (fromText . T.pack <$> Opt.strArgument+            (Opt.metavar "FILE" <> Opt.help "Verilog input file."))+    <*> textOption ( Opt.short 't'+                     <> Opt.long "top"+                     <> Opt.metavar "TOP"+                     <> Opt.help "Name of top level module."+                     <> Opt.showDefault+                     <> Opt.value "top"+                   )+    <*> ( Opt.optional+          . Opt.strOption+          $ Opt.long "output"+          <> Opt.short 'o'+          <> Opt.metavar "FILE"+          <> Opt.help "Output file to write the parsed file to.")+    <*> (Opt.switch $ Opt.long "remove-const-in-concat" <> Opt.help+            "Remove constants in concatenation to simplify the Verilog.")++reduceOpts :: Parser Opts+reduceOpts =+    Reduce+        .   fromText+        .   T.pack+        <$> Opt.strArgument (Opt.metavar "FILE" <> Opt.help "Verilog input file.")+        <*> textOption+                (  Opt.short 't'+                <> Opt.long "top"+                <> Opt.metavar "TOP"+                <> Opt.help "Name of top level module."+                <> Opt.showDefault+                <> Opt.value "top"+                )+        <*> (  Opt.optional+            .  Opt.strOption+            $  Opt.long "script"+            <> Opt.metavar "SCRIPT"+            <> Opt.help+                   "Script that determines if the current file is interesting, which is determined by the script returning 0."+            )+        <*> (  Opt.many+            .  Opt.option (optReader parseSynthDesc)+            $  Opt.short 's'+            <> Opt.long "synth"+            <> Opt.metavar "SYNTH"+            <> Opt.help "Specify synthesiser to use."+            )+        <*> (  Opt.switch+            $  Opt.short 'r'+            <> Opt.long "rerun"+            <> Opt.help+                   "Only rerun the current synthesis file with all the synthesisers."+            )++configOpts :: Parser Opts+configOpts =+    ConfigOpt+        <$> (  Opt.optional+            .  Opt.strOption+            $  Opt.long "output"+            <> Opt.short 'o'+            <> Opt.metavar "FILE"+            <> Opt.help "Output to a TOML Config file."+            )+        <*> (  Opt.optional+            .  Opt.strOption+            $  Opt.long "config"+            <> Opt.short 'c'+            <> Opt.metavar "FILE"+            <> Opt.help "Config file for the current fuzz run."+            )+        <*> (  Opt.switch+            $  Opt.long "randomise"+            <> Opt.short 'r'+            <> Opt.help+                   "Randomise the given default config, or the default config by randomly switchin on and off options."+            )++argparse :: Parser Opts+argparse =+    Opt.hsubparser+            (  Opt.command+                    "fuzz"+                    (Opt.info+                        fuzzOpts+                        (Opt.progDesc+                            "Run fuzzing on the specified simulators and synthesisers."+                        )+                    )+            <> Opt.metavar "fuzz"+            )+        <|> Opt.hsubparser+                (  Opt.command+                        "generate"+                        (Opt.info+                            genOpts+                            (Opt.progDesc "Generate a random Verilog program.")+                        )+                <> Opt.metavar "generate"+                )+        <|> Opt.hsubparser+                (  Opt.command+                        "parse"+                        (Opt.info+                            parseOpts+                            (Opt.progDesc+                                "Parse a verilog file and output a pretty printed version."+                            )+                        )+                <> Opt.metavar "parse"+                )+        <|> Opt.hsubparser+                (  Opt.command+                        "reduce"+                        (Opt.info+                            reduceOpts+                            (Opt.progDesc+                                "Reduce a Verilog file by rerunning the fuzzer on the file."+                            )+                        )+                <> Opt.metavar "reduce"+                )+        <|> Opt.hsubparser+                (  Opt.command+                        "config"+                        (Opt.info+                            configOpts+                            (Opt.progDesc+                                "Print the current configuration of the fuzzer."+                            )+                        )+                <> Opt.metavar "config"+                )++version :: Parser (a -> a)+version = Opt.infoOption versionInfo $ mconcat+    [Opt.long "version", Opt.short 'v', Opt.help "Show version information.", Opt.hidden]++opts :: ParserInfo Opts+opts = Opt.info+    (argparse <**> Opt.helper <**> version)+    (  Opt.fullDesc+    <> Opt.progDesc "Fuzz different simulators and synthesisers."+    <> Opt.header+           "Verismith - A hardware simulator and synthesiser Verilog fuzzer."+    )

@@ -18,6 +18,7 @@       reduceWithScript     , reduceSynth     , reduceSynthesis+    , reduceSimIc     , reduce     , reduce_     , Replacement(..)@@ -31,6 +32,8 @@     , cleanSourceInfo     , cleanSourceInfoAll     , removeDecl+    , removeConstInConcat+    , takeReplace     , filterExpr     ) where@@ -38,18 +41,21 @@ import           Control.Lens             hiding ((<.>)) import           Control.Monad            (void) import           Control.Monad.IO.Class   (MonadIO, liftIO)+import           Data.ByteString          (ByteString) import           Data.Foldable            (foldrM) import           Data.List                (nub) import           Data.List.NonEmpty       (NonEmpty (..)) import qualified Data.List.NonEmpty       as NonEmpty import           Data.Maybe               (mapMaybe) import           Data.Text                (Text)-import           Shelly                   ((<.>))+import           Shelly                   (fromText, (<.>)) import qualified Shelly-import           Shelly.Lifted            (MonadSh, liftSh)+import           Shelly.Lifted            (MonadSh, liftSh, rm_rf, writefile) import           Verismith.Internal import           Verismith.Result import           Verismith.Tool+import           Verismith.Tool.Icarus+import           Verismith.Tool.Identity import           Verismith.Tool.Internal import           Verismith.Verilog import           Verismith.Verilog.AST@@ -156,6 +162,21 @@ clean :: (Mutate a) => [Identifier] -> a -> a clean ids = mutExpr (transform $ filterExpr ids) +takeReplace :: (Monoid a) => Replacement a -> a+takeReplace (Single a) = a+takeReplace (Dual a _) = a+takeReplace None       = mempty++removeConstInConcat :: Replace SourceInfo+removeConstInConcat = Single . mutExpr replace+  where+    replace :: Expr -> Expr+    replace (Concat expr) = maybe (Number 0) Concat . NonEmpty.nonEmpty+                            $ NonEmpty.filter notConstant expr+    replace e             = e+    notConstant (Number _) = False+    notConstant _          = True+ cleanUndefined :: [Identifier] -> [ModItem] -> [ModItem] cleanUndefined ids mis = clean usedWires mis   where@@ -496,13 +517,15 @@ -- | Reduction using custom reduction strategies. reduce_     :: MonadSh m-    => Text+    => Shelly.FilePath+    -> Text     -> Replace SourceInfo     -> (SourceInfo -> Bool)     -> (SourceInfo -> m Bool)     -> SourceInfo     -> m SourceInfo-reduce_ title repl bot eval src = do+reduce_ out title repl bot eval src = do+    writefile out $ genSource src     liftSh         .  Shelly.echo         $  "Reducing "@@ -535,24 +558,26 @@             None -> return src   where     cond s = s /= src-    recReduction = reduce_ title repl bot eval+    recReduction = reduce_ out title repl bot eval  -- | Reduce an input to a minimal representation. It follows the reduction -- strategy mentioned above. reduce     :: MonadSh m-    => (SourceInfo -> m Bool) -- ^ Failed or not.+    => Shelly.FilePath -- ^ Filepath for temporary file.+    -> (SourceInfo -> m Bool) -- ^ Failed or not.     -> SourceInfo              -- ^ Input verilog source to be reduced.     -> m SourceInfo           -- ^ Reduced output.-reduce eval src =+reduce fp eval src =     fmap removeDecl         $   red "Modules" moduleBot halveModules src-        >>= redAll "Module Items" modItemBot         halveModItems+        >>= redAll "Module items" modItemBot         halveModItems         >>= redAll "Statements"   (const defaultBot) halveStatements         -- >>= redAll "Expressions"  (const defaultBot) halveExpr+        >>= red "Remove constants in concat" defaultBot removeConstInConcat   where-    red s bot a = reduce_ s a bot eval-    red' s bot a t = reduce_ s (a t) (bot t) eval+    red s bot a = reduce_ fp s a bot eval+    red' s bot a t = reduce_ fp s (a t) (bot t) eval     redAll s bot halve' src' = foldrM         (\t -> red' (s <> " (" <> getIdentifier t <> ")") bot halve' t)         src'@@ -577,33 +602,53 @@ reduceWithScript top script file = do     liftSh . Shelly.cp file $ file <.> "original"     srcInfo <- liftIO . parseSourceInfoFile top $ Shelly.toTextIgnore file-    void $ reduce (runScript script file) srcInfo+    void $ reduce (fromText "reduce_script.v") (runScript script file) srcInfo  -- | Reduce a 'SourceInfo' using two 'Synthesiser' that are passed to it. reduceSynth     :: (Synthesiser a, Synthesiser b, MonadSh m)-    => a+    => Shelly.FilePath+    -> a     -> b     -> SourceInfo     -> m SourceInfo-reduceSynth a b = reduce synth+reduceSynth datadir a b = reduce (fromText $ "reduce_" <> toText a <> "_" <> toText b <> ".v") synth   where     synth src' = liftSh $ do         r <- runResultT $ do             runSynth a src'             runSynth b src'-            runEquiv a b src'+            runEquiv datadir a b src'         return $ case r of-            Fail EquivFail -> True-            Fail _         -> False-            Pass _         -> False+            Fail (EquivFail _) -> True+            _                  -> False  reduceSynthesis :: (Synthesiser a, MonadSh m) => a -> SourceInfo -> m SourceInfo-reduceSynthesis a = reduce synth+reduceSynthesis a = reduce (fromText $ "reduce_" <> toText a <> ".v") synth   where     synth src = liftSh $ do         r <- runResultT $ runSynth a src         return $ case r of             Fail SynthFail -> True-            Fail _         -> False-            Pass _         -> False+            _              -> False++runInTmp :: Shelly.Sh a -> Shelly.Sh a+runInTmp a = Shelly.withTmpDir $ (\f -> do+    dir <- Shelly.pwd+    Shelly.cd f+    r <- a+    Shelly.cd dir+    return r)++reduceSimIc :: (Synthesiser a, MonadSh m) => Shelly.FilePath -> [ByteString] -> a -> SourceInfo -> m SourceInfo+reduceSimIc fp bs a = reduce (fromText $ "reduce_sim_" <> toText a <> ".v") synth+  where+    synth src = liftSh . runInTmp $ do+        r <- runResultT $ do+            runSynth a src+            runSynth defaultIdentity src+            i <- runSimIc fp defaultIcarus defaultIdentity src bs Nothing+            runSimIc fp defaultIcarus a src bs $ Just i+        return $ case r of+            Fail (SimFail _) -> True+            _                -> False

@@ -35,6 +35,7 @@     , defaultYosysSynth     , defaultXSTSynth     , defaultQuartusSynth+    , defaultQuartusLightSynth     , defaultIdentitySynth     , descriptionToSim     , descriptionToSynth@@ -76,47 +77,54 @@                | VivadoSynth {-# UNPACK #-} !Vivado                | YosysSynth {-# UNPACK #-} !Yosys                | QuartusSynth {-# UNPACK #-} !Quartus+               | QuartusLightSynth {-# UNPACK #-} !QuartusLight                | IdentitySynth {-# UNPACK #-} !Identity                deriving (Eq)  instance NFData SynthTool where-    rnf (XSTSynth a)      = rnf a-    rnf (VivadoSynth a)   = rnf a-    rnf (YosysSynth a)    = rnf a-    rnf (QuartusSynth a)  = rnf a-    rnf (IdentitySynth a) = rnf a+    rnf (XSTSynth a)          = rnf a+    rnf (VivadoSynth a)       = rnf a+    rnf (YosysSynth a)        = rnf a+    rnf (QuartusSynth a)      = rnf a+    rnf (QuartusLightSynth a) = rnf a+    rnf (IdentitySynth a)     = rnf a  instance Show SynthTool where-    show (XSTSynth xst)           = show xst-    show (VivadoSynth vivado)     = show vivado-    show (YosysSynth yosys)       = show yosys-    show (QuartusSynth quartus)   = show quartus-    show (IdentitySynth identity) = show identity+    show (XSTSynth xst)              = show xst+    show (VivadoSynth vivado)        = show vivado+    show (YosysSynth yosys)          = show yosys+    show (QuartusSynth quartus)      = show quartus+    show (QuartusLightSynth quartus) = show quartus+    show (IdentitySynth identity)    = show identity  instance Tool SynthTool where-    toText (XSTSynth xst)           = toText xst-    toText (VivadoSynth vivado)     = toText vivado-    toText (YosysSynth yosys)       = toText yosys-    toText (QuartusSynth quartus)   = toText quartus-    toText (IdentitySynth identity) = toText identity+    toText (XSTSynth xst)              = toText xst+    toText (VivadoSynth vivado)        = toText vivado+    toText (YosysSynth yosys)          = toText yosys+    toText (QuartusSynth quartus)      = toText quartus+    toText (QuartusLightSynth quartus) = toText quartus+    toText (IdentitySynth identity)    = toText identity  instance Synthesiser SynthTool where-    runSynth (XSTSynth xst)           = runSynth xst-    runSynth (VivadoSynth vivado)     = runSynth vivado-    runSynth (YosysSynth yosys)       = runSynth yosys-    runSynth (QuartusSynth quartus)   = runSynth quartus-    runSynth (IdentitySynth identity) = runSynth identity+    runSynth (XSTSynth xst)              = runSynth xst+    runSynth (VivadoSynth vivado)        = runSynth vivado+    runSynth (YosysSynth yosys)          = runSynth yosys+    runSynth (QuartusSynth quartus)      = runSynth quartus+    runSynth (QuartusLightSynth quartus) = runSynth quartus+    runSynth (IdentitySynth identity)    = runSynth identity -    synthOutput (XSTSynth xst)           = synthOutput xst-    synthOutput (VivadoSynth vivado)     = synthOutput vivado-    synthOutput (YosysSynth yosys)       = synthOutput yosys-    synthOutput (QuartusSynth quartus)   = synthOutput quartus-    synthOutput (IdentitySynth identity) = synthOutput identity+    synthOutput (XSTSynth xst)              = synthOutput xst+    synthOutput (VivadoSynth vivado)        = synthOutput vivado+    synthOutput (YosysSynth yosys)          = synthOutput yosys+    synthOutput (QuartusSynth quartus)      = synthOutput quartus+    synthOutput (QuartusLightSynth quartus) = synthOutput quartus+    synthOutput (IdentitySynth identity)    = synthOutput identity      setSynthOutput (YosysSynth yosys)     = YosysSynth . setSynthOutput yosys     setSynthOutput (XSTSynth xst)         = XSTSynth . setSynthOutput xst     setSynthOutput (VivadoSynth vivado)   = VivadoSynth . setSynthOutput vivado     setSynthOutput (QuartusSynth quartus) = QuartusSynth . setSynthOutput quartus+    setSynthOutput (QuartusLightSynth quartus) = QuartusLightSynth . setSynthOutput quartus     setSynthOutput (IdentitySynth identity) = IdentitySynth . setSynthOutput identity  defaultYosysSynth :: SynthTool@@ -125,6 +133,9 @@ defaultQuartusSynth :: SynthTool defaultQuartusSynth = QuartusSynth defaultQuartus +defaultQuartusLightSynth :: SynthTool+defaultQuartusLightSynth = QuartusLightSynth defaultQuartusLight+ defaultVivadoSynth :: SynthTool defaultVivadoSynth = VivadoSynth defaultVivado @@ -155,15 +166,15 @@  -- | The results from running a tool through a simulator. It can either fail or -- return a result, which is most likely a 'ByteString'.-data SimResult = SimResult !SynthTool !SimTool !BResult !NominalDiffTime+data SimResult = SimResult !SynthTool !SimTool ![ByteString] !BResult !NominalDiffTime                  deriving (Eq)  instance Show SimResult where-    show (SimResult synth sim r d) = show synth <> ", " <> show sim <> ": " <> show (bimap show (T.unpack . showBS) r) <> " (" <> show d <> ")"+    show (SimResult synth sim _ r d) = show synth <> ", " <> show sim <> ": " <> show (bimap show (T.unpack . showBS) r) <> " (" <> show d <> ")"  getSimResult :: SimResult -> UResult-getSimResult (SimResult _ _ (Pass _) _) = Pass ()-getSimResult (SimResult _ _ (Fail b) _) = Fail b+getSimResult (SimResult _ _ _ (Pass _) _) = Pass ()+getSimResult (SimResult _ _ _ (Fail b) _) = Fail b  -- | The results of comparing the synthesised outputs of two files using a -- formal equivalence checker. This will either return a failure or an output@@ -228,6 +239,11 @@         . Quartus (fromText <$> bin)                   (fromMaybe (quartusDesc defaultQuartus) desc)         $ maybe (quartusOutput defaultQuartus) fromText out+descriptionToSynth (SynthDescription "quartuslight" bin desc out) =+    QuartusLightSynth+        . QuartusLight (fromText <$> bin)+                  (fromMaybe (quartusDesc defaultQuartus) desc)+        $ maybe (quartusOutput defaultQuartus) fromText out descriptionToSynth (SynthDescription "identity" _ desc out) =     IdentitySynth         . Identity (fromMaybe (identityDesc defaultIdentity) desc)@@ -236,13 +252,13 @@     error $ "Could not find implementation for synthesiser '" <> show s <> "'"  status :: Result Failed () -> Html-status (Pass _           ) = H.td ! A.class_ "is-success" $ "Passed"-status (Fail EmptyFail   ) = H.td ! A.class_ "is-danger" $ "Failed"-status (Fail EquivFail   ) = H.td ! A.class_ "is-danger" $ "Equivalence failed"-status (Fail SimFail     ) = H.td ! A.class_ "is-danger" $ "Simulation failed"-status (Fail SynthFail   ) = H.td ! A.class_ "is-danger" $ "Synthesis failed"-status (Fail EquivError  ) = H.td ! A.class_ "is-danger" $ "Equivalence error"-status (Fail TimeoutError) = H.td ! A.class_ "is-warning" $ "Time out"+status (Pass _           )  = H.td ! A.class_ "is-success" $ "Passed"+status (Fail EmptyFail   )  = H.td ! A.class_ "is-danger" $ "Failed"+status (Fail (EquivFail _)) = H.td ! A.class_ "is-danger" $ "Equivalence failed"+status (Fail (SimFail  _))  = H.td ! A.class_ "is-danger" $ "Simulation failed"+status (Fail SynthFail   )  = H.td ! A.class_ "is-danger" $ "Synthesis failed"+status (Fail EquivError  )  = H.td ! A.class_ "is-danger" $ "Equivalence error"+status (Fail TimeoutError)  = H.td ! A.class_ "is-warning" $ "Time out"  synthStatusHtml :: SynthStatus -> Html synthStatusHtml (SynthStatus synth res diff) = H.tr $ do

@@ -22,6 +22,8 @@ module Verismith.Result     ( Result(..)     , ResultT(..)+    , justPass+    , justFail     , (<?>)     , annotate     )@@ -41,6 +43,14 @@ data Result a b = Fail a                 | Pass b                 deriving (Eq, Show)++justPass :: Result a b -> Maybe b+justPass (Fail _) = Nothing+justPass (Pass a) = Just a++justFail :: Result a b -> Maybe a+justFail (Pass _) = Nothing+justFail (Fail a) = Just a  instance Semigroup (Result a b) where     Pass _ <> a = a

@@ -29,6 +29,9 @@     -- ** Quartus     , Quartus(..)     , defaultQuartus+    -- ** Quartus Light+    , QuartusLight(..)+    , defaultQuartusLight     -- ** Identity     , Identity(..)     , defaultIdentity@@ -46,6 +49,7 @@ import           Verismith.Tool.Identity import           Verismith.Tool.Internal import           Verismith.Tool.Quartus+import           Verismith.Tool.QuartusLight import           Verismith.Tool.Vivado import           Verismith.Tool.XST import           Verismith.Tool.Yosys

@@ -14,6 +14,7 @@     ( Icarus(..)     , defaultIcarus     , runSimIc+    , runSimIcEC     ) where @@ -39,6 +40,8 @@ import           Prelude                    hiding (FilePath) import           Shelly import           Shelly.Lifted              (liftSh)+import           Verismith.CounterEg        (CounterEg (..))+import           Verismith.Result import           Verismith.Tool.Internal import           Verismith.Tool.Template import           Verismith.Verilog.AST@@ -114,12 +117,12 @@     let newtb     = instantiateMod m tb     let modWithTb = Verilog [newtb, m]     liftSh . writefile "main.v" $ genSource modWithTb-    annotate SimFail $ runSimWithFile sim "main.v" bss+    annotate (SimFail mempty) $ runSimWithFile sim "main.v" bss     where m = rinfo ^. mainModule  runSimIcarusWithFile     :: Icarus -> FilePath -> [ByteString] -> ResultSh ByteString-runSimIcarusWithFile sim f _ = annotate SimFail . liftSh $ do+runSimIcarusWithFile sim f _ = annotate (SimFail mempty) . liftSh $ do     dir <- pwd     logCommand_ dir "icarus"         $ run (icarusPath sim) ["-o", "main", toTextIgnore f]@@ -131,48 +134,46 @@ fromBytes :: ByteString -> Integer fromBytes = B.foldl' f 0 where f a b = a `shiftL` 8 .|. fromIntegral b -runSimIc-    :: (Synthesiser b)-    => Icarus-    -> b-    -> SourceInfo-    -> [ByteString]-    -> ResultSh ByteString-runSimIc sim1 synth1 srcInfo bss = do-    dir <- liftSh pwd-    let top      = srcInfo ^. mainModule-    let inConcat = (RegConcat (Id . fromPort <$> (top ^. modInPorts)))-    let-        tb = instantiateMod top $ ModDecl-            "testbench"-            []-            []-            [ Initial-            $  fold-                   [ BlockAssign (Assign "clk" Nothing 0)-                   , BlockAssign (Assign inConcat Nothing 0)-                   ]-            <> fold-                   (   (\r -> TimeCtrl-                           10-                           (Just $ BlockAssign (Assign inConcat Nothing r))-                       )-                   .   fromInteger-                   .   fromBytes-                   <$> bss-                   )-            <> (SysTaskEnable $ Task "finish" [])-            , Always . TimeCtrl 5 . Just $ BlockAssign+tbModule :: [ByteString] -> ModDecl -> Verilog+tbModule bss top =+    Verilog [ instantiateMod top $ ModDecl "testbench" [] []+              [ Initial+                $  fold [ BlockAssign (Assign "clk" Nothing 0)+                        , BlockAssign (Assign inConcat Nothing 0)+                        ]+                <> fold ((\r -> TimeCtrl 10+                             (Just $ BlockAssign (Assign inConcat Nothing r)))+                         . fromInteger . fromBytes <$> bss)+                <> (TimeCtrl 10 . Just . SysTaskEnable $ Task "finish" [])+              , Always . TimeCtrl 5 . Just $ BlockAssign                 (Assign "clk" Nothing (UnOp UnNot (Id "clk")))-            , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable $ Task-                "strobe"-                ["%b", Id "y"]+              , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable+                $ Task "strobe" ["%b", Id "y"]+              ] []             ]-            []+  where+    inConcat = (RegConcat . filter (/= (Id "clk")) $ (Id . fromPort <$> (top ^. modInPorts))) -    liftSh . writefile "testbench.v" $ icarusTestbench (Verilog [tb]) synth1-    liftSh $ exe dir "icarus" "iverilog" ["-o", "main", "testbench.v"]-    liftSh+counterTestBench :: CounterEg -> ModDecl -> Verilog+counterTestBench (CounterEg _ states) m = tbModule filtered m+  where+    filtered = convert . fold . fmap snd . filter ((/= "clk") . fst) <$> states++runSimIc' :: (Synthesiser b) => ([ByteString] -> ModDecl -> Verilog)+          -> FilePath+          -> Icarus+          -> b+          -> SourceInfo+          -> [ByteString]+          -> Maybe ByteString+          -> ResultSh ByteString+runSimIc' fun datadir sim1 synth1 srcInfo bss bs = do+    dir <- liftSh pwd+    let top      = srcInfo ^. mainModule+    let tb = fun bss top+    liftSh . writefile tbname $ icarusTestbench datadir tb synth1+    liftSh $ exe dir "icarus" "iverilog" ["-o", exename, toTextIgnore tbname]+    s <- liftSh         $   B.take 8         .   BA.convert         .   (hash :: ByteString -> Digest SHA256)@@ -182,7 +183,29 @@                 (runFoldLines (mempty :: ByteString)                               callback                               (vvpPath sim1)-                              ["main"]-                )+                              [exename])+    case (bs, s) of+        (Nothing, s') -> ResultT . return $ Pass s'+        (Just bs', s') -> if bs' == s'+                    then ResultT . return $ Pass s'+                    else ResultT . return $ Fail (SimFail s')   where     exe dir name e = void . errExit False . logCommand dir name . timeout e+    tbname = fromText $ toText synth1 <> "_testbench.v"+    exename = toText synth1 <> "_main"++runSimIc :: (Synthesiser b)+         => FilePath         -- ^ Data directory.+         -> Icarus           -- ^ Icarus simulator.+         -> b                -- ^ Synthesis tool to be tested.+         -> SourceInfo       -- ^ Original generated program to test.+         -> [ByteString]     -- ^ Test vectors to be passed as inputs to the generated Verilog.+         -> Maybe ByteString -- ^ What the correct output should be. If+                             -- 'Nothing' is passed, then just return 'Pass+                             -- ByteString' with the answer.+         -> ResultSh ByteString+runSimIc = runSimIc' tbModule++runSimIcEC :: (Synthesiser b) => FilePath -> Icarus -> b+           -> SourceInfo -> CounterEg -> Maybe ByteString -> ResultSh ByteString+runSimIcEC a b c d e = runSimIc' (const $ counterTestBench e) a b c d []

@@ -54,6 +54,7 @@ import           Shelly import           Shelly.Lifted         (MonadSh, liftSh) import           System.FilePath.Posix (takeBaseName)+import           Verismith.CounterEg   (CounterEg) import           Verismith.Internal import           Verismith.Result import           Verismith.Verilog.AST@@ -74,12 +75,20 @@                  -> ResultSh ByteString  data Failed = EmptyFail-            | EquivFail+            | EquivFail CounterEg             | EquivError-            | SimFail+            | SimFail ByteString             | SynthFail             | TimeoutError-            deriving (Eq, Show)+            deriving (Eq)++instance Show Failed where+    show EmptyFail     = "EmptyFail"+    show (EquivFail _) = "EquivFail"+    show EquivError    = "EquivError"+    show (SimFail bs)  = "SimFail " <> T.unpack (T.take 10 $ showBS bs)+    show SynthFail     = "SynthFail"+    show TimeoutError  = "TimeoutError"  instance Semigroup Failed where     EmptyFail <> a = a

@@ -22,6 +22,7 @@ import           Shelly import           Shelly.Lifted             (liftSh) import           Verismith.Tool.Internal+import           Verismith.Tool.Template import           Verismith.Verilog.AST import           Verismith.Verilog.CodeGen @@ -52,18 +53,16 @@ runSynthQuartus sim (SourceInfo top src) = do     dir <- liftSh pwd     let ex = execute_ SynthFail dir "quartus"-    liftSh . writefile inpf $ genSource src-    liftSh . noPrint $ run_-        "sed"-        [ "-i"-        , "s/^module/(* multstyle = \"logic\" *) module/;"-        , toTextIgnore inpf-        ]-    ex (exec "quartus_map")-       [top, "--source=" <> toTextIgnore inpf, "--family=Cyclone V"]-    ex (exec "quartus_fit") [top, "--part=5CGXFC7D6F31C6"]-    ex (exec "quartus_eda") [top, "--simulation", "--tool=vcs"]     liftSh $ do+        writefile inpf $ genSource src+        noPrint $ run_ "sed" [ "-i"+                             , "s/^module/(* multstyle = \"logic\" *) module/;"+                             , toTextIgnore inpf+                             ]+        writefile quartusSdc $ "create_clock -period 5 -name clk [get_ports clock]"+        writefile quartusTcl $ quartusSynthConfig sim quartusSdc top inpf+    ex (exec "quartus_sh") ["-t", toTextIgnore quartusTcl]+    liftSh $ do         cp (fromText "simulation/vcs" </> fromText top <.> "vo")             $ synthOutput sim         run_@@ -75,3 +74,5 @@   where     inpf = "rtl.v"     exec s = maybe (fromText s) (</> fromText s) $ quartusBin sim+    quartusTcl = fromText top <.> "tcl"+    quartusSdc = fromText top <.> "sdc"

@@ -0,0 +1,78 @@+{-|+Module      : Verismith.Tool.QuartusLight+Description : QuartusLight synthesiser implementation.+Copyright   : (c) 2019, Yann Herklotz Grave+License     : GPL-3+Maintainer  : yann [at] yannherklotz [dot] com+Stability   : experimental+Portability : POSIX++QuartusLight synthesiser implementation.+-}++module Verismith.Tool.QuartusLight+    ( QuartusLight(..)+    , defaultQuartusLight+    )+where++import           Control.DeepSeq           (NFData, rnf, rwhnf)+import           Data.Text                 (Text, unpack)+import           Prelude                   hiding (FilePath)+import           Shelly+import           Shelly.Lifted             (liftSh)+import           Verismith.Tool.Internal+import           Verismith.Tool.Template+import           Verismith.Verilog.AST+import           Verismith.Verilog.CodeGen++data QuartusLight = QuartusLight { quartusLightBin    :: !(Maybe FilePath)+                                 , quartusLightDesc   :: {-# UNPACK #-} !Text+                                 , quartusLightOutput :: {-# UNPACK #-} !FilePath+                                 }+                  deriving (Eq)++instance Tool QuartusLight where+    toText (QuartusLight _ t _) = t++instance Show QuartusLight where+    show t = unpack $ toText t++instance Synthesiser QuartusLight where+    runSynth = runSynthQuartusLight+    synthOutput = quartusLightOutput+    setSynthOutput (QuartusLight a b _) = QuartusLight a b++instance NFData QuartusLight where+    rnf = rwhnf++defaultQuartusLight :: QuartusLight+defaultQuartusLight = QuartusLight Nothing "quartus" "syn_quartus.v"++runSynthQuartusLight :: QuartusLight -> SourceInfo -> ResultSh ()+runSynthQuartusLight sim (SourceInfo top src) = do+    dir <- liftSh pwd+    let ex = execute_ SynthFail dir "quartus"+    liftSh $ do+        writefile inpf $ genSource src+        noPrint $ run_ "sed" [ "-i"+                             , "s/^module/(* multstyle = \"logic\" *) module/;"+                             , toTextIgnore inpf+                             ]+        writefile quartusSdc $ "create_clock -period 5 -name clk [get_ports clock]"+        writefile quartusTcl $ quartusSynthConfig sim quartusSdc top inpf+    ex (exec "quartus_sh") ["-t", toTextIgnore quartusTcl]+    liftSh $ do+        cp (fromText "simulation/vcs" </> fromText top <.> "vo")+            $ synthOutput sim+        run_+            "sed"+            [ "-ri"+            , "s,^// DATE.*,,; s,^tri1 (.*);,wire \\1 = 1;,; /^\\/\\/ +synopsys/ d;"+            , toTextIgnore $ synthOutput sim+            ]+  where+    inpf = "rtl.v"+    exec s = maybe (fromText s) (</> fromText s) $ quartusLightBin sim+    quartusTcl = fromText top <.> "tcl"+    quartusSdc = fromText top <.> "sdc"

@@ -13,8 +13,11 @@ {-# LANGUAGE QuasiQuotes #-}  module Verismith.Tool.Template-    ( yosysSatConfig+    ( yosysSynthConfigStd+    , yosysSatConfig     , yosysSimConfig+    , quartusLightSynthConfig+    , quartusSynthConfig     , xstSynthConfig     , vivadoSynthConfig     , sbyConfig@@ -48,7 +51,15 @@ outputText :: Synthesiser a => a -> Text outputText = toTextIgnore . synthOutput --- brittany-disable-next-binding+yosysSynthConfig :: Synthesiser a => Text -> a -> FilePath -> Text+yosysSynthConfig t a fp = [st|read_verilog #{toTextIgnore fp}+#{t}+write_verilog #{outputText a}+|]++yosysSynthConfigStd :: Synthesiser a => a -> FilePath -> Text+yosysSynthConfigStd = yosysSynthConfig "synth"+ yosysSatConfig :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> Text yosysSatConfig sim1 sim2 (SourceInfo top src) = [st|read_verilog #{outputText sim1} #{rename "_1" mis}@@ -62,13 +73,51 @@   where     mis = src ^.. getSourceId --- brittany-disable-next-binding yosysSimConfig :: Text yosysSimConfig = [st|read_verilog rtl.v; proc;; rename mod mod_rtl |] --- brittany-disable-next-binding+quartusLightSynthConfig :: Synthesiser a => a -> FilePath -> Text -> FilePath -> Text+quartusLightSynthConfig q sdc top fp = [st|load_package flow++project_new -overwrite #{top}++set_global_assignment -name FAMILY "Cyclone V"+set_global_assignment -name SYSTEMVERILOG_FILE #{toTextIgnore fp}+set_global_assignment -name TOP_LEVEL_ENTITY #{top}+set_global_assignment -name SDC_FILE #{toTextIgnore sdc}+set_global_assignment -name INI_VARS "qatm_force_vqm=on;"+set_global_assignment -name NUM_PARALLEL_PROCESSORS 2+set_instance_assignment -name VIRTUAL_PIN ON -to *++execute_module -tool map+execute_module -tool fit+execute_module -tool sta -args "--mode=implement"+execute_module -tool eda -args "--simulation --tool=vcs"++project_close+|]++quartusSynthConfig :: Synthesiser a => a -> FilePath -> Text -> FilePath -> Text+quartusSynthConfig q sdc top fp = [st|load_package flow++project_new -overwrite #{top}++set_global_assignment -name FAMILY "Cyclone 10 GX"+set_global_assignment -name SYSTEMVERILOG_FILE #{toTextIgnore fp}+set_global_assignment -name TOP_LEVEL_ENTITY #{top}+set_global_assignment -name SDC_FILE #{toTextIgnore sdc}+set_global_assignment -name INI_VARS "qatm_force_vqm=on;"+set_global_assignment -name NUM_PARALLEL_PROCESSORS 2+set_instance_assignment -name VIRTUAL_PIN ON -to *++execute_module -tool syn+execute_module -tool eda -args "--simulation --tool=vcs"++project_close+|]+ xstSynthConfig :: Text -> Text xstSynthConfig top = [st|run -ifn #{top}.prj -ofn #{top} -p artix7 -top #{top}@@ -77,7 +126,6 @@ -change_error_to_warning "HDLCompiler:226 HDLCompiler:1832" |] --- brittany-disable-next-binding vivadoSynthConfig :: Text -> Text -> Text vivadoSynthConfig top outf = [st| # CRITICAL WARNING: [Synth 8-5821] Potential divide by zero@@ -88,11 +136,11 @@ write_verilog -force #{outf} |] --- brittany-disable-next-binding-sbyConfig :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> Text-sbyConfig sim1 sim2 (SourceInfo top _) = [st|[options]+sbyConfig :: (Synthesiser a, Synthesiser b) => FilePath -> a -> b -> SourceInfo -> Text+sbyConfig datadir sim1 sim2 (SourceInfo top _) = [st|[options] multiclock on mode prove+aigsmt z3  [engines] abc pdr@@ -115,19 +163,21 @@     depList =       T.intercalate "\n"         $   toTextIgnore-        .   (fromText "data" </>)+        .   (datadir </> fromText "data" </>)         .   fromText         <$> deps     readL = T.intercalate "\n" $ mappend "read -formal " <$> deps -icarusTestbench :: (Synthesiser a) => Verilog -> a -> Text-icarusTestbench t synth1 = [st|-`include "data/cells_cmos.v"-`include "data/cells_cyclone_v.v"-`include "data/cells_verific.v"-`include "data/cells_xilinx_7.v"-`include "data/cells_yosys.v"+icarusTestbench :: (Synthesiser a) => FilePath -> Verilog -> a -> Text+icarusTestbench datadir t synth1 = [st|+`include "#{ddir}/data/cells_cmos.v"+`include "#{ddir}/data/cells_cyclone_v.v"+`include "#{ddir}/data/cells_verific.v"+`include "#{ddir}/data/cells_xilinx_7.v"+`include "#{ddir}/data/cells_yosys.v" `include "#{toTextIgnore $ synthOutput synth1}"  #{genSource t} |]+  where+    ddir = toTextIgnore datadir

@@ -23,11 +23,14 @@ import           Control.DeepSeq           (NFData, rnf, rwhnf) import           Control.Lens import           Control.Monad             (void)+import           Data.Either               (fromRight) import           Data.Text                 (Text, unpack) import           Prelude                   hiding (FilePath)-import           Shelly-import           Shelly.Lifted             (liftSh)+import           Shelly                    (FilePath, (</>))+import qualified Shelly                    as S+import           Shelly.Lifted             (liftSh, readfile) import           Text.Shakespeare.Text     (st)+import           Verismith.CounterEg       (parseCounterEg) import           Verismith.Result import           Verismith.Tool.Internal import           Verismith.Tool.Template@@ -59,13 +62,13 @@ defaultYosys = Yosys Nothing "yosys" "syn_yosys.v"  yosysPath :: Yosys -> FilePath-yosysPath sim = maybe (fromText "yosys") (</> fromText "yosys") $ yosysBin sim+yosysPath sim = maybe (S.fromText "yosys") (</> S.fromText "yosys") $ yosysBin sim  runSynthYosys :: Yosys -> SourceInfo -> ResultSh () runSynthYosys sim (SourceInfo _ src) = do     dir <- liftSh $ do-        dir' <- pwd-        writefile inpf $ genSource src+        dir' <- S.pwd+        S.writefile inpf $ genSource src         return dir'     execute_         SynthFail@@ -77,8 +80,8 @@         ]   where     inpf = "rtl.v"-    inp  = toTextIgnore inpf-    out  = toTextIgnore $ synthOutput sim+    inp  = S.toTextIgnore inpf+    out  = S.toTextIgnore $ synthOutput sim  runEquivYosys     :: (Synthesiser a, Synthesiser b)@@ -89,24 +92,24 @@     -> ResultSh () runEquivYosys yosys sim1 sim2 srcInfo = do     liftSh $ do-        writefile "top.v"+        S.writefile "top.v"             .  genSource             .  initMod             .  makeTop 2             $  srcInfo             ^. mainModule-        writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo+        S.writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo     runSynth sim1 srcInfo     runSynth sim2 srcInfo-    liftSh $ run_ (yosysPath yosys) [toTextIgnore checkFile]-    where checkFile = fromText [st|test.#{toText sim1}.#{toText sim2}.ys|]+    liftSh $ S.run_ (yosysPath yosys) [S.toTextIgnore checkFile]+    where checkFile = S.fromText [st|test.#{toText sim1}.#{toText sim2}.ys|]  runEquiv-    :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> ResultSh ()-runEquiv sim1 sim2 srcInfo = do-    dir <- liftSh pwd+    :: (Synthesiser a, Synthesiser b) => FilePath -> a -> b -> SourceInfo -> ResultSh ()+runEquiv datadir sim1 sim2 srcInfo = do+    dir <- liftSh S.pwd     liftSh $ do-        writefile "top.v"+        S.writefile "top.v"             .  genSource             .  initMod             .  makeTopAssert@@ -114,14 +117,15 @@             ^. mainModule         replaceMods (synthOutput sim1) "_1" srcInfo         replaceMods (synthOutput sim2) "_2" srcInfo-        writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo+        S.writefile "proof.sby" $ sbyConfig datadir sim1 sim2 srcInfo     e <- liftSh $ do         exe dir "symbiyosys" "sby" ["-f", "proof.sby"]-        lastExitCode+        S.lastExitCode     case e of         0   -> ResultT . return $ Pass ()-        2   -> ResultT . return $ Fail EquivFail+        2   -> ResultT $ Fail . EquivFail . fromRight mempty+                       . parseCounterEg <$> readfile "proof/engine_0/trace.smtc"         124 -> ResultT . return $ Fail TimeoutError         _   -> ResultT . return $ Fail EquivError   where-    exe dir name e = void . errExit False . logCommand dir name . timeout e+    exe dir name e = void . S.errExit False . logCommand dir name . timeout e

@@ -524,6 +524,12 @@                              }                   deriving (Eq, Show, Ord, Data, Generic, NFData) +instance Semigroup SourceInfo where+    (SourceInfo t v) <> (SourceInfo _ v2) = SourceInfo t $ v <> v2++instance Monoid SourceInfo where+    mempty = SourceInfo mempty mempty+ $(makeLenses ''Expr) $(makeLenses ''ConstExpr) $(makeLenses ''Task)

@@ -115,7 +115,7 @@     mutExpr f (TaskEnable a)     = TaskEnable $ mutExpr f a     mutExpr f (SysTaskEnable a)  = SysTaskEnable $ mutExpr f a     mutExpr f (CondStmnt a b c) = CondStmnt (f a) (mutExpr f <$> b) $ mutExpr f <$> c-    mutExpr f (ForLoop a1 e a2 s) = ForLoop (mutExpr f a1) (f e) (mutExpr f a2) $ mutExpr f s+    mutExpr f (ForLoop a1 e a2 s) = ForLoop a1 e a2 $ mutExpr f s  instance Mutate Parameter where     mutExpr _ = id@@ -244,7 +244,7 @@             ^.. modItems             .   traverse             .   modInstId-    conns = ModConn . Id <$> allVars m+    conns = uncurry ModConnNamed . fmap Id <$> zip (allVars m) (allVars m)  -- | Instantiate without adding wire declarations. It also does not count the -- current instantiations of the same module.

@@ -17,10 +17,10 @@ where  import           Control.Lens-import           Data.Either              (either, isRight)-import           Hedgehog                 (Gen, Property, (===))-import qualified Hedgehog                 as Hog-import qualified Hedgehog.Gen             as Hog+import           Data.Either                  (either, isRight)+import           Hedgehog                     (Gen, Property, (===))+import qualified Hedgehog                     as Hog+import qualified Hedgehog.Gen                 as Hog import           Test.Tasty import           Test.Tasty.Hedgehog import           Test.Tasty.HUnit@@ -29,6 +29,7 @@ import           Verismith.Internal import           Verismith.Verilog.Lex import           Verismith.Verilog.Parser+import           Verismith.Verilog.Preprocess (uncomment)  smallConfig :: Config smallConfig = defaultConfig & configProperty . propSize .~ 5@@ -38,11 +39,10 @@  parserInputMod :: Property parserInputMod = Hog.property $ do-    v <- Hog.forAll randomMod'+    v <- GenVerilog <$> Hog.forAll randomMod'     Hog.assert . isRight $ parse parseModDecl                                  "input_test_mod"-                                 (alexScanTokens $ str v)-    where str = show . GenVerilog+                                 (alexScanTokens . uncomment "test" $ show v)  parserIdempotentMod :: Property parserIdempotentMod = Hog.property $ do@@ -58,11 +58,10 @@  parserInput :: Property parserInput = Hog.property $ do-    v <- Hog.forAll (procedural "top" smallConfig)+    v <- Hog.forAll (GenVerilog <$> procedural "top" smallConfig)     Hog.assert . isRight $ parse parseModDecl                                  "input_test"-                                 (alexScanTokens $ str v)-    where str = show . GenVerilog+                                 (alexScanTokens . uncomment "test" $ show v)  parserIdempotent :: Property parserIdempotent = Hog.property $ do

@@ -36,7 +36,37 @@     , removeDeclTest     ] --- brittany-disable-next-binding+removeConstInConcatTest :: TestTree+removeConstInConcatTest = testCase "Remove const in concat" $ do+    GenVerilog (removeDecl srcInfo1) @?= golden1+  where+    srcInfo1 = SourceInfo "top" [verilog|+module top;+  wire a;+  reg b;++  assign a = {1'b0, 1'b0, 1'b0, (1'b0), b, (1'b0), (1'b0)};++  always @(posedge clk) begin+    if (a)+      b <= 1 + 5 + {1'b0, 1'b1, 5'h20, b, 2'b0};+  end+endmodule+|]+    golden1 = GenVerilog $ SourceInfo "top" [verilog|+module top;+  wire a;+  reg b;++  assign a = {b};++  always @(posedge clk) begin+    if (a)+      b <= 1 + 5 + {b};+  end+endmodule+|]+ removeDeclTest :: TestTree removeDeclTest = testCase "Remove declarations" $ do     GenVerilog (removeDecl srcInfo1) @?= golden1@@ -95,7 +125,6 @@ endmodule |] --- brittany-disable-next-binding cleanAllTest :: TestTree cleanAllTest = testCase "Clean all" $ do     GenVerilog (cleanSourceInfoAll srcInfo1) @?= golden1@@ -157,7 +186,6 @@ endmodule |] --- brittany-disable-next-binding cleanTest :: TestTree cleanTest = testCase "Clean expression" $ do     clean ["wire1", "wire2"] srcInfo1 @?= golden1@@ -197,7 +225,6 @@ |]  --- brittany-disable-next-binding activeWireTest :: TestTree activeWireTest = testCase "Active wires" $ do     findActiveWires "top" verilog1 \\ ["x", "y", "z", "w"]          @?= []@@ -271,7 +298,6 @@ endmodule |] --- brittany-disable-next-binding halveStatementsTest :: TestTree halveStatementsTest = testCase "Statements" $ do     GenVerilog <$> halveStatements "top" srcInfo1 @?= golden1@@ -336,7 +362,6 @@ endmodule |]) --- brittany-disable-next-binding modItemReduceTest :: TestTree modItemReduceTest = testCase "Module items" $ do     GenVerilog <$> halveModItems "top" srcInfo1 @?= golden1@@ -372,7 +397,6 @@ endmodule |]) --- brittany-disable-next-binding statementReducerTest :: TestTree statementReducerTest = testCase "Statement reducer" $ do     GenVerilog <$> halveStatements "top" srcInfo1 @?= fmap GenVerilog golden1@@ -460,7 +484,6 @@ endmodule |] --- brittany-disable-next-binding moduleReducerTest :: TestTree moduleReducerTest = testCase "Module reducer" $ do     halveModules srcInfo1 @?= golden1

@@ -1,5 +1,5 @@ name: verismith-version: 0.4.0.1+version: 0.5.0.0 synopsis: Random verilog generation and simulator testing. description:   Verismith provides random verilog generation modules@@ -14,11 +14,11 @@ build-type: Custom cabal-version: >=1.10 extra-source-files: README.md-                  , data/*.v                   , examples/*.v                   , examples/config.toml                   , scripts/*.py                   , scripts/*.sh+data-files: data/*.v  source-repository head   type:     git@@ -27,7 +27,7 @@ source-repository this   type:     git   location: https://github.com/ymherklotz/verismith-  tag:      v0.4.0.0+  tag:      v0.5.0.0  custom-setup   setup-depends:@@ -47,9 +47,11 @@                  , Verismith.Circuit.Internal                  , Verismith.Circuit.Random                  , Verismith.Config+                 , Verismith.CounterEg                  , Verismith.Fuzz                  , Verismith.Generate                  , Verismith.Internal+                 , Verismith.OptParser                  , Verismith.Reduce                  , Verismith.Report                  , Verismith.Result@@ -58,6 +60,7 @@                  , Verismith.Tool.Identity                  , Verismith.Tool.Internal                  , Verismith.Tool.Quartus+                 , Verismith.Tool.QuartusLight                  , Verismith.Tool.Template                  , Verismith.Tool.Vivado                  , Verismith.Tool.XST@@ -74,42 +77,41 @@                  , Verismith.Verilog.Preprocess                  , Verismith.Verilog.Quote                  , Verismith.Verilog.Token-  build-depends: base >=4.7 && <5-               -- Cannot upgrade to 1.0 because of missing MonadGen instance for-               -- StateT.-               , hedgehog >=1.0 && <1.2+  build-depends: DRBG >=0.5 && <0.6+               , array >=0.5 && <0.6+               , base >=4.7 && <5+               , binary >= 0.8.5.1 && <0.9+               , blaze-html >=0.9.0.1 && <0.10+               , bytestring >=0.10 && <0.11+               , cryptonite >=0.25 && <0.26+               , deepseq >= 1.4.3.0 && <1.5+               , exceptions >=0.10.0 && <0.11                , fgl >=5.6 && <5.8                , fgl-visualize >=0.1 && <0.2+               , filepath >=1.4.2 && <1.5+               , gitrev >= 1.3.1 && <1.4+               , hedgehog >=1.0 && <1.2                , lens >=4.16.1 && <4.18+               , lifted-base >=0.2.3 && <0.3+               , memory >=0.14 && <0.15+               , monad-control >=1.0.2 && <1.1+               , mtl >=2.2.2 && <2.3+               , optparse-applicative >=0.14 && <0.15+               , parsec >=3.1 && <3.2+               , prettyprinter >=1.2.0.1 && <1.3                , random >=1.1 && <1.2+               , recursion-schemes >=5.0.2 && <5.2                , shakespeare >=2 && <2.1                , shelly >=1.8.0 && <1.9+               , statistics >=0.14.0.2 && <0.16+               , template-haskell >=2.13.0 && <2.15                , text >=1.2 && <1.3-               , bytestring >=0.10 && <0.11-               , filepath >=1.4.2 && <1.5-               , binary >= 0.8.5.1 && <0.9-               , cryptonite >=0.25 && <0.26-               , memory >=0.14 && <0.15-               , DRBG >=0.5 && <0.6-               , parsec >=3.1 && <3.2+               , time >= 1.8.0.2 && <1.9+               , tomland >=1.0 && <1.2                , transformers >=0.5 && <0.6                , transformers-base >=0.4.5 && <0.5-               , tomland >=1.0 && <1.2-               , prettyprinter >=1.2.0.1 && <1.3-               , array >=0.5 && <0.6-               , recursion-schemes >=5.0.2 && <5.2-               , time >= 1.8.0.2 && <1.9-               , lifted-base >=0.2.3 && <0.3-               , monad-control >=1.0.2 && <1.1-               , gitrev >= 1.3.1 && <1.4-               , deepseq >= 1.4.3.0 && <1.5-               , template-haskell >=2.13.0 && <2.15-               , optparse-applicative >=0.14 && <0.15-               , exceptions >=0.10.0 && <0.11-               , blaze-html >=0.9.0.1 && <0.10-               , statistics >=0.14.0.2 && <0.16-               , vector >=0.12.0.1 && <0.13                , unordered-containers >=0.2.10 && <0.3+               , vector >=0.12.0.1 && <0.13   default-extensions: OverloadedStrings  executable verismith@@ -144,14 +146,14 @@   build-depends: base >=4 && <5                , verismith                , fgl >=5.6 && <5.8-               , tasty >=1.0.1.1 && <1.3-               , tasty-hunit >=0.10 && <0.11-               , tasty-hedgehog >=1.0 && <1.1                , hedgehog >=1.0 && <1.2                , lens >=4.16.1 && <4.18+               , parsec >= 3.1 && < 3.2                , shakespeare >=2 && <2.1+               , tasty >=1.0.1.1 && <1.3+               , tasty-hedgehog >=1.0 && <1.1+               , tasty-hunit >=0.10 && <0.11                , text >=1.2 && <1.3-               , parsec >= 3.1 && < 3.2   default-extensions: OverloadedStrings  --test-suite doctest