packages feed

verismith 0.4.0.0 → 0.4.0.1

raw patch · 33 files changed

+1141/−1215 lines, 33 files

Files

README.md view
@@ -1,10 +1,6 @@ # Verismith [![Build Status](https://travis-ci.com/ymherklotz/verismith.svg?token=qfBKKGwxeWkjDsy7e16x&branch=master)](https://travis-ci.com/ymherklotz/verismith) -Verilog Fuzzer to test the major verilog compilers by generating random, valid-and deterministic Verilog. There is a-[presentation](https://yannherklotz.com/docs/presentation.pdf) about Verismith-and a [thesis](https://yannherklotz.com/docs/thesis.pdf) which goes over all the-details of the implementation and results that were found.+Verilog Fuzzer to test the major verilog compilers by generating random, valid and deterministic Verilog. There is a [presentation](https://yannherklotz.com/docs/presentation.pdf) about Verismith and a [thesis](https://yannherklotz.com/docs/thesis.pdf) which goes over all the details of the implementation and results that were found.  It currently supports the following synthesis tools: @@ -19,9 +15,7 @@  ## Supported Verilog Constructs -The fuzzer generates combinational and behavioural Verilog to test the various-tools. The most notable constructs that are supported and generated are the-following:+The fuzzer generates combinational and behavioural Verilog to test the various tools. The most notable constructs that are supported and generated are the following:  - module definitions with parameter definitions, inputs and outputs - module items, such as instantiations, continuous assignment, always blocks,@@ -35,8 +29,7 @@  ## Reported bugs -21 bugs were found in total over the course of a month. 8 of those bugs were-reported and 3 were fixed.+9 bugs have been reported and confirmed to be bugs by the vendors, out of which 4 have been fixed.  ### Yosys @@ -57,11 +50,9 @@ | Mis-synthesis | [Forum 982518](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Signed-with-shift-in-condition-synthesis-mistmatch/td-p/982518) | ✓         | 𐄂     | | Mis-synthesis | [Forum 982419](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Bit-selection-synthesis-mismatch/td-p/982419)                   | ✓         | 𐄂     | -## Build the Fuzzer+## Install the Fuzzer -The fuzzer now supports building with [nix](https://nixos.org/nix/manual/),-which pulls in all the extra dependencies that are needed to build the-project. The main files and their functions are described below:+The fuzzer now supports building with [nix](https://nixos.org/nix/manual/), which pulls in all the extra dependencies that are needed to build the project. The main files and their functions are described below:  - `default.nix`: describes the main Haskell package and it's dependencies that   have to be pulled in.@@ -72,82 +63,70 @@   dependencies so that everything builds nicely. The exact versions of the   packages that should be overridden are in [nix](/nix). -It may be possible to build it purely with-[cabal-install](https://hackage.haskell.org/package/cabal-install), however-it may not have all the right versions of the dependencies that are needed.+It may be possible to build it purely with [cabal-install](https://hackage.haskell.org/package/cabal-install), however it may not have all the right versions of the dependencies that are needed. -Instead, stack could be used and the `stack.yaml` file could contain the-overrides that are used by nix.+Instead, stack could be used and the `stack.yaml` file could contain the overrides that are used by nix. -### Build with nix+### Build from hackage -Nix build is completely supported, therefore if nix is installed, building the-project is as simple as+A stable version of Verismith is available on [hackage](https://hackage.haskell.org/package/verismith) and can be installed using cabal directly without having to build the project from the repository:  ``` shell-nix-build release.nix+cabal install verismith ``` -If one wants to work in the project with all the right dependencies loaded, one-can use+It will be placed under the `bin` cabal folder which can be added to your path to run Verismith. +### Build with nix from source++Nix build is completely supported, therefore if nix is installed, building the project is as simple as+ ``` shell+nix-build+```++If one wants to work in the project with all the right dependencies loaded, one can use++``` shell nix-shell ``` -### Build with cabal and nix+and use cabal to build and run the program. -After entering a development environment with `nix-shell`, the project can-safely be built with `cabal-install`.+### Build with cabal from source +After entering a development environment with `nix-shell`, the project can safely be built with `cabal-install`. However, even without `nix`, the project can still be built with cabal alone using:+ ``` shell-cabal v2-configure-cabal v2-build+cabal configure+cabal build ``` -This should not have to download any extra dependencies and just have to build-the actual project itself.+Verismith can then be run using: +``` shell+cabal run verismith+```+ ## Configuration -Verismith can be configured using a [TOML](https://github.com/toml-lang/toml)-file. There are four main sections in the configuration file, an example can be-seen [here](/examples/config.toml).+Verismith can be configured using a [TOML](https://github.com/toml-lang/toml) file. There are four main sections in the configuration file, an example can be seen [here](/examples/config.toml).  ### Information section  -Contains information about the command line tool being used, such as the hash of-the commit it was compiled with and the version of the tool. The tool then-verifies that these match the current configuration, and will emit a warning if-they do not. This ensures that if one wants a deterministic run and is therefore-passing a seed to the generation, that it will always give the same-result. Different versions might change some aspects of the Verilog generation,-which would affect how a seed would generate Verilog.+Contains information about the command line tool being used, such as the hash of the commit it was compiled with and the version of the tool. The tool then verifies that these match the current configuration, and will emit a warning if they do not. This ensures that if one wants a deterministic run and is therefore passing a seed to the generation, that it will always give the same result. Different versions might change some aspects of the Verilog generation, which would affect how a seed would generate Verilog.  ### Probability section  -Provides a way to assign frequency values to each of the nodes in the-AST. During the state-based generation, each node is chosen randomly based on-those probabilities. This provides a simple way to drastically change the-Verilog that is generated, by changing how often a construct is chosen or by not-generating a construct at all.+Provides a way to assign frequency values to each of the nodes in the AST. During the state-based generation, each node is chosen randomly based on those probabilities. This provides a simple way to drastically change the Verilog that is generated, by changing how often a construct is chosen or by not generating a construct at all.  ### Property section  -Changes properties of the generated Verilog code, such as the size of the-output, maximum statement or module depth and sampling method of Verilog-programs. This section also allows a seed to be specified, which would mean that-only that particular seed will be used in the fuzz run. This is extremely useful-when wanting to replay a specific failure and the output is missing.+Changes properties of the generated Verilog code, such as the size of the output, maximum statement or module depth and sampling method of Verilog programs. This section also allows a seed to be specified, which would mean that only that particular seed will be used in the fuzz run. This is extremely useful when wanting to replay a specific failure and the output is missing.  ### Synthesiser section  -Accepts a list of synthesisers which will be fuzzed. These have to first be-defined in the code and implement the required interface. They can then be-configured by having a name assigned to them and the name of the output Verilog-file. By each having a different name, multiple instances of the same-synthesiser can be included in a fuzz run. The instances might differ in the-optimisations that are performed, or in the version of the synthesiser.+Accepts a list of synthesisers which will be fuzzed. These have to first be defined in the code and implement the required interface. They can then be configured by having a name assigned to them and the name of the output Verilog file. By each having a different name, multiple instances of the same synthesiser can be included in a fuzz run. The instances might differ in the optimisations that are performed, or in the version of the synthesiser.  ## Benchmark Results @@ -179,11 +158,6 @@  ## Acknowledgement -Clifford Wolf's [VlogHammer](http://www.clifford.at/yosys/vloghammer.html) is an-existing Verilog fuzzer that generates random Verilog to test how expressions-are handled in synthesis tools and simulators. It was the inspiration for the-general structure of this fuzzer, which extends the fuzzing to the behavioural-parts of Verilog.+Clifford Wolf's [VlogHammer](http://www.clifford.at/yosys/vloghammer.html) is an existing Verilog fuzzer that generates random Verilog to test how expressions are handled in synthesis tools and simulators. It was the inspiration for thegeneral structure of this fuzzer, which extends the fuzzing to the behavioural parts of Verilog. -Tom Hawkins' Verilog parser was used to write the lexer, the parser was then-rewritten using [Parsec](https://hackage.haskell.org/package/parsec).+Tom Hawkins' Verilog parser was used to write the lexer, the parser was then rewritten using [Parsec](https://hackage.haskell.org/package/parsec).
examples/config.toml view
@@ -1,7 +1,7 @@  [info]-  commit = "d32f4cc45bc8c0670fb788b1fcd4c2f2b15fa094"-  version = "0.3.0.0"+  commit = "e57b16651684e0f9e9d0a3cd6f81fccd5b8c7cb6"+  version = "0.4.0.1"  [probability]   expr.binary = 5@@ -24,8 +24,10 @@   statement.nonblocking = 3  [property]+  determinism = 1   module.depth = 2   module.max = 5+  nondeterminism = 0   output.combine = false   sample.method = "random"   sample.size = 10
− nix/hedgehog-fn.nix 
@@ -1,17 +0,0 @@-{ mkDerivation, base, contravariant, hedgehog, stdenv, transformers-}:-mkDerivation {-  pname = "hedgehog-fn";-  version = "0.6";-  sha256 = "fb02b67fba97e24c226feba010d2b308934c54e20a0723b6ea7e4eb199f02176";-  revision = "1";-  editedCabalFile = "19v7amg8l6s1gadnya8nxkcbi0vd3wqc7h6gvqvs099qaqm7zbb1";-  isLibrary = true;-  isExecutable = true;-  libraryHaskellDepends = [-    base contravariant hedgehog transformers-  ];-  homepage = "https://github.com/qfpl/hedgehog-fn";-  description = "Function generation for `hedgehog`";-  license = stdenv.lib.licenses.bsd3;-}
− nix/parser-combinators.nix 
@@ -1,10 +0,0 @@-{ mkDerivation, base, stdenv }:-mkDerivation {-  pname = "parser-combinators";-  version = "1.1.0";-  sha256 = "ac7642972b18a47c575d2bcd0b2f6c34f33ca2ed3adb28034420d09ced823e91";-  libraryHaskellDepends = [ base ];-  homepage = "https://github.com/mrkkrp/parser-combinators";-  description = "Lightweight package providing commonly useful parser combinators";-  license = stdenv.lib.licenses.bsd3;-}
− nix/tasty-hedgehog.nix 
@@ -1,17 +0,0 @@-{ mkDerivation, base, hedgehog, stdenv, tagged, tasty-, tasty-expected-failure-}:-mkDerivation {-  pname = "tasty-hedgehog";-  version = "0.2.0.0";-  sha256 = "5a107fc3094efc50663e4634331a296281318b38c9902969c2d2d215d754a182";-  revision = "6";-  editedCabalFile = "0d7s1474pvnyad6ilr5rvpama7s468ya9ns4ksbl0827z9vvga43";-  libraryHaskellDepends = [ base hedgehog tagged tasty ];-  testHaskellDepends = [-    base hedgehog tasty tasty-expected-failure-  ];-  homepage = "https://github.com/qfpl/tasty-hedgehog";-  description = "Integration for tasty and hedgehog";-  license = stdenv.lib.licenses.bsd3;-}
− nix/tomland.nix 
@@ -1,33 +0,0 @@-{ mkDerivation, aeson, base, bytestring, containers, deepseq-, directory, gauge, hashable, hedgehog, hspec-megaparsec, htoml-, htoml-megaparsec, markdown-unlit, megaparsec, mtl, parsec-, parser-combinators, stdenv, tasty, tasty-discover, tasty-hedgehog-, tasty-hspec, tasty-silver, text, time, toml-parser, transformers-, unordered-containers-}:-mkDerivation {-  pname = "tomland";-  version = "1.1.0.1";-  sha256 = "51cde31c25056c6a0714758eb782bda0c019bdd2ef58f29baf6364cbf6451f46";-  isLibrary = true;-  isExecutable = true;-  libraryHaskellDepends = [-    base bytestring containers deepseq hashable megaparsec mtl-    parser-combinators text time transformers unordered-containers-  ];-  executableHaskellDepends = [ base text time unordered-containers ];-  executableToolDepends = [ markdown-unlit ];-  testHaskellDepends = [-    base bytestring containers directory hashable hedgehog-    hspec-megaparsec megaparsec tasty tasty-hedgehog tasty-hspec-    tasty-silver text time unordered-containers-  ];-  testToolDepends = [ tasty-discover ];-  benchmarkHaskellDepends = [-    aeson base deepseq gauge htoml htoml-megaparsec parsec text time-    toml-parser-  ];-  homepage = "https://github.com/kowainik/tomland";-  description = "Bidirectional TOML serialization";-  license = stdenv.lib.licenses.mpl20;-}
scripts/run.py view
@@ -2,21 +2,28 @@  import subprocess import os+import sys+import datetime -def main():-        i = 0-        name = "mediumB"-        config = "experiments/config_yosys.toml"-        iterations = 50-        directory = "yosys_all"-        if not os.path.exists(directory):-                os.makedirs(directory)-        while True:-                subprocess.call(["verismith", "fuzz"-                                 , "-o", directory + "/" + name + str(i)-                                 , "-c", config-                                 , "-n", str(iterations)])-                i += 1+def main(run_id):+    i = 0+    name = "medium_{}_".format(run_id)+    config = "config.toml"+    iterations = 100+    directory = "yosys_all"+    try:+        os.makedirs(directory)+    except IOError:+        pass+    while True:+        output_directory = directory + "/" + name + str(i)+        print("{} :: {}".format(datetime.datetime.now(), output_directory))+        with open(output_directory + ".log", "w") as f:+            subprocess.call(["cabal", "run", "-O2", "verismith", "--", "fuzz"+                             , "-o", output_directory+                             , "-c", config+                             , "-n", str(iterations)], stdout=f)+        i += 1  if __name__ == '__main__':-        main()+    main(sys.argv[1])
src/Verismith.hs view
@@ -30,7 +30,7 @@     , module Verismith.Verilog     , module Verismith.Config     , module Verismith.Circuit-    , module Verismith.Sim+    , module Verismith.Tool     , module Verismith.Fuzz     , module Verismith.Report     )@@ -65,8 +65,8 @@ import           Verismith.Reduce import           Verismith.Report import           Verismith.Result-import           Verismith.Sim-import           Verismith.Sim.Internal+import           Verismith.Tool+import           Verismith.Tool.Internal import           Verismith.Verilog import           Verismith.Verilog.Parser (parseSourceInfoFile) @@ -363,12 +363,12 @@     ce = config ^. configProbability . probExpr  handleOpts :: Opts -> IO ()-handleOpts (Fuzz o configF _ _ n) = do+handleOpts (Fuzz o configF _ k n) = do     config <- getConfig configF     _      <- runFuzz         config         defaultYosys-        (fuzzMultiple n (Just $ fromText o) (proceduralSrc "top" config))+        (fuzzMultiple n k (Just $ fromText o) (proceduralSrc "top" config))     return () handleOpts (Generate f c) = do     config <- getConfig c
src/Verismith/Config.hs view
@@ -92,10 +92,10 @@ import           Shelly                 (toTextIgnore) import           Toml                   (TomlCodec, (.=)) import qualified Toml-import           Verismith.Sim.Quartus-import           Verismith.Sim.Vivado-import           Verismith.Sim.XST-import           Verismith.Sim.Yosys+import           Verismith.Tool.Quartus+import           Verismith.Tool.Vivado+import           Verismith.Tool.XST+import           Verismith.Tool.Yosys  -- $conf --
src/Verismith/Fuzz.hs view
@@ -59,9 +59,9 @@ import           Verismith.Reduce import           Verismith.Report import           Verismith.Result-import           Verismith.Sim.Icarus-import           Verismith.Sim.Internal-import           Verismith.Sim.Yosys+import           Verismith.Tool.Icarus+import           Verismith.Tool.Internal+import           Verismith.Tool.Yosys import           Verismith.Verilog.AST import           Verismith.Verilog.CodeGen @@ -194,24 +194,19 @@     equiv a b =         toolRun ("equivalence check for " <> toText a <> " and " <> toText b)             . runResultT-            $ do-                  make dir-                  pop dir $ do-                      liftSh $ do-                          cp-                                  (   fromText ".."-                                  </> fromText (toText a)-                                  </> synthOutput a-                                  )-                              $ synthOutput a-                          cp-                                  (   fromText ".."-                                  </> fromText (toText b)-                                  </> synthOutput b-                                  )-                              $ synthOutput b-                          writefile "rtl.v" $ genSource src-                      runEquiv a b src+            $ do make dir+                 pop dir $ do+                     liftSh $ do+                         cp ( fromText ".."+                              </> fromText (toText a)+                              </> synthOutput a+                            ) $ synthOutput a+                         cp ( fromText ".."+                              </> fromText (toText b)+                              </> synthOutput b+                            ) $ synthOutput b+                         writefile "rtl.v" $ genSource src+                     runEquiv a b src         where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b  simulation :: (MonadIO m, MonadSh m) => SourceInfo -> Fuzz m ()@@ -382,11 +377,9 @@                             tsynth                             tequiv                             (getTime redResult)-    liftSh . writefile "index.html" $ printResultReport (bname currdir) report     return report   where     seed      = conf ^. configProperty . propSeed-    bname     = T.pack . takeBaseName . T.unpack . toTextIgnore     genMethod = case T.toLower $ conf ^. configProperty . propSampleMethod of         "hat" -> do             logT "Using the hat function"@@ -407,21 +400,47 @@     newPath <- relPath dir     return $ (fuzzDir .~ newPath) fr +filterSynth :: SynthResult -> Bool+filterSynth (SynthResult _ _ (Pass _) _) = True+filterSynth _                            = False++filterSim :: SimResult -> Bool+filterSim (SimResult _ _ (Pass _) _) = True+filterSim _                          = False++filterSynthStat :: SynthStatus -> Bool+filterSynthStat (SynthStatus _ (Pass _) _) = True+filterSynthStat _                          = False++passedFuzz :: FuzzReport -> Bool+passedFuzz (FuzzReport _ synth sim synthstat _ _ _ _) =+    (passedSynth + passedSim + passedSynthStat) == 0+  where+    passedSynth = length $ filter (not . filterSynth) synth+    passedSim = length $ filter (not . filterSim) sim+    passedSynthStat = length $ filter (not . filterSynthStat) synthstat+ fuzzInDir-    :: MonadFuzz m => FilePath -> Gen SourceInfo -> Config -> Fuzz m FuzzReport-fuzzInDir fp src conf = do+    :: MonadFuzz m => Bool -> FilePath -> Gen SourceInfo -> Config -> Fuzz m FuzzReport+fuzzInDir k fp src conf = do     make fp     res <- pop fp $ fuzz src conf+    liftSh $ do+        writefile (fp <.> "html") $ printResultReport (bname fp) res+        when (passedFuzz res && not k) $ rm_rf fp     relativeFuzzReport res+  where+    bname = T.pack . takeBaseName . T.unpack . toTextIgnore  fuzzMultiple     :: MonadFuzz m     => Int+    -> Bool     -> Maybe FilePath     -> Gen SourceInfo     -> Config     -> Fuzz m [FuzzReport]-fuzzMultiple n fp src conf = do+fuzzMultiple n k fp src conf = do     x <- case fp of         Nothing -> do             ct <- liftIO getZonedTime@@ -441,7 +460,7 @@             results         return results   where-    fuzzDir' n' = fuzzInDir (fromText $ "fuzz_" <> showT n') src conf+    fuzzDir' n' = fuzzInDir k (fromText $ "fuzz_" <> showT n') src conf     seed = conf ^. configProperty . propSeed  sampleSeed :: MonadSh m => Maybe Seed -> Gen a -> m (Seed, a)
src/Verismith/Generate.hs view
@@ -445,13 +445,15 @@     context <- lget     outs    <- replicateM (length outP) (nextPort Wire)     ins <- take (length inpFixed) <$> Hog.shuffle (context ^. variables)+    insLit <- replicateM (length inpFixed - length ins) (Number <$> genBitVec)     mapM_ (uncurry process) . zip (ins ^.. traverse . portName) $ inpFixed ^.. traverse . portSize     ident <- makeIdentifier "modinst"     vs <- view variables <$> lget     Hog.choice-        [ return . ModInst i ident $ ModConn <$> toE (outs <> clkPort <> ins)+        [ return . ModInst i ident $ ModConn <$> (toE (outs <> clkPort <> ins) <> insLit)         , ModInst i ident <$> Hog.shuffle-            (zipWith ModConnNamed (view portName <$> outP <> clkPort <> inpFixed) (toE $ outs <> clkPort <> ins))+            (zipWith ModConnNamed (view portName <$> outP <> clkPort <> inpFixed)+             (toE (outs <> clkPort <> ins) <> insLit))         ]     where         toE ins = Id . view portName <$> ins
src/Verismith/Reduce.hs view
@@ -49,8 +49,8 @@ import           Shelly.Lifted            (MonadSh, liftSh) import           Verismith.Internal import           Verismith.Result-import           Verismith.Sim-import           Verismith.Sim.Internal+import           Verismith.Tool+import           Verismith.Tool.Internal import           Verismith.Verilog import           Verismith.Verilog.AST import           Verismith.Verilog.Mutate
src/Verismith/Report.hs view
@@ -63,8 +63,8 @@ import           Verismith.Config import           Verismith.Internal import           Verismith.Result-import           Verismith.Sim-import           Verismith.Sim.Internal+import           Verismith.Tool+import           Verismith.Tool.Internal  -- | Common type alias for synthesis results type UResult = Result Failed ()@@ -192,9 +192,9 @@ -- | The complete state that will be used during fuzzing, which contains the -- results from all the operations. data FuzzReport = FuzzReport { _fuzzDir      :: !FilePath-                             , _synthResults :: ![SynthResult]-                             , _simResults   :: ![SimResult]-                             , _synthStatus  :: ![SynthStatus]+                             , _synthResults :: ![SynthResult] -- ^ Results of the equivalence check.+                             , _simResults   :: ![SimResult]   -- ^ Results of the simulation.+                             , _synthStatus  :: ![SynthStatus] -- ^ Results of the synthesis step.                              , _fileLines    :: {-# UNPACK #-} !Int                              , _synthTime    :: !NominalDiffTime                              , _equivTime    :: !NominalDiffTime@@ -316,7 +316,7 @@         . ( H.a           ! A.href                 ( H.textValue-                $ toTextIgnore (dir </> fromText "index" <.> "html")+                $ toTextIgnore (dir <.> "html")                 )           )         $ H.toHtml name
− src/Verismith/Sim.hs 
@@ -1,51 +0,0 @@-{-|-Module      : Verismith.Sim-Description : Simulator implementations.-Copyright   : (c) 2019, Yann Herklotz Grave-License     : GPL-3-Maintainer  : yann [at] yannherklotz [dot] com-Stability   : experimental-Portability : POSIX--Simulator implementations.--}--module Verismith.Sim-    (-    -- * Simulators-    -- ** Icarus-      Icarus(..)-    , defaultIcarus-    -- * Synthesisers-    -- ** Yosys-    , Yosys(..)-    , defaultYosys-    -- ** Vivado-    , Vivado(..)-    , defaultVivado-    -- ** XST-    , XST(..)-    , defaultXST-    -- ** Quartus-    , Quartus(..)-    , defaultQuartus-    -- ** Identity-    , Identity(..)-    , defaultIdentity-    -- * Equivalence-    , runEquiv-    -- * Simulation-    , runSim-    -- * Synthesis-    , runSynth-    , logger-    )-where--import           Verismith.Sim.Icarus-import           Verismith.Sim.Identity-import           Verismith.Sim.Internal-import           Verismith.Sim.Quartus-import           Verismith.Sim.Vivado-import           Verismith.Sim.XST-import           Verismith.Sim.Yosys
− src/Verismith/Sim/Icarus.hs 
@@ -1,188 +0,0 @@-{-|-Module      : Verismith.Sim.Icarus-Description : Icarus verilog module.-Copyright   : (c) 2018-2019, Yann Herklotz-License     : BSD-3-Maintainer  : yann [at] yannherklotz [dot] com-Stability   : experimental-Portability : POSIX--Icarus verilog module.--}--module Verismith.Sim.Icarus-    ( Icarus(..)-    , defaultIcarus-    , runSimIc-    )-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.Sim.Internal-import           Verismith.Sim.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)--instance Show Icarus where-    show _ = "iverilog"--instance Tool Icarus where-  toText _ = "iverilog"--instance Simulator Icarus where-  runSim = runSimIcarus-  runSimWithFile = runSimIcarusWithFile--instance NFData Icarus where-    rnf = rwhnf--defaultIcarus :: Icarus-defaultIcarus = Icarus "iverilog" "vvp"--addDisplay :: [Statement] -> [Statement]-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-assignFunc inp bs =-    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--mask :: Text -> Text-mask = T.replace "x" "0"--callback :: ByteString -> Text -> ByteString-callback b t = b <> convert (mask t)--runSimIcarus :: Icarus -> SourceInfo -> [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 $ runSimWithFile sim "main.v" bss-    where m = rinfo ^. mainModule--runSimIcarusWithFile-    :: Icarus -> FilePath -> [ByteString] -> ResultSh ByteString-runSimIcarusWithFile sim f _ = annotate SimFail . 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"])--fromBytes :: ByteString -> Integer-fromBytes = B.foldl' f 0 where f a b = a `shiftL` 8 .|. fromIntegral b--runSimIc-    :: (Synthesiser b)-    => Icarus-    -> b-    -> SourceInfo-    -> [ByteString]-    -> ResultSh ByteString-runSimIc sim1 synth1 srcInfo bss = do-    dir <- liftSh pwd-    let top      = srcInfo ^. mainModule-    let inConcat = (RegConcat (Id . fromPort <$> (top ^. modInPorts)))-    let-        tb = instantiateMod top $ ModDecl-            "testbench"-            []-            []-            [ Initial-            $  fold-                   [ BlockAssign (Assign "clk" Nothing 0)-                   , BlockAssign (Assign inConcat Nothing 0)-                   ]-            <> fold-                   (   (\r -> TimeCtrl-                           10-                           (Just $ BlockAssign (Assign inConcat Nothing r))-                       )-                   .   fromInteger-                   .   fromBytes-                   <$> bss-                   )-            <> (SysTaskEnable $ Task "finish" [])-            , Always . TimeCtrl 5 . Just $ BlockAssign-                (Assign "clk" Nothing (UnOp UnNot (Id "clk")))-            , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable $ Task-                "strobe"-                ["%b", Id "y"]-            ]-            []--    liftSh . writefile "testbench.v" $ icarusTestbench (Verilog [tb]) synth1-    liftSh $ exe dir "icarus" "iverilog" ["-o", "main", "testbench.v"]-    liftSh-        $   B.take 8-        .   BA.convert-        .   (hash :: ByteString -> Digest SHA256)-        <$> logCommand-                dir-                "vvp"-                (runFoldLines (mempty :: ByteString)-                              callback-                              (vvpPath sim1)-                              ["main"]-                )-  where-    exe dir name e = void . errExit False . logCommand dir name . timeout e
− src/Verismith/Sim/Identity.hs 
@@ -1,51 +0,0 @@-{-|-Module      : Verismith.Sim.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.Sim.Identity-    ( 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.Sim.Internal-import           Verismith.Verilog.AST-import           Verismith.Verilog.CodeGen--data Identity = Identity { identityDesc   :: {-# UNPACK #-} !Text-                         , identityOutput :: {-# UNPACK #-} !FilePath-                         }-              deriving (Eq)--instance Tool Identity where-    toText (Identity d _) = d--instance Show Identity where-    show t = unpack $ toText t--instance Synthesiser Identity where-    runSynth = runSynthIdentity-    synthOutput = identityOutput-    setSynthOutput (Identity a _) = Identity a--instance NFData Identity where-    rnf = rwhnf--runSynthIdentity :: Identity -> SourceInfo -> ResultSh ()-runSynthIdentity (Identity _ out) = writefile out . genSource--defaultIdentity :: Identity-defaultIdentity = Identity "identity" "syn_identity.v"
− src/Verismith/Sim/Internal.hs 
@@ -1,215 +0,0 @@-{-|-Module      : Verismith.Sim.Internal-Description : Class of the simulator.-Copyright   : (c) 2018-2019, Yann Herklotz-License     : BSD-3-Maintainer  : yann [at] yannherklotz [dot] com-Stability   : experimental-Portability : POSIX--Class of the simulator and the synthesize tool.--}--{-# LANGUAGE DeriveFunctor #-}--module Verismith.Sim.Internal-    ( 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.Internal-import           Verismith.Result-import           Verismith.Verilog.AST---- | Tool class.-class Tool a where-  toText :: a -> Text---- | Simulation type class.-class Tool a => Simulator a where-  runSim :: a             -- ^ Simulator instance-         -> SourceInfo       -- ^ 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-            | EquivError-            | SimFail-            | SynthFail-            | TimeoutError-            deriving (Eq, Show)--instance Semigroup Failed where-    EmptyFail <> a = a-    b <> _ = b--instance Monoid Failed where-    mempty = EmptyFail---- | Synthesiser type class.-class Tool a => Synthesiser a where-    runSynth :: a        -- ^ Synthesiser tool instance-             -> SourceInfo  -- ^ Run information-             -> ResultSh ()    -- ^ does not return any values-    synthOutput :: a -> FilePath-    setSynthOutput :: a -> FilePath -> a--renameSource :: (Synthesiser a) => a -> SourceInfo -> SourceInfo-renameSource a src =-    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--- with also has those instances.-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'--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---- | 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 -> Sh [Text]-checkPresentModules fp (SourceInfo _ src) = do-    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]---- | 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--- should find all the instantiations and definitions. This could again be made--- much simpler if the parser works.-replaceMods :: FilePath -> Text -> SourceInfo -> Sh ()-replaceMods fp t (SourceInfo _ src) =-    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"--timeout :: FilePath -> [Text] -> Sh Text-timeout = command1 "timeout" ["300"] . toTextIgnore-{-# INLINE timeout #-}--timeout_ :: FilePath -> [Text] -> Sh ()-timeout_ = command1_ "timeout" ["300"] . toTextIgnore-{-# INLINE timeout_ #-}---- | Helper function to convert bytestrings to integers-bsToI :: ByteString -> Integer-bsToI = B.foldl' (\i b -> (i `shiftL` 8) + fromIntegral b) 0-{-# INLINE bsToI #-}--noPrint :: Sh a -> Sh a-noPrint = print_stdout False . print_stderr False-{-# INLINE noPrint #-}--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--logCommand :: FilePath -> Text -> Sh a -> Sh a-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"-    file s = T.unpack (toTextIgnore $ fp </> fromText name) <> s--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 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 ()-execute_ a b c d = void . execute a b c d
− src/Verismith/Sim/Quartus.hs 
@@ -1,77 +0,0 @@-{-|-Module      : Verismith.Sim.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.Sim.Quartus-    ( 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.Sim.Internal-import           Verismith.Verilog.AST-import           Verismith.Verilog.CodeGen--data Quartus = Quartus { quartusBin    :: !(Maybe FilePath)-                       , quartusDesc   :: {-# UNPACK #-} !Text-                       , quartusOutput :: {-# UNPACK #-} !FilePath-                       }-                deriving (Eq)--instance Tool Quartus where-    toText (Quartus _ t _) = t--instance Show Quartus where-    show t = unpack $ toText t--instance Synthesiser Quartus where-    runSynth = runSynthQuartus-    synthOutput = quartusOutput-    setSynthOutput (Quartus a b _) = Quartus a b--instance NFData Quartus where-    rnf = rwhnf--defaultQuartus :: Quartus-defaultQuartus = Quartus Nothing "quartus" "syn_quartus.v"--runSynthQuartus :: Quartus -> SourceInfo -> ResultSh ()-runSynthQuartus sim (SourceInfo top src) = do-    dir <- liftSh pwd-    let ex = execute_ SynthFail dir "quartus"-    liftSh . writefile inpf $ genSource src-    liftSh . noPrint $ run_-        "sed"-        [ "-i"-        , "s/^module/(* multstyle = \"logic\" *) module/;"-        , toTextIgnore inpf-        ]-    ex (exec "quartus_map")-       [top, "--source=" <> toTextIgnore inpf, "--family=Cyclone V"]-    ex (exec "quartus_fit") [top, "--part=5CGXFC7D6F31C6"]-    ex (exec "quartus_eda") [top, "--simulation", "--tool=vcs"]-    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
− src/Verismith/Sim/Template.hs 
@@ -1,133 +0,0 @@-{-|-Module      : Verismith.Sim.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.Sim.Template-    ( yosysSatConfig-    , yosysSimConfig-    , xstSynthConfig-    , vivadoSynthConfig-    , sbyConfig-    , icarusTestbench-    )-where--import           Control.Lens              ((^..))-import           Data.Text                 (Text)-import qualified Data.Text                 as T-import           Prelude                   hiding (FilePath)-import           Shelly-import           Text.Shakespeare.Text     (st)-import           Verismith.Sim.Internal-import           Verismith.Verilog.AST-import           Verismith.Verilog.CodeGen--rename :: Text -> [Text] -> Text-rename end entries =-    T.intercalate "\n"-        $   flip mappend end-        .   mappend "rename "-        .   doubleName-        <$> entries-{-# INLINE rename #-}--doubleName :: Text -> Text-doubleName n = n <> " " <> n-{-# INLINE doubleName #-}--outputText :: Synthesiser a => a -> Text-outputText = toTextIgnore . synthOutput---- brittany-disable-next-binding-yosysSatConfig :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> Text-yosysSatConfig sim1 sim2 (SourceInfo top src) = [st|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---- brittany-disable-next-binding-yosysSimConfig :: Text-yosysSimConfig = [st|read_verilog rtl.v; proc;;-rename mod mod_rtl-|]---- brittany-disable-next-binding-xstSynthConfig :: Text -> Text-xstSynthConfig top = [st|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"-|]---- brittany-disable-next-binding-vivadoSynthConfig :: Text -> Text -> Text-vivadoSynthConfig top outf = [st|-# 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}-|]---- brittany-disable-next-binding-sbyConfig :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> Text-sbyConfig sim1 sim2 (SourceInfo top _) = [st|[options]-multiclock on-mode prove--[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-        .   (fromText "data" </>)-        .   fromText-        <$> deps-    readL = T.intercalate "\n" $ mappend "read -formal " <$> deps--icarusTestbench :: (Synthesiser a) => Verilog -> a -> Text-icarusTestbench t synth1 = [st|-`include "data/cells_cmos.v"-`include "data/cells_cyclone_v.v"-`include "data/cells_verific.v"-`include "data/cells_xilinx_7.v"-`include "data/cells_yosys.v"-`include "#{toTextIgnore $ synthOutput synth1}"--#{genSource t}-|]
− src/Verismith/Sim/Vivado.hs 
@@ -1,71 +0,0 @@-{-|-Module      : Verismith.Sim.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.Sim.Vivado-    ( 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.Sim.Internal-import           Verismith.Sim.Template-import           Verismith.Verilog.AST-import           Verismith.Verilog.CodeGen--data Vivado = Vivado { vivadoBin    :: !(Maybe FilePath)-                     , vivadoDesc   :: {-# UNPACK #-} !Text-                     , vivadoOutput :: {-# UNPACK #-} !FilePath-                     }-               deriving (Eq)--instance Tool Vivado where-    toText (Vivado _ t _) = t--instance Show Vivado where-    show t = unpack $ toText t--instance Synthesiser Vivado where-    runSynth = runSynthVivado-    synthOutput = vivadoOutput-    setSynthOutput (Vivado a b _) = Vivado a b--instance NFData Vivado where-    rnf = rwhnf--defaultVivado :: Vivado-defaultVivado = Vivado Nothing "vivado" "syn_vivado.v"--runSynthVivado :: Vivado -> SourceInfo -> 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"
− src/Verismith/Sim/XST.hs 
@@ -1,85 +0,0 @@-{-|-Module      : Verismith.Sim.XST-Description : XST (ise) simulator implementation.-Copyright   : (c) 2018-2019, Yann Herklotz-License     : BSD-3-Maintainer  : yann [at] yannherklotz [dot] com-Stability   : experimental-Portability : POSIX--XST (ise) simulator implementation.--}--{-# LANGUAGE QuasiQuotes #-}--module Verismith.Sim.XST-    ( 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           Text.Shakespeare.Text     (st)-import           Verismith.Sim.Internal-import           Verismith.Sim.Template-import           Verismith.Verilog.AST-import           Verismith.Verilog.CodeGen--data XST = XST { xstBin    :: !(Maybe FilePath)-               , xstDesc   :: {-# UNPACK #-} !Text-               , xstOutput :: {-# UNPACK #-} !FilePath-               }-         deriving (Eq)--instance Tool XST where-    toText (XST _ t _) = t--instance Show XST where-    show t = unpack $ toText t--instance Synthesiser XST where-    runSynth = runSynthXST-    synthOutput = xstOutput-    setSynthOutput (XST a b _) = XST a b--instance NFData XST where-    rnf = rwhnf--defaultXST :: XST-defaultXST = XST Nothing "xst" "syn_xst.v"--runSynthXST :: XST -> SourceInfo -> 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 [st|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"-    prjFile = modFile <.> "prj"
− src/Verismith/Sim/Yosys.hs 
@@ -1,127 +0,0 @@-{-|-Module      : Verismith.Sim.Yosys-Description : Yosys simulator implementation.-Copyright   : (c) 2018-2019, Yann Herklotz-License     : BSD-3-Maintainer  : yann [at] yannherklotz [dot] com-Stability   : experimental-Portability : POSIX--Yosys simulator implementation.--}--{-# LANGUAGE QuasiQuotes #-}--module Verismith.Sim.Yosys-    ( Yosys(..)-    , defaultYosys-    , runEquiv-    , runEquivYosys-    )-where--import           Control.DeepSeq           (NFData, rnf, rwhnf)-import           Control.Lens-import           Control.Monad             (void)-import           Data.Text                 (Text, unpack)-import           Prelude                   hiding (FilePath)-import           Shelly-import           Shelly.Lifted             (liftSh)-import           Text.Shakespeare.Text     (st)-import           Verismith.Result-import           Verismith.Sim.Internal-import           Verismith.Sim.Template-import           Verismith.Verilog.AST-import           Verismith.Verilog.CodeGen-import           Verismith.Verilog.Mutate--data Yosys = Yosys { yosysBin    :: !(Maybe FilePath)-                   , yosysDesc   :: {-# UNPACK #-} !Text-                   , yosysOutput :: {-# UNPACK #-} !FilePath-                   }-              deriving (Eq)--instance Tool Yosys where-    toText (Yosys _ t _) = t--instance Show Yosys where-    show t = unpack $ toText t--instance Synthesiser Yosys where-  runSynth = runSynthYosys-  synthOutput = yosysOutput-  setSynthOutput (Yosys a b _) = Yosys a b--instance NFData Yosys where-    rnf = rwhnf--defaultYosys :: Yosys-defaultYosys = Yosys Nothing "yosys" "syn_yosys.v"--yosysPath :: Yosys -> FilePath-yosysPath sim = maybe (fromText "yosys") (</> fromText "yosys") $ yosysBin sim--runSynthYosys :: Yosys -> SourceInfo -> ResultSh ()-runSynthYosys sim (SourceInfo _ src) = do-    dir <- liftSh $ do-        dir' <- pwd-        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  = toTextIgnore inpf-    out  = toTextIgnore $ synthOutput sim--runEquivYosys-    :: (Synthesiser a, Synthesiser b)-    => Yosys-    -> a-    -> b-    -> SourceInfo-    -> ResultSh ()-runEquivYosys yosys sim1 sim2 srcInfo = do-    liftSh $ do-        writefile "top.v"-            .  genSource-            .  initMod-            .  makeTop 2-            $  srcInfo-            ^. mainModule-        writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo-    runSynth sim1 srcInfo-    runSynth sim2 srcInfo-    liftSh $ run_ (yosysPath yosys) [toTextIgnore checkFile]-    where checkFile = fromText [st|test.#{toText sim1}.#{toText sim2}.ys|]--runEquiv-    :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> ResultSh ()-runEquiv sim1 sim2 srcInfo = do-    dir <- liftSh pwd-    liftSh $ do-        writefile "top.v"-            .  genSource-            .  initMod-            .  makeTopAssert-            $  srcInfo-            ^. mainModule-        replaceMods (synthOutput sim1) "_1" srcInfo-        replaceMods (synthOutput sim2) "_2" srcInfo-        writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo-    e <- liftSh $ do-        exe dir "symbiyosys" "sby" ["-f", "proof.sby"]-        lastExitCode-    case e of-        0   -> ResultT . return $ Pass ()-        2   -> ResultT . return $ Fail EquivFail-        124 -> ResultT . return $ Fail TimeoutError-        _   -> ResultT . return $ Fail EquivError-  where-    exe dir name e = void . errExit False . logCommand dir name . timeout e
+ src/Verismith/Tool.hs view
@@ -0,0 +1,51 @@+{-|+Module      : Verismith.Tool+Description : Simulator implementations.+Copyright   : (c) 2019, Yann Herklotz Grave+License     : GPL-3+Maintainer  : yann [at] yannherklotz [dot] com+Stability   : experimental+Portability : POSIX++Simulator implementations.+-}++module Verismith.Tool+    (+    -- * Simulators+    -- ** Icarus+      Icarus(..)+    , defaultIcarus+    -- * Synthesisers+    -- ** Yosys+    , Yosys(..)+    , defaultYosys+    -- ** Vivado+    , Vivado(..)+    , defaultVivado+    -- ** XST+    , XST(..)+    , defaultXST+    -- ** Quartus+    , Quartus(..)+    , defaultQuartus+    -- ** Identity+    , Identity(..)+    , defaultIdentity+    -- * Equivalence+    , runEquiv+    -- * Simulation+    , runSim+    -- * Synthesis+    , runSynth+    , logger+    )+where++import           Verismith.Tool.Icarus+import           Verismith.Tool.Identity+import           Verismith.Tool.Internal+import           Verismith.Tool.Quartus+import           Verismith.Tool.Vivado+import           Verismith.Tool.XST+import           Verismith.Tool.Yosys
+ src/Verismith/Tool/Icarus.hs view
@@ -0,0 +1,188 @@+{-|+Module      : Verismith.Tool.Icarus+Description : Icarus verilog module.+Copyright   : (c) 2018-2019, Yann Herklotz+License     : BSD-3+Maintainer  : yann [at] yannherklotz [dot] com+Stability   : experimental+Portability : POSIX++Icarus verilog module.+-}++module Verismith.Tool.Icarus+    ( Icarus(..)+    , defaultIcarus+    , runSimIc+    )+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.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)++instance Show Icarus where+    show _ = "iverilog"++instance Tool Icarus where+  toText _ = "iverilog"++instance Simulator Icarus where+  runSim = runSimIcarus+  runSimWithFile = runSimIcarusWithFile++instance NFData Icarus where+    rnf = rwhnf++defaultIcarus :: Icarus+defaultIcarus = Icarus "iverilog" "vvp"++addDisplay :: [Statement] -> [Statement]+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+assignFunc inp bs =+    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++mask :: Text -> Text+mask = T.replace "x" "0"++callback :: ByteString -> Text -> ByteString+callback b t = b <> convert (mask t)++runSimIcarus :: Icarus -> SourceInfo -> [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 $ runSimWithFile sim "main.v" bss+    where m = rinfo ^. mainModule++runSimIcarusWithFile+    :: Icarus -> FilePath -> [ByteString] -> ResultSh ByteString+runSimIcarusWithFile sim f _ = annotate SimFail . 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"])++fromBytes :: ByteString -> Integer+fromBytes = B.foldl' f 0 where f a b = a `shiftL` 8 .|. fromIntegral b++runSimIc+    :: (Synthesiser b)+    => Icarus+    -> b+    -> SourceInfo+    -> [ByteString]+    -> ResultSh ByteString+runSimIc sim1 synth1 srcInfo bss = do+    dir <- liftSh pwd+    let top      = srcInfo ^. mainModule+    let inConcat = (RegConcat (Id . fromPort <$> (top ^. modInPorts)))+    let+        tb = instantiateMod top $ ModDecl+            "testbench"+            []+            []+            [ Initial+            $  fold+                   [ BlockAssign (Assign "clk" Nothing 0)+                   , BlockAssign (Assign inConcat Nothing 0)+                   ]+            <> fold+                   (   (\r -> TimeCtrl+                           10+                           (Just $ BlockAssign (Assign inConcat Nothing r))+                       )+                   .   fromInteger+                   .   fromBytes+                   <$> bss+                   )+            <> (SysTaskEnable $ Task "finish" [])+            , Always . TimeCtrl 5 . Just $ BlockAssign+                (Assign "clk" Nothing (UnOp UnNot (Id "clk")))+            , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable $ Task+                "strobe"+                ["%b", Id "y"]+            ]+            []++    liftSh . writefile "testbench.v" $ icarusTestbench (Verilog [tb]) synth1+    liftSh $ exe dir "icarus" "iverilog" ["-o", "main", "testbench.v"]+    liftSh+        $   B.take 8+        .   BA.convert+        .   (hash :: ByteString -> Digest SHA256)+        <$> logCommand+                dir+                "vvp"+                (runFoldLines (mempty :: ByteString)+                              callback+                              (vvpPath sim1)+                              ["main"]+                )+  where+    exe dir name e = void . errExit False . logCommand dir name . timeout e
+ src/Verismith/Tool/Identity.hs view
@@ -0,0 +1,51 @@+{-|+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+    )+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   :: {-# UNPACK #-} !Text+                         , identityOutput :: {-# UNPACK #-} !FilePath+                         }+              deriving (Eq)++instance Tool Identity where+    toText (Identity d _) = d++instance Show Identity where+    show t = unpack $ toText t++instance Synthesiser Identity where+    runSynth = runSynthIdentity+    synthOutput = identityOutput+    setSynthOutput (Identity a _) = Identity a++instance NFData Identity where+    rnf = rwhnf++runSynthIdentity :: Identity -> SourceInfo -> ResultSh ()+runSynthIdentity (Identity _ out) = writefile out . genSource++defaultIdentity :: Identity+defaultIdentity = Identity "identity" "syn_identity.v"
+ src/Verismith/Tool/Internal.hs view
@@ -0,0 +1,215 @@+{-|+Module      : Verismith.Tool.Internal+Description : Class of the simulator.+Copyright   : (c) 2018-2019, Yann Herklotz+License     : BSD-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+    ( 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.Internal+import           Verismith.Result+import           Verismith.Verilog.AST++-- | Tool class.+class Tool a where+  toText :: a -> Text++-- | Simulation type class.+class Tool a => Simulator a where+  runSim :: a             -- ^ Simulator instance+         -> SourceInfo       -- ^ 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+            | EquivError+            | SimFail+            | SynthFail+            | TimeoutError+            deriving (Eq, Show)++instance Semigroup Failed where+    EmptyFail <> a = a+    b <> _ = b++instance Monoid Failed where+    mempty = EmptyFail++-- | Synthesiser type class.+class Tool a => Synthesiser a where+    runSynth :: a        -- ^ Synthesiser tool instance+             -> SourceInfo  -- ^ Run information+             -> ResultSh ()    -- ^ does not return any values+    synthOutput :: a -> FilePath+    setSynthOutput :: a -> FilePath -> a++renameSource :: (Synthesiser a) => a -> SourceInfo -> SourceInfo+renameSource a src =+    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+-- with also has those instances.+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'++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++-- | 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 -> Sh [Text]+checkPresentModules fp (SourceInfo _ src) = do+    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]++-- | 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+-- should find all the instantiations and definitions. This could again be made+-- much simpler if the parser works.+replaceMods :: FilePath -> Text -> SourceInfo -> Sh ()+replaceMods fp t (SourceInfo _ src) =+    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"++timeout :: FilePath -> [Text] -> Sh Text+timeout = command1 "timeout" ["300"] . toTextIgnore+{-# INLINE timeout #-}++timeout_ :: FilePath -> [Text] -> Sh ()+timeout_ = command1_ "timeout" ["300"] . toTextIgnore+{-# INLINE timeout_ #-}++-- | Helper function to convert bytestrings to integers+bsToI :: ByteString -> Integer+bsToI = B.foldl' (\i b -> (i `shiftL` 8) + fromIntegral b) 0+{-# INLINE bsToI #-}++noPrint :: Sh a -> Sh a+noPrint = print_stdout False . print_stderr False+{-# INLINE noPrint #-}++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++logCommand :: FilePath -> Text -> Sh a -> Sh a+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"+    file s = T.unpack (toTextIgnore $ fp </> fromText name) <> s++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 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 ()+execute_ a b c d = void . execute a b c d
+ src/Verismith/Tool/Quartus.hs view
@@ -0,0 +1,77 @@+{-|+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+    )+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.Verilog.AST+import           Verismith.Verilog.CodeGen++data Quartus = Quartus { quartusBin    :: !(Maybe FilePath)+                       , quartusDesc   :: {-# UNPACK #-} !Text+                       , quartusOutput :: {-# UNPACK #-} !FilePath+                       }+                deriving (Eq)++instance Tool Quartus where+    toText (Quartus _ t _) = t++instance Show Quartus where+    show t = unpack $ toText t++instance Synthesiser Quartus where+    runSynth = runSynthQuartus+    synthOutput = quartusOutput+    setSynthOutput (Quartus a b _) = Quartus a b++instance NFData Quartus where+    rnf = rwhnf++defaultQuartus :: Quartus+defaultQuartus = Quartus Nothing "quartus" "syn_quartus.v"++runSynthQuartus :: Quartus -> SourceInfo -> ResultSh ()+runSynthQuartus sim (SourceInfo top src) = do+    dir <- liftSh pwd+    let ex = execute_ SynthFail dir "quartus"+    liftSh . writefile inpf $ genSource src+    liftSh . noPrint $ run_+        "sed"+        [ "-i"+        , "s/^module/(* multstyle = \"logic\" *) module/;"+        , toTextIgnore inpf+        ]+    ex (exec "quartus_map")+       [top, "--source=" <> toTextIgnore inpf, "--family=Cyclone V"]+    ex (exec "quartus_fit") [top, "--part=5CGXFC7D6F31C6"]+    ex (exec "quartus_eda") [top, "--simulation", "--tool=vcs"]+    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
+ src/Verismith/Tool/Template.hs view
@@ -0,0 +1,133 @@+{-|+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+    ( yosysSatConfig+    , yosysSimConfig+    , xstSynthConfig+    , vivadoSynthConfig+    , sbyConfig+    , icarusTestbench+    )+where++import           Control.Lens              ((^..))+import           Data.Text                 (Text)+import qualified Data.Text                 as T+import           Prelude                   hiding (FilePath)+import           Shelly+import           Text.Shakespeare.Text     (st)+import           Verismith.Tool.Internal+import           Verismith.Verilog.AST+import           Verismith.Verilog.CodeGen++rename :: Text -> [Text] -> Text+rename end entries =+    T.intercalate "\n"+        $   flip mappend end+        .   mappend "rename "+        .   doubleName+        <$> entries+{-# INLINE rename #-}++doubleName :: Text -> Text+doubleName n = n <> " " <> n+{-# INLINE doubleName #-}++outputText :: Synthesiser a => a -> Text+outputText = toTextIgnore . synthOutput++-- brittany-disable-next-binding+yosysSatConfig :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> Text+yosysSatConfig sim1 sim2 (SourceInfo top src) = [st|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++-- brittany-disable-next-binding+yosysSimConfig :: Text+yosysSimConfig = [st|read_verilog rtl.v; proc;;+rename mod mod_rtl+|]++-- brittany-disable-next-binding+xstSynthConfig :: Text -> Text+xstSynthConfig top = [st|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"+|]++-- brittany-disable-next-binding+vivadoSynthConfig :: Text -> Text -> Text+vivadoSynthConfig top outf = [st|+# 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}+|]++-- brittany-disable-next-binding+sbyConfig :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> Text+sbyConfig sim1 sim2 (SourceInfo top _) = [st|[options]+multiclock on+mode prove++[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+        .   (fromText "data" </>)+        .   fromText+        <$> deps+    readL = T.intercalate "\n" $ mappend "read -formal " <$> deps++icarusTestbench :: (Synthesiser a) => Verilog -> a -> Text+icarusTestbench t synth1 = [st|+`include "data/cells_cmos.v"+`include "data/cells_cyclone_v.v"+`include "data/cells_verific.v"+`include "data/cells_xilinx_7.v"+`include "data/cells_yosys.v"+`include "#{toTextIgnore $ synthOutput synth1}"++#{genSource t}+|]
+ src/Verismith/Tool/Vivado.hs view
@@ -0,0 +1,71 @@+{-|+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+    )+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++data Vivado = Vivado { vivadoBin    :: !(Maybe FilePath)+                     , vivadoDesc   :: {-# UNPACK #-} !Text+                     , vivadoOutput :: {-# UNPACK #-} !FilePath+                     }+               deriving (Eq)++instance Tool Vivado where+    toText (Vivado _ t _) = t++instance Show Vivado where+    show t = unpack $ toText t++instance Synthesiser Vivado where+    runSynth = runSynthVivado+    synthOutput = vivadoOutput+    setSynthOutput (Vivado a b _) = Vivado a b++instance NFData Vivado where+    rnf = rwhnf++defaultVivado :: Vivado+defaultVivado = Vivado Nothing "vivado" "syn_vivado.v"++runSynthVivado :: Vivado -> SourceInfo -> 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"
+ src/Verismith/Tool/XST.hs view
@@ -0,0 +1,85 @@+{-|+Module      : Verismith.Tool.XST+Description : XST (ise) simulator implementation.+Copyright   : (c) 2018-2019, Yann Herklotz+License     : BSD-3+Maintainer  : yann [at] yannherklotz [dot] com+Stability   : experimental+Portability : POSIX++XST (ise) simulator implementation.+-}++{-# LANGUAGE QuasiQuotes #-}++module Verismith.Tool.XST+    ( 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           Text.Shakespeare.Text     (st)+import           Verismith.Tool.Internal+import           Verismith.Tool.Template+import           Verismith.Verilog.AST+import           Verismith.Verilog.CodeGen++data XST = XST { xstBin    :: !(Maybe FilePath)+               , xstDesc   :: {-# UNPACK #-} !Text+               , xstOutput :: {-# UNPACK #-} !FilePath+               }+         deriving (Eq)++instance Tool XST where+    toText (XST _ t _) = t++instance Show XST where+    show t = unpack $ toText t++instance Synthesiser XST where+    runSynth = runSynthXST+    synthOutput = xstOutput+    setSynthOutput (XST a b _) = XST a b++instance NFData XST where+    rnf = rwhnf++defaultXST :: XST+defaultXST = XST Nothing "xst" "syn_xst.v"++runSynthXST :: XST -> SourceInfo -> 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 [st|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"+    prjFile = modFile <.> "prj"
+ src/Verismith/Tool/Yosys.hs view
@@ -0,0 +1,127 @@+{-|+Module      : Verismith.Tool.Yosys+Description : Yosys simulator implementation.+Copyright   : (c) 2018-2019, Yann Herklotz+License     : BSD-3+Maintainer  : yann [at] yannherklotz [dot] com+Stability   : experimental+Portability : POSIX++Yosys simulator implementation.+-}++{-# LANGUAGE QuasiQuotes #-}++module Verismith.Tool.Yosys+    ( Yosys(..)+    , defaultYosys+    , runEquiv+    , runEquivYosys+    )+where++import           Control.DeepSeq           (NFData, rnf, rwhnf)+import           Control.Lens+import           Control.Monad             (void)+import           Data.Text                 (Text, unpack)+import           Prelude                   hiding (FilePath)+import           Shelly+import           Shelly.Lifted             (liftSh)+import           Text.Shakespeare.Text     (st)+import           Verismith.Result+import           Verismith.Tool.Internal+import           Verismith.Tool.Template+import           Verismith.Verilog.AST+import           Verismith.Verilog.CodeGen+import           Verismith.Verilog.Mutate++data Yosys = Yosys { yosysBin    :: !(Maybe FilePath)+                   , yosysDesc   :: {-# UNPACK #-} !Text+                   , yosysOutput :: {-# UNPACK #-} !FilePath+                   }+              deriving (Eq)++instance Tool Yosys where+    toText (Yosys _ t _) = t++instance Show Yosys where+    show t = unpack $ toText t++instance Synthesiser Yosys where+  runSynth = runSynthYosys+  synthOutput = yosysOutput+  setSynthOutput (Yosys a b _) = Yosys a b++instance NFData Yosys where+    rnf = rwhnf++defaultYosys :: Yosys+defaultYosys = Yosys Nothing "yosys" "syn_yosys.v"++yosysPath :: Yosys -> FilePath+yosysPath sim = maybe (fromText "yosys") (</> fromText "yosys") $ yosysBin sim++runSynthYosys :: Yosys -> SourceInfo -> ResultSh ()+runSynthYosys sim (SourceInfo _ src) = do+    dir <- liftSh $ do+        dir' <- pwd+        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  = toTextIgnore inpf+    out  = toTextIgnore $ synthOutput sim++runEquivYosys+    :: (Synthesiser a, Synthesiser b)+    => Yosys+    -> a+    -> b+    -> SourceInfo+    -> ResultSh ()+runEquivYosys yosys sim1 sim2 srcInfo = do+    liftSh $ do+        writefile "top.v"+            .  genSource+            .  initMod+            .  makeTop 2+            $  srcInfo+            ^. mainModule+        writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo+    runSynth sim1 srcInfo+    runSynth sim2 srcInfo+    liftSh $ run_ (yosysPath yosys) [toTextIgnore checkFile]+    where checkFile = fromText [st|test.#{toText sim1}.#{toText sim2}.ys|]++runEquiv+    :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> ResultSh ()+runEquiv sim1 sim2 srcInfo = do+    dir <- liftSh pwd+    liftSh $ do+        writefile "top.v"+            .  genSource+            .  initMod+            .  makeTopAssert+            $  srcInfo+            ^. mainModule+        replaceMods (synthOutput sim1) "_1" srcInfo+        replaceMods (synthOutput sim2) "_2" srcInfo+        writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo+    e <- liftSh $ do+        exe dir "symbiyosys" "sby" ["-f", "proof.sby"]+        lastExitCode+    case e of+        0   -> ResultT . return $ Pass ()+        2   -> ResultT . return $ Fail EquivFail+        124 -> ResultT . return $ Fail TimeoutError+        _   -> ResultT . return $ Fail EquivError+  where+    exe dir name e = void . errExit False . logCommand dir name . timeout e
src/Verismith/Verilog/CodeGen.hs view
@@ -45,7 +45,7 @@  -- | Convert the 'Verilog' type to 'Text' so that it can be rendered. verilogSrc :: Verilog -> Doc a-verilogSrc (Verilog modules) = vsep . punctuate line $ moduleDecl <$> modules+verilogSrc (Verilog modules) = vsep . ("// -*- mode: verilog -*-" :) . punctuate line $ moduleDecl <$> modules  -- | Generate the 'ModDecl' for a module and convert it to 'Text'. moduleDecl :: ModDecl -> Doc a
verismith.cabal view
@@ -1,5 +1,5 @@ name: verismith-version: 0.4.0.0+version: 0.4.0.1 synopsis: Random verilog generation and simulator testing. description:   Verismith provides random verilog generation modules@@ -17,7 +17,6 @@                   , data/*.v                   , examples/*.v                   , examples/config.toml-                  , nix/*.nix                   , scripts/*.py                   , scripts/*.sh @@ -54,15 +53,15 @@                  , Verismith.Reduce                  , Verismith.Report                  , Verismith.Result-                 , Verismith.Sim-                 , Verismith.Sim.Icarus-                 , Verismith.Sim.Identity-                 , Verismith.Sim.Internal-                 , Verismith.Sim.Quartus-                 , Verismith.Sim.Template-                 , Verismith.Sim.Vivado-                 , Verismith.Sim.XST-                 , Verismith.Sim.Yosys+                 , Verismith.Tool+                 , Verismith.Tool.Icarus+                 , Verismith.Tool.Identity+                 , Verismith.Tool.Internal+                 , Verismith.Tool.Quartus+                 , Verismith.Tool.Template+                 , Verismith.Tool.Vivado+                 , Verismith.Tool.XST+                 , Verismith.Tool.Yosys                  , Verismith.Verilog                  , Verismith.Verilog.AST                  , Verismith.Verilog.BitVec