aboutsummaryrefslogtreecommitdiffstats
path: root/src/Verismith/Tool
diff options
context:
space:
mode:
Diffstat (limited to 'src/Verismith/Tool')
-rw-r--r--src/Verismith/Tool/Icarus.hs346
-rw-r--r--src/Verismith/Tool/Identity.hs68
-rw-r--r--src/Verismith/Tool/Internal.hs293
-rw-r--r--src/Verismith/Tool/Quartus.hs113
-rw-r--r--src/Verismith/Tool/QuartusLight.hs113
-rw-r--r--src/Verismith/Tool/Template.hs288
-rw-r--r--src/Verismith/Tool/Vivado.hs109
-rw-r--r--src/Verismith/Tool/XST.hs122
-rw-r--r--src/Verismith/Tool/Yosys.hs206
9 files changed, 869 insertions, 789 deletions
diff --git a/src/Verismith/Tool/Icarus.hs b/src/Verismith/Tool/Icarus.hs
index 4b91652..8504640 100644
--- a/src/Verismith/Tool/Icarus.hs
+++ b/src/Verismith/Tool/Icarus.hs
@@ -1,62 +1,62 @@
-{-|
-Module : Verismith.Tool.Icarus
-Description : Icarus verilog module.
-Copyright : (c) 2018-2019, Yann Herklotz
-License : GPL-3
-Maintainer : yann [at] yannherklotz [dot] com
-Stability : experimental
-Portability : POSIX
-
-Icarus verilog module.
--}
-
+-- |
+-- Module : Verismith.Tool.Icarus
+-- Description : Icarus verilog module.
+-- Copyright : (c) 2018-2019, Yann Herklotz
+-- License : GPL-3
+-- Maintainer : yann [at] yannherklotz [dot] com
+-- Stability : experimental
+-- Portability : POSIX
+--
+-- Icarus verilog module.
module Verismith.Tool.Icarus
- ( Icarus(..)
- , defaultIcarus
- , runSimIc
- , runSimIcEC
- )
+ ( Icarus (..),
+ defaultIcarus,
+ runSimIc,
+ runSimIcEC,
+ )
where
-import Control.DeepSeq (NFData, rnf, rwhnf)
-import Control.Lens
-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 Verismith.CounterEg (CounterEg (..))
-import Verismith.Result
-import Verismith.Tool.Internal
-import Verismith.Tool.Template
-import Verismith.Verilog.AST
-import Verismith.Verilog.BitVec
-import Verismith.Verilog.CodeGen
-import Verismith.Verilog.Internal
-import Verismith.Verilog.Mutate
-
-data Icarus = Icarus { icarusPath :: FilePath
- , vvpPath :: FilePath
- }
- deriving (Eq)
+import Control.DeepSeq (NFData, rnf, rwhnf)
+import Control.Lens
+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 Shelly
+import Shelly.Lifted (liftSh)
+import Verismith.CounterEg (CounterEg (..))
+import Verismith.Result
+import Verismith.Tool.Internal
+import Verismith.Tool.Template
+import Verismith.Verilog.AST
+import Verismith.Verilog.BitVec
+import Verismith.Verilog.CodeGen
+import Verismith.Verilog.Internal
+import Verismith.Verilog.Mutate
+import Prelude hiding (FilePath)
+
+data Icarus
+ = Icarus
+ { icarusPath :: FilePath,
+ vvpPath :: FilePath
+ }
+ deriving (Eq)
instance Show Icarus where
- show _ = "iverilog"
+ show _ = "iverilog"
instance Tool Icarus where
toText _ = "iverilog"
@@ -66,36 +66,40 @@ instance Simulator Icarus where
runSimWithFile = runSimIcarusWithFile
instance NFData Icarus where
- rnf = rwhnf
+ rnf = rwhnf
defaultIcarus :: Icarus
defaultIcarus = Icarus "iverilog" "vvp"
addDisplay :: [Statement ann] -> [Statement ann]
-addDisplay s = concat $ transpose
- [ s
- , replicate l $ TimeCtrl 1 Nothing
- , replicate l . SysTaskEnable $ Task "display" ["%b", Id "y"]
- ]
- where l = length s
+addDisplay s =
+ concat $
+ transpose
+ [ s,
+ replicate l $ TimeCtrl 1 Nothing,
+ replicate l . SysTaskEnable $ Task "display" ["%b", Id "y"]
+ ]
+ where
+ l = length s
assignFunc :: [Port] -> ByteString -> Statement ann
assignFunc inp bs =
- NonBlockAssign
- . Assign conc Nothing
- . Number
- . BitVec (B.length bs * 8)
- $ bsToI bs
- where conc = RegConcat (portToExpr <$> inp)
+ NonBlockAssign
+ . Assign conc Nothing
+ . Number
+ . BitVec (B.length bs * 8)
+ $ bsToI bs
+ where
+ conc = RegConcat (portToExpr <$> inp)
convert :: Text -> ByteString
convert =
- toStrict
- . (encode :: Integer -> L.ByteString)
- . maybe 0 fst
- . listToMaybe
- . readInt 2 (`elem` ("01" :: String)) digitToInt
- . T.unpack
+ toStrict
+ . (encode :: Integer -> L.ByteString)
+ . maybe 0 fst
+ . listToMaybe
+ . readInt 2 (`elem` ("01" :: String)) digitToInt
+ . T.unpack
mask :: Text -> Text
mask = T.replace "x" "0"
@@ -105,52 +109,69 @@ callback b t = b <> convert (mask t)
runSimIcarus :: Show ann => Icarus -> (SourceInfo ann) -> [ByteString] -> ResultSh ByteString
runSimIcarus sim rinfo bss = do
- let tb = ModDecl
- "main"
- []
- []
- [ Initial
- $ fold (addDisplay $ assignFunc (_modInPorts m) <$> bss)
- <> (SysTaskEnable $ Task "finish" [])
- ]
- []
- let newtb = instantiateMod m tb
- let modWithTb = Verilog [newtb, m]
- liftSh . writefile "main.v" $ genSource modWithTb
- annotate (SimFail mempty) $ runSimWithFile sim "main.v" bss
- where m = rinfo ^. mainModule
-
-runSimIcarusWithFile
- :: Icarus -> FilePath -> [ByteString] -> ResultSh ByteString
+ let tb =
+ ModDecl
+ "main"
+ []
+ []
+ [ Initial $
+ fold (addDisplay $ assignFunc (_modInPorts m) <$> bss)
+ <> (SysTaskEnable $ Task "finish" [])
+ ]
+ []
+ let newtb = instantiateMod m tb
+ let modWithTb = Verilog [newtb, m]
+ liftSh . writefile "main.v" $ genSource modWithTb
+ annotate (SimFail mempty) $ runSimWithFile sim "main.v" bss
+ where
+ m = rinfo ^. mainModule
+
+runSimIcarusWithFile ::
+ Icarus -> FilePath -> [ByteString] -> ResultSh ByteString
runSimIcarusWithFile sim f _ = annotate (SimFail mempty) . liftSh $ do
- dir <- pwd
- logCommand_ dir "icarus"
- $ run (icarusPath sim) ["-o", "main", toTextIgnore f]
- B.take 8 . BA.convert . (hash :: ByteString -> Digest SHA256) <$> logCommand
- dir
- "vvp"
- (runFoldLines (mempty :: ByteString) callback (vvpPath sim) ["main"])
+ dir <- pwd
+ logCommand_ dir "icarus" $
+ run (icarusPath sim) ["-o", "main", toTextIgnore f]
+ 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
tbModule :: [ByteString] -> (ModDecl ann) -> (Verilog ann)
tbModule bss top =
- Verilog [ instantiateMod top $ ModDecl "testbench" [] []
- [ Initial
- $ fold [ BlockAssign (Assign "clk" Nothing 0)
- , BlockAssign (Assign inConcat Nothing 0)
- ]
- <> fold ((\r -> TimeCtrl 10
- (Just $ BlockAssign (Assign inConcat Nothing r)))
- . fromInteger . fromBytes <$> bss)
- <> (TimeCtrl 10 . Just . SysTaskEnable $ Task "finish" [])
- , Always . TimeCtrl 5 . Just $ BlockAssign
- (Assign "clk" Nothing (UnOp UnNot (Id "clk")))
- , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable
- $ Task "strobe" ["%b", Id "y"]
- ] []
- ]
+ Verilog
+ [ instantiateMod top $
+ ModDecl
+ "testbench"
+ []
+ []
+ [ Initial $
+ fold
+ [ BlockAssign (Assign "clk" Nothing 0),
+ BlockAssign (Assign inConcat Nothing 0)
+ ]
+ <> fold
+ ( ( \r ->
+ TimeCtrl
+ 10
+ (Just $ BlockAssign (Assign inConcat Nothing r))
+ )
+ . fromInteger
+ . fromBytes <$> bss
+ )
+ <> (TimeCtrl 10 . Just . SysTaskEnable $ Task "finish" []),
+ Always . TimeCtrl 5 . Just $
+ BlockAssign
+ (Assign "clk" Nothing (UnOp UnNot (Id "clk"))),
+ Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable $
+ Task "strobe" ["%b", Id "y"]
+ ]
+ []
+ ]
where
inConcat = (RegConcat . filter (/= (Id "clk")) $ (Id . fromPort <$> (top ^. modInPorts)))
@@ -159,54 +180,73 @@ counterTestBench (CounterEg _ states) m = tbModule filtered m
where
filtered = convert . fold . fmap snd . filter ((/= "clk") . fst) <$> states
-runSimIc' :: (Synthesiser b, Show ann)
- => ([ByteString] -> (ModDecl ann) -> (Verilog ann))
- -> FilePath
- -> Icarus
- -> b
- -> (SourceInfo ann)
- -> [ByteString]
- -> Maybe ByteString
- -> ResultSh ByteString
+runSimIc' ::
+ (Synthesiser b, Show ann) =>
+ ([ByteString] -> (ModDecl ann) -> (Verilog ann)) ->
+ FilePath ->
+ Icarus ->
+ b ->
+ (SourceInfo ann) ->
+ [ByteString] ->
+ Maybe ByteString ->
+ ResultSh ByteString
runSimIc' fun datadir sim1 synth1 srcInfo bss bs = do
- dir <- liftSh pwd
- let top = srcInfo ^. mainModule
- let tb = fun bss top
- liftSh . writefile tbname $ icarusTestbench datadir tb synth1
- liftSh $ exe dir "icarus" "iverilog" ["-o", exename, toTextIgnore tbname]
- s <- liftSh
- $ B.take 8
- . BA.convert
- . (hash :: ByteString -> Digest SHA256)
+ dir <- liftSh pwd
+ let top = srcInfo ^. mainModule
+ let tb = fun bss top
+ liftSh . writefile tbname $ icarusTestbench datadir tb synth1
+ liftSh $ exe dir "icarus" "iverilog" ["-o", exename, toTextIgnore tbname]
+ s <-
+ liftSh $
+ B.take 8
+ . BA.convert
+ . (hash :: ByteString -> Digest SHA256)
<$> logCommand
- dir
- "vvp"
- (runFoldLines (mempty :: ByteString)
- callback
- (vvpPath sim1)
- [exename])
- case (bs, s) of
- (Nothing, s') -> ResultT . return $ Pass s'
- (Just bs', s') -> if bs' == s'
- then ResultT . return $ Pass s'
- else ResultT . return $ Fail (SimFail s')
+ dir
+ "vvp"
+ ( runFoldLines
+ (mempty :: ByteString)
+ callback
+ (vvpPath sim1)
+ [exename]
+ )
+ case (bs, s) of
+ (Nothing, s') -> ResultT . return $ Pass s'
+ (Just bs', s') ->
+ if bs' == s'
+ then ResultT . return $ Pass s'
+ else ResultT . return $ Fail (SimFail s')
where
exe dir name e = void . errExit False . logCommand dir name . timeout e
tbname = fromText $ toText synth1 <> "_testbench.v"
exename = toText synth1 <> "_main"
-runSimIc :: (Synthesiser b, Show ann)
- => FilePath -- ^ Data directory.
- -> Icarus -- ^ Icarus simulator.
- -> b -- ^ Synthesis tool to be tested.
- -> (SourceInfo ann) -- ^ Original generated program to test.
- -> [ByteString] -- ^ Test vectors to be passed as inputs to the generated Verilog.
- -> Maybe ByteString -- ^ What the correct output should be. If
- -- 'Nothing' is passed, then just return 'Pass
- -- ByteString' with the answer.
- -> ResultSh ByteString
+runSimIc ::
+ (Synthesiser b, Show ann) =>
+ -- | Data directory.
+ FilePath ->
+ -- | Icarus simulator.
+ Icarus ->
+ -- | Synthesis tool to be tested.
+ b ->
+ -- | Original generated program to test.
+ (SourceInfo ann) ->
+ -- | Test vectors to be passed as inputs to the generated Verilog.
+ [ByteString] ->
+ -- | What the correct output should be. If
+ -- 'Nothing' is passed, then just return 'Pass
+ -- ByteString' with the answer.
+ Maybe ByteString ->
+ ResultSh ByteString
runSimIc = runSimIc' tbModule
-runSimIcEC :: (Synthesiser b, Show ann) => FilePath -> Icarus -> b
- -> (SourceInfo ann) -> CounterEg -> Maybe ByteString -> ResultSh ByteString
+runSimIcEC ::
+ (Synthesiser b, Show ann) =>
+ FilePath ->
+ Icarus ->
+ b ->
+ (SourceInfo ann) ->
+ CounterEg ->
+ Maybe ByteString ->
+ ResultSh ByteString
runSimIcEC a b c d e = runSimIc' (const $ counterTestBench e) a b c d []
diff --git a/src/Verismith/Tool/Identity.hs b/src/Verismith/Tool/Identity.hs
index 804f096..f8b9026 100644
--- a/src/Verismith/Tool/Identity.hs
+++ b/src/Verismith/Tool/Identity.hs
@@ -1,48 +1,48 @@
-{-|
-Module : Verismith.Tool.Identity
-Description : The identity simulator and synthesiser.
-Copyright : (c) 2019, Yann Herklotz Grave
-License : GPL-3
-Maintainer : yann [at] yannherklotz [dot] com
-Stability : experimental
-Portability : POSIX
-
-The identity simulator and synthesiser.
--}
-
+-- |
+-- Module : Verismith.Tool.Identity
+-- Description : The identity simulator and synthesiser.
+-- Copyright : (c) 2019, Yann Herklotz Grave
+-- License : GPL-3
+-- Maintainer : yann [at] yannherklotz [dot] com
+-- Stability : experimental
+-- Portability : POSIX
+--
+-- The identity simulator and synthesiser.
module Verismith.Tool.Identity
- ( Identity(..)
- , defaultIdentity
- )
+ ( Identity (..),
+ defaultIdentity,
+ )
where
-import Control.DeepSeq (NFData, rnf, rwhnf)
-import Data.Text (Text, unpack)
-import Prelude hiding (FilePath)
-import Shelly (FilePath)
-import Shelly.Lifted (writefile)
-import Verismith.Tool.Internal
-import Verismith.Verilog.AST
-import Verismith.Verilog.CodeGen
-
-data Identity = Identity { identityDesc :: !Text
- , identityOutput :: !FilePath
- }
- deriving (Eq)
+import Control.DeepSeq (NFData, rnf, rwhnf)
+import Data.Text (Text, unpack)
+import Shelly (FilePath)
+import Shelly.Lifted (writefile)
+import Verismith.Tool.Internal
+import Verismith.Verilog.AST
+import Verismith.Verilog.CodeGen
+import Prelude hiding (FilePath)
+
+data Identity
+ = Identity
+ { identityDesc :: !Text,
+ identityOutput :: !FilePath
+ }
+ deriving (Eq)
instance Tool Identity where
- toText (Identity d _) = d
+ toText (Identity d _) = d
instance Show Identity where
- show t = unpack $ toText t
+ show t = unpack $ toText t
instance Synthesiser Identity where
- runSynth = runSynthIdentity
- synthOutput = identityOutput
- setSynthOutput (Identity a _) = Identity a
+ runSynth = runSynthIdentity
+ synthOutput = identityOutput
+ setSynthOutput (Identity a _) = Identity a
instance NFData Identity where
- rnf = rwhnf
+ rnf = rwhnf
runSynthIdentity :: Show ann => Identity -> (SourceInfo ann) -> ResultSh ()
runSynthIdentity (Identity _ out) = writefile out . genSource
diff --git a/src/Verismith/Tool/Internal.hs b/src/Verismith/Tool/Internal.hs
index f462c74..ab2892e 100644
--- a/src/Verismith/Tool/Internal.hs
+++ b/src/Verismith/Tool/Internal.hs
@@ -1,63 +1,61 @@
-{-|
-Module : Verismith.Tool.Internal
-Description : Class of the simulator.
-Copyright : (c) 2018-2019, Yann Herklotz
-License : GPL-3
-Maintainer : yann [at] yannherklotz [dot] com
-Stability : experimental
-Portability : POSIX
-
-Class of the simulator and the synthesize tool.
--}
-
{-# LANGUAGE DeriveFunctor #-}
+-- |
+-- Module : Verismith.Tool.Internal
+-- Description : Class of the simulator.
+-- Copyright : (c) 2018-2019, Yann Herklotz
+-- License : GPL-3
+-- Maintainer : yann [at] yannherklotz [dot] com
+-- Stability : experimental
+-- Portability : POSIX
+--
+-- Class of the simulator and the synthesize tool.
module Verismith.Tool.Internal
- ( ResultSh
- , resultSh
- , Tool(..)
- , Simulator(..)
- , Synthesiser(..)
- , Failed(..)
- , renameSource
- , checkPresent
- , checkPresentModules
- , replace
- , replaceMods
- , rootPath
- , timeout
- , timeout_
- , bsToI
- , noPrint
- , logger
- , logCommand
- , logCommand_
- , execute
- , execute_
- , (<?>)
- , annotate
- )
+ ( ResultSh,
+ resultSh,
+ Tool (..),
+ Simulator (..),
+ Synthesiser (..),
+ Failed (..),
+ renameSource,
+ checkPresent,
+ checkPresentModules,
+ replace,
+ replaceMods,
+ rootPath,
+ timeout,
+ timeout_,
+ bsToI,
+ noPrint,
+ logger,
+ logCommand,
+ logCommand_,
+ execute,
+ execute_,
+ (<?>),
+ annotate,
+ )
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 Shelly
-import Shelly.Lifted (MonadSh, liftSh)
-import System.FilePath.Posix (takeBaseName)
-import Verismith.CounterEg (CounterEg)
-import Verismith.Internal
-import Verismith.Result
-import Verismith.Verilog.AST
+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 Shelly
+import Shelly.Lifted (MonadSh, liftSh)
+import System.FilePath.Posix (takeBaseName)
+import Verismith.CounterEg (CounterEg)
+import Verismith.Internal
+import Verismith.Result
+import Verismith.Verilog.AST
+import Prelude hiding (FilePath)
-- | Tool class.
class Tool a where
@@ -65,51 +63,62 @@ class Tool a where
-- | Simulation type class.
class Tool a => Simulator a where
- runSim :: Show ann
- => a -- ^ Simulator instance
- -> SourceInfo ann -- ^ Run information
- -> [ByteString] -- ^ Inputs to simulate
- -> ResultSh ByteString -- ^ Returns the value of the hash at the output of the testbench.
- runSimWithFile :: a
- -> FilePath
- -> [ByteString]
- -> ResultSh ByteString
-
-data Failed = EmptyFail
- | EquivFail (Maybe CounterEg)
- | EquivError
- | SimFail ByteString
- | SynthFail
- | TimeoutError
- deriving (Eq)
+ runSim ::
+ Show ann =>
+ -- | Simulator instance
+ a ->
+ -- | Run information
+ SourceInfo ann ->
+ -- | Inputs to simulate
+ [ByteString] ->
+ -- | Returns the value of the hash at the output of the testbench.
+ ResultSh ByteString
+ runSimWithFile ::
+ a ->
+ FilePath ->
+ [ByteString] ->
+ ResultSh ByteString
+
+data Failed
+ = EmptyFail
+ | EquivFail (Maybe CounterEg)
+ | EquivError
+ | SimFail ByteString
+ | SynthFail
+ | TimeoutError
+ deriving (Eq)
instance Show Failed where
- show EmptyFail = "EmptyFail"
- show (EquivFail _) = "EquivFail"
- show EquivError = "EquivError"
- show (SimFail bs) = "SimFail " <> T.unpack (T.take 10 $ showBS bs)
- show SynthFail = "SynthFail"
- show TimeoutError = "TimeoutError"
+ show EmptyFail = "EmptyFail"
+ show (EquivFail _) = "EquivFail"
+ show EquivError = "EquivError"
+ show (SimFail bs) = "SimFail " <> T.unpack (T.take 10 $ showBS bs)
+ show SynthFail = "SynthFail"
+ show TimeoutError = "TimeoutError"
instance Semigroup Failed where
- EmptyFail <> a = a
- b <> _ = b
+ EmptyFail <> a = a
+ b <> _ = b
instance Monoid Failed where
- mempty = EmptyFail
+ mempty = EmptyFail
-- | Synthesiser type class.
class Tool a => Synthesiser a where
- runSynth :: Show ann
- => a -- ^ Synthesiser tool instance
- -> SourceInfo ann -- ^ Run information
- -> ResultSh () -- ^ does not return any values
- synthOutput :: a -> FilePath
- setSynthOutput :: a -> FilePath -> a
+ runSynth ::
+ Show ann =>
+ -- | Synthesiser tool instance
+ a ->
+ -- | Run information
+ SourceInfo ann ->
+ -- | does not return any values
+ ResultSh ()
+ synthOutput :: a -> FilePath
+ setSynthOutput :: a -> FilePath -> a
renameSource :: (Synthesiser a) => a -> SourceInfo ann -> SourceInfo ann
renameSource a src =
- src & infoSrc . _Wrapped . traverse . modId . _Wrapped %~ (<> toText a)
+ src & infoSrc . _Wrapped . traverse . modId . _Wrapped %~ (<> toText a)
-- | Type synonym for a 'ResultT' that will be used throughout 'Verismith'. This
-- has instances for 'MonadSh' and 'MonadIO' if the 'Monad' it is parametrised
@@ -118,31 +127,33 @@ type ResultSh = ResultT Failed Sh
resultSh :: ResultSh a -> Sh a
resultSh s = do
- result <- runResultT s
- case result of
- Fail e -> throwM . RunFailed "" [] 1 $ showT e
- Pass s' -> return s'
+ result <- runResultT s
+ case result of
+ Fail e -> throwM . RunFailed "" [] 1 $ showT e
+ Pass s' -> return s'
checkPresent :: FilePath -> Text -> Sh (Maybe Text)
checkPresent fp t = do
- errExit False $ run_ "grep" [t, toTextIgnore fp]
- i <- lastExitCode
- if i == 0 then return $ Just t else return Nothing
+ errExit False $ run_ "grep" [t, toTextIgnore fp]
+ i <- lastExitCode
+ if i == 0 then return $ Just t else return Nothing
-- | Checks what modules are present in the synthesised output, as some modules
-- may have been inlined. This could be improved if the parser worked properly.
checkPresentModules :: FilePath -> SourceInfo ann -> Sh [Text]
checkPresentModules fp (SourceInfo _ src) = do
- vals <- forM (src ^.. _Wrapped . traverse . modId . _Wrapped)
- $ checkPresent fp
- return $ catMaybes vals
+ vals <-
+ forM (src ^.. _Wrapped . traverse . modId . _Wrapped) $
+ checkPresent fp
+ return $ catMaybes vals
-- | Uses sed to replace a string in a text file.
replace :: FilePath -> Text -> Text -> Sh ()
replace fp t1 t2 = do
- errExit False . noPrint $ run_
- "sed"
- ["-i", "s/" <> t1 <> "/" <> t2 <> "/g", toTextIgnore fp]
+ errExit False . noPrint $
+ run_
+ "sed"
+ ["-i", "s/" <> t1 <> "/" <> t2 <> "/g", toTextIgnore fp]
-- | This is used because rename only renames the definitions of modules of
-- course, so instead this just searches and replaces all the module names. This
@@ -150,14 +161,14 @@ replace fp t1 t2 = do
-- much simpler if the parser works.
replaceMods :: FilePath -> Text -> SourceInfo ann -> Sh ()
replaceMods fp t (SourceInfo _ src) =
- void
- . forM (src ^.. _Wrapped . traverse . modId . _Wrapped)
- $ (\a -> replace fp a (a <> t))
+ void
+ . forM (src ^.. _Wrapped . traverse . modId . _Wrapped)
+ $ (\a -> replace fp a (a <> t))
rootPath :: Sh FilePath
rootPath = do
- current <- pwd
- maybe current fromText <$> get_env "VERISMITH_ROOT"
+ current <- pwd
+ maybe current fromText <$> get_env "VERISMITH_ROOT"
timeout :: FilePath -> [Text] -> Sh Text
timeout = command1 "timeout" ["300"] . toTextIgnore
@@ -178,18 +189,20 @@ noPrint = print_stdout False . print_stderr False
logger :: Text -> Sh ()
logger t = do
- fn <- pwd
- currentTime <- liftIO getZonedTime
- echo
- $ "Verismith "
- <> T.pack (formatTime defaultTimeLocale "%H:%M:%S " currentTime)
- <> bname fn
- <> " - "
- <> t
- where bname = T.pack . takeBaseName . T.unpack . toTextIgnore
+ fn <- pwd
+ currentTime <- liftIO getZonedTime
+ echo $
+ "Verismith "
+ <> T.pack (formatTime defaultTimeLocale "%H:%M:%S " currentTime)
+ <> bname fn
+ <> " - "
+ <> t
+ where
+ bname = T.pack . takeBaseName . T.unpack . toTextIgnore
logCommand :: FilePath -> Text -> Sh a -> Sh a
-logCommand fp name = log_stderr_with (l "_stderr.log")
+logCommand fp name =
+ log_stderr_with (l "_stderr.log")
. log_stdout_with (l ".log")
where
l s t = appendFile (file s) (T.unpack t) >> appendFile (file s) "\n"
@@ -198,29 +211,29 @@ logCommand fp name = log_stderr_with (l "_stderr.log")
logCommand_ :: FilePath -> Text -> Sh a -> Sh ()
logCommand_ fp name = void . logCommand fp name
-execute
- :: (MonadSh m, Monad m)
- => Failed
- -> FilePath
- -> Text
- -> FilePath
- -> [Text]
- -> ResultT Failed m Text
+execute ::
+ (MonadSh m, Monad m) =>
+ Failed ->
+ FilePath ->
+ Text ->
+ FilePath ->
+ [Text] ->
+ 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)
- => Failed
- -> FilePath
- -> Text
- -> FilePath
- -> [Text]
- -> ResultT Failed m ()
+ (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) =>
+ Failed ->
+ FilePath ->
+ Text ->
+ FilePath ->
+ [Text] ->
+ ResultT Failed m ()
execute_ a b c d = void . execute a b c d
diff --git a/src/Verismith/Tool/Quartus.hs b/src/Verismith/Tool/Quartus.hs
index ff8a62b..70908eb 100644
--- a/src/Verismith/Tool/Quartus.hs
+++ b/src/Verismith/Tool/Quartus.hs
@@ -1,76 +1,79 @@
-{-|
-Module : Verismith.Tool.Quartus
-Description : Quartus synthesiser implementation.
-Copyright : (c) 2019, Yann Herklotz Grave
-License : GPL-3
-Maintainer : yann [at] yannherklotz [dot] com
-Stability : experimental
-Portability : POSIX
-
-Quartus synthesiser implementation.
--}
-
+-- |
+-- Module : Verismith.Tool.Quartus
+-- Description : Quartus synthesiser implementation.
+-- Copyright : (c) 2019, Yann Herklotz Grave
+-- License : GPL-3
+-- Maintainer : yann [at] yannherklotz [dot] com
+-- Stability : experimental
+-- Portability : POSIX
+--
+-- Quartus synthesiser implementation.
module Verismith.Tool.Quartus
- ( Quartus(..)
- , defaultQuartus
- )
+ ( Quartus (..),
+ defaultQuartus,
+ )
where
-import Control.DeepSeq (NFData, rnf, rwhnf)
-import Data.Text (Text, unpack)
-import Prelude hiding (FilePath)
-import Shelly
-import Shelly.Lifted (liftSh)
-import Verismith.Tool.Internal
-import Verismith.Tool.Template
-import Verismith.Verilog.AST
-import Verismith.Verilog.CodeGen
+import Control.DeepSeq (NFData, rnf, rwhnf)
+import Data.Text (Text, unpack)
+import Shelly
+import Shelly.Lifted (liftSh)
+import Verismith.Tool.Internal
+import Verismith.Tool.Template
+import Verismith.Verilog.AST
+import Verismith.Verilog.CodeGen
+import Prelude hiding (FilePath)
-data Quartus = Quartus { quartusBin :: !(Maybe FilePath)
- , quartusDesc :: !Text
- , quartusOutput :: !FilePath
- }
- deriving (Eq)
+data Quartus
+ = Quartus
+ { quartusBin :: !(Maybe FilePath),
+ quartusDesc :: !Text,
+ quartusOutput :: !FilePath
+ }
+ deriving (Eq)
instance Tool Quartus where
- toText (Quartus _ t _) = t
+ toText (Quartus _ t _) = t
instance Show Quartus where
- show t = unpack $ toText t
+ show t = unpack $ toText t
instance Synthesiser Quartus where
- runSynth = runSynthQuartus
- synthOutput = quartusOutput
- setSynthOutput (Quartus a b _) = Quartus a b
+ runSynth = runSynthQuartus
+ synthOutput = quartusOutput
+ setSynthOutput (Quartus a b _) = Quartus a b
instance NFData Quartus where
- rnf = rwhnf
+ rnf = rwhnf
defaultQuartus :: Quartus
defaultQuartus = Quartus Nothing "quartus" "syn_quartus.v"
runSynthQuartus :: Show ann => Quartus -> (SourceInfo ann) -> ResultSh ()
runSynthQuartus sim (SourceInfo top src) = do
- dir <- liftSh pwd
- let ex = execute_ SynthFail dir "quartus"
- liftSh $ do
- writefile inpf $ genSource src
- noPrint $ run_ "sed" [ "-i"
- , "s/^module/(* multstyle = \"logic\" *) module/;"
- , toTextIgnore inpf
- ]
- writefile quartusSdc $ "create_clock -period 5 -name clk [get_ports clock]"
- writefile quartusTcl $ quartusSynthConfig sim quartusSdc top inpf
- ex (exec "quartus_sh") ["-t", toTextIgnore quartusTcl]
- liftSh $ do
- cp (fromText "simulation/vcs" </> fromText top <.> "vo")
- $ synthOutput sim
- run_
- "sed"
- [ "-ri"
- , "s,^// DATE.*,,; s,^tri1 (.*);,wire \\1 = 1;,; /^\\/\\/ +synopsys/ d;"
- , toTextIgnore $ synthOutput sim
- ]
+ dir <- liftSh pwd
+ let ex = execute_ SynthFail dir "quartus"
+ liftSh $ do
+ writefile inpf $ genSource src
+ noPrint $
+ run_
+ "sed"
+ [ "-i",
+ "s/^module/(* multstyle = \"logic\" *) module/;",
+ toTextIgnore inpf
+ ]
+ writefile quartusSdc $ "create_clock -period 5 -name clk [get_ports clock]"
+ writefile quartusTcl $ quartusSynthConfig sim quartusSdc top inpf
+ ex (exec "quartus_sh") ["-t", toTextIgnore quartusTcl]
+ liftSh $ do
+ cp (fromText "simulation/vcs" </> fromText top <.> "vo") $
+ synthOutput sim
+ run_
+ "sed"
+ [ "-ri",
+ "s,^// DATE.*,,; s,^tri1 (.*);,wire \\1 = 1;,; /^\\/\\/ +synopsys/ d;",
+ toTextIgnore $ synthOutput sim
+ ]
where
inpf = "rtl.v"
exec s = maybe (fromText s) (</> fromText s) $ quartusBin sim
diff --git a/src/Verismith/Tool/QuartusLight.hs b/src/Verismith/Tool/QuartusLight.hs
index cdf2636..cab1087 100644
--- a/src/Verismith/Tool/QuartusLight.hs
+++ b/src/Verismith/Tool/QuartusLight.hs
@@ -1,76 +1,79 @@
-{-|
-Module : Verismith.Tool.QuartusLight
-Description : QuartusLight synthesiser implementation.
-Copyright : (c) 2019, Yann Herklotz Grave
-License : GPL-3
-Maintainer : yann [at] yannherklotz [dot] com
-Stability : experimental
-Portability : POSIX
-
-QuartusLight synthesiser implementation.
--}
-
+-- |
+-- Module : Verismith.Tool.QuartusLight
+-- Description : QuartusLight synthesiser implementation.
+-- Copyright : (c) 2019, Yann Herklotz Grave
+-- License : GPL-3
+-- Maintainer : yann [at] yannherklotz [dot] com
+-- Stability : experimental
+-- Portability : POSIX
+--
+-- QuartusLight synthesiser implementation.
module Verismith.Tool.QuartusLight
- ( QuartusLight(..)
- , defaultQuartusLight
- )
+ ( QuartusLight (..),
+ defaultQuartusLight,
+ )
where
-import Control.DeepSeq (NFData, rnf, rwhnf)
-import Data.Text (Text, unpack)
-import Prelude hiding (FilePath)
-import Shelly
-import Shelly.Lifted (liftSh)
-import Verismith.Tool.Internal
-import Verismith.Tool.Template
-import Verismith.Verilog.AST
-import Verismith.Verilog.CodeGen
+import Control.DeepSeq (NFData, rnf, rwhnf)
+import Data.Text (Text, unpack)
+import Shelly
+import Shelly.Lifted (liftSh)
+import Verismith.Tool.Internal
+import Verismith.Tool.Template
+import Verismith.Verilog.AST
+import Verismith.Verilog.CodeGen
+import Prelude hiding (FilePath)
-data QuartusLight = QuartusLight { quartusLightBin :: !(Maybe FilePath)
- , quartusLightDesc :: !Text
- , quartusLightOutput :: !FilePath
- }
- deriving (Eq)
+data QuartusLight
+ = QuartusLight
+ { quartusLightBin :: !(Maybe FilePath),
+ quartusLightDesc :: !Text,
+ quartusLightOutput :: !FilePath
+ }
+ deriving (Eq)
instance Tool QuartusLight where
- toText (QuartusLight _ t _) = t
+ toText (QuartusLight _ t _) = t
instance Show QuartusLight where
- show t = unpack $ toText t
+ show t = unpack $ toText t
instance Synthesiser QuartusLight where
- runSynth = runSynthQuartusLight
- synthOutput = quartusLightOutput
- setSynthOutput (QuartusLight a b _) = QuartusLight a b
+ runSynth = runSynthQuartusLight
+ synthOutput = quartusLightOutput
+ setSynthOutput (QuartusLight a b _) = QuartusLight a b
instance NFData QuartusLight where
- rnf = rwhnf
+ rnf = rwhnf
defaultQuartusLight :: QuartusLight
defaultQuartusLight = QuartusLight Nothing "quartus" "syn_quartus.v"
runSynthQuartusLight :: Show ann => QuartusLight -> (SourceInfo ann) -> ResultSh ()
runSynthQuartusLight sim (SourceInfo top src) = do
- dir <- liftSh pwd
- let ex = execute_ SynthFail dir "quartus"
- liftSh $ do
- writefile inpf $ genSource src
- noPrint $ run_ "sed" [ "-i"
- , "s/^module/(* multstyle = \"logic\" *) module/;"
- , toTextIgnore inpf
- ]
- writefile quartusSdc "create_clock -period 5 -name clk [get_ports clock]"
- writefile quartusTcl $ quartusLightSynthConfig sim quartusSdc top inpf
- ex (exec "quartus_sh") ["-t", toTextIgnore quartusTcl]
- liftSh $ do
- cp (fromText "simulation/vcs" </> fromText top <.> "vo")
- $ synthOutput sim
- run_
- "sed"
- [ "-ri"
- , "s,^// DATE.*,,; s,^tri1 (.*);,wire \\1 = 1;,; /^\\/\\/ +synopsys/ d;"
- , toTextIgnore $ synthOutput sim
- ]
+ dir <- liftSh pwd
+ let ex = execute_ SynthFail dir "quartus"
+ liftSh $ do
+ writefile inpf $ genSource src
+ noPrint $
+ run_
+ "sed"
+ [ "-i",
+ "s/^module/(* multstyle = \"logic\" *) module/;",
+ toTextIgnore inpf
+ ]
+ writefile quartusSdc "create_clock -period 5 -name clk [get_ports clock]"
+ writefile quartusTcl $ quartusLightSynthConfig sim quartusSdc top inpf
+ ex (exec "quartus_sh") ["-t", toTextIgnore quartusTcl]
+ liftSh $ do
+ cp (fromText "simulation/vcs" </> fromText top <.> "vo") $
+ synthOutput sim
+ run_
+ "sed"
+ [ "-ri",
+ "s,^// DATE.*,,; s,^tri1 (.*);,wire \\1 = 1;,; /^\\/\\/ +synopsys/ d;",
+ toTextIgnore $ synthOutput sim
+ ]
where
inpf = "rtl.v"
exec s = maybe (fromText s) (</> fromText s) $ quartusLightBin sim
diff --git a/src/Verismith/Tool/Template.hs b/src/Verismith/Tool/Template.hs
index 5a20ff5..d141d46 100644
--- a/src/Verismith/Tool/Template.hs
+++ b/src/Verismith/Tool/Template.hs
@@ -1,47 +1,45 @@
-{-|
-Module : Verismith.Tool.Template
-Description : Template file for different configuration files
-Copyright : (c) 2019, Yann Herklotz
-License : GPL-3
-Maintainer : yann [at] yannherklotz [dot] com
-Stability : experimental
-Portability : POSIX
-
-Template file for different configuration files.
--}
-
{-# LANGUAGE QuasiQuotes #-}
+-- |
+-- Module : Verismith.Tool.Template
+-- Description : Template file for different configuration files
+-- Copyright : (c) 2019, Yann Herklotz
+-- License : GPL-3
+-- Maintainer : yann [at] yannherklotz [dot] com
+-- Stability : experimental
+-- Portability : POSIX
+--
+-- Template file for different configuration files.
module Verismith.Tool.Template
- ( yosysSynthConfigStd
- , yosysSatConfig
- , yosysSimConfig
- , quartusLightSynthConfig
- , quartusSynthConfig
- , xstSynthConfig
- , vivadoSynthConfig
- , sbyConfig
- , icarusTestbench
- )
+ ( yosysSynthConfigStd,
+ yosysSatConfig,
+ yosysSimConfig,
+ quartusLightSynthConfig,
+ quartusSynthConfig,
+ xstSynthConfig,
+ vivadoSynthConfig,
+ sbyConfig,
+ icarusTestbench,
+ )
where
-import Control.Lens ((^..))
-import Data.Maybe (fromMaybe)
-import Data.Text (Text)
-import qualified Data.Text as T
-import Prelude hiding (FilePath)
-import Shelly
-import Verismith.Tool.Internal
-import Verismith.Verilog.AST
-import Verismith.Verilog.CodeGen
+import Control.Lens ((^..))
+import Data.Maybe (fromMaybe)
+import Data.Text (Text)
+import qualified Data.Text as T
+import Shelly
+import Verismith.Tool.Internal
+import Verismith.Verilog.AST
+import Verismith.Verilog.CodeGen
+import Prelude hiding (FilePath)
rename :: Text -> [Text] -> Text
rename end entries =
- T.intercalate "\n"
- $ flip mappend end
- . mappend "rename "
- . doubleName
- <$> entries
+ T.intercalate "\n" $
+ flip mappend end
+ . mappend "rename "
+ . doubleName
+ <$> entries
{-# INLINE rename #-}
doubleName :: Text -> Text
@@ -52,26 +50,28 @@ outputText :: Synthesiser a => a -> Text
outputText = toTextIgnore . synthOutput
yosysSynthConfig :: Synthesiser a => Text -> a -> FilePath -> Text
-yosysSynthConfig t a fp = T.unlines
- [ "read_verilog " <> toTextIgnore fp
- , t
- , "write_verilog " <> outputText a
- ]
+yosysSynthConfig t a fp =
+ T.unlines
+ [ "read_verilog " <> toTextIgnore fp,
+ t,
+ "write_verilog " <> outputText a
+ ]
yosysSynthConfigStd :: Synthesiser a => a -> FilePath -> Text
yosysSynthConfigStd = yosysSynthConfig "synth"
yosysSatConfig :: (Synthesiser a, Synthesiser b) => a -> b -> (SourceInfo ann) -> Text
-yosysSatConfig sim1 sim2 (SourceInfo top src) = T.unlines
- [ "read_verilog " <> outputText sim1
- , rename "_1" mis
- , "read_verilog syn_" <> outputText sim2 <> ".v"
- , rename "_2" mis
- , "read_verilog " <> top <> ".v"
- , "proc; opt_clean"
- , "flatten " <> top
- , "sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 " <> top
- ]
+yosysSatConfig sim1 sim2 (SourceInfo top src) =
+ T.unlines
+ [ "read_verilog " <> outputText sim1,
+ rename "_1" mis,
+ "read_verilog syn_" <> outputText sim2 <> ".v",
+ rename "_2" mis,
+ "read_verilog " <> top <> ".v",
+ "proc; opt_clean",
+ "flatten " <> top,
+ "sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 " <> top
+ ]
where
mis = src ^.. getSourceId
@@ -79,109 +79,115 @@ yosysSimConfig :: Text
yosysSimConfig = "read_verilog rtl.v; proc;;\nrename mod mod_rtl"
quartusLightSynthConfig :: Synthesiser a => a -> FilePath -> Text -> FilePath -> Text
-quartusLightSynthConfig q sdc top fp = T.unlines
- [ "load_package flow"
- , ""
- , "project_new -overwrite " <> top
- , ""
- , "set_global_assignment -name FAMILY \"Cyclone V\""
- , "set_global_assignment -name SYSTEMVERILOG_FILE " <> toTextIgnore fp
- , "set_global_assignment -name TOP_LEVEL_ENTITY " <> top
- , "set_global_assignment -name SDC_FILE " <> toTextIgnore sdc
- , "set_global_assignment -name INI_VARS \"qatm_force_vqm=on;\""
- , "set_global_assignment -name NUM_PARALLEL_PROCESSORS 2"
- , "set_instance_assignment -name VIRTUAL_PIN ON -to *"
- , ""
- , "execute_module -tool map"
- , "execute_module -tool fit"
- , "execute_module -tool sta -args \"--mode=implement\""
- , "execute_module -tool eda -args \"--simulation --tool=vcs\""
- , ""
- , "project_close"
- ]
+quartusLightSynthConfig q sdc top fp =
+ T.unlines
+ [ "load_package flow",
+ "",
+ "project_new -overwrite " <> top,
+ "",
+ "set_global_assignment -name FAMILY \"Cyclone V\"",
+ "set_global_assignment -name SYSTEMVERILOG_FILE " <> toTextIgnore fp,
+ "set_global_assignment -name TOP_LEVEL_ENTITY " <> top,
+ "set_global_assignment -name SDC_FILE " <> toTextIgnore sdc,
+ "set_global_assignment -name INI_VARS \"qatm_force_vqm=on;\"",
+ "set_global_assignment -name NUM_PARALLEL_PROCESSORS 2",
+ "set_instance_assignment -name VIRTUAL_PIN ON -to *",
+ "",
+ "execute_module -tool map",
+ "execute_module -tool fit",
+ "execute_module -tool sta -args \"--mode=implement\"",
+ "execute_module -tool eda -args \"--simulation --tool=vcs\"",
+ "",
+ "project_close"
+ ]
quartusSynthConfig :: Synthesiser a => a -> FilePath -> Text -> FilePath -> Text
-quartusSynthConfig q sdc top fp = T.unlines
- [ "load_package flow"
- , ""
- , "project_new -overwrite " <> top
- , ""
- , "set_global_assignment -name FAMILY \"Cyclone 10 GX\""
- , "set_global_assignment -name SYSTEMVERILOG_FILE " <> toTextIgnore fp
- , "set_global_assignment -name TOP_LEVEL_ENTITY " <> top
- , "set_global_assignment -name SDC_FILE " <> toTextIgnore sdc
- , "set_global_assignment -name INI_VARS \"qatm_force_vqm=on;\""
- , "set_global_assignment -name NUM_PARALLEL_PROCESSORS 2"
- , "set_instance_assignment -name VIRTUAL_PIN ON -to *"
- , ""
- , "execute_module -tool syn"
- , "execute_module -tool eda -args \"--simulation --tool=vcs\""
- , ""
- , "project_close"
- ]
+quartusSynthConfig q sdc top fp =
+ T.unlines
+ [ "load_package flow",
+ "",
+ "project_new -overwrite " <> top,
+ "",
+ "set_global_assignment -name FAMILY \"Cyclone 10 GX\"",
+ "set_global_assignment -name SYSTEMVERILOG_FILE " <> toTextIgnore fp,
+ "set_global_assignment -name TOP_LEVEL_ENTITY " <> top,
+ "set_global_assignment -name SDC_FILE " <> toTextIgnore sdc,
+ "set_global_assignment -name INI_VARS \"qatm_force_vqm=on;\"",
+ "set_global_assignment -name NUM_PARALLEL_PROCESSORS 2",
+ "set_instance_assignment -name VIRTUAL_PIN ON -to *",
+ "",
+ "execute_module -tool syn",
+ "execute_module -tool eda -args \"--simulation --tool=vcs\"",
+ "",
+ "project_close"
+ ]
xstSynthConfig :: Text -> Text
-xstSynthConfig top = T.unlines
- [ "run"
- , "-ifn " <> top <> ".prj -ofn " <> top <> " -p artix7 -top " <> top
- , "-iobuf NO -ram_extract NO -rom_extract NO -use_dsp48 NO"
- , "-fsm_extract YES -fsm_encoding Auto"
- , "-change_error_to_warning \"HDLCompiler:226 HDLCompiler:1832\""
- ]
+xstSynthConfig top =
+ T.unlines
+ [ "run",
+ "-ifn " <> top <> ".prj -ofn " <> top <> " -p artix7 -top " <> top,
+ "-iobuf NO -ram_extract NO -rom_extract NO -use_dsp48 NO",
+ "-fsm_extract YES -fsm_encoding Auto",
+ "-change_error_to_warning \"HDLCompiler:226 HDLCompiler:1832\""
+ ]
vivadoSynthConfig :: Text -> Text -> Text
-vivadoSynthConfig top outf = T.unlines
- [ "# CRITICAL WARNING: [Synth 8-5821] Potential divide by zero"
- , "set_msg_config -id {Synth 8-5821} -new_severity {WARNING}"
- , ""
- , "read_verilog rtl.v"
- , "synth_design -part xc7k70t -top " <> top
- , "write_verilog -force " <> outf
- ]
+vivadoSynthConfig top outf =
+ T.unlines
+ [ "# CRITICAL WARNING: [Synth 8-5821] Potential divide by zero",
+ "set_msg_config -id {Synth 8-5821} -new_severity {WARNING}",
+ "",
+ "read_verilog rtl.v",
+ "synth_design -part xc7k70t -top " <> top,
+ "write_verilog -force " <> outf
+ ]
sbyConfig :: (Synthesiser a, Synthesiser b) => Maybe Text -> FilePath -> a -> b -> (SourceInfo ann) -> Text
-sbyConfig mt datadir sim1 sim2 (SourceInfo top _) = T.unlines
- [ "[options]"
- , "multiclock on"
- , "mode prove"
- , "aigsmt " <> fromMaybe "none" mt
- , ""
- , "[engines]"
- , "abc pdr"
- , ""
- , "[script]"
- , readL
- , "read -formal " <> outputText sim1
- , "read -formal " <> outputText sim2
- , "read -formal top.v"
- , "prep -top " <> top
- , ""
- , "[files]"
- , depList
- , outputText sim2
- , outputText sim1
- , "top.v"
- ]
+sbyConfig mt datadir sim1 sim2 (SourceInfo top _) =
+ T.unlines
+ [ "[options]",
+ "multiclock on",
+ "mode prove",
+ "aigsmt " <> fromMaybe "none" mt,
+ "",
+ "[engines]",
+ "abc pdr",
+ "",
+ "[script]",
+ readL,
+ "read -formal " <> outputText sim1,
+ "read -formal " <> outputText sim2,
+ "read -formal top.v",
+ "prep -top " <> top,
+ "",
+ "[files]",
+ depList,
+ outputText sim2,
+ outputText sim1,
+ "top.v"
+ ]
where
deps = ["cells_cmos.v", "cells_cyclone_v.v", "cells_verific.v", "cells_xilinx_7.v", "cells_yosys.v"]
depList =
- T.intercalate "\n"
- $ toTextIgnore
- . (datadir </> fromText "data" </>)
- . fromText
- <$> deps
+ T.intercalate "\n" $
+ toTextIgnore
+ . (datadir </> fromText "data" </>)
+ . fromText
+ <$> deps
readL = T.intercalate "\n" $ mappend "read -formal " <$> deps
icarusTestbench :: (Synthesiser a, Show ann) => FilePath -> (Verilog ann) -> a -> Text
-icarusTestbench datadir t synth1 = T.unlines
- [ "`include \"" <> ddir <> "/data/cells_cmos.v\""
- , "`include \"" <> ddir <> "/data/cells_cyclone_v.v\""
- , "`include \"" <> ddir <> "/data/cells_verific.v\""
- , "`include \"" <> ddir <> "/data/cells_xilinx_7.v\""
- , "`include \"" <> ddir <> "/data/cells_yosys.v\""
- , "`include \"" <> toTextIgnore (synthOutput synth1) <> "\""
- , ""
- , genSource t
- ]
+icarusTestbench datadir t synth1 =
+ T.unlines
+ [ "`include \"" <> ddir <> "/data/cells_cmos.v\"",
+ "`include \"" <> ddir <> "/data/cells_cyclone_v.v\"",
+ "`include \"" <> ddir <> "/data/cells_verific.v\"",
+ "`include \"" <> ddir <> "/data/cells_xilinx_7.v\"",
+ "`include \"" <> ddir <> "/data/cells_yosys.v\"",
+ "`include \"" <> toTextIgnore (synthOutput synth1) <> "\"",
+ "",
+ genSource t
+ ]
where
ddir = toTextIgnore datadir
diff --git a/src/Verismith/Tool/Vivado.hs b/src/Verismith/Tool/Vivado.hs
index ef8b1b7..f0f8a23 100644
--- a/src/Verismith/Tool/Vivado.hs
+++ b/src/Verismith/Tool/Vivado.hs
@@ -1,71 +1,74 @@
-{-|
-Module : Verismith.Tool.Vivado
-Description : Vivado Synthesiser implementation.
-Copyright : (c) 2019, Yann Herklotz Grave
-License : GPL-3
-Maintainer : yann [at] yannherklotz [dot] com
-Stability : experimental
-Portability : POSIX
-
-Vivado Synthesiser implementation.
--}
-
+-- |
+-- Module : Verismith.Tool.Vivado
+-- Description : Vivado Synthesiser implementation.
+-- Copyright : (c) 2019, Yann Herklotz Grave
+-- License : GPL-3
+-- Maintainer : yann [at] yannherklotz [dot] com
+-- Stability : experimental
+-- Portability : POSIX
+--
+-- Vivado Synthesiser implementation.
module Verismith.Tool.Vivado
- ( Vivado(..)
- , defaultVivado
- )
+ ( Vivado (..),
+ defaultVivado,
+ )
where
-import Control.DeepSeq (NFData, rnf, rwhnf)
-import Data.Text (Text, unpack)
-import Prelude hiding (FilePath)
-import Shelly
-import Shelly.Lifted (liftSh)
-import Verismith.Tool.Internal
-import Verismith.Tool.Template
-import Verismith.Verilog.AST
-import Verismith.Verilog.CodeGen
+import Control.DeepSeq (NFData, rnf, rwhnf)
+import Data.Text (Text, unpack)
+import Shelly
+import Shelly.Lifted (liftSh)
+import Verismith.Tool.Internal
+import Verismith.Tool.Template
+import Verismith.Verilog.AST
+import Verismith.Verilog.CodeGen
+import Prelude hiding (FilePath)
-data Vivado = Vivado { vivadoBin :: !(Maybe FilePath)
- , vivadoDesc :: !Text
- , vivadoOutput :: !FilePath
- }
- deriving (Eq)
+data Vivado
+ = Vivado
+ { vivadoBin :: !(Maybe FilePath),
+ vivadoDesc :: !Text,
+ vivadoOutput :: !FilePath
+ }
+ deriving (Eq)
instance Tool Vivado where
- toText (Vivado _ t _) = t
+ toText (Vivado _ t _) = t
instance Show Vivado where
- show t = unpack $ toText t
+ show t = unpack $ toText t
instance Synthesiser Vivado where
- runSynth = runSynthVivado
- synthOutput = vivadoOutput
- setSynthOutput (Vivado a b _) = Vivado a b
+ runSynth = runSynthVivado
+ synthOutput = vivadoOutput
+ setSynthOutput (Vivado a b _) = Vivado a b
instance NFData Vivado where
- rnf = rwhnf
+ rnf = rwhnf
defaultVivado :: Vivado
defaultVivado = Vivado Nothing "vivado" "syn_vivado.v"
runSynthVivado :: Show ann => Vivado -> (SourceInfo ann) -> ResultSh ()
runSynthVivado sim (SourceInfo top src) = do
- dir <- liftSh pwd
- liftSh $ do
- writefile vivadoTcl . vivadoSynthConfig top . toTextIgnore $ synthOutput
- sim
- writefile "rtl.v" $ genSource src
- run_
- "sed"
- [ "s/^module/(* use_dsp48=\"no\" *) (* use_dsp=\"no\" *) module/;"
- , "-i"
- , "rtl.v"
- ]
- let exec_ n = execute_
- SynthFail
- dir
- "vivado"
- (maybe (fromText n) (</> fromText n) $ vivadoBin sim)
- exec_ "vivado" ["-mode", "batch", "-source", toTextIgnore vivadoTcl]
- where vivadoTcl = fromText ("vivado_" <> top) <.> "tcl"
+ dir <- liftSh pwd
+ liftSh $ do
+ writefile vivadoTcl . vivadoSynthConfig top . toTextIgnore $
+ synthOutput
+ sim
+ writefile "rtl.v" $ genSource src
+ run_
+ "sed"
+ [ "s/^module/(* use_dsp48=\"no\" *) (* use_dsp=\"no\" *) module/;",
+ "-i",
+ "rtl.v"
+ ]
+ let exec_ n =
+ execute_
+ SynthFail
+ dir
+ "vivado"
+ (maybe (fromText n) (</> fromText n) $ vivadoBin sim)
+ exec_ "vivado" ["-mode", "batch", "-source", toTextIgnore vivadoTcl]
+ where
+ vivadoTcl = fromText ("vivado_" <> top) <.> "tcl"
diff --git a/src/Verismith/Tool/XST.hs b/src/Verismith/Tool/XST.hs
index 213fae8..9447675 100644
--- a/src/Verismith/Tool/XST.hs
+++ b/src/Verismith/Tool/XST.hs
@@ -1,83 +1,85 @@
-{-|
-Module : Verismith.Tool.XST
-Description : XST (ise) simulator implementation.
-Copyright : (c) 2018-2019, Yann Herklotz
-License : GPL-3
-Maintainer : yann [at] yannherklotz [dot] com
-Stability : experimental
-Portability : POSIX
-
-XST (ise) simulator implementation.
--}
-
{-# LANGUAGE QuasiQuotes #-}
+-- |
+-- Module : Verismith.Tool.XST
+-- Description : XST (ise) simulator implementation.
+-- Copyright : (c) 2018-2019, Yann Herklotz
+-- License : GPL-3
+-- Maintainer : yann [at] yannherklotz [dot] com
+-- Stability : experimental
+-- Portability : POSIX
+--
+-- XST (ise) simulator implementation.
module Verismith.Tool.XST
- ( XST(..)
- , defaultXST
- )
+ ( XST (..),
+ defaultXST,
+ )
where
-import Control.DeepSeq (NFData, rnf, rwhnf)
-import Data.Text (Text, unpack)
-import Prelude hiding (FilePath)
-import Shelly
-import Shelly.Lifted (liftSh)
-import Verismith.Tool.Internal
-import Verismith.Tool.Template
-import Verismith.Verilog.AST
-import Verismith.Verilog.CodeGen
+import Control.DeepSeq (NFData, rnf, rwhnf)
+import Data.Text (Text, unpack)
+import Shelly
+import Shelly.Lifted (liftSh)
+import Verismith.Tool.Internal
+import Verismith.Tool.Template
+import Verismith.Verilog.AST
+import Verismith.Verilog.CodeGen
+import Prelude hiding (FilePath)
-data XST = XST { xstBin :: !(Maybe FilePath)
- , xstDesc :: !Text
- , xstOutput :: !FilePath
- }
- deriving (Eq)
+data XST
+ = XST
+ { xstBin :: !(Maybe FilePath),
+ xstDesc :: !Text,
+ xstOutput :: !FilePath
+ }
+ deriving (Eq)
instance Tool XST where
- toText (XST _ t _) = t
+ toText (XST _ t _) = t
instance Show XST where
- show t = unpack $ toText t
+ show t = unpack $ toText t
instance Synthesiser XST where
- runSynth = runSynthXST
- synthOutput = xstOutput
- setSynthOutput (XST a b _) = XST a b
+ runSynth = runSynthXST
+ synthOutput = xstOutput
+ setSynthOutput (XST a b _) = XST a b
instance NFData XST where
- rnf = rwhnf
+ rnf = rwhnf
defaultXST :: XST
defaultXST = XST Nothing "xst" "syn_xst.v"
runSynthXST :: Show ann => XST -> (SourceInfo ann) -> ResultSh ()
runSynthXST sim (SourceInfo top src) = do
- dir <- liftSh pwd
- let exec n = execute_
- SynthFail
- dir
- "xst"
- (maybe (fromText n) (</> fromText n) $ xstBin sim)
- liftSh $ do
- writefile xstFile $ xstSynthConfig top
- writefile prjFile "verilog work \"rtl.v\""
- writefile "rtl.v" $ genSource src
- exec "xst" ["-ifn", toTextIgnore xstFile]
- exec
- "netgen"
- [ "-w"
- , "-ofmt"
- , "verilog"
- , toTextIgnore $ modFile <.> "ngc"
- , toTextIgnore $ synthOutput sim
- ]
- liftSh . noPrint $ run_
- "sed"
- [ "-i"
- , "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;"
- , toTextIgnore $ synthOutput sim
- ]
+ dir <- liftSh pwd
+ let exec n =
+ execute_
+ SynthFail
+ dir
+ "xst"
+ (maybe (fromText n) (</> fromText n) $ xstBin sim)
+ liftSh $ do
+ writefile xstFile $ xstSynthConfig top
+ writefile prjFile "verilog work \"rtl.v\""
+ writefile "rtl.v" $ genSource src
+ exec "xst" ["-ifn", toTextIgnore xstFile]
+ exec
+ "netgen"
+ [ "-w",
+ "-ofmt",
+ "verilog",
+ toTextIgnore $ modFile <.> "ngc",
+ toTextIgnore $ synthOutput sim
+ ]
+ liftSh . noPrint $
+ run_
+ "sed"
+ [ "-i",
+ "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;",
+ toTextIgnore $ synthOutput sim
+ ]
where
modFile = fromText top
xstFile = modFile <.> "xst"
diff --git a/src/Verismith/Tool/Yosys.hs b/src/Verismith/Tool/Yosys.hs
index f68f39f..32c3fee 100644
--- a/src/Verismith/Tool/Yosys.hs
+++ b/src/Verismith/Tool/Yosys.hs
@@ -1,53 +1,53 @@
-{-|
-Module : Verismith.Tool.Yosys
-Description : Yosys simulator implementation.
-Copyright : (c) 2018-2019, Yann Herklotz
-License : GPL-3
-Maintainer : yann [at] yannherklotz [dot] com
-Stability : experimental
-Portability : POSIX
-
-Yosys simulator implementation.
--}
-
{-# LANGUAGE QuasiQuotes #-}
+-- |
+-- Module : Verismith.Tool.Yosys
+-- Description : Yosys simulator implementation.
+-- Copyright : (c) 2018-2019, Yann Herklotz
+-- License : GPL-3
+-- Maintainer : yann [at] yannherklotz [dot] com
+-- Stability : experimental
+-- Portability : POSIX
+--
+-- Yosys simulator implementation.
module Verismith.Tool.Yosys
- ( Yosys(..)
- , defaultYosys
- , runEquiv
- , runEquivYosys
- )
+ ( Yosys (..),
+ defaultYosys,
+ runEquiv,
+ runEquivYosys,
+ )
where
-import Control.DeepSeq (NFData, rnf, rwhnf)
-import Control.Lens
-import Control.Monad (void)
-import Data.Either (fromRight)
-import Data.Text (Text, unpack)
-import Prelude hiding (FilePath)
-import Shelly (FilePath, (</>))
-import qualified Shelly as S
-import Shelly.Lifted (liftSh, readfile)
-import Verismith.CounterEg (parseCounterEg)
-import Verismith.Result
-import Verismith.Tool.Internal
-import Verismith.Tool.Template
-import Verismith.Verilog.AST
-import Verismith.Verilog.CodeGen
-import Verismith.Verilog.Mutate
+import Control.DeepSeq (NFData, rnf, rwhnf)
+import Control.Lens
+import Control.Monad (void)
+import Data.Either (fromRight)
+import Data.Text (Text, unpack)
+import Shelly ((</>), FilePath)
+import qualified Shelly as S
+import Shelly.Lifted (liftSh, readfile)
+import Verismith.CounterEg (parseCounterEg)
+import Verismith.Result
+import Verismith.Tool.Internal
+import Verismith.Tool.Template
+import Verismith.Verilog.AST
+import Verismith.Verilog.CodeGen
+import Verismith.Verilog.Mutate
+import Prelude hiding (FilePath)
-data Yosys = Yosys { yosysBin :: !(Maybe FilePath)
- , yosysDesc :: !Text
- , yosysOutput :: !FilePath
- }
- deriving (Eq)
+data Yosys
+ = Yosys
+ { yosysBin :: !(Maybe FilePath),
+ yosysDesc :: !Text,
+ yosysOutput :: !FilePath
+ }
+ deriving (Eq)
instance Tool Yosys where
- toText (Yosys _ t _) = t
+ toText (Yosys _ t _) = t
instance Show Yosys where
- show t = unpack $ toText t
+ show t = unpack $ toText t
instance Synthesiser Yosys where
runSynth = runSynthYosys
@@ -55,7 +55,7 @@ instance Synthesiser Yosys where
setSynthOutput (Yosys a b _) = Yosys a b
instance NFData Yosys where
- rnf = rwhnf
+ rnf = rwhnf
defaultYosys :: Yosys
defaultYosys = Yosys Nothing "yosys" "syn_yosys.v"
@@ -65,68 +65,78 @@ yosysPath sim = maybe (S.fromText "yosys") (</> S.fromText "yosys") $ yosysBin s
runSynthYosys :: Show ann => Yosys -> (SourceInfo ann) -> ResultSh ()
runSynthYosys sim (SourceInfo _ src) = do
- dir <- liftSh $ do
- dir' <- S.pwd
- S.writefile inpf $ genSource src
- return dir'
- execute_
- SynthFail
- dir
- "yosys"
- (yosysPath sim)
- [ "-p"
- , "read_verilog " <> inp <> "; synth; write_verilog -noattr " <> out
- ]
+ dir <- liftSh $ do
+ dir' <- S.pwd
+ S.writefile inpf $ genSource src
+ return dir'
+ execute_
+ SynthFail
+ dir
+ "yosys"
+ (yosysPath sim)
+ [ "-p",
+ "read_verilog " <> inp <> "; synth; write_verilog -noattr " <> out
+ ]
where
inpf = "rtl.v"
- inp = S.toTextIgnore inpf
- out = S.toTextIgnore $ synthOutput sim
+ inp = S.toTextIgnore inpf
+ out = S.toTextIgnore $ synthOutput sim
-runEquivYosys
- :: (Synthesiser a, Synthesiser b, Show ann)
- => Yosys
- -> a
- -> b
- -> (SourceInfo ann)
- -> ResultSh ()
+runEquivYosys ::
+ (Synthesiser a, Synthesiser b, Show ann) =>
+ Yosys ->
+ a ->
+ b ->
+ (SourceInfo ann) ->
+ ResultSh ()
runEquivYosys yosys sim1 sim2 srcInfo = do
- liftSh $ do
- S.writefile "top.v"
- . genSource
- . initMod
- . makeTop 2
- $ srcInfo
- ^. mainModule
- S.writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo
- runSynth sim1 srcInfo
- runSynth sim2 srcInfo
- liftSh $ S.run_ (yosysPath yosys) [S.toTextIgnore checkFile]
- where checkFile = S.fromText $ "test." <> toText sim1 <> "." <> toText sim2 <> ".ys"
+ liftSh $ do
+ S.writefile "top.v"
+ . genSource
+ . initMod
+ . makeTop 2
+ $ srcInfo
+ ^. mainModule
+ S.writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo
+ runSynth sim1 srcInfo
+ runSynth sim2 srcInfo
+ liftSh $ S.run_ (yosysPath yosys) [S.toTextIgnore checkFile]
+ where
+ checkFile = S.fromText $ "test." <> toText sim1 <> "." <> toText sim2 <> ".ys"
-runEquiv :: (Synthesiser a, Synthesiser b, Show ann)
- => Maybe Text -> FilePath -> a -> b -> (SourceInfo ann) -> ResultSh ()
+runEquiv ::
+ (Synthesiser a, Synthesiser b, Show ann) =>
+ Maybe Text ->
+ FilePath ->
+ a ->
+ b ->
+ (SourceInfo ann) ->
+ ResultSh ()
runEquiv mt datadir sim1 sim2 srcInfo = do
- dir <- liftSh S.pwd
- liftSh $ do
- S.writefile "top.v"
- . genSource
- . initMod
- . makeTopAssert
- $ srcInfo
- ^. mainModule
- replaceMods (synthOutput sim1) "_1" srcInfo
- replaceMods (synthOutput sim2) "_2" srcInfo
- S.writefile "proof.sby" $ sbyConfig mt datadir sim1 sim2 srcInfo
- e <- liftSh $ do
- exe dir "symbiyosys" "sby" ["-f", "proof.sby"]
- S.lastExitCode
- case e of
- 0 -> ResultT . return $ Pass ()
- 2 -> case mt of
- Nothing -> ResultT . return . Fail $ EquivFail Nothing
- Just _ -> ResultT $ Fail . EquivFail . Just . fromRight mempty
- . parseCounterEg <$> readfile "proof/engine_0/trace.smtc"
- 124 -> ResultT . return $ Fail TimeoutError
- _ -> ResultT . return $ Fail EquivError
+ dir <- liftSh S.pwd
+ liftSh $ do
+ S.writefile "top.v"
+ . genSource
+ . initMod
+ . makeTopAssert
+ $ srcInfo
+ ^. mainModule
+ replaceMods (synthOutput sim1) "_1" srcInfo
+ replaceMods (synthOutput sim2) "_2" srcInfo
+ S.writefile "proof.sby" $ sbyConfig mt datadir sim1 sim2 srcInfo
+ e <- liftSh $ do
+ exe dir "symbiyosys" "sby" ["-f", "proof.sby"]
+ S.lastExitCode
+ case e of
+ 0 -> ResultT . return $ Pass ()
+ 2 -> case mt of
+ Nothing -> ResultT . return . Fail $ EquivFail Nothing
+ Just _ ->
+ ResultT $
+ Fail . EquivFail . Just . fromRight mempty
+ . parseCounterEg
+ <$> readfile "proof/engine_0/trace.smtc"
+ 124 -> ResultT . return $ Fail TimeoutError
+ _ -> ResultT . return $ Fail EquivError
where
exe dir name e = void . S.errExit False . logCommand dir name . timeout e
generated by cgit (git 2.34.1) at 2024-05-20 13:51:49 +0000