From 720fa7a822a077458cf0b29e9dcdc754a881e8bd Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 5 Jun 2019 13:52:20 +0100 Subject: Format all files --- src/VeriFuzz.hs | 46 +++++++++++++---------- src/VeriFuzz/Config.hs | 12 +++--- src/VeriFuzz/Fuzz.hs | 85 ++++++++++++++++++++++-------------------- src/VeriFuzz/Reduce.hs | 56 ++++++++++++++-------------- src/VeriFuzz/Report.hs | 10 ++++- src/VeriFuzz/Sim/Quartus.hs | 7 +++- src/VeriFuzz/Sim/Vivado.hs | 7 +++- src/VeriFuzz/Sim/Yosys.hs | 6 ++- src/VeriFuzz/Verilog/Gen.hs | 9 +++-- src/VeriFuzz/Verilog/Mutate.hs | 9 ++++- 10 files changed, 143 insertions(+), 104 deletions(-) diff --git a/src/VeriFuzz.hs b/src/VeriFuzz.hs index 4b9878d..7bc562f 100644 --- a/src/VeriFuzz.hs +++ b/src/VeriFuzz.hs @@ -111,12 +111,15 @@ parseSynth val | val == "yosys" = Just TYosys | 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 +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 @@ -191,22 +194,26 @@ reduceOpts = <> showDefault <> value "top" ) - <*> ( optional . strOption + <*> ( 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.") + <*> ( 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 = @@ -386,8 +393,7 @@ handleOpts (Reduce f t _ ls' False) = do _ -> do putStrLn "Not reducing because no synthesiser was specified" return () - where - dir = fromText "reduce" + where dir = fromText "reduce" handleOpts (Reduce f t _ ls' True) = do src <- parseSourceInfoFile t (toTextIgnore f) case descriptionToSynth <$> ls' of @@ -409,7 +415,7 @@ handleOpts (Reduce f t _ ls' True) = do putStrLn "Synthesis check" _ <- shelly . runResultT $ mapM (flip runSynth src) as return () - where dir = fromText "equiv" + where dir = fromText "equiv" handleOpts (ConfigOpt c conf r) = do config <- if r then getConfig conf >>= randomise else getConfig conf maybe (T.putStrLn . encodeConfig $ config) (`encodeConfigFile` config) diff --git a/src/VeriFuzz/Config.hs b/src/VeriFuzz/Config.hs index dd61d31..19cdd68 100644 --- a/src/VeriFuzz/Config.hs +++ b/src/VeriFuzz/Config.hs @@ -380,12 +380,14 @@ propCodec = .= _propModDepth <*> defaultValue (defProp propMaxModules) (int "module" "max") .= _propMaxModules - <*> defaultValue (defProp propSampleMethod) (Toml.text (twoKey "sample" "method")) - .= _propSampleMethod + <*> defaultValue (defProp propSampleMethod) + (Toml.text (twoKey "sample" "method")) + .= _propSampleMethod <*> defaultValue (defProp propSampleSize) (int "sample" "size") - .= _propSampleSize - <*> defaultValue (defProp propCombine) (Toml.bool (twoKey "output" "combine")) - .= _propCombine + .= _propSampleSize + <*> defaultValue (defProp propCombine) + (Toml.bool (twoKey "output" "combine")) + .= _propCombine where defProp i = defaultConfig ^. configProperty . i simulator :: TomlCodec SimDescription diff --git a/src/VeriFuzz/Fuzz.hs b/src/VeriFuzz/Fuzz.hs index 00f1926..dadae90 100644 --- a/src/VeriFuzz/Fuzz.hs +++ b/src/VeriFuzz/Fuzz.hs @@ -221,10 +221,10 @@ failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get -- | Always reduces with respect to 'Identity'. reduction :: (MonadSh m) => SourceInfo -> Fuzz m () reduction src = do - fails <- failEquivWithIdentity + fails <- failEquivWithIdentity synthFails <- failedSynthesis - _ <- liftSh $ mapM red fails - _ <- liftSh $ mapM redSynth synthFails + _ <- liftSh $ mapM red fails + _ <- liftSh $ mapM redSynth synthFails return () where red (SynthResult a b _ _) = do @@ -271,38 +271,41 @@ verilogSize :: (Source a) => a -> Int verilogSize = length . lines . T.unpack . genSource sampleVerilog - :: (MonadSh m, MonadIO m, Source a, Ord a) => - Frequency a -> Int -> Maybe Seed -> Gen a -> m (Seed, a) -sampleVerilog _ _ seed@(Just _) gen = sampleSeed seed gen -sampleVerilog freq n Nothing gen = do + :: (MonadSh m, MonadIO m, Source a, Ord a) + => Frequency a + -> Int + -> Maybe Seed + -> Gen a + -> m (Seed, a) +sampleVerilog _ _ seed@(Just _) gen = sampleSeed seed gen +sampleVerilog freq n Nothing gen = do res <- replicateM n $ sampleSeed Nothing gen - let sizes = fmap getSize res + let sizes = fmap getSize res let samples = fmap snd . sort $ zip sizes res liftIO $ Hog.sample . Hog.frequency $ freq samples - where - getSize (_, s) = verilogSize s + where getSize (_, s) = verilogSize s hatFreqs :: Frequency a hatFreqs l = zip hat (return <$> l) - where - h = length l `div` 2 - hat = (+ h) . negate . abs . (h - ) <$> [1..length l] + where + h = length l `div` 2 + hat = (+ h) . negate . abs . (h -) <$> [1 .. length l] meanFreqs :: Source a => Frequency a meanFreqs l = zip hat (return <$> l) - where - hat = calc <$> sizes - calc i = if abs (mean - i) == min_ then 1 else 0 - mean = sum sizes `div` length l - min_ = minimum $ abs . (mean -) <$> sizes - sizes = verilogSize . snd <$> l + where + hat = calc <$> sizes + calc i = if abs (mean - i) == min_ then 1 else 0 + mean = sum sizes `div` length l + min_ = minimum $ abs . (mean -) <$> sizes + sizes = verilogSize . snd <$> l medianFreqs :: Frequency a medianFreqs l = zip hat (return <$> l) - where - h = length l `div` 2 - hat = set_ <$> [1..length l] - set_ n = if n == h then 1 else 0 + where + h = length l `div` 2 + 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 @@ -318,9 +321,11 @@ fuzz gen conf = do (tsynth, _) <- titleRun "Synthesis" $ synthesis src (tequiv, _) <- titleRun "Equivalence Check" $ equivalence src fails <- failEquivWithIdentity - synthFails <- failedSynthesis - redResult <- whenMaybe (not $ null fails && null synthFails) . titleRun "Reduction" $ reduction - src + synthFails <- failedSynthesis + redResult <- + whenMaybe (not $ null fails && null synthFails) + . titleRun "Reduction" + $ reduction src state_ <- get currdir <- liftSh pwd let vi = flip view state_ @@ -335,21 +340,21 @@ fuzz gen conf = do liftSh . writefile "index.html" $ printResultReport (bname currdir) report return report where - seed = conf ^. configProperty . propSeed - bname = T.pack . takeBaseName . T.unpack . toTextIgnore + seed = conf ^. configProperty . propSeed + bname = T.pack . takeBaseName . T.unpack . toTextIgnore 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 + "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 diff --git a/src/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs index 2a8b489..7cee31c 100644 --- a/src/VeriFuzz/Reduce.hs +++ b/src/VeriFuzz/Reduce.hs @@ -257,7 +257,7 @@ exprId (RangeSelect i _) = Just i exprId _ = Nothing eventId :: Event -> Maybe Identifier -eventId (EId i) = Just i +eventId (EId i) = Just i eventId (EPosEdge i) = Just i eventId (ENegEdge i) = Just i eventId _ = Nothing @@ -411,12 +411,13 @@ toIdsEvent = nub . mapMaybe eventId . concatMap universe allStatIds' :: Statement -> [Identifier] allStatIds' s = nub $ assignIds <> otherExpr <> eventProcessedIds where - assignIds = toIds + assignIds = + toIds $ (s ^.. stmntBA . assignExpr) <> (s ^.. stmntNBA . assignExpr) <> (s ^.. forAssign . assignExpr) <> (s ^.. forIncr . assignExpr) - otherExpr = toIds $ (s ^.. forExpr) <> (s ^.. stmntCondExpr) + otherExpr = toIds $ (s ^.. forExpr) <> (s ^.. stmntCondExpr) eventProcessedIds = toIdsEvent $ s ^.. statEvent allStatIds :: Statement -> [Identifier] @@ -517,21 +518,21 @@ reduce_ title repl bot eval src = do if bot src then return src else case repl src of - Single s -> do - red <- eval s - if red - then if cond s then recReduction s else return s - else return src - Dual l r -> do - red <- eval l - if red - then if cond l then recReduction l else return l - else do - red' <- eval r - if red' - then if cond r then recReduction r else return r - else return src - None -> return src + Single s -> do + red <- eval s + if red + then if cond s then recReduction s else return s + else return src + Dual l r -> do + red <- eval l + if red + then if cond l then recReduction l else return l + else do + red' <- eval r + if red' + then if cond r then recReduction r else return r + else return src + None -> return src where cond s = s /= src recReduction = reduce_ title repl bot eval @@ -597,15 +598,12 @@ reduceSynth a b = reduce synth Fail _ -> False Pass _ -> False -reduceSynthesis :: (Synthesiser a, MonadSh m) - => a - -> SourceInfo - -> m SourceInfo +reduceSynthesis :: (Synthesiser a, MonadSh m) => a -> SourceInfo -> m SourceInfo reduceSynthesis a = reduce synth - where - synth src = liftSh $ do - r <- runResultT $ runSynth a src - return $ case r of - Fail SynthFail -> True - Fail _ -> False - Pass _ -> False + where + synth src = liftSh $ do + r <- runResultT $ runSynth a src + return $ case r of + Fail SynthFail -> True + Fail _ -> False + Pass _ -> False diff --git a/src/VeriFuzz/Report.hs b/src/VeriFuzz/Report.hs index 20addfb..fb66275 100644 --- a/src/VeriFuzz/Report.hs +++ b/src/VeriFuzz/Report.hs @@ -356,7 +356,13 @@ summary name fuzz = H.docTypeHtml $ do H.tr $ H.toHtml [ H.td $ H.strong "Total" , H.td mempty - , H.td . H.string . show . sum $ fuzz ^.. traverse . fileLines + , H.td + . H.string + . show + . sum + $ fuzz + ^.. traverse + . fileLines , sumUp synthTime , sumUp equivTime , sumUp reducTime @@ -382,7 +388,7 @@ summary name fuzz = H.docTypeHtml $ do meanVar s = bimap d2T d2T $ fuzzStats s fuzz showHtml = H.td . H.string . show d2T = showHtml . (realToFrac :: Double -> NominalDiffTime) - d2I = H.td . H.string . show + d2I = H.td . H.string . show printResultReport :: Text -> FuzzReport -> Text printResultReport t f = toStrict . renderHtml $ resultReport t f diff --git a/src/VeriFuzz/Sim/Quartus.hs b/src/VeriFuzz/Sim/Quartus.hs index a099495..4217abb 100644 --- a/src/VeriFuzz/Sim/Quartus.hs +++ b/src/VeriFuzz/Sim/Quartus.hs @@ -53,7 +53,12 @@ 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] + 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"] diff --git a/src/VeriFuzz/Sim/Vivado.hs b/src/VeriFuzz/Sim/Vivado.hs index 90eed2d..a4feb07 100644 --- a/src/VeriFuzz/Sim/Vivado.hs +++ b/src/VeriFuzz/Sim/Vivado.hs @@ -56,7 +56,12 @@ runSynthVivado sim (SourceInfo top src) = do writefile vivadoTcl . vivadoSynthConfig top . toTextIgnore $ synthOutput sim writefile "rtl.v" $ genSource src - run_ "sed" ["s/^module/(* use_dsp48=\"no\" *) (* use_dsp=\"no\" *) module/;", "-i", "rtl.v"] + run_ + "sed" + [ "s/^module/(* use_dsp48=\"no\" *) (* use_dsp=\"no\" *) module/;" + , "-i" + , "rtl.v" + ] let exec_ n = execute_ SynthFail dir diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs index 3729a1e..02a00d5 100644 --- a/src/VeriFuzz/Sim/Yosys.hs +++ b/src/VeriFuzz/Sim/Yosys.hs @@ -67,7 +67,11 @@ runSynthYosys sim (SourceInfo _ src) = do dir' <- pwd writefile inpf $ genSource src return dir' - execute_ SynthFail dir "yosys" (yosysPath sim) + execute_ + SynthFail + dir + "yosys" + (yosysPath sim) [ "-p" , "read -formal " <> inp <> "; synth; write_verilog -noattr " <> out ] diff --git a/src/VeriFuzz/Verilog/Gen.hs b/src/VeriFuzz/Verilog/Gen.hs index c8860ce..e52a158 100644 --- a/src/VeriFuzz/Verilog/Gen.hs +++ b/src/VeriFuzz/Verilog/Gen.hs @@ -455,7 +455,7 @@ moduleDef top = do mi <- Hog.list (Hog.linear 4 100) modItem ps <- Hog.list (Hog.linear 0 10) parameter context <- get - config <- lift ask + config <- lift ask let local = filter (`notElem` portList) $ _variables context let size = @@ -465,9 +465,10 @@ moduleDef top = do ^.. traverse . portSize let combine = config ^. configProperty . propCombine - let clock = Port Wire False 1 "clk" - let yport = if combine then Port Wire False 1 "y" else Port Wire False size "y" - let comb = combineAssigns_ combine yport local + let clock = Port Wire False 1 "clk" + let yport = + if combine then Port Wire False 1 "y" else Port Wire False size "y" + let comb = combineAssigns_ combine yport local return . declareMod local . ModDecl name [yport] (clock : portList) (comb : mi) diff --git a/src/VeriFuzz/Verilog/Mutate.hs b/src/VeriFuzz/Verilog/Mutate.hs index 7496935..0fb4c49 100644 --- a/src/VeriFuzz/Verilog/Mutate.hs +++ b/src/VeriFuzz/Verilog/Mutate.hs @@ -377,7 +377,14 @@ removeId i = transform trans combineAssigns :: Port -> [ModItem] -> [ModItem] combineAssigns p a = - a <> [ModCA . ContAssign (p ^. portName) . UnOp UnXor . fold $ Id <$> assigns] + a + <> [ ModCA + . ContAssign (p ^. portName) + . UnOp UnXor + . fold + $ Id + <$> assigns + ] where assigns = a ^.. traverse . modContAssign . contAssignNetLVal combineAssigns_ :: Bool -> Port -> [Port] -> ModItem -- cgit