From 805f67c07cc15d784078b00a84f4055f84016cec Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 11 May 2020 18:29:06 +0100 Subject: Fix types with annotations --- src/Verismith/Tool/Icarus.hs | 9 +++++---- src/Verismith/Tool/Identity.hs | 2 +- src/Verismith/Tool/Internal.hs | 10 ++++++---- src/Verismith/Tool/Quartus.hs | 2 +- src/Verismith/Tool/QuartusLight.hs | 2 +- src/Verismith/Tool/Template.hs | 2 +- src/Verismith/Tool/Vivado.hs | 2 +- src/Verismith/Tool/XST.hs | 2 +- src/Verismith/Tool/Yosys.hs | 8 ++++---- 9 files changed, 21 insertions(+), 18 deletions(-) (limited to 'src/Verismith/Tool') diff --git a/src/Verismith/Tool/Icarus.hs b/src/Verismith/Tool/Icarus.hs index 0fb2146..4b91652 100644 --- a/src/Verismith/Tool/Icarus.hs +++ b/src/Verismith/Tool/Icarus.hs @@ -103,7 +103,7 @@ mask = T.replace "x" "0" callback :: ByteString -> Text -> ByteString callback b t = b <> convert (mask t) -runSimIcarus :: Icarus -> (SourceInfo ann) -> [ByteString] -> ResultSh ByteString +runSimIcarus :: Show ann => Icarus -> (SourceInfo ann) -> [ByteString] -> ResultSh ByteString runSimIcarus sim rinfo bss = do let tb = ModDecl "main" @@ -159,7 +159,8 @@ counterTestBench (CounterEg _ states) m = tbModule filtered m where filtered = convert . fold . fmap snd . filter ((/= "clk") . fst) <$> states -runSimIc' :: (Synthesiser b) => ([ByteString] -> (ModDecl ann) -> (Verilog ann)) +runSimIc' :: (Synthesiser b, Show ann) + => ([ByteString] -> (ModDecl ann) -> (Verilog ann)) -> FilePath -> Icarus -> b @@ -194,7 +195,7 @@ runSimIc' fun datadir sim1 synth1 srcInfo bss bs = do tbname = fromText $ toText synth1 <> "_testbench.v" exename = toText synth1 <> "_main" -runSimIc :: (Synthesiser b) +runSimIc :: (Synthesiser b, Show ann) => FilePath -- ^ Data directory. -> Icarus -- ^ Icarus simulator. -> b -- ^ Synthesis tool to be tested. @@ -206,6 +207,6 @@ runSimIc :: (Synthesiser b) -> ResultSh ByteString runSimIc = runSimIc' tbModule -runSimIcEC :: (Synthesiser b) => FilePath -> Icarus -> b +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 8f6901f..804f096 100644 --- a/src/Verismith/Tool/Identity.hs +++ b/src/Verismith/Tool/Identity.hs @@ -44,7 +44,7 @@ instance Synthesiser Identity where instance NFData Identity where rnf = rwhnf -runSynthIdentity :: Identity -> (SourceInfo ann) -> ResultSh () +runSynthIdentity :: Show ann => Identity -> (SourceInfo ann) -> ResultSh () runSynthIdentity (Identity _ out) = writefile out . genSource defaultIdentity :: Identity diff --git a/src/Verismith/Tool/Internal.hs b/src/Verismith/Tool/Internal.hs index 77ec4c9..f462c74 100644 --- a/src/Verismith/Tool/Internal.hs +++ b/src/Verismith/Tool/Internal.hs @@ -65,9 +65,10 @@ class Tool a where -- | Simulation type class. class Tool a => Simulator a where - runSim :: a -- ^ Simulator instance - -> SourceInfo ann -- ^ Run information - -> [ByteString] -- ^ Inputs to simulate + 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 @@ -99,7 +100,8 @@ instance Monoid Failed where -- | Synthesiser type class. class Tool a => Synthesiser a where - runSynth :: a -- ^ Synthesiser tool instance + runSynth :: Show ann + => a -- ^ Synthesiser tool instance -> SourceInfo ann -- ^ Run information -> ResultSh () -- ^ does not return any values synthOutput :: a -> FilePath diff --git a/src/Verismith/Tool/Quartus.hs b/src/Verismith/Tool/Quartus.hs index e6624eb..ff8a62b 100644 --- a/src/Verismith/Tool/Quartus.hs +++ b/src/Verismith/Tool/Quartus.hs @@ -49,7 +49,7 @@ instance NFData Quartus where defaultQuartus :: Quartus defaultQuartus = Quartus Nothing "quartus" "syn_quartus.v" -runSynthQuartus :: Quartus -> (SourceInfo ann) -> ResultSh () +runSynthQuartus :: Show ann => Quartus -> (SourceInfo ann) -> ResultSh () runSynthQuartus sim (SourceInfo top src) = do dir <- liftSh pwd let ex = execute_ SynthFail dir "quartus" diff --git a/src/Verismith/Tool/QuartusLight.hs b/src/Verismith/Tool/QuartusLight.hs index f703da0..cdf2636 100644 --- a/src/Verismith/Tool/QuartusLight.hs +++ b/src/Verismith/Tool/QuartusLight.hs @@ -49,7 +49,7 @@ instance NFData QuartusLight where defaultQuartusLight :: QuartusLight defaultQuartusLight = QuartusLight Nothing "quartus" "syn_quartus.v" -runSynthQuartusLight :: QuartusLight -> (SourceInfo ann) -> ResultSh () +runSynthQuartusLight :: Show ann => QuartusLight -> (SourceInfo ann) -> ResultSh () runSynthQuartusLight sim (SourceInfo top src) = do dir <- liftSh pwd let ex = execute_ SynthFail dir "quartus" diff --git a/src/Verismith/Tool/Template.hs b/src/Verismith/Tool/Template.hs index a2e0675..5a20ff5 100644 --- a/src/Verismith/Tool/Template.hs +++ b/src/Verismith/Tool/Template.hs @@ -172,7 +172,7 @@ sbyConfig mt datadir sim1 sim2 (SourceInfo top _) = T.unlines <$> deps readL = T.intercalate "\n" $ mappend "read -formal " <$> deps -icarusTestbench :: (Synthesiser a) => FilePath -> (Verilog ann) -> a -> Text +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\"" diff --git a/src/Verismith/Tool/Vivado.hs b/src/Verismith/Tool/Vivado.hs index 35cda2e..ef8b1b7 100644 --- a/src/Verismith/Tool/Vivado.hs +++ b/src/Verismith/Tool/Vivado.hs @@ -49,7 +49,7 @@ instance NFData Vivado where defaultVivado :: Vivado defaultVivado = Vivado Nothing "vivado" "syn_vivado.v" -runSynthVivado :: Vivado -> (SourceInfo ann) -> ResultSh () +runSynthVivado :: Show ann => Vivado -> (SourceInfo ann) -> ResultSh () runSynthVivado sim (SourceInfo top src) = do dir <- liftSh pwd liftSh $ do diff --git a/src/Verismith/Tool/XST.hs b/src/Verismith/Tool/XST.hs index 1e37149..213fae8 100644 --- a/src/Verismith/Tool/XST.hs +++ b/src/Verismith/Tool/XST.hs @@ -51,7 +51,7 @@ instance NFData XST where defaultXST :: XST defaultXST = XST Nothing "xst" "syn_xst.v" -runSynthXST :: XST -> (SourceInfo ann) -> ResultSh () +runSynthXST :: Show ann => XST -> (SourceInfo ann) -> ResultSh () runSynthXST sim (SourceInfo top src) = do dir <- liftSh pwd let exec n = execute_ diff --git a/src/Verismith/Tool/Yosys.hs b/src/Verismith/Tool/Yosys.hs index 24b83fd..f68f39f 100644 --- a/src/Verismith/Tool/Yosys.hs +++ b/src/Verismith/Tool/Yosys.hs @@ -63,7 +63,7 @@ defaultYosys = Yosys Nothing "yosys" "syn_yosys.v" yosysPath :: Yosys -> FilePath yosysPath sim = maybe (S.fromText "yosys") ( S.fromText "yosys") $ yosysBin sim -runSynthYosys :: Yosys -> (SourceInfo ann) -> ResultSh () +runSynthYosys :: Show ann => Yosys -> (SourceInfo ann) -> ResultSh () runSynthYosys sim (SourceInfo _ src) = do dir <- liftSh $ do dir' <- S.pwd @@ -83,7 +83,7 @@ runSynthYosys sim (SourceInfo _ src) = do out = S.toTextIgnore $ synthOutput sim runEquivYosys - :: (Synthesiser a, Synthesiser b) + :: (Synthesiser a, Synthesiser b, Show ann) => Yosys -> a -> b @@ -103,8 +103,8 @@ runEquivYosys yosys sim1 sim2 srcInfo = do liftSh $ S.run_ (yosysPath yosys) [S.toTextIgnore checkFile] where checkFile = S.fromText $ "test." <> toText sim1 <> "." <> toText sim2 <> ".ys" -runEquiv - :: (Synthesiser a, Synthesiser b) => 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 -- cgit From 7124a4f00e536b4d5323a7488c1f65469dddb102 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 12 May 2020 12:21:36 +0100 Subject: Format with ormolu --- src/Verismith/Tool/Icarus.hs | 346 +++++++++++++++++++++---------------- src/Verismith/Tool/Identity.hs | 68 ++++---- src/Verismith/Tool/Internal.hs | 293 ++++++++++++++++--------------- src/Verismith/Tool/Quartus.hs | 113 ++++++------ src/Verismith/Tool/QuartusLight.hs | 113 ++++++------ src/Verismith/Tool/Template.hs | 288 +++++++++++++++--------------- src/Verismith/Tool/Vivado.hs | 109 ++++++------ src/Verismith/Tool/XST.hs | 122 ++++++------- src/Verismith/Tool/Yosys.hs | 206 +++++++++++----------- 9 files changed, 869 insertions(+), 789 deletions(-) (limited to 'src/Verismith/Tool') 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 -- cgit