diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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: diff --git a/scripts/filter_icarus.sh b/scripts/filter_icarus.sh new file mode 100644 --- /dev/null +++ b/scripts/filter_icarus.sh @@ -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 diff --git a/src/Verismith.hs b/src/Verismith.hs --- a/src/Verismith.hs +++ b/src/Verismith.hs @@ -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 diff --git a/src/Verismith/Fuzz.hs b/src/Verismith/Fuzz.hs --- a/src/Verismith/Fuzz.hs +++ b/src/Verismith/Fuzz.hs @@ -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) diff --git a/src/Verismith/OptParser.hs b/src/Verismith/OptParser.hs --- a/src/Verismith/OptParser.hs +++ b/src/Verismith/OptParser.hs @@ -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 = diff --git a/src/Verismith/Reduce.hs b/src/Verismith/Reduce.hs --- a/src/Verismith/Reduce.hs +++ b/src/Verismith/Reduce.hs @@ -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 diff --git a/src/Verismith/Tool/Internal.hs b/src/Verismith/Tool/Internal.hs --- a/src/Verismith/Tool/Internal.hs +++ b/src/Verismith/Tool/Internal.hs @@ -75,7 +75,7 @@ -> ResultSh ByteString data Failed = EmptyFail - | EquivFail CounterEg + | EquivFail (Maybe CounterEg) | EquivError | SimFail ByteString | SynthFail diff --git a/src/Verismith/Tool/QuartusLight.hs b/src/Verismith/Tool/QuartusLight.hs --- a/src/Verismith/Tool/QuartusLight.hs +++ b/src/Verismith/Tool/QuartusLight.hs @@ -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") diff --git a/src/Verismith/Tool/Template.hs b/src/Verismith/Tool/Template.hs --- a/src/Verismith/Tool/Template.hs +++ b/src/Verismith/Tool/Template.hs @@ -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 diff --git a/src/Verismith/Tool/Yosys.hs b/src/Verismith/Tool/Yosys.hs --- a/src/Verismith/Tool/Yosys.hs +++ b/src/Verismith/Tool/Yosys.hs @@ -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 diff --git a/verismith.cabal b/verismith.cabal --- a/verismith.cabal +++ b/verismith.cabal @@ -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: