diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/data/cells_cyclone_v.v b/data/cells_cyclone_v.v --- a/data/cells_cyclone_v.v +++ b/data/cells_cyclone_v.v @@ -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 diff --git a/scripts/reducer.sh b/scripts/reducer.sh new file mode 100644 --- /dev/null +++ b/scripts/reducer.sh @@ -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 <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 <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 diff --git a/src/Verismith.hs b/src/Verismith.hs --- a/src/Verismith.hs +++ b/src/Verismith.hs @@ -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 diff --git a/src/Verismith/Config.hs b/src/Verismith/Config.hs --- a/src/Verismith/Config.hs +++ b/src/Verismith/Config.hs @@ -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) diff --git a/src/Verismith/CounterEg.hs b/src/Verismith/CounterEg.hs new file mode 100644 --- /dev/null +++ b/src/Verismith/CounterEg.hs @@ -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 diff --git a/src/Verismith/Fuzz.hs b/src/Verismith/Fuzz.hs --- a/src/Verismith/Fuzz.hs +++ b/src/Verismith/Fuzz.hs @@ -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" diff --git a/src/Verismith/Generate.hs b/src/Verismith/Generate.hs --- a/src/Verismith/Generate.hs +++ b/src/Verismith/Generate.hs @@ -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 = diff --git a/src/Verismith/OptParser.hs b/src/Verismith/OptParser.hs new file mode 100644 --- /dev/null +++ b/src/Verismith/OptParser.hs @@ -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." + ) diff --git a/src/Verismith/Reduce.hs b/src/Verismith/Reduce.hs --- a/src/Verismith/Reduce.hs +++ b/src/Verismith/Reduce.hs @@ -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 diff --git a/src/Verismith/Report.hs b/src/Verismith/Report.hs --- a/src/Verismith/Report.hs +++ b/src/Verismith/Report.hs @@ -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 diff --git a/src/Verismith/Result.hs b/src/Verismith/Result.hs --- a/src/Verismith/Result.hs +++ b/src/Verismith/Result.hs @@ -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 diff --git a/src/Verismith/Tool.hs b/src/Verismith/Tool.hs --- a/src/Verismith/Tool.hs +++ b/src/Verismith/Tool.hs @@ -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 diff --git a/src/Verismith/Tool/Icarus.hs b/src/Verismith/Tool/Icarus.hs --- a/src/Verismith/Tool/Icarus.hs +++ b/src/Verismith/Tool/Icarus.hs @@ -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 [] diff --git a/src/Verismith/Tool/Internal.hs b/src/Verismith/Tool/Internal.hs --- a/src/Verismith/Tool/Internal.hs +++ b/src/Verismith/Tool/Internal.hs @@ -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 diff --git a/src/Verismith/Tool/Quartus.hs b/src/Verismith/Tool/Quartus.hs --- a/src/Verismith/Tool/Quartus.hs +++ b/src/Verismith/Tool/Quartus.hs @@ -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" diff --git a/src/Verismith/Tool/QuartusLight.hs b/src/Verismith/Tool/QuartusLight.hs new file mode 100644 --- /dev/null +++ b/src/Verismith/Tool/QuartusLight.hs @@ -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" diff --git a/src/Verismith/Tool/Template.hs b/src/Verismith/Tool/Template.hs --- a/src/Verismith/Tool/Template.hs +++ b/src/Verismith/Tool/Template.hs @@ -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 diff --git a/src/Verismith/Tool/Yosys.hs b/src/Verismith/Tool/Yosys.hs --- a/src/Verismith/Tool/Yosys.hs +++ b/src/Verismith/Tool/Yosys.hs @@ -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 diff --git a/src/Verismith/Verilog/AST.hs b/src/Verismith/Verilog/AST.hs --- a/src/Verismith/Verilog/AST.hs +++ b/src/Verismith/Verilog/AST.hs @@ -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) diff --git a/src/Verismith/Verilog/Mutate.hs b/src/Verismith/Verilog/Mutate.hs --- a/src/Verismith/Verilog/Mutate.hs +++ b/src/Verismith/Verilog/Mutate.hs @@ -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. diff --git a/test/Parser.hs b/test/Parser.hs --- a/test/Parser.hs +++ b/test/Parser.hs @@ -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 diff --git a/test/Reduce.hs b/test/Reduce.hs --- a/test/Reduce.hs +++ b/test/Reduce.hs @@ -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 diff --git a/verismith.cabal b/verismith.cabal --- a/verismith.cabal +++ b/verismith.cabal @@ -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