diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2019-07-21 13:37:25 +0200 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2019-07-21 13:37:25 +0200 |
| commit | 30fbe26f59e54a276f88650ffa5e78343b5411eb (patch) | |
| tree | aa3166c423f262ee6296826d2c815a0b54084c31 /src | |
| parent | b5c035e45949945cc62845fa6492cffa77992524 (diff) | |
| parent | c19a51a8156bbcaee13d9819c8fe54ed0ca5c4cc (diff) | |
| download | verismith-30fbe26f59e54a276f88650ffa5e78343b5411eb.tar.gz verismith-30fbe26f59e54a276f88650ffa5e78343b5411eb.zip | |
Merge branch 'master' into fix/resize-modports
Diffstat (limited to 'src')
29 files changed, 1007 insertions, 389 deletions
diff --git a/src/VeriFuzz.hs b/src/VeriFuzz.hs index 66c795f..0bbdc4f 100644 --- a/src/VeriFuzz.hs +++ b/src/VeriFuzz.hs @@ -28,27 +28,29 @@ module VeriFuzz where import Control.Concurrent -import Control.Lens -import Control.Monad.IO.Class (liftIO) -import qualified Crypto.Random.DRBG as C -import Data.ByteString (ByteString) -import Data.ByteString.Builder (byteStringHex, toLazyByteString) -import qualified Data.ByteString.Lazy as L -import qualified Data.Graph.Inductive as G -import qualified Data.Graph.Inductive.Dot as G -import Data.Maybe (isNothing) -import Data.Text (Text) -import qualified Data.Text as T -import Data.Text.Encoding (decodeUtf8) -import qualified Data.Text.IO as T -import Hedgehog (Gen) -import qualified Hedgehog.Gen as Hog -import Hedgehog.Internal.Seed (Seed) +import Control.Lens hiding ( (<.>) ) +import Control.Monad.IO.Class ( liftIO ) +import qualified Crypto.Random.DRBG as C +import Data.ByteString ( ByteString ) +import Data.ByteString.Builder ( byteStringHex + , toLazyByteString + ) +import qualified Data.ByteString.Lazy as L +import qualified Data.Graph.Inductive as G +import qualified Data.Graph.Inductive.Dot as G +import Data.Maybe ( isNothing ) +import Data.Text ( Text ) +import qualified Data.Text as T +import Data.Text.Encoding ( decodeUtf8 ) +import qualified Data.Text.IO as T +import Hedgehog ( Gen ) +import qualified Hedgehog.Gen as Hog +import Hedgehog.Internal.Seed ( Seed ) import Options.Applicative -import Prelude hiding (FilePath) -import Shelly hiding (command) -import Shelly.Lifted (liftSh) -import System.Random (randomIO) +import Prelude hiding ( FilePath ) +import Shelly hiding ( command ) +import Shelly.Lifted ( liftSh ) +import System.Random ( randomIO ) import VeriFuzz.Circuit import VeriFuzz.Config import VeriFuzz.Fuzz @@ -58,6 +60,7 @@ import VeriFuzz.Result import VeriFuzz.Sim import VeriFuzz.Sim.Internal import VeriFuzz.Verilog +import VeriFuzz.Verilog.Parser ( parseSourceInfoFile ) data OptTool = TYosys | TXST @@ -79,9 +82,11 @@ data Opts = Fuzz { fuzzOutput :: {-# UNPACK #-} !Text } | Parse { fileName :: {-# UNPACK #-} !FilePath } - | Reduce { fileName :: {-# UNPACK #-} !FilePath - , top :: {-# UNPACK #-} !Text - , reduceScript :: {-# UNPACK #-} !FilePath + | Reduce { fileName :: {-# UNPACK #-} !FilePath + , top :: {-# UNPACK #-} !Text + , reduceScript :: {-# UNPACK #-} !(Maybe FilePath) + , synthesiserDesc :: ![SynthDescription] + , rerun :: Bool } | ConfigOpt { writeConfig :: !(Maybe FilePath) , configFile :: !(Maybe FilePath) @@ -107,6 +112,17 @@ 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 @@ -180,13 +196,26 @@ reduceOpts = <> showDefault <> value "top" ) - <*> ( strOption + <*> ( optional + . strOption $ long "script" - <> short 's' <> 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 = @@ -346,7 +375,49 @@ handleOpts (Parse f) = do Left l -> print l Right v -> print $ GenVerilog v where file = T.unpack . toTextIgnore $ f -handleOpts (Reduce f t s) = shelly $ reduceWithScript t s f +handleOpts (Reduce f t _ ls' False) = do + src <- parseSourceInfoFile t (toTextIgnore f) + case descriptionToSynth <$> ls' of + a : b : _ -> do + putStrLn "Reduce with equivalence check" + shelly $ do + make dir + pop dir $ do + src' <- reduceSynth a b src + writefile (fromText ".." </> dir <.> "v") $ genSource src' + a : _ -> do + putStrLn "Reduce with synthesis failure" + shelly $ do + make dir + pop dir $ do + src' <- reduceSynthesis a src + writefile (fromText ".." </> dir <.> "v") $ genSource src' + _ -> do + putStrLn "Not reducing because no synthesiser was specified" + return () + where dir = fromText "reduce" +handleOpts (Reduce f t _ ls' True) = do + src <- parseSourceInfoFile t (toTextIgnore f) + case descriptionToSynth <$> ls' of + a : b : _ -> do + putStrLn "Starting equivalence check" + res <- shelly . runResultT $ do + make dir + pop dir $ do + runSynth a src + runSynth b src + runEquiv 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" + return () + as -> do + putStrLn "Synthesis check" + _ <- shelly . runResultT $ mapM (flip runSynth src) as + return () + 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/Circuit.hs b/src/VeriFuzz/Circuit.hs index 58027b1..9ee601f 100644 --- a/src/VeriFuzz/Circuit.hs +++ b/src/VeriFuzz/Circuit.hs @@ -26,8 +26,8 @@ module VeriFuzz.Circuit where import Control.Lens -import Hedgehog (Gen) -import qualified Hedgehog.Gen as Hog +import Hedgehog ( Gen ) +import qualified Hedgehog.Gen as Hog import VeriFuzz.Circuit.Base import VeriFuzz.Circuit.Gen import VeriFuzz.Circuit.Random diff --git a/src/VeriFuzz/Circuit/Base.hs b/src/VeriFuzz/Circuit/Base.hs index ed63105..adc7d52 100644 --- a/src/VeriFuzz/Circuit/Base.hs +++ b/src/VeriFuzz/Circuit/Base.hs @@ -18,7 +18,10 @@ module VeriFuzz.Circuit.Base ) where -import Data.Graph.Inductive (Gr, LEdge, LNode) +import Data.Graph.Inductive ( Gr + , LEdge + , LNode + ) import System.Random -- | The types for all the gates. diff --git a/src/VeriFuzz/Circuit/Gen.hs b/src/VeriFuzz/Circuit/Gen.hs index 0b13ece..323d8bb 100644 --- a/src/VeriFuzz/Circuit/Gen.hs +++ b/src/VeriFuzz/Circuit/Gen.hs @@ -15,9 +15,11 @@ module VeriFuzz.Circuit.Gen ) where -import Data.Graph.Inductive (LNode, Node) -import qualified Data.Graph.Inductive as G -import Data.Maybe (catMaybes) +import Data.Graph.Inductive ( LNode + , Node + ) +import qualified Data.Graph.Inductive as G +import Data.Maybe ( catMaybes ) import VeriFuzz.Circuit.Base import VeriFuzz.Circuit.Internal import VeriFuzz.Verilog.AST diff --git a/src/VeriFuzz/Circuit/Internal.hs b/src/VeriFuzz/Circuit/Internal.hs index 3a7346f..5220f4d 100644 --- a/src/VeriFuzz/Circuit/Internal.hs +++ b/src/VeriFuzz/Circuit/Internal.hs @@ -19,9 +19,11 @@ module VeriFuzz.Circuit.Internal ) where -import Data.Graph.Inductive (Graph, Node) -import qualified Data.Graph.Inductive as G -import qualified Data.Text as T +import Data.Graph.Inductive ( Graph + , Node + ) +import qualified Data.Graph.Inductive as G +import qualified Data.Text as T -- | Convert an integer into a label. -- diff --git a/src/VeriFuzz/Circuit/Random.hs b/src/VeriFuzz/Circuit/Random.hs index 58e855c..2750de8 100644 --- a/src/VeriFuzz/Circuit/Random.hs +++ b/src/VeriFuzz/Circuit/Random.hs @@ -18,13 +18,14 @@ module VeriFuzz.Circuit.Random ) where -import Data.Graph.Inductive (Context) -import qualified Data.Graph.Inductive as G -import Data.Graph.Inductive.PatriciaTree (Gr) -import Data.List (nub) -import Hedgehog (Gen) -import qualified Hedgehog.Gen as Hog -import qualified Hedgehog.Range as Hog +import Data.Graph.Inductive ( Context ) +import qualified Data.Graph.Inductive as G +import Data.Graph.Inductive.PatriciaTree + ( Gr ) +import Data.List ( nub ) +import Hedgehog ( Gen ) +import qualified Hedgehog.Gen as Hog +import qualified Hedgehog.Range as Hog import VeriFuzz.Circuit.Base dupFolder :: (Eq a, Eq b) => Context a b -> [Context a b] -> [Context a b] diff --git a/src/VeriFuzz/Config.hs b/src/VeriFuzz/Config.hs index 9295f71..0fc9435 100644 --- a/src/VeriFuzz/Config.hs +++ b/src/VeriFuzz/Config.hs @@ -61,11 +61,14 @@ module VeriFuzz.Config , probStmntNonBlock , probStmntCond , probStmntFor + , propSampleSize + , propSampleMethod , propSize , propSeed , propStmntDepth , propModDepth , propMaxModules + , propCombine , parseConfigFile , parseConfig , encodeConfig @@ -74,18 +77,22 @@ module VeriFuzz.Config ) 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_verifuzz (version) -import Shelly (toTextIgnore) -import Toml (TomlCodec, (.=)) +import Hedgehog.Internal.Seed ( Seed ) +import Paths_verifuzz ( version ) +import Shelly ( toTextIgnore ) +import Toml ( TomlCodec + , (.=) + ) import qualified Toml import VeriFuzz.Sim.Quartus import VeriFuzz.Sim.Vivado @@ -189,11 +196,14 @@ data Probability = Probability { _probModItem :: {-# UNPACK #-} !ProbModItem } deriving (Eq, Show) -data ConfProperty = ConfProperty { _propSize :: {-# UNPACK #-} !Int - , _propSeed :: !(Maybe Seed) - , _propStmntDepth :: {-# UNPACK #-} !Int - , _propModDepth :: {-# UNPACK #-} !Int - , _propMaxModules :: {-# UNPACK #-} !Int +data ConfProperty = ConfProperty { _propSize :: {-# UNPACK #-} !Int + , _propSeed :: !(Maybe Seed) + , _propStmntDepth :: {-# UNPACK #-} !Int + , _propModDepth :: {-# UNPACK #-} !Int + , _propMaxModules :: {-# UNPACK #-} !Int + , _propSampleMethod :: !Text + , _propSampleSize :: {-# UNPACK #-} !Int + , _propCombine :: {-# UNPACK #-} !Bool } deriving (Eq, Show) @@ -261,7 +271,7 @@ defaultConfig :: Config defaultConfig = Config (Info (pack $(gitHash)) (pack $ showVersion version)) (Probability defModItem defStmnt defExpr) - (ConfProperty 20 Nothing 3 2 5) + (ConfProperty 20 Nothing 3 2 5 "random" 10 False) [] [fromYosys defaultYosys, fromVivado defaultVivado] where @@ -374,6 +384,14 @@ propCodec = .= _propModDepth <*> defaultValue (defProp propMaxModules) (int "module" "max") .= _propMaxModules + <*> 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 where defProp i = defaultConfig ^. configProperty . i simulator :: TomlCodec SimDescription diff --git a/src/VeriFuzz/Fuzz.hs b/src/VeriFuzz/Fuzz.hs index 77962b5..dd7fe7b 100644 --- a/src/VeriFuzz/Fuzz.hs +++ b/src/VeriFuzz/Fuzz.hs @@ -21,38 +21,52 @@ module VeriFuzz.Fuzz , fuzzMultiple , runFuzz , sampleSeed + -- * Helpers + , make + , pop ) where -import Control.DeepSeq (force) -import Control.Exception.Lifted (finally) -import Control.Lens hiding ((<.>)) -import Control.Monad (forM, void) +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.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 Data.List (nubBy) -import Data.Maybe (isNothing) -import Data.Text (Text) -import qualified Data.Text as T +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 Data.Time -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 VeriFuzz.Config import VeriFuzz.Internal import VeriFuzz.Reduce import VeriFuzz.Report import VeriFuzz.Result +import VeriFuzz.Sim.Icarus import VeriFuzz.Sim.Internal import VeriFuzz.Sim.Yosys import VeriFuzz.Verilog.AST @@ -64,9 +78,19 @@ data FuzzEnv = FuzzEnv { getSynthesisers :: ![SynthTool] } deriving (Eq, Show) +data FuzzState = FuzzState { _fuzzSynthResults :: ![SynthResult] + , _fuzzSimResults :: ![SimResult] + , _fuzzSynthStatus :: ![SynthStatus] + } + deriving (Eq, Show) + +$(makeLenses ''FuzzState) + +type Frequency a = [(Seed, a)] -> [(Int, Gen (Seed, a))] + -- | The main type for the fuzzing, which contains an environment that can be -- read from and the current state of all the results. -type Fuzz m = StateT FuzzReport (ReaderT FuzzEnv m) +type Fuzz m = StateT FuzzState (ReaderT FuzzEnv m) type MonadFuzz m = (MonadBaseControl IO m, MonadIO m, MonadSh m) @@ -75,7 +99,7 @@ runFuzz conf yos m = shelly $ runFuzz' conf yos m runFuzz' :: Monad m => Config -> Yosys -> (Config -> Fuzz m b) -> m b runFuzz' conf yos m = runReaderT - (evalStateT (m conf) (FuzzReport [] [] [])) + (evalStateT (m conf) (FuzzState [] [] [])) (FuzzEnv ( force $ defaultIdentitySynth @@ -106,32 +130,29 @@ timeit a = do synthesis :: (MonadBaseControl IO m, MonadSh m) => SourceInfo -> Fuzz m () synthesis src = do - synth <- synthesisers - results <- liftSh $ mapM exec synth - synthStatus .= zipWith SynthStatus synth results - liftSh $ inspect results + synth <- synthesisers + resTimes <- liftSh $ mapM exec synth + fuzzSynthStatus + .= applyList (uncurry . SynthStatus <$> synth) (fmap swap resTimes) + liftSh $ inspect resTimes where - exec a = runResultT $ do + exec a = toolRun ("synthesis with " <> toText a) . runResultT $ do liftSh . mkdir_p . fromText $ toText a pop (fromText $ toText a) $ runSynth a src -generateSample - :: (MonadIO m, MonadSh m) - => Maybe Seed - -> Gen SourceInfo - -> Fuzz m (Seed, SourceInfo) -generateSample seed gen = do - logT "Sampling Verilog from generator" - (t, v) <- timeit $ sampleSeed seed gen - logT $ "Generated Verilog (" <> showT t <> ")" - return v - passedSynthesis :: MonadSh m => Fuzz m [SynthTool] -passedSynthesis = fmap toSynth . filter passed . _synthStatus <$> get +passedSynthesis = fmap toSynth . filter passed . _fuzzSynthStatus <$> get + where + passed (SynthStatus _ (Pass _) _) = True + passed _ = False + toSynth (SynthStatus s _ _) = s + +failedSynthesis :: MonadSh m => Fuzz m [SynthTool] +failedSynthesis = fmap toSynth . filter failed . _fuzzSynthStatus <$> get where - passed (SynthStatus _ (Pass _)) = True - passed _ = False - toSynth (SynthStatus s _) = s + failed (SynthStatus _ (Fail SynthFail) _) = True + failed _ = False + toSynth (SynthStatus s _ _) = s make :: MonadSh m => FilePath -> m () make f = liftSh $ do @@ -146,8 +167,21 @@ pop f a = do applyList :: [a -> b] -> [a] -> [b] applyList a b = apply' <$> zip a b where apply' (a', b') = a' b' -toSynthResult :: [(SynthTool, SynthTool)] -> [Result Failed ()] -> [SynthResult] -toSynthResult a b = flip applyList b $ uncurry SynthResult <$> a +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 a b = applyLots SynthResult a $ fmap swap b + +toolRun :: (MonadIO m, MonadSh m) => 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) equivalence :: (MonadBaseControl IO m, MonadSh m) => SourceInfo -> Fuzz m () equivalence src = do @@ -159,71 +193,233 @@ equivalence src = do . filter (uncurry (/=)) $ (,) defaultIdentitySynth <$> synth - results <- liftSh $ mapM (uncurry equiv) synthComb - synthResults .= toSynthResult synthComb results - liftSh $ inspect results + resTimes <- liftSh $ mapM (uncurry equiv) 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 = runResultT $ do + equiv a b = + toolRun ("equivalence check for " <> toText a <> " and " <> toText b) + . runResultT + $ do + make dir + pop dir $ do + liftSh $ do + cp + ( fromText ".." + </> fromText (toText a) + </> synthOutput a + ) + $ synthOutput a + cp + ( fromText ".." + </> fromText (toText b) + </> synthOutput b + ) + $ synthOutput b + writefile "rtl.v" $ genSource src + runEquiv a b src + where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b + +simulation :: (MonadIO m, MonadSh m) => SourceInfo -> Fuzz m () +simulation src = do + synth <- passEquiv + vals <- liftIO $ generateByteString 20 + ident <- liftSh $ equiv vals defaultIdentitySynth + resTimes <- liftSh $ mapM (equiv vals) $ conv <$> synth + 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 make dir pop dir $ do liftSh $ do cp (fromText ".." </> fromText (toText a) </> synthOutput a) $ synthOutput a - cp (fromText ".." </> fromText (toText b) </> synthOutput b) - $ synthOutput b writefile "rtl.v" $ genSource src - runEquiv a b src - where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b + runSimIc defaultIcarus a src b + where dir = fromText $ "simulation_" <> toText a + +-- | 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 [] failEquivWithIdentity :: (MonadSh m) => Fuzz m [SynthResult] -failEquivWithIdentity = filter withIdentity . _synthResults <$> get +failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get + where + withIdentity (SynthResult (IdentitySynth _) _ (Fail EquivFail) _) = True + withIdentity (SynthResult _ (IdentitySynth _) (Fail EquivFail) _) = True + withIdentity _ = False + +passEquiv :: (MonadSh m) => Fuzz m [SynthResult] +passEquiv = filter withIdentity . _fuzzSynthResults <$> get where - withIdentity (SynthResult (IdentitySynth _) _ (Fail EquivFail)) = True - withIdentity (SynthResult _ (IdentitySynth _) (Fail EquivFail)) = True - withIdentity _ = False + withIdentity (SynthResult _ _ (Pass _) _) = True + withIdentity _ = False -- | Always reduces with respect to 'Identity'. reduction :: (MonadSh m) => SourceInfo -> Fuzz m () reduction src = do - fails <- failEquivWithIdentity - _ <- liftSh $ mapM red fails + fails <- failEquivWithIdentity + synthFails <- failedSynthesis + _ <- liftSh $ mapM red fails + _ <- liftSh $ mapM redSynth synthFails return () where - red (SynthResult a b _) = do + 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 + +titleRun + :: (MonadIO m, MonadSh m) => Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a) +titleRun t f = do + logT $ "### Starting " <> t <> " ###" + (diff, res) <- timeit f + logT $ "### Finished " <> t <> " (" <> showT diff <> ") ###" + return (diff, res) + +whenMaybe :: Applicative m => Bool -> m a -> m (Maybe a) +whenMaybe b x = if b then Just <$> x else pure Nothing + +getTime :: (Num n) => Maybe (n, a) -> n +getTime = maybe 0 fst + +generateSample + :: (MonadIO m, MonadSh m) + => Fuzz m (Seed, SourceInfo) + -> Fuzz m (Seed, SourceInfo) +generateSample f = do + logT "Sampling Verilog from generator" + (t, v@(s, _)) <- timeit f + logT $ "Chose " <> showT s + logT $ "Generated Verilog (" <> showT t <> ")" + return v + +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 + res <- replicateM n $ sampleSeed Nothing gen + 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 + +hatFreqs :: Frequency a +hatFreqs l = zip hat (return <$> 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 + +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 fuzz :: MonadFuzz m => Gen SourceInfo -> Config -> Fuzz m FuzzReport fuzz gen conf = do - (seed', src) <- generateSample seed gen + (seed', src) <- generateSample genMethod + let size = length . lines . T.unpack $ genSource src liftSh . writefile "config.toml" . encodeConfig $ conf & configProperty . propSeed - .~ Just seed' - synthesis src - equivalence src - reduction src - report <- get + ?~ seed' + (tsynth, _) <- titleRun "Synthesis" $ synthesis src + (tequiv, _) <- titleRun "Equivalence Check" $ equivalence src + (_ , _) <- titleRun "Simulation" $ simulation src + fails <- failEquivWithIdentity + synthFails <- failedSynthesis + redResult <- + whenMaybe (not $ null fails && null synthFails) + . titleRun "Reduction" + $ reduction src + state_ <- get currdir <- liftSh pwd + let vi = flip view state_ + let report = FuzzReport currdir + (vi fuzzSynthResults) + (vi fuzzSimResults) + (vi fuzzSynthStatus) + size + tsynth + tequiv + (getTime redResult) 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 + 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 fuzzInDir :: MonadFuzz m => FilePath -> Gen SourceInfo -> Config -> Fuzz m FuzzReport fuzzInDir fp src conf = do make fp - pop fp $ fuzz src conf + res <- pop fp $ fuzz src conf + relativeFuzzReport res fuzzMultiple :: MonadFuzz m @@ -231,7 +427,7 @@ fuzzMultiple -> Maybe FilePath -> Gen SourceInfo -> Config - -> Fuzz m FuzzReport + -> Fuzz m [FuzzReport] fuzzMultiple n fp src conf = do x <- case fp of Nothing -> do @@ -243,11 +439,16 @@ fuzzMultiple n fp src conf = do <> formatTime defaultTimeLocale "%Y-%m-%d_%H-%M-%S" ct Just f -> return f make x - when (isNothing seed) . void . pop x . forM [1 .. n] $ fuzzDir - unless (isNothing seed) . void . pop x $ fuzzDir (1 :: Int) - return mempty + pop x $ do + results <- if isNothing seed + then forM [1 .. n] fuzzDir' + else (: []) <$> fuzzDir' (1 :: Int) + liftSh . writefile (fromText "index" <.> "html") $ printSummary + "Fuzz Summary" + results + return results where - fuzzDir n' = fuzzInDir (fromText $ "fuzz_" <> showT n') src conf + fuzzDir' n' = fuzzInDir (fromText $ "fuzz_" <> showT n') src conf seed = conf ^. configProperty . propSeed sampleSeed :: MonadSh m => Maybe Seed -> Gen a -> m (Seed, a) @@ -267,7 +468,5 @@ sampleSeed s gen = $ Hog.runGenT 30 seed gen of Nothing -> loop (n - 1) - Just x -> do - liftSh . logT $ showT seed - return (seed, Hog.nodeValue x) + Just x -> return (seed, Hog.nodeValue x) in loop (100 :: Int) diff --git a/src/VeriFuzz/Internal.hs b/src/VeriFuzz/Internal.hs index 22efa92..b5ce3ba 100644 --- a/src/VeriFuzz/Internal.hs +++ b/src/VeriFuzz/Internal.hs @@ -14,13 +14,24 @@ module VeriFuzz.Internal ( -- * Useful functions safe , showT + , showBS , comma , commaNL ) where -import Data.Text (Text) -import qualified Data.Text as T +import Data.ByteString ( ByteString ) +import Data.ByteString.Builder ( byteStringHex + , toLazyByteString + ) +import qualified Data.ByteString.Lazy as L +import Data.Text ( Text ) +import qualified Data.Text as T +import Data.Text.Encoding ( decodeUtf8 ) + +-- | Function to show a bytestring in a hex format. +showBS :: ByteString -> Text +showBS = decodeUtf8 . L.toStrict . toLazyByteString . byteStringHex -- | Converts unsafe list functions in the Prelude to a safe version. safe :: ([a] -> b) -> [a] -> Maybe b diff --git a/src/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs index 33cb648..6bae371 100644 --- a/src/VeriFuzz/Reduce.hs +++ b/src/VeriFuzz/Reduce.hs @@ -17,6 +17,7 @@ module VeriFuzz.Reduce ( -- $strategy reduceWithScript , reduceSynth + , reduceSynthesis , reduce , reduce_ , Replacement(..) @@ -34,27 +35,32 @@ module VeriFuzz.Reduce ) where -import Control.Lens hiding ((<.>)) -import Control.Monad (void) -import Control.Monad.IO.Class (MonadIO, liftIO) -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 Control.Lens hiding ( (<.>) ) +import Control.Monad ( void ) +import Control.Monad.IO.Class ( MonadIO + , liftIO + ) +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 qualified Shelly -import Shelly.Lifted (MonadSh, liftSh) +import Shelly.Lifted ( MonadSh + , liftSh + ) import VeriFuzz.Internal import VeriFuzz.Result import VeriFuzz.Sim import VeriFuzz.Sim.Internal +import VeriFuzz.Verilog import VeriFuzz.Verilog.AST -import VeriFuzz.Verilog.CodeGen import VeriFuzz.Verilog.Mutate import VeriFuzz.Verilog.Parser + -- $strategy -- The reduction strategy has multiple different steps. 'reduce' will run these -- strategies one after another, starting at the most coarse grained one. The @@ -111,7 +117,7 @@ instance Traversable Replacement where -- | Split a list in two halves. halve :: Replace [a] -halve [] = None +halve [] = Single [] halve [_] = Single [] halve l = Dual a b where (a, b) = splitAt (length l `div` 2) l @@ -254,6 +260,12 @@ exprId (VecSelect i _) = Just i exprId (RangeSelect i _) = Just i exprId _ = Nothing +eventId :: Event -> Maybe Identifier +eventId (EId i) = Just i +eventId (EPosEdge i) = Just i +eventId (ENegEdge i) = Just i +eventId _ = Nothing + portToId :: Port -> Identifier portToId (Port _ _ _ i) = i @@ -327,6 +339,7 @@ matchesModName :: Identifier -> ModDecl -> Bool matchesModName top (ModDecl i _ _ _ _) = top == i halveStatement :: Replace Statement +halveStatement (SeqBlock [s]) = halveStatement s halveStatement (SeqBlock s) = SeqBlock <$> halve s halveStatement (CondStmnt _ (Just s1) (Just s2)) = Dual s1 s2 halveStatement (CondStmnt _ (Just s1) Nothing) = Single s1 @@ -396,8 +409,11 @@ toIds = nub . mapMaybe exprId . concatMap universe toIdsConst :: [ConstExpr] -> [Identifier] toIdsConst = toIds . fmap constToExpr +toIdsEvent :: [Event] -> [Identifier] +toIdsEvent = nub . mapMaybe eventId . concatMap universe + allStatIds' :: Statement -> [Identifier] -allStatIds' s = nub $ assignIds <> otherExpr +allStatIds' s = nub $ assignIds <> otherExpr <> eventProcessedIds where assignIds = toIds @@ -405,7 +421,8 @@ allStatIds' s = nub $ assignIds <> otherExpr <> (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] allStatIds s = nub . concat $ allStatIds' <$> universe s @@ -502,28 +519,27 @@ reduce_ title repl bot eval src = do (src ^.. infoSrc . _Wrapped . traverse . modItems . traverse) ) <> ")" - replAnswer <- sequenceA $ evalIfNotEmpty <$> replacement - case (replacement, replAnswer) of - (Single s, Single True ) -> runIf s - (Dual _ r, Dual False True) -> runIf r - (Dual l _, Dual True False) -> runIf l - (Dual l r, Dual True True ) -> check l r - _ -> return src + 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 where - replacement = repl src - runIf s = if s /= src && not (bot s) - then reduce_ title repl bot eval s - else return s - evalIfNotEmpty = eval - check l r - | bot l = return l - | bot r = return r - | otherwise = do - lreduced <- runIf l - rreduced <- runIf r - if _infoSrc lreduced < _infoSrc rreduced - then return lreduced - else return rreduced + cond s = s /= src + recReduction = reduce_ title repl bot eval -- | Reduce an input to a minimal representation. It follows the reduction -- strategy mentioned above. @@ -537,7 +553,7 @@ reduce eval src = $ red "Modules" moduleBot halveModules src >>= redAll "Module Items" modItemBot halveModItems >>= redAll "Statements" (const defaultBot) halveStatements - >>= redAll "Expressions" (const defaultBot) halveExpr + -- >>= redAll "Expressions" (const defaultBot) halveExpr where red s bot a = reduce_ s a bot eval red' s bot a t = reduce_ s (a t) (bot t) eval @@ -585,3 +601,13 @@ reduceSynth a b = reduce synth Fail EquivFail -> True Fail _ -> False Pass _ -> False + +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 diff --git a/src/VeriFuzz/Report.hs b/src/VeriFuzz/Report.hs index 2edd31e..3037b34 100644 --- a/src/VeriFuzz/Report.hs +++ b/src/VeriFuzz/Report.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE RankNTypes #-} {-| Module : VeriFuzz.Report Description : Generate a report from a fuzz run. @@ -16,12 +17,19 @@ module VeriFuzz.Report ( SynthTool(..) , SynthStatus(..) , SynthResult(..) + , SimResult(..) , SimTool(..) , FuzzReport(..) , printResultReport + , printSummary , synthResults , simResults , synthStatus + , equivTime + , fuzzDir + , fileLines + , reducTime + , synthTime , defaultIcarusSim , defaultVivadoSynth , defaultYosysSynth @@ -33,19 +41,37 @@ module VeriFuzz.Report ) where -import Control.DeepSeq (NFData, rnf) -import Control.Lens hiding (Identity) -import Data.ByteString (ByteString) -import Data.Maybe (fromMaybe) -import Data.Text (Text) -import Data.Text.Lazy (toStrict) -import Prelude hiding (FilePath) -import Shelly (fromText) -import Text.Blaze.Html (Html, (!)) -import Text.Blaze.Html.Renderer.Text (renderHtml) +import Control.DeepSeq ( NFData + , rnf + ) +import Control.Lens hiding ( Identity + , (<.>) + ) +import Data.Bifunctor ( bimap ) +import Data.ByteString ( ByteString ) +import Data.Maybe ( fromMaybe ) +import Data.Monoid ( Endo ) +import Data.Text ( Text ) +import qualified Data.Text as T +import Data.Text.Lazy ( toStrict ) +import Data.Time +import Data.Vector ( fromList ) +import Prelude hiding ( FilePath ) +import Shelly ( FilePath + , fromText + , toTextIgnore + , (<.>) + , (</>) + ) +import Statistics.Sample ( meanVariance ) +import Text.Blaze.Html ( Html + , (!) + ) +import Text.Blaze.Html.Renderer.Text ( renderHtml ) import qualified Text.Blaze.Html5 as H import qualified Text.Blaze.Html5.Attributes as A import VeriFuzz.Config +import VeriFuzz.Internal import VeriFuzz.Result import VeriFuzz.Sim import VeriFuzz.Sim.Internal @@ -139,46 +165,55 @@ defaultIcarusSim = IcarusSim defaultIcarus -- | 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 +data SimResult = SimResult !SynthTool !SimTool !BResult !NominalDiffTime deriving (Eq) instance Show SimResult where - show (SimResult synth sim r) = show synth <> ", " <> show sim <> ": " <> show r + 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 -- | The results of comparing the synthesised outputs of two files using a -- formal equivalence checker. This will either return a failure or an output -- which is most likely '()'. -data SynthResult = SynthResult !SynthTool !SynthTool !UResult +data SynthResult = SynthResult !SynthTool !SynthTool !UResult !NominalDiffTime deriving (Eq) instance Show SynthResult where - show (SynthResult synth synth2 r) = show synth <> ", " <> show synth2 <> ": " <> show r + show (SynthResult synth synth2 r d) = show synth <> ", " <> show synth2 <> ": " <> show r <> " (" <> show d <> ")" + +getSynthResult :: SynthResult -> UResult +getSynthResult (SynthResult _ _ a _) = a -- | The status of the synthesis using a simulator. This will be checked before -- attempting to run the equivalence checks on the simulator, as that would be -- unnecessary otherwise. -data SynthStatus = SynthStatus !SynthTool !UResult +data SynthStatus = SynthStatus !SynthTool !UResult !NominalDiffTime deriving (Eq) +getSynthStatus :: SynthStatus -> UResult +getSynthStatus (SynthStatus _ a _) = a + instance Show SynthStatus where - show (SynthStatus synth r) = "synthesis " <> show synth <> ": " <> show r + show (SynthStatus synth r d) = "synthesis " <> show synth <> ": " <> show r <> " (" <> show d <> ")" -- | The complete state that will be used during fuzzing, which contains the -- results from all the operations. -data FuzzReport = FuzzReport { _synthResults :: ![SynthResult] +data FuzzReport = FuzzReport { _fuzzDir :: !FilePath + , _synthResults :: ![SynthResult] , _simResults :: ![SimResult] , _synthStatus :: ![SynthStatus] + , _fileLines :: {-# UNPACK #-} !Int + , _synthTime :: {-# UNPACK #-} !NominalDiffTime + , _equivTime :: {-# UNPACK #-} !NominalDiffTime + , _reducTime :: {-# UNPACK #-} !NominalDiffTime } deriving (Eq, Show) $(makeLenses ''FuzzReport) -instance Semigroup FuzzReport where - FuzzReport a1 b1 c1 <> FuzzReport a2 b2 c2 = FuzzReport (a1 <> a2) (b1 <> b2) (c1 <> c2) - -instance Monoid FuzzReport where - mempty = FuzzReport [] [] [] - descriptionToSim :: SimDescription -> SimTool descriptionToSim (SimDescription "icarus") = defaultIcarusSim descriptionToSim s = @@ -201,11 +236,11 @@ descriptionToSynth (SynthDescription "xst" bin desc out) = descriptionToSynth (SynthDescription "quartus" bin desc out) = QuartusSynth . Quartus (fromText <$> bin) - (fromMaybe (quartusDesc defaultQuartus) $ desc) + (fromMaybe (quartusDesc defaultQuartus) desc) $ maybe (quartusOutput defaultQuartus) fromText out descriptionToSynth (SynthDescription "identity" _ desc out) = IdentitySynth - . Identity (fromMaybe (identityDesc defaultIdentity) $ desc) + . Identity (fromMaybe (identityDesc defaultIdentity) desc) $ maybe (identityOutput defaultIdentity) fromText out descriptionToSynth s = error $ "Could not find implementation for synthesiser '" <> show s <> "'" @@ -220,42 +255,46 @@ 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) = H.tr $ do +synthStatusHtml (SynthStatus synth res diff) = H.tr $ do H.td . H.toHtml $ toText synth status res + H.td . H.toHtml $ showT diff synthResultHtml :: SynthResult -> Html -synthResultHtml (SynthResult synth1 synth2 res) = H.tr $ do +synthResultHtml (SynthResult synth1 synth2 res diff) = H.tr $ do H.td . H.toHtml $ toText synth1 H.td . H.toHtml $ toText synth2 status res + H.td . H.toHtml $ showT diff + +resultHead :: Text -> Html +resultHead name = H.head $ do + H.title $ "Fuzz Report - " <> H.toHtml name + H.meta ! A.name "viewport" ! A.content "width=device-width, initial-scale=1" + H.meta ! A.charset "utf8" + H.link + ! A.rel "stylesheet" + ! A.href + "https://cdnjs.cloudflare.com/ajax/libs/bulma/0.7.4/css/bulma.min.css" resultReport :: Text -> FuzzReport -> Html -resultReport name (FuzzReport synth _ stat) = H.docTypeHtml $ do - H.head $ do - H.title $ "Fuzz Report - " <> H.toHtml name - H.meta ! A.name "viewport" ! A.content - "width=device-width, initial-scale=1" - H.meta ! A.charset "utf8" - H.link - ! A.rel "stylesheet" - ! A.href - "https://cdnjs.cloudflare.com/ajax/libs/bulma/0.7.4/css/bulma.min.css" +resultReport name (FuzzReport _ synth _ stat _ _ _ _) = H.docTypeHtml $ do + resultHead name H.body . (H.section ! A.class_ "section") . (H.div ! A.class_ "container") $ do - H.h1 ! A.class_ "title" $ "Fuzz Report - " <> H.toHtml name - H.h2 ! A.class_ "subtitle" $ "Synthesis Failure" + H.h1 ! A.class_ "title is-1" $ "Fuzz Report - " <> H.toHtml name + H.h2 ! A.class_ "title is-2" $ "Synthesis" H.table ! A.class_ "table" $ do H.thead . H.toHtml $ ( H.tr . H.toHtml - $ [H.th "Synthesis tool", H.th "Synthesis Status"] + $ [H.th "Tool", H.th "Status", H.th "Run time"] ) H.tbody . H.toHtml $ fmap synthStatusHtml stat - H.h2 ! A.class_ "subtitle" $ "Equivalence Check Status" + H.h2 ! A.class_ "title is-2" $ "Equivalence Check" H.table ! A.class_ "table" $ do H.thead . H.toHtml @@ -263,10 +302,107 @@ resultReport name (FuzzReport synth _ stat) = H.docTypeHtml $ do . H.toHtml $ [ H.th "First tool" , H.th "Second tool" - , H.th "Equivalence Status" + , H.th "Status" + , H.th "Run time" ] ) H.tbody . H.toHtml $ fmap synthResultHtml synth +resultStatus :: Result a b -> Html +resultStatus (Pass _) = H.td ! A.class_ "is-success" $ "Passed" +resultStatus (Fail _) = H.td ! A.class_ "is-danger" $ "Failed" + +fuzzStats + :: (Real a1, Traversable t) + => ((a1 -> Const (Endo [a1]) a1) -> a2 -> Const (Endo [a1]) a2) + -> t a2 + -> (Double, Double) +fuzzStats sel fr = meanVariance converted + where converted = fromList . fmap realToFrac $ fr ^.. traverse . sel + +fuzzStatus :: Text -> FuzzReport -> Html +fuzzStatus name (FuzzReport dir s1 s2 s3 sz t1 t2 t3) = H.tr $ do + H.td + . ( H.a + ! A.href + ( H.textValue + $ toTextIgnore (dir </> fromText "index" <.> "html") + ) + ) + $ H.toHtml name + resultStatus + $ mconcat (fmap getSynthResult s1) + <> mconcat (fmap getSimResult s2) + <> mconcat (fmap getSynthStatus s3) + H.td . H.string $ show sz + H.td . H.string $ show t1 + H.td . H.string $ show t2 + H.td . H.string $ show t3 + +summary :: Text -> [FuzzReport] -> Html +summary name fuzz = H.docTypeHtml $ do + resultHead name + H.body + . (H.section ! A.class_ "section") + . (H.div ! A.class_ "container") + $ do + H.h1 ! A.class_ "title is-1" $ "FuzzReport - " <> H.toHtml name + H.table ! A.class_ "table" $ do + H.thead . H.tr $ H.toHtml + [ H.th "Name" + , H.th "Status" + , H.th "Size (loc)" + , H.th "Synthesis time" + , H.th "Equivalence check time" + , H.th "Reduction time" + ] + H.tbody + . H.toHtml + . fmap + (\(i, r) -> + fuzzStatus ("Fuzz " <> showT (i :: Int)) r + ) + $ zip [1 ..] fuzz + H.tfoot . H.toHtml $ do + H.tr $ H.toHtml + [ H.td $ H.strong "Total" + , H.td mempty + , H.td + . H.string + . show + . sum + $ fuzz + ^.. traverse + . fileLines + , sumUp synthTime + , sumUp equivTime + , sumUp reducTime + ] + H.tr $ H.toHtml + [ H.td $ H.strong "Mean" + , H.td mempty + , fst $ bimap d2I d2I $ fuzzStats fileLines fuzz + , fst $ meanVar synthTime + , fst $ meanVar equivTime + , fst $ meanVar reducTime + ] + H.tr $ H.toHtml + [ H.td $ H.strong "Variance" + , H.td mempty + , snd $ bimap d2I d2I $ fuzzStats fileLines fuzz + , snd $ meanVar synthTime + , snd $ meanVar equivTime + , snd $ meanVar reducTime + ] + where + sumUp s = showHtml . sum $ fuzz ^.. traverse . s + 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 + printResultReport :: Text -> FuzzReport -> Text printResultReport t f = toStrict . renderHtml $ resultReport t f + +printSummary :: Text -> [FuzzReport] -> Text +printSummary t f = toStrict . renderHtml $ summary t f diff --git a/src/VeriFuzz/Result.hs b/src/VeriFuzz/Result.hs index 4d1f5b8..4ea7988 100644 --- a/src/VeriFuzz/Result.hs +++ b/src/VeriFuzz/Result.hs @@ -31,8 +31,14 @@ import Control.Monad.Base import Control.Monad.IO.Class import Control.Monad.Trans.Class import Control.Monad.Trans.Control -import Shelly (RunFailed (..), Sh, catch_sh) -import Shelly.Lifted (MonadSh, liftSh) +import Data.Bifunctor ( Bifunctor(..) ) +import Shelly ( RunFailed(..) + , Sh + , catch_sh + ) +import Shelly.Lifted ( MonadSh + , liftSh + ) -- | Result type which is equivalent to 'Either' or 'Error'. This is -- reimplemented so that there is full control over the 'Monad' definition and @@ -42,7 +48,7 @@ data Result a b = Fail a deriving (Eq, Show) instance Semigroup (Result a b) where - Fail _ <> b = b + Pass _ <> a = a a <> _ = a instance (Monoid b) => Monoid (Result a b) where @@ -64,6 +70,10 @@ instance Monad (Result a) where instance MonadBase (Result a) (Result a) where liftBase = id +instance Bifunctor Result where + bimap a _ (Fail c) = Fail $ a c + bimap _ b (Pass c) = Pass $ b c + -- | The transformer for the 'Result' type. This newtype ResultT a m b = ResultT { runResultT :: m (Result a b) } diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs index 423d51b..8e62136 100644 --- a/src/VeriFuzz/Sim/Icarus.hs +++ b/src/VeriFuzz/Sim/Icarus.hs @@ -13,30 +13,41 @@ Icarus verilog module. module VeriFuzz.Sim.Icarus ( Icarus(..) , defaultIcarus + , runSimIc ) where -import Control.DeepSeq (NFData, rnf, rwhnf) +import Control.DeepSeq ( NFData + , rnf + , rwhnf + ) import Control.Lens -import Crypto.Hash (Digest, hash) -import Crypto.Hash.Algorithms (SHA256) -import Data.Binary (encode) -import qualified Data.ByteArray as BA (convert) -import Data.ByteString (ByteString) -import qualified Data.ByteString as B -import Data.ByteString.Lazy (toStrict) -import qualified Data.ByteString.Lazy as L (ByteString) -import Data.Char (digitToInt) -import Data.Foldable (fold) -import Data.List (transpose) -import Data.Maybe (listToMaybe) -import Data.Text (Text) -import qualified Data.Text as T -import Numeric (readInt) -import Prelude hiding (FilePath) +import Control.Monad ( void ) +import Crypto.Hash ( Digest + , hash + ) +import Crypto.Hash.Algorithms ( SHA256 ) +import Data.Binary ( encode ) +import Data.Bits +import qualified Data.ByteArray as BA + ( convert ) +import Data.ByteString ( ByteString ) +import qualified Data.ByteString as B +import Data.ByteString.Lazy ( toStrict ) +import qualified Data.ByteString.Lazy as L + ( ByteString ) +import Data.Char ( digitToInt ) +import Data.Foldable ( fold ) +import Data.List ( transpose ) +import Data.Maybe ( listToMaybe ) +import Data.Text ( Text ) +import qualified Data.Text as T +import Numeric ( readInt ) +import Prelude hiding ( FilePath ) import Shelly -import Shelly.Lifted (liftSh) +import Shelly.Lifted ( liftSh ) import VeriFuzz.Sim.Internal +import VeriFuzz.Sim.Template import VeriFuzz.Verilog.AST import VeriFuzz.Verilog.BitVec import VeriFuzz.Verilog.CodeGen @@ -117,11 +128,68 @@ runSimIcarusWithFile :: Icarus -> FilePath -> [ByteString] -> ResultSh ByteString runSimIcarusWithFile sim f _ = annotate SimFail . liftSh $ do dir <- pwd - logger "Icarus: Compile" logCommand_ dir "icarus" $ run (icarusPath sim) ["-o", "main", toTextIgnore f] - logger "Icarus: Run" B.take 8 . BA.convert . (hash :: ByteString -> Digest SHA256) <$> logCommand dir "vvp" (runFoldLines (mempty :: ByteString) callback (vvpPath sim) ["main"]) + +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 + (Assign "clk" Nothing (UnOp UnNot (Id "clk"))) + , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable $ Task + "strobe" + ["%b", Id "y"] + ] + [] + + liftSh . writefile "testbench.v" $ icarusTestbench (Verilog [tb]) synth1 + liftSh $ exe dir "icarus" "iverilog" ["-o", "main", "testbench.v"] + liftSh + $ B.take 8 + . BA.convert + . (hash :: ByteString -> Digest SHA256) + <$> logCommand + dir + "vvp" + (runFoldLines (mempty :: ByteString) + callback + (vvpPath sim1) + ["main"] + ) + where + exe dir name e = void . errExit False . logCommand dir name . timeout e diff --git a/src/VeriFuzz/Sim/Identity.hs b/src/VeriFuzz/Sim/Identity.hs index bfded0b..95b4097 100644 --- a/src/VeriFuzz/Sim/Identity.hs +++ b/src/VeriFuzz/Sim/Identity.hs @@ -16,11 +16,16 @@ module VeriFuzz.Sim.Identity ) where -import Control.DeepSeq (NFData, rnf, rwhnf) -import Data.Text (Text, unpack) -import Prelude hiding (FilePath) -import Shelly (FilePath) -import Shelly.Lifted (writefile) +import Control.DeepSeq ( NFData + , rnf + , rwhnf + ) +import Data.Text ( Text + , unpack + ) +import Prelude hiding ( FilePath ) +import Shelly ( FilePath ) +import Shelly.Lifted ( writefile ) import VeriFuzz.Sim.Internal import VeriFuzz.Verilog.AST import VeriFuzz.Verilog.CodeGen diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs index 5c58e1a..a05a96f 100644 --- a/src/VeriFuzz/Sim/Internal.hs +++ b/src/VeriFuzz/Sim/Internal.hs @@ -40,20 +40,26 @@ module VeriFuzz.Sim.Internal where import Control.Lens -import Control.Monad (forM, void) -import Control.Monad.Catch (throwM) -import Data.Bits (shiftL) -import Data.ByteString (ByteString) -import qualified Data.ByteString as B -import Data.Maybe (catMaybes) -import Data.Text (Text) -import qualified Data.Text as T -import Data.Time.Format (defaultTimeLocale, formatTime) -import Data.Time.LocalTime (getZonedTime) -import Prelude hiding (FilePath) +import Control.Monad ( forM + , void + ) +import Control.Monad.Catch ( throwM ) +import Data.Bits ( shiftL ) +import Data.ByteString ( ByteString ) +import qualified Data.ByteString as B +import Data.Maybe ( catMaybes ) +import Data.Text ( Text ) +import qualified Data.Text as T +import Data.Time.Format ( defaultTimeLocale + , formatTime + ) +import Data.Time.LocalTime ( getZonedTime ) +import Prelude hiding ( FilePath ) import Shelly -import Shelly.Lifted (MonadSh, liftSh) -import System.FilePath.Posix (takeBaseName) +import Shelly.Lifted ( MonadSh + , liftSh + ) +import System.FilePath.Posix ( takeBaseName ) import VeriFuzz.Internal import VeriFuzz.Result import VeriFuzz.Verilog.AST @@ -188,21 +194,28 @@ logCommand_ :: FilePath -> Text -> Sh a -> Sh () logCommand_ fp name = void . logCommand fp name execute - :: (MonadSh m, Monad m, Monoid a) - => a + :: (MonadSh m, Monad m) + => Failed -> FilePath -> Text -> FilePath -> [Text] - -> ResultT a m Text -execute f dir name e = annotate f . liftSh . logCommand dir name . timeout e + -> ResultT Failed m Text +execute f dir name e cs = do + (res, exitCode) <- liftSh $ do + res <- errExit False . logCommand dir name $ timeout e cs + (,) res <$> lastExitCode + case exitCode of + 0 -> ResultT . return $ Pass res + 124 -> ResultT . return $ Fail TimeoutError + _ -> ResultT . return $ Fail f execute_ - :: (MonadSh m, Monad m, Monoid a) - => a + :: (MonadSh m, Monad m) + => Failed -> FilePath -> Text -> FilePath -> [Text] - -> ResultT a m () + -> ResultT Failed m () execute_ a b c d = void . execute a b c d diff --git a/src/VeriFuzz/Sim/Quartus.hs b/src/VeriFuzz/Sim/Quartus.hs index ece00eb..e0fbba5 100644 --- a/src/VeriFuzz/Sim/Quartus.hs +++ b/src/VeriFuzz/Sim/Quartus.hs @@ -16,11 +16,16 @@ module VeriFuzz.Sim.Quartus ) where -import Control.DeepSeq (NFData, rnf, rwhnf) -import Data.Text (Text, unpack) -import Prelude hiding (FilePath) +import Control.DeepSeq ( NFData + , rnf + , rwhnf + ) +import Data.Text ( Text + , unpack + ) +import Prelude hiding ( FilePath ) import Shelly -import Shelly.Lifted (liftSh) +import Shelly.Lifted ( liftSh ) import VeriFuzz.Sim.Internal import VeriFuzz.Verilog.AST import VeriFuzz.Verilog.CodeGen @@ -52,12 +57,16 @@ runSynthQuartus :: Quartus -> SourceInfo -> ResultSh () runSynthQuartus sim (SourceInfo top src) = do dir <- liftSh pwd let ex = execute_ SynthFail dir "quartus" - liftSh $ do - writefile inpf $ genSource src - logger "Running Quartus synthesis" + 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=5CGTFD9E5F35C7N"] + ex (exec "quartus_fit") [top, "--part=5CGXFC7D6F31C6"] ex (exec "quartus_eda") [top, "--simulation", "--tool=vcs"] liftSh $ do cp (fromText "simulation/vcs" </> fromText top <.> "vo") @@ -68,7 +77,6 @@ runSynthQuartus sim (SourceInfo top src) = do , "s,^// DATE.*,,; s,^tri1 (.*);,wire \\1 = 1;,; /^\\/\\/ +synopsys/ d;" , toTextIgnore $ synthOutput sim ] - logger "Quartus synthesis done" where inpf = "rtl.v" exec s = maybe (fromText s) (</> fromText s) $ quartusBin sim diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs index 4aa07f6..3be6558 100644 --- a/src/VeriFuzz/Sim/Template.hs +++ b/src/VeriFuzz/Sim/Template.hs @@ -18,17 +18,19 @@ module VeriFuzz.Sim.Template , xstSynthConfig , vivadoSynthConfig , sbyConfig + , icarusTestbench ) where -import Control.Lens ((^..)) -import Data.Text (Text) -import qualified Data.Text as T -import Prelude hiding (FilePath) +import Control.Lens ((^..)) +import Data.Text (Text) +import qualified Data.Text as T +import Prelude hiding (FilePath) import Shelly -import Text.Shakespeare.Text (st) +import Text.Shakespeare.Text (st) import VeriFuzz.Sim.Internal import VeriFuzz.Verilog.AST +import VeriFuzz.Verilog.CodeGen rename :: Text -> [Text] -> Text rename end entries = @@ -117,3 +119,15 @@ top.v . 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" +`include "#{toTextIgnore $ synthOutput synth1}" + +#{genSource t} +|] diff --git a/src/VeriFuzz/Sim/Vivado.hs b/src/VeriFuzz/Sim/Vivado.hs index ee67a78..8697a0f 100644 --- a/src/VeriFuzz/Sim/Vivado.hs +++ b/src/VeriFuzz/Sim/Vivado.hs @@ -16,11 +16,16 @@ module VeriFuzz.Sim.Vivado ) where -import Control.DeepSeq (NFData, rnf, rwhnf) -import Data.Text (Text, unpack) -import Prelude hiding (FilePath) +import Control.DeepSeq ( NFData + , rnf + , rwhnf + ) +import Data.Text ( Text + , unpack + ) +import Prelude hiding ( FilePath ) import Shelly -import Shelly.Lifted (liftSh) +import Shelly.Lifted ( liftSh ) import VeriFuzz.Sim.Internal import VeriFuzz.Sim.Template import VeriFuzz.Verilog.AST @@ -56,13 +61,16 @@ runSynthVivado sim (SourceInfo top src) = do writefile vivadoTcl . vivadoSynthConfig top . toTextIgnore $ synthOutput sim writefile "rtl.v" $ genSource src - run_ "sed" ["s/^module/(* use_dsp=\"no\" *) module/;", "-i", "rtl.v"] - logger "Vivado: run" + run_ + "sed" + [ "s/^module/(* use_dsp48=\"no\" *) (* use_dsp=\"no\" *) module/;" + , "-i" + , "rtl.v" + ] let exec_ n = execute_ SynthFail dir "vivado" (maybe (fromText n) (</> fromText n) $ vivadoBin sim) exec_ "vivado" ["-mode", "batch", "-source", toTextIgnore vivadoTcl] - liftSh $ logger "Vivado: done" where vivadoTcl = fromText ("vivado_" <> top) <.> "tcl" diff --git a/src/VeriFuzz/Sim/XST.hs b/src/VeriFuzz/Sim/XST.hs index 11be094..f5faae5 100644 --- a/src/VeriFuzz/Sim/XST.hs +++ b/src/VeriFuzz/Sim/XST.hs @@ -18,12 +18,17 @@ module VeriFuzz.Sim.XST ) where -import Control.DeepSeq (NFData, rnf, rwhnf) -import Data.Text (Text, unpack) -import Prelude hiding (FilePath) +import Control.DeepSeq ( NFData + , rnf + , rwhnf + ) +import Data.Text ( Text + , unpack + ) +import Prelude hiding ( FilePath ) import Shelly -import Shelly.Lifted (liftSh) -import Text.Shakespeare.Text (st) +import Shelly.Lifted ( liftSh ) +import Text.Shakespeare.Text ( st ) import VeriFuzz.Sim.Internal import VeriFuzz.Sim.Template import VeriFuzz.Verilog.AST @@ -64,9 +69,7 @@ runSynthXST sim (SourceInfo top src) = do writefile xstFile $ xstSynthConfig top writefile prjFile [st|verilog work "rtl.v"|] writefile "rtl.v" $ genSource src - logger "XST: run" exec "xst" ["-ifn", toTextIgnore xstFile] - liftSh $ logger "XST: netgen" exec "netgen" [ "-w" @@ -75,15 +78,12 @@ runSynthXST sim (SourceInfo top src) = do , toTextIgnore $ modFile <.> "ngc" , toTextIgnore $ synthOutput sim ] - liftSh $ do - logger "XST: clean" - noPrint $ run_ - "sed" - [ "-i" - , "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;" - , toTextIgnore $ synthOutput sim - ] - logger "XST: done" + liftSh . noPrint $ run_ + "sed" + [ "-i" + , "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;" + , toTextIgnore $ synthOutput sim + ] where modFile = fromText top xstFile = modFile <.> "xst" diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs index 3081a65..8f9d4a7 100644 --- a/src/VeriFuzz/Sim/Yosys.hs +++ b/src/VeriFuzz/Sim/Yosys.hs @@ -20,14 +20,19 @@ module VeriFuzz.Sim.Yosys ) where -import Control.DeepSeq (NFData, rnf, rwhnf) +import Control.DeepSeq ( NFData + , rnf + , rwhnf + ) import Control.Lens -import Control.Monad (void) -import Data.Text (Text, unpack) -import Prelude hiding (FilePath) +import Control.Monad ( void ) +import Data.Text ( Text + , unpack + ) +import Prelude hiding ( FilePath ) import Shelly -import Shelly.Lifted (liftSh) -import Text.Shakespeare.Text (st) +import Shelly.Lifted ( liftSh ) +import Text.Shakespeare.Text ( st ) import VeriFuzz.Result import VeriFuzz.Sim.Internal import VeriFuzz.Sim.Template @@ -62,16 +67,19 @@ yosysPath :: Yosys -> FilePath yosysPath sim = maybe (fromText "yosys") (</> fromText "yosys") $ yosysBin sim runSynthYosys :: Yosys -> SourceInfo -> ResultSh () -runSynthYosys sim (SourceInfo _ src) = (<?> SynthFail) . liftSh $ do - dir <- pwd - writefile inpf $ genSource src - logger "Yosys: synthesis" - logCommand_ dir "yosys" $ timeout +runSynthYosys sim (SourceInfo _ src) = do + dir <- liftSh $ do + dir' <- pwd + writefile inpf $ genSource src + return dir' + execute_ + SynthFail + dir + "yosys" (yosysPath sim) [ "-p" , "read -formal " <> inp <> "; synth; write_verilog -noattr " <> out ] - logger "Yosys: synthesis done" where inpf = "rtl.v" inp = toTextIgnore inpf @@ -95,10 +103,7 @@ runEquivYosys yosys sim1 sim2 srcInfo = do writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo runSynth sim1 srcInfo runSynth sim2 srcInfo - liftSh $ do - logger "Yosys: equivalence check" - run_ (yosysPath yosys) [toTextIgnore checkFile] - logger "Yosys: equivalence done" + liftSh $ run_ (yosysPath yosys) [toTextIgnore checkFile] where checkFile = fromText [st|test.#{toText sim1}.#{toText sim2}.ys|] runEquiv @@ -115,12 +120,11 @@ runEquiv sim1 sim2 srcInfo = do replaceMods (synthOutput sim1) "_1" srcInfo replaceMods (synthOutput sim2) "_2" srcInfo writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo - liftSh $ logger "Running SymbiYosys" e <- liftSh $ do exe dir "symbiyosys" "sby" ["-f", "proof.sby"] lastExitCode case e of - 0 -> liftSh $ logger "SymbiYosys equivalence check passed" + 0 -> ResultT . return $ Pass () 2 -> ResultT . return $ Fail EquivFail 124 -> ResultT . return $ Fail TimeoutError _ -> ResultT . return $ Fail EquivError diff --git a/src/VeriFuzz/Verilog.hs b/src/VeriFuzz/Verilog.hs index 3e8d2c7..628b00a 100644 --- a/src/VeriFuzz/Verilog.hs +++ b/src/VeriFuzz/Verilog.hs @@ -10,6 +10,8 @@ Portability : POSIX Verilog implementation with random generation and mutations. -} +{-# LANGUAGE QuasiQuotes #-} + module VeriFuzz.Verilog ( SourceInfo(..) , Verilog(..) diff --git a/src/VeriFuzz/Verilog/AST.hs b/src/VeriFuzz/Verilog/AST.hs index 306366c..43063e6 100644 --- a/src/VeriFuzz/Verilog/AST.hs +++ b/src/VeriFuzz/Verilog/AST.hs @@ -139,14 +139,18 @@ module VeriFuzz.Verilog.AST ) where -import Control.Lens hiding ((<|)) +import Control.Lens hiding ( (<|) ) import Data.Data import Data.Data.Lens -import Data.Functor.Foldable.TH (makeBaseFunctor) -import Data.List.NonEmpty (NonEmpty (..), (<|)) -import Data.String (IsString, fromString) -import Data.Text (Text) -import Data.Traversable (sequenceA) +import Data.Functor.Foldable.TH ( makeBaseFunctor ) +import Data.List.NonEmpty ( NonEmpty(..) + , (<|) + ) +import Data.String ( IsString + , fromString + ) +import Data.Text ( Text ) +import Data.Traversable ( sequenceA ) import VeriFuzz.Verilog.BitVec -- | Identifier in Verilog. This is just a string of characters that can either @@ -169,6 +173,9 @@ data Event = EId {-# UNPACK #-} !Identifier | EComb !Event !Event deriving (Eq, Show, Ord, Data) +instance Plated Event where + plate = uniplate + -- | Binary operators that are currently supported in the verilog generation. data BinaryOperator = BinPlus -- ^ @+@ | BinMinus -- ^ @-@ @@ -492,7 +499,7 @@ newtype Verilog = Verilog { getVerilog :: [ModDecl] } data SourceInfo = SourceInfo { _infoTop :: {-# UNPACK #-} !Text , _infoSrc :: !Verilog } - deriving (Eq, Show) + deriving (Eq, Ord, Data, Show) $(makeLenses ''Expr) $(makeLenses ''ConstExpr) diff --git a/src/VeriFuzz/Verilog/CodeGen.hs b/src/VeriFuzz/Verilog/CodeGen.hs index a0ec0cc..82945aa 100644 --- a/src/VeriFuzz/Verilog/CodeGen.hs +++ b/src/VeriFuzz/Verilog/CodeGen.hs @@ -17,18 +17,20 @@ This module generates the code from the Verilog AST defined in module VeriFuzz.Verilog.CodeGen ( -- * Code Generation GenVerilog(..) - , genSource + , Source(..) , render ) where -import Data.Data (Data) -import Data.List.NonEmpty (NonEmpty (..), toList) -import Data.Text (Text) -import qualified Data.Text as T +import Data.Data ( Data ) +import Data.List.NonEmpty ( NonEmpty(..) + , toList + ) +import Data.Text ( Text ) +import qualified Data.Text as T import Data.Text.Prettyprint.Doc -import Numeric (showHex) -import VeriFuzz.Internal hiding (comma) +import Numeric ( showHex ) +import VeriFuzz.Internal hiding ( comma ) import VeriFuzz.Verilog.AST import VeriFuzz.Verilog.BitVec diff --git a/src/VeriFuzz/Verilog/Eval.hs b/src/VeriFuzz/Verilog/Eval.hs index 4a43c19..d8840e3 100644 --- a/src/VeriFuzz/Verilog/Eval.hs +++ b/src/VeriFuzz/Verilog/Eval.hs @@ -17,9 +17,9 @@ module VeriFuzz.Verilog.Eval where import Data.Bits -import Data.Foldable (fold) -import Data.Functor.Foldable hiding (fold) -import Data.Maybe (listToMaybe) +import Data.Foldable ( fold ) +import Data.Functor.Foldable hiding ( fold ) +import Data.Maybe ( listToMaybe ) import VeriFuzz.Verilog.AST import VeriFuzz.Verilog.BitVec diff --git a/src/VeriFuzz/Verilog/Gen.hs b/src/VeriFuzz/Verilog/Gen.hs index f2d2b0a..f08e5a6 100644 --- a/src/VeriFuzz/Verilog/Gen.hs +++ b/src/VeriFuzz/Verilog/Gen.hs @@ -237,14 +237,6 @@ someI m f = do amount <- gen $ Hog.int (Hog.linear 1 m) replicateM amount f -some :: StateGen a -> StateGen [a] -some = someI 50 - -many :: StateGen a -> StateGen [a] -many f = do - amount <- gen $ Hog.int (Hog.linear 0 50) - replicateM amount f - makeIdentifier :: T.Text -> StateGen Identifier makeIdentifier prefix = do context <- get @@ -481,10 +473,11 @@ calcRange ps i (Range l r) = eval l - eval r + 1 moduleDef :: Maybe Identifier -> StateGen ModDecl moduleDef top = do name <- moduleName top - portList <- some $ nextPort Wire + portList <- Hog.list (Hog.linear 4 10) $ nextPort Wire mi <- Hog.list (Hog.linear 4 100) modItem - ps <- many parameter + ps <- Hog.list (Hog.linear 0 10) parameter context <- get + config <- lift ask let local = filter (`notElem` portList) $ _variables context let size = @@ -493,12 +486,14 @@ moduleDef top = do $ local ^.. traverse . portSize - let clock = Port Wire False 1 "clk" - let yport = Port Wire False size "y" - let comb = combineAssigns_ yport local + 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 return . declareMod local - . ModDecl name [yport] (clock : portList) (mi <> [comb]) + . ModDecl name [yport] (clock : portList) (comb : mi) $ ps -- | Procedural generation method for random Verilog. Uses internal 'Reader' and diff --git a/src/VeriFuzz/Verilog/Internal.hs b/src/VeriFuzz/Verilog/Internal.hs index 8d19c14..16148cf 100644 --- a/src/VeriFuzz/Verilog/Internal.hs +++ b/src/VeriFuzz/Verilog/Internal.hs @@ -29,7 +29,7 @@ module VeriFuzz.Verilog.Internal where import Control.Lens -import Data.Text (Text) +import Data.Text ( Text ) import VeriFuzz.Verilog.AST regDecl :: Identifier -> ModItem diff --git a/src/VeriFuzz/Verilog/Mutate.hs b/src/VeriFuzz/Verilog/Mutate.hs index 66f3c37..e4a10df 100644 --- a/src/VeriFuzz/Verilog/Mutate.hs +++ b/src/VeriFuzz/Verilog/Mutate.hs @@ -41,10 +41,12 @@ module VeriFuzz.Verilog.Mutate where import Control.Lens -import Data.Foldable (fold) -import Data.Maybe (catMaybes, fromMaybe) -import Data.Text (Text) -import qualified Data.Text as T +import Data.Foldable ( fold ) +import Data.Maybe ( catMaybes + , fromMaybe + ) +import Data.Text ( Text ) +import qualified Data.Text as T import VeriFuzz.Circuit.Internal import VeriFuzz.Internal import VeriFuzz.Verilog.AST @@ -337,30 +339,30 @@ declareMod ports = initMod . (modItems %~ (decl ++)) -- >>> GenVerilog . simplify $ (Id "y") + (Id "x") -- (y + x) simplify :: Expr -> Expr -simplify (BinOp (Number (BitVec _ 1)) BinAnd e) = e -simplify (BinOp e BinAnd (Number (BitVec _ 1))) = e -simplify (BinOp (Number (BitVec _ 0)) BinAnd _) = Number 0 -simplify (BinOp _ BinAnd (Number (BitVec _ 0))) = Number 0 -simplify (BinOp e BinPlus (Number (BitVec _ 0))) = e -simplify (BinOp (Number (BitVec _ 0)) BinPlus e) = e +simplify (BinOp (Number (BitVec _ 1)) BinAnd e) = e +simplify (BinOp e BinAnd (Number (BitVec _ 1))) = e +simplify (BinOp (Number (BitVec _ 0)) BinAnd _) = Number 0 +simplify (BinOp _ BinAnd (Number (BitVec _ 0))) = Number 0 +simplify (BinOp e BinPlus (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinPlus e) = e simplify (BinOp e BinMinus (Number (BitVec _ 0))) = e simplify (BinOp (Number (BitVec _ 0)) BinMinus e) = e simplify (BinOp e BinTimes (Number (BitVec _ 1))) = e simplify (BinOp (Number (BitVec _ 1)) BinTimes e) = e simplify (BinOp _ BinTimes (Number (BitVec _ 0))) = Number 0 simplify (BinOp (Number (BitVec _ 0)) BinTimes _) = Number 0 -simplify (BinOp e BinOr (Number (BitVec _ 0))) = e -simplify (BinOp (Number (BitVec _ 0)) BinOr e) = e -simplify (BinOp e BinLSL (Number (BitVec _ 0))) = e -simplify (BinOp (Number (BitVec _ 0)) BinLSL e) = e -simplify (BinOp e BinLSR (Number (BitVec _ 0))) = e -simplify (BinOp (Number (BitVec _ 0)) BinLSR e) = e -simplify (BinOp e BinASL (Number (BitVec _ 0))) = e -simplify (BinOp (Number (BitVec _ 0)) BinASL e) = e -simplify (BinOp e BinASR (Number (BitVec _ 0))) = e -simplify (BinOp (Number (BitVec _ 0)) BinASR e) = e -simplify (UnOp UnPlus e) = e -simplify e = e +simplify (BinOp e BinOr (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinOr e) = e +simplify (BinOp e BinLSL (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinLSL e) = e +simplify (BinOp e BinLSR (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinLSR e) = e +simplify (BinOp e BinASL (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinASL e) = e +simplify (BinOp e BinASR (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinASR e) = e +simplify (UnOp UnPlus e) = e +simplify e = e -- | Remove all 'Identifier' that do not appeare in the input list from an -- 'Expr'. The identifier will be replaced by @1'b0@, which can then later be @@ -377,13 +379,21 @@ removeId i = transform trans combineAssigns :: Port -> [ModItem] -> [ModItem] combineAssigns p a = - a <> [ModCA . ContAssign (p ^. portName) . fold $ Id <$> assigns] + a + <> [ ModCA + . ContAssign (p ^. portName) + . UnOp UnXor + . fold + $ Id + <$> assigns + ] where assigns = a ^.. traverse . modContAssign . contAssignNetLVal -combineAssigns_ :: Port -> [Port] -> ModItem -combineAssigns_ p ps = +combineAssigns_ :: Bool -> Port -> [Port] -> ModItem +combineAssigns_ comb p ps = ModCA . ContAssign (p ^. portName) + . (if comb then UnOp UnXor else id) . fold $ Id <$> ps diff --git a/src/VeriFuzz/Verilog/Parser.hs b/src/VeriFuzz/Verilog/Parser.hs index 68d0ef3..0820e48 100644 --- a/src/VeriFuzz/Verilog/Parser.hs +++ b/src/VeriFuzz/Verilog/Parser.hs @@ -26,17 +26,20 @@ module VeriFuzz.Verilog.Parser where import Control.Lens -import Control.Monad (void) -import Data.Bifunctor (bimap) +import Control.Monad ( void ) +import Data.Bifunctor ( bimap ) import Data.Bits -import Data.Functor (($>)) -import Data.Functor.Identity (Identity) -import Data.List (isInfixOf, isPrefixOf, null) -import Data.List.NonEmpty (NonEmpty (..)) -import Data.Text (Text) -import qualified Data.Text as T -import qualified Data.Text.IO as T -import Text.Parsec hiding (satisfy) +import Data.Functor ( ($>) ) +import Data.Functor.Identity ( Identity ) +import Data.List ( isInfixOf + , isPrefixOf + , null + ) +import Data.List.NonEmpty ( NonEmpty(..) ) +import Data.Text ( Text ) +import qualified Data.Text as T +import qualified Data.Text.IO as T +import Text.Parsec hiding ( satisfy ) import Text.Parsec.Expr import VeriFuzz.Internal import VeriFuzz.Verilog.AST diff --git a/src/VeriFuzz/Verilog/Quote.hs b/src/VeriFuzz/Verilog/Quote.hs index 362cf06..f0b7c96 100644 --- a/src/VeriFuzz/Verilog/Quote.hs +++ b/src/VeriFuzz/Verilog/Quote.hs @@ -18,8 +18,8 @@ module VeriFuzz.Verilog.Quote where import Data.Data -import qualified Data.Text as T -import qualified Language.Haskell.TH as TH +import qualified Data.Text as T +import qualified Language.Haskell.TH as TH import Language.Haskell.TH.Quote import Language.Haskell.TH.Syntax import VeriFuzz.Verilog.Parser |