aboutsummaryrefslogtreecommitdiffstats
path: root/src/Verismith.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/Verismith.hs')
-rw-r--r--src/Verismith.hs503
1 files changed, 264 insertions, 239 deletions
diff --git a/src/Verismith.hs b/src/Verismith.hs
index e709ff4..4fb52ac 100644
--- a/src/Verismith.hs
+++ b/src/Verismith.hs
@@ -1,133 +1,137 @@
-{-|
-Module : Verismith
-Description : Verismith
-Copyright : (c) 2018-2019, Yann Herklotz
-License : GPL-3
-Maintainer : yann [at] yannherklotz [dot] com
-Stability : experimental
-Portability : POSIX
--}
-
{-# OPTIONS_GHC -Wno-unused-top-binds #-}
+-- |
+-- Module : Verismith
+-- Description : Verismith
+-- Copyright : (c) 2018-2019, Yann Herklotz
+-- License : GPL-3
+-- Maintainer : yann [at] yannherklotz [dot] com
+-- Stability : experimental
+-- Portability : POSIX
module Verismith
- ( defaultMain
+ ( defaultMain,
+
-- * Types
- , Opts(..)
- , SourceInfo(..)
+ Opts (..),
+ SourceInfo (..),
+
-- * Run functions
- , runEquivalence
- , runSimulation
- , runReduce
- , draw
+ runEquivalence,
+ runSimulation,
+ runReduce,
+ draw,
+
-- * Verilog generation functions
- , procedural
- , proceduralIO
- , proceduralSrc
- , proceduralSrcIO
- , randomMod
+ procedural,
+ proceduralIO,
+ proceduralSrc,
+ proceduralSrcIO,
+ randomMod,
+
-- * Extra modules
- , module Verismith.Verilog
- , module Verismith.Config
- , module Verismith.Circuit
- , module Verismith.Tool
- , module Verismith.Fuzz
- , module Verismith.Report
- )
+ module Verismith.Verilog,
+ module Verismith.Config,
+ module Verismith.Circuit,
+ module Verismith.Tool,
+ module Verismith.Fuzz,
+ module Verismith.Report,
+ )
where
-import Control.Concurrent
-import Control.Lens hiding ((<.>))
-import Control.Monad.IO.Class (liftIO)
-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 Control.Concurrent
+import Control.Lens hiding ((<.>))
+import Control.Monad.IO.Class (liftIO)
+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 Paths_verismith (getDataDir)
-import Prelude hiding (FilePath)
-import Shelly hiding (command)
-import Shelly.Lifted (liftSh)
-import System.Random (randomIO)
-import Verismith.Circuit
-import Verismith.Config
-import Verismith.Fuzz
-import Verismith.Generate
-import Verismith.OptParser
-import Verismith.Reduce
-import Verismith.Report
-import Verismith.Result
-import Verismith.Tool
-import Verismith.Tool.Internal
-import Verismith.Verilog
-import Verismith.Verilog.Parser (parseSourceInfoFile)
+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 Paths_verismith (getDataDir)
+import Shelly hiding (command)
+import Shelly.Lifted (liftSh)
+import System.Random (randomIO)
+import Verismith.Circuit
+import Verismith.Config
+import Verismith.Fuzz
+import Verismith.Generate
+import Verismith.OptParser
+import Verismith.Reduce
+import Verismith.Report
+import Verismith.Result
+import Verismith.Tool
+import Verismith.Tool.Internal
import Verismith.Utils (generateByteString)
+import Verismith.Verilog
+import Verismith.Verilog.Parser (parseSourceInfoFile)
+import Prelude hiding (FilePath)
toFP :: String -> FilePath
toFP = fromText . T.pack
myForkIO :: IO () -> IO (MVar ())
myForkIO io = do
- mvar <- newEmptyMVar
- _ <- forkFinally io (\_ -> putMVar mvar ())
- return mvar
+ mvar <- newEmptyMVar
+ _ <- forkFinally io (\_ -> putMVar mvar ())
+ return mvar
getConfig :: Maybe FilePath -> IO Config
getConfig s =
- maybe (return defaultConfig) parseConfigFile $ T.unpack . toTextIgnore <$> 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
+ 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
- r <- randomIO
- return $ if r then i else 0
+ r <- randomIO
+ return $ if r then i else 0
randomise :: Config -> IO Config
randomise config@(Config a _ c d e) = do
- mia <- return $ cm ^. probModItemAssign
- misa <- return $ cm ^. probModItemSeqAlways
- mica <- return $ cm ^. probModItemCombAlways
- mii <- return $ cm ^. probModItemInst
- ssb <- return $ cs ^. probStmntBlock
- ssnb <- return $ cs ^. probStmntNonBlock
- ssc <- return $ cs ^. probStmntCond
- ssf <- return $ cs ^. probStmntFor
- en <- return $ ce ^. probExprNum
- keep_out <- return $ cmo ^. probModDropOutput
- drop_out <- randDelete $ cmo ^. probModDropOutput
- ei <- randDelete $ ce ^. probExprId
- ers <- randDelete $ ce ^. probExprRangeSelect
- euo <- randDelete $ ce ^. probExprUnOp
- ebo <- randDelete $ ce ^. probExprBinOp
- ec <- randDelete $ ce ^. probExprCond
- eco <- randDelete $ ce ^. probExprConcat
- estr <- randDelete $ ce ^. probExprStr
- esgn <- randDelete $ ce ^. probExprSigned
- eus <- randDelete $ ce ^. probExprUnsigned
- return $ Config
- a
- (Probability (ProbModItem mia misa mica mii)
- (ProbStatement ssb ssnb ssc ssf)
- (ProbExpr en ei ers euo ebo ec eco estr esgn eus)
- (ProbMod drop_out keep_out)
- )
- c
- d
- e
+ mia <- return $ cm ^. probModItemAssign
+ misa <- return $ cm ^. probModItemSeqAlways
+ mica <- return $ cm ^. probModItemCombAlways
+ mii <- return $ cm ^. probModItemInst
+ ssb <- return $ cs ^. probStmntBlock
+ ssnb <- return $ cs ^. probStmntNonBlock
+ ssc <- return $ cs ^. probStmntCond
+ ssf <- return $ cs ^. probStmntFor
+ en <- return $ ce ^. probExprNum
+ keep_out <- return $ cmo ^. probModDropOutput
+ drop_out <- randDelete $ cmo ^. probModDropOutput
+ ei <- randDelete $ ce ^. probExprId
+ ers <- randDelete $ ce ^. probExprRangeSelect
+ euo <- randDelete $ ce ^. probExprUnOp
+ ebo <- randDelete $ ce ^. probExprBinOp
+ ec <- randDelete $ ce ^. probExprCond
+ eco <- randDelete $ ce ^. probExprConcat
+ estr <- randDelete $ ce ^. probExprStr
+ esgn <- randDelete $ ce ^. probExprSigned
+ eus <- randDelete $ ce ^. probExprUnsigned
+ return $
+ Config
+ a
+ ( Probability
+ (ProbModItem mia misa mica mii)
+ (ProbStatement ssb ssnb ssc ssf)
+ (ProbExpr en ei ers euo ebo ec eco estr esgn eus)
+ (ProbMod drop_out keep_out)
+ )
+ c
+ d
+ e
where
cm = config ^. configProbability . probModItem
cs = config ^. configProbability . probStmnt
@@ -136,91 +140,107 @@ randomise config@(Config a _ c d e) = do
handleOpts :: Opts -> IO ()
handleOpts (Fuzz o configF f k n nosim noequiv noreduction file top cc checker) = do
- config <- getConfig configF
- gen <- getGenerator config top file
- datadir <- getDataDir
- _ <- runFuzz
- (FuzzOpts (Just $ fromText o)
- f k n nosim noequiv noreduction config (toFP datadir) cc checker)
- defaultYosys
- (fuzzMultiple gen)
- return ()
+ config <- getConfig configF
+ gen <- getGenerator config top file
+ datadir <- getDataDir
+ _ <-
+ runFuzz
+ ( FuzzOpts
+ (Just $ fromText o)
+ f
+ k
+ n
+ nosim
+ noequiv
+ noreduction
+ config
+ (toFP datadir)
+ cc
+ checker
+ )
+ defaultYosys
+ (fuzzMultiple gen)
+ return ()
handleOpts (Generate f c) = do
- config <- getConfig c
- source <- proceduralIO "top" config :: IO (Verilog ())
- maybe (T.putStrLn $ genSource source) (flip T.writeFile $ genSource source)
- $ T.unpack
- . toTextIgnore
- <$> f
+ config <- getConfig c
+ source <- proceduralIO "top" config :: IO (Verilog ())
+ maybe (T.putStrLn $ genSource source) (flip T.writeFile $ genSource source) $
+ T.unpack
+ . toTextIgnore
+ <$> f
handleOpts (Parse f t o rc) = do
- verilogSrc <- T.readFile file
- case parseVerilog (T.pack file) verilogSrc of
- Left l -> print l
- 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
+ verilogSrc <- T.readFile file
+ case parseVerilog (T.pack file) verilogSrc of
+ Left l -> print l
+ 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 Nothing (toFP datadir) a b src :: Sh (SourceInfo ())
- 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"
+ 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 Nothing (toFP datadir) a b src :: Sh (SourceInfo ())
+ 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) :: IO (SourceInfo ())
- datadir <- getDataDir
- 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 Nothing (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"
- return ()
- as -> do
- putStrLn "Synthesis check"
- _ <- shelly . runResultT $ mapM (flip runSynth src) as
- return ()
- where dir = fromText "equiv"
+ src <- parseSourceInfoFile t (toTextIgnore f) :: IO (SourceInfo ())
+ datadir <- getDataDir
+ 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 Nothing (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"
+ 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)
- $ T.unpack
- . toTextIgnore
- <$> c
+ config <- if r then getConfig conf >>= randomise else getConfig conf
+ maybe (T.putStrLn . encodeConfig $ config) (`encodeConfigFile` config) $
+ T.unpack
+ . toTextIgnore
+ <$> c
defaultMain :: IO ()
defaultMain = do
- optsparsed <- execParser opts
- handleOpts optsparsed
+ optsparsed <- execParser opts
+ handleOpts optsparsed
makeSrcInfo :: (ModDecl ann) -> (SourceInfo ann)
makeSrcInfo m = SourceInfo (getIdentifier $ m ^. modId) (Verilog [m])
@@ -229,10 +249,10 @@ makeSrcInfo m = SourceInfo (getIdentifier $ m ^. modId) (Verilog [m])
-- can be seen.
draw :: IO ()
draw = do
- gr <- Hog.sample $ rDups . getCircuit <$> Hog.resize 10 randomDAG
- let dot = G.showDot . G.fglToDotString $ G.nemap show (const "") gr
- writeFile "file.dot" dot
- shelly $ run_ "dot" ["-Tpng", "-o", "file.png", "file.dot"]
+ gr <- Hog.sample $ rDups . getCircuit <$> Hog.resize 10 randomDAG
+ let dot = G.showDot . G.fglToDotString $ G.nemap show (const "") gr
+ writeFile "file.dot" dot
+ shelly $ run_ "dot" ["-Tpng", "-o", "file.png", "file.dot"]
-- | Function to show a bytestring in a hex format.
showBS :: ByteString -> Text
@@ -247,80 +267,85 @@ runSimulation = do
-- shelly $ run_ "dot" ["-Tpng", "-o", "file.png", "file.dot"]
-- let circ =
-- head $ (nestUpTo 30 . generateAST $ Circuit gr) ^.. getVerilog . traverse . getDescription
- rand <- generateByteString Nothing 32 20
- rand2 <- Hog.sample (randomMod 10 100) :: IO (ModDecl ())
- val <- shelly . runResultT $ runSim defaultIcarus (makeSrcInfo rand2) rand
- case val of
- Pass a -> T.putStrLn $ showBS a
- _ -> T.putStrLn "Test failed"
-
+ rand <- generateByteString Nothing 32 20
+ rand2 <- Hog.sample (randomMod 10 100) :: IO (ModDecl ())
+ val <- shelly . runResultT $ runSim defaultIcarus (makeSrcInfo rand2) rand
+ case val of
+ Pass a -> T.putStrLn $ showBS a
+ _ -> T.putStrLn "Test failed"
-- | Code to be executed on a failure. Also checks if the failure was a timeout,
-- as the timeout command will return the 124 error code if that was the
-- case. In that case, the error will be moved to a different directory.
onFailure :: Text -> RunFailed -> Sh (Result Failed ())
onFailure t _ = do
- ex <- lastExitCode
- case ex of
- 124 -> do
- logger "Test TIMEOUT"
- chdir ".." $ cp_r (fromText t) $ fromText (t <> "_timeout")
- return $ Fail EmptyFail
- _ -> do
- logger "Test FAIL"
- chdir ".." $ cp_r (fromText t) $ fromText (t <> "_failed")
- return $ Fail EmptyFail
+ ex <- lastExitCode
+ case ex of
+ 124 -> do
+ logger "Test TIMEOUT"
+ chdir ".." $ cp_r (fromText t) $ fromText (t <> "_timeout")
+ return $ Fail EmptyFail
+ _ -> do
+ logger "Test FAIL"
+ chdir ".." $ cp_r (fromText t) $ fromText (t <> "_failed")
+ return $ Fail EmptyFail
checkEquivalence :: Show ann => SourceInfo ann -> Text -> IO Bool
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 Nothing (toFP datadir) defaultYosys defaultVivado src) >> return True)
- ((\_ -> return False) :: RunFailed -> Sh Bool)
+ mkdir_p (fromText dir)
+ curr <- toTextIgnore <$> pwd
+ datadir <- liftIO getDataDir
+ setenv "VERISMITH_ROOT" curr
+ cd (fromText dir)
+ catch_sh
+ ((runResultT $ runEquiv Nothing (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
-- generated Verilog files are equivalent.
-runEquivalence
- :: Maybe Seed
- -> Gen (Verilog ()) -- ^ Generator for the Verilog file.
- -> Text -- ^ Name of the folder on each thread.
- -> Text -- ^ Name of the general folder being used.
- -> Bool -- ^ Keep flag.
- -> Int -- ^ Used to track the recursion.
- -> IO ()
+runEquivalence ::
+ Maybe Seed ->
+ -- | Generator for the Verilog file.
+ Gen (Verilog ()) ->
+ -- | Name of the folder on each thread.
+ Text ->
+ -- | Name of the general folder being used.
+ Text ->
+ -- | Keep flag.
+ Bool ->
+ -- | Used to track the recursion.
+ Int ->
+ IO ()
runEquivalence seed gm t d k i = do
- (_, m) <- shelly $ sampleSeed seed gm
- let srcInfo = SourceInfo "top" m
- rand <- generateByteString Nothing 32 20
- datadir <- getDataDir
- shellyFailDir $ do
- mkdir_p (fromText d </> fromText n)
- curr <- toTextIgnore <$> pwd
- setenv "VERISMITH_ROOT" curr
- cd (fromText "output" </> fromText n)
- _ <-
- catch_sh
- ( runResultT
- $ runEquiv Nothing (toFP datadir) defaultYosys defaultVivado srcInfo
- >> liftSh (logger "Test OK")
- )
- $ onFailure n
- _ <-
- catch_sh
- ( runResultT
- $ runSim (Icarus "iverilog" "vvp") srcInfo rand
- >>= (\b -> liftSh $ logger ("RTL Sim: " <> showBS b))
- )
- $ onFailure n
- cd ".."
- unless k . rm_rf $ fromText n
- when (i < 5 && isNothing seed) (runEquivalence seed gm t d k $ i + 1)
- where n = t <> "_" <> T.pack (show i)
+ (_, m) <- shelly $ sampleSeed seed gm
+ let srcInfo = SourceInfo "top" m
+ rand <- generateByteString Nothing 32 20
+ datadir <- getDataDir
+ shellyFailDir $ do
+ mkdir_p (fromText d </> fromText n)
+ curr <- toTextIgnore <$> pwd
+ setenv "VERISMITH_ROOT" curr
+ cd (fromText "output" </> fromText n)
+ _ <-
+ catch_sh
+ ( runResultT $
+ runEquiv Nothing (toFP datadir) defaultYosys defaultVivado srcInfo
+ >> liftSh (logger "Test OK")
+ )
+ $ onFailure n
+ _ <-
+ catch_sh
+ ( runResultT $
+ runSim (Icarus "iverilog" "vvp") srcInfo rand
+ >>= (\b -> liftSh $ logger ("RTL Sim: " <> showBS b))
+ )
+ $ onFailure n
+ cd ".."
+ unless k . rm_rf $ fromText n
+ when (i < 5 && isNothing seed) (runEquivalence seed gm t d k $ i + 1)
+ where
+ n = t <> "_" <> T.pack (show i)
runReduce :: (SourceInfo ()) -> IO (SourceInfo ())
runReduce s =
- shelly $ reduce "reduce.v" (\s' -> not <$> liftIO (checkEquivalence s' "reduce")) s
+ shelly $ reduce "reduce.v" (\s' -> not <$> liftIO (checkEquivalence s' "reduce")) s
generated by cgit (git 2.34.1) at 2024-05-10 06:41:28 +0000