verismith 0.5.0.1 → 0.6.0.0

raw patch · 11 files changed

+77/−31 lines, 11 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• README.md +11/−0
• scripts/filter_icarus.sh +15/−0
• src/Verismith.hs +6/−6
• src/Verismith/Fuzz.hs +20/−9
• src/Verismith/OptParser.hs +5/−0
• src/Verismith/Reduce.hs +4/−3
• src/Verismith/Tool/Internal.hs +1/−1
• src/Verismith/Tool/QuartusLight.hs +2/−2
• src/Verismith/Tool/Template.hs +4/−3
• src/Verismith/Tool/Yosys.hs +7/−5
• verismith.cabal +2/−2

@@ -35,6 +35,7 @@  | Type          | Issue                                                      | Confirmed | Fixed | |---------------|------------------------------------------------------------|-----------|-------|+| Mis-synthesis | [Issue 1531](https://github.com/YosysHQ/yosys/issues/1531) | ✓         | ✓     | | Mis-synthesis | [Issue 1243](https://github.com/YosysHQ/yosys/issues/1243) | ✓         | ✓     | | Mis-synthesis | [Issue 1047](https://github.com/YosysHQ/yosys/issues/1047) | ✓         | ✓     | | Mis-synthesis | [Issue 997](https://github.com/YosysHQ/yosys/issues/997)   | ✓         | ✓     |@@ -74,6 +75,16 @@ Instead, stack could be used and the `stack.yaml` file could contain the overrides that are used by nix.  ### Build from hackage++Some external packages are required to use Verismith properly:++- [Yosys](https://github.com/yosyshq/yosys) with ABC+- [SymbiYosys](https://github.com/YosysHQ/SymbiYosys)+- [Icarus Verilog](http://iverilog.icarus.com/)+- (Optional) [Z3](https://github.com/Z3Prover/z3)+- (Optional) [Xst](https://www.xilinx.com/support/documentation/sw_manuals/xilinx11/ise_c_using_xst_for_synthesis.htm)+- (Optional) [Vivado](https://www.xilinx.com/products/design-tools/ise-design-suite.html)+- (Optional) [Quartus](https://www.intel.com/content/www/us/en/programmable/downloads/download-center.html)  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: 

@@ -0,0 +1,15 @@+#!/usr/bin/env bash++base=$(dirname $1)++current1=$(find ${base} -maxdepth 1 -mindepth 1 -name 'reduce_sim_yosys_0_8.v')+current2=$(find ${base} -maxdepth 1 -mindepth 1 -name 'reduce_sim_yosys_0_9.v')+current3=$(find ${base} -maxdepth 1 -mindepth 1 -name 'reduce_sim_yosys_master.v')+current4=$(find ${base} -maxdepth 1 -mindepth 1 -name 'reduce_equiv_yosys_master.v')+current5=$(find ${base} -maxdepth 1 -mindepth 1 -name 'reduce_equiv_yosys_0_8.v')+current6=$(find ${base} -maxdepth 1 -mindepth 1 -name 'reduce_equiv_yosys_0_9.v')++if [[ $current1 != "" ]] && [[ $current2 != "" ]] && [[ $current3 != "" ]] &&+   [[ $current4 = "" ]] && [[ $current4 = "" ]] && [[ $current5 = "" ]]; then+  echo $base+fi

@@ -144,13 +144,13 @@     ce = config ^. configProbability . probExpr  handleOpts :: Opts -> IO ()-handleOpts (Fuzz o configF f k n nosim noequiv noreduction file top cc) = do+handleOpts (Fuzz o configF f k n nosim noequiv noreduction file top cc checker) = do     config <- getConfig configF     gen <- getGenerator config top file     datadir <- getDataDir     _      <- runFuzz         (FuzzOpts (Just $ fromText o)-         f k n nosim noequiv noreduction config (toFP datadir) cc)+         f k n nosim noequiv noreduction config (toFP datadir) cc checker)         defaultYosys         (fuzzMultiple gen)     return ()@@ -183,7 +183,7 @@             shelly $ do                 make dir                 pop dir $ do-                    src' <- reduceSynth (toFP datadir) a b src+                    src' <- reduceSynth Nothing (toFP datadir) a b src                     writefile (fromText ".." </> dir <.> "v") $ genSource src'         a : _ -> do             putStrLn "Reduce with synthesis failure"@@ -207,7 +207,7 @@                 pop dir $ do                     runSynth a src                     runSynth b src-                    runEquiv (toFP datadir) a b src+                    runEquiv Nothing (toFP datadir) a b src             case res of                 Pass _             -> putStrLn "Equivalence check passed"                 Fail (EquivFail _) -> putStrLn "Equivalence check failed"@@ -288,7 +288,7 @@     setenv "VERISMITH_ROOT" curr     cd (fromText dir)     catch_sh-        ((runResultT $ runEquiv (toFP datadir) defaultYosys defaultVivado src) >> return True)+        ((runResultT $ runEquiv Nothing (toFP datadir) defaultYosys defaultVivado src) >> return True)         ((\_ -> return False) :: RunFailed -> Sh Bool)  -- | Run a fuzz run and check if all of the simulators passed by checking if the@@ -314,7 +314,7 @@         _ <-             catch_sh                     (  runResultT-                    $  runEquiv (toFP datadir) defaultYosys defaultVivado srcInfo+                    $  runEquiv Nothing (toFP datadir) defaultYosys defaultVivado srcInfo                     >> liftSh (logger "Test OK")                     )                 $ onFailure n

