From 404a828cd1bb7d69d1e879882a6b79f3378cd98d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 25 May 2019 22:37:01 +0100 Subject: Add more command line options for replay --- src/VeriFuzz.hs | 76 +++++++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 69 insertions(+), 7 deletions(-) (limited to 'src/VeriFuzz.hs') diff --git a/src/VeriFuzz.hs b/src/VeriFuzz.hs index 66c795f..6d4f839 100644 --- a/src/VeriFuzz.hs +++ b/src/VeriFuzz.hs @@ -28,7 +28,7 @@ module VeriFuzz where import Control.Concurrent -import Control.Lens +import Control.Lens hiding ((<.>)) import Control.Monad.IO.Class (liftIO) import qualified Crypto.Random.DRBG as C import Data.ByteString (ByteString) @@ -58,6 +58,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 +80,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 +110,14 @@ 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 +191,22 @@ 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 +366,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 -> error "Equivalence check failed" + Fail _ -> error "Equivalence check errored out" + 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) -- cgit From 11bd73faa516cde0af74e5359c36c8f1fa4e816a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 25 May 2019 23:26:27 +0100 Subject: Fix reduction for statements --- src/VeriFuzz.hs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'src/VeriFuzz.hs') diff --git a/src/VeriFuzz.hs b/src/VeriFuzz.hs index 6d4f839..4b9878d 100644 --- a/src/VeriFuzz.hs +++ b/src/VeriFuzz.hs @@ -400,9 +400,10 @@ handleOpts (Reduce f t _ ls' True) = do runSynth b src runEquiv a b src case res of - Pass _ -> putStrLn "Equivalence check passed" - Fail EquivFail -> error "Equivalence check failed" - Fail _ -> error "Equivalence check errored out" + 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" -- cgit 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 ++++++++++++++++++++++++++-------------------- 1 file changed, 26 insertions(+), 20 deletions(-) (limited to 'src/VeriFuzz.hs') 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) -- cgit From d32f4cc45bc8c0670fb788b1fcd4c2f2b15fa094 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 29 Jun 2019 20:33:59 +0100 Subject: Format files --- src/VeriFuzz.hs | 44 +++++++++++++++++++++++--------------------- 1 file changed, 23 insertions(+), 21 deletions(-) (limited to 'src/VeriFuzz.hs') diff --git a/src/VeriFuzz.hs b/src/VeriFuzz.hs index 7bc562f..0bbdc4f 100644 --- a/src/VeriFuzz.hs +++ b/src/VeriFuzz.hs @@ -28,27 +28,29 @@ module VeriFuzz where import Control.Concurrent -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 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,7 +60,7 @@ import VeriFuzz.Result import VeriFuzz.Sim import VeriFuzz.Sim.Internal import VeriFuzz.Verilog -import VeriFuzz.Verilog.Parser (parseSourceInfoFile) +import VeriFuzz.Verilog.Parser ( parseSourceInfoFile ) data OptTool = TYosys | TXST -- cgit