@@ -75,6 +75,7 @@                          , _fuzzOptsConfig      :: {-# UNPACK #-} !Config                          , _fuzzDataDir         :: {-# UNPACK #-} !FilePath                          , _fuzzOptsCrossCheck  :: !Bool+                         , _fuzzOptsChecker     :: !(Maybe Text)                          }               deriving (Show, Eq) @@ -91,6 +92,7 @@                            , _fuzzOptsConfig      = defaultConfig                            , _fuzzDataDir = fromText "."                            , _fuzzOptsCrossCheck = False+                           , _fuzzOptsChecker = Nothing                            }  data FuzzEnv = FuzzEnv { _getSynthesisers :: ![SynthTool]@@ -269,17 +271,18 @@ equivalence src = do     doCrossCheck <- fmap _fuzzOptsCrossCheck askOpts     datadir <- fmap _fuzzDataDir askOpts+    checker <- fmap _fuzzOptsChecker askOpts     synth <- passedSynthesis     let synthComb =             if doCrossCheck             then nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth             else nubBy tupEq . filter (uncurry (/=)) $ (,) defaultIdentitySynth <$> synth-    resTimes <- liftSh $ mapM (uncurry (equiv datadir)) synthComb+    resTimes <- liftSh $ mapM (uncurry (equiv checker datadir)) synthComb     fuzzSynthResults .= toSynthResult synthComb resTimes     liftSh $ inspect resTimes   where     tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a')-    equiv datadir a b =+    equiv checker datadir a b =         toolRun ("equivalence check for " <> toText a <> " and " <> toText b)             . runResultT             $ do make dir@@ -294,7 +297,7 @@                               </> synthOutput b                             ) $ synthOutput b                          writefile "rtl.v" $ genSource src-                     runEquiv datadir a b src+                     runEquiv checker datadir a b src         where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b  simulation :: (MonadIO m, MonadSh m) => SourceInfo -> Fuzz m ()@@ -321,7 +324,8 @@                 writefile "rtl.v" $ genSource src             runSimIc datadir defaultIcarus a src b i         where dir = fromText $ "simulation_" <> toText a-    simCounterEg datadir (a, b) = toolRun ("counter-example simulation for " <> toText a) . runResultT $ do+    simCounterEg datadir (a, Nothing) = toolRun ("counter-example simulation for " <> toText a) . return $ Fail EmptyFail+    simCounterEg datadir (a, Just b) = toolRun ("counter-example simulation for " <> toText a) . runResultT $ do         make dir         pop dir $ do             liftSh $ do@@ -351,7 +355,7 @@     withIdentity (SynthResult _ (IdentitySynth _) (Fail (EquivFail _)) _) = True     withIdentity _                                                    = False -failEquivWithIdentityCE :: (MonadSh m) => Fuzz m [(SynthTool, CounterEg)]+failEquivWithIdentityCE :: (MonadSh m) => Fuzz m [(SynthTool, Maybe CounterEg)] failEquivWithIdentityCE = catMaybes . fmap withIdentity . _fuzzSynthResults <$> get   where     withIdentity (SynthResult (IdentitySynth _) s (Fail (EquivFail c)) _) = Just (s, c)@@ -374,17 +378,24 @@ reduction :: (MonadSh m) => SourceInfo -> Fuzz m () reduction src = do     datadir <- fmap _fuzzDataDir askOpts+    checker <- fmap _fuzzOptsChecker askOpts     fails      <- failEquivWithIdentity     synthFails <- failedSynthesis     simFails <- failedSimulations-    _          <- liftSh $ mapM (red datadir) fails+    _          <- liftSh $ mapM (red checker datadir) fails     _          <- liftSh $ mapM redSynth synthFails     _ <- liftSh $ mapM (redSim datadir) simFails     return ()   where-    red datadir (SynthResult a b _ _) = reduceSynth datadir a b src-    redSynth a = reduceSynthesis a src-    redSim datadir (SimResult t _ bs _ _) = reduceSimIc datadir bs t src+    red checker datadir (SynthResult a b _ _) = do+        r <- reduceSynth checker datadir a b src+        writefile (fromText $ "reduce_" <> toText a <> "_" <> toText b <> ".v") $ genSource r+    redSynth a = do+        r <- reduceSynthesis a src+        writefile (fromText $ "reduce_" <> toText a <> ".v") $ genSource r+    redSim datadir (SimResult t _ bs _ _) = do+        r <- reduceSimIc datadir bs t src+        writefile (fromText $ "reduce_sim_" <> toText t <> ".v") $ genSource r  titleRun     :: (MonadIO m, MonadSh m) => Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a)

@@ -35,6 +35,7 @@                  , fuzzExistingFile    :: !(Maybe FilePath)                  , fuzzExistingFileTop :: !Text                  , fuzzCrossCheck      :: !Bool+                 , fuzzChecker         :: !(Maybe Text)                  }           | Generate { generateFilename   :: !(Maybe FilePath)                      , generateConfigFile :: !(Maybe FilePath)@@ -131,6 +132,10 @@                 <> Opt.value "top")         <*> (Opt.switch $ Opt.long "crosscheck" <> Opt.help                 "Do not only compare against the original design, but also against other netlists.")+        <*> (Opt.optional . textOption $+                Opt.long "checker"+                <> Opt.metavar "CHECKER"+                <> Opt.help "Define the checker to use.")  genOpts :: Parser Opts genOpts =

@@ -607,18 +607,19 @@ -- | Reduce a 'SourceInfo' using two 'Synthesiser' that are passed to it. reduceSynth     :: (Synthesiser a, Synthesiser b, MonadSh m)-    => Shelly.FilePath+    => Maybe Text+    -> Shelly.FilePath     -> a     -> b     -> SourceInfo     -> m SourceInfo-reduceSynth datadir a b = reduce (fromText $ "reduce_" <> toText a <> "_" <> toText b <> ".v") synth+reduceSynth mt datadir a b = reduce (fromText $ "reduce_" <> toText a <> "_" <> toText b <> ".v") synth   where     synth src' = liftSh $ do         r <- runResultT $ do             runSynth a src'             runSynth b src'-            runEquiv datadir a b src'+            runEquiv mt datadir a b src'         return $ case r of             Fail (EquivFail _) -> True             _                  -> False

@@ -75,7 +75,7 @@                  -> ResultSh ByteString  data Failed = EmptyFail-            | EquivFail CounterEg+            | EquivFail (Maybe CounterEg)             | EquivError             | SimFail ByteString             | SynthFail

@@ -59,8 +59,8 @@                              , "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+        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")

@@ -26,6 +26,7 @@ where  import           Control.Lens              ((^..))+import           Data.Maybe                (fromMaybe) import           Data.Text                 (Text) import qualified Data.Text                 as T import           Prelude                   hiding (FilePath)@@ -136,11 +137,11 @@ write_verilog -force #{outf} |] -sbyConfig :: (Synthesiser a, Synthesiser b) => FilePath -> a -> b -> SourceInfo -> Text-sbyConfig datadir sim1 sim2 (SourceInfo top _) = [st|[options]+sbyConfig :: (Synthesiser a, Synthesiser b) => Maybe Text -> FilePath -> a -> b -> SourceInfo -> Text+sbyConfig mt datadir sim1 sim2 (SourceInfo top _) = [st|[options] multiclock on mode prove-aigsmt z3+aigsmt #{fromMaybe "none" mt}  [engines] abc pdr

@@ -105,8 +105,8 @@     where checkFile = S.fromText [st|test.#{toText sim1}.#{toText sim2}.ys|]  runEquiv-    :: (Synthesiser a, Synthesiser b) => FilePath -> a -> b -> SourceInfo -> ResultSh ()-runEquiv datadir sim1 sim2 srcInfo = do+    :: (Synthesiser a, Synthesiser b) => Maybe Text -> FilePath -> a -> b -> SourceInfo -> ResultSh ()+runEquiv mt datadir sim1 sim2 srcInfo = do     dir <- liftSh S.pwd     liftSh $ do         S.writefile "top.v"@@ -117,14 +117,16 @@             ^. mainModule         replaceMods (synthOutput sim1) "_1" srcInfo         replaceMods (synthOutput sim2) "_2" srcInfo-        S.writefile "proof.sby" $ sbyConfig datadir sim1 sim2 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   -> ResultT $ Fail . EquivFail . fromRight mempty-                       . parseCounterEg <$> readfile "proof/engine_0/trace.smtc"+        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

@@ -1,5 +1,5 @@ name: verismith-version: 0.5.0.1+version: 0.6.0.0 synopsis: Random verilog generation and simulator testing. description:   Verismith provides random verilog generation modules@@ -27,7 +27,7 @@ source-repository this   type:     git   location: https://github.com/ymherklotz/verismith-  tag:      v0.5.0.1+  tag:      v0.6.0.0  custom-setup   setup-depends: