From 72ca7b273a8adf421d481e0caa97caa8a565187a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 18 Apr 2019 23:42:48 +0100 Subject: Add output information to Type --- .gitignore | 2 - src/VeriFuzz/Fuzz.hs | 103 +++++++++++++++++++++++++------------------ src/VeriFuzz/Sim/Internal.hs | 1 - src/VeriFuzz/Sim/Quartus.hs | 10 ++--- src/VeriFuzz/Sim/Template.hs | 18 ++++---- src/VeriFuzz/Sim/Vivado.hs | 10 ++--- src/VeriFuzz/Sim/XST.hs | 12 ++--- src/VeriFuzz/Sim/Yosys.hs | 21 +++++---- 8 files changed, 95 insertions(+), 82 deletions(-) diff --git a/.gitignore b/.gitignore index 4608789..615416c 100644 --- a/.gitignore +++ b/.gitignore @@ -4,6 +4,4 @@ TAGS # Folders .stack-work .shelly -equiv* -output* failed \ No newline at end of file diff --git a/src/VeriFuzz/Fuzz.hs b/src/VeriFuzz/Fuzz.hs index 084caee..5372d94 100644 --- a/src/VeriFuzz/Fuzz.hs +++ b/src/VeriFuzz/Fuzz.hs @@ -50,6 +50,7 @@ import VeriFuzz.Sim.Vivado import VeriFuzz.Sim.XST import VeriFuzz.Sim.Yosys import VeriFuzz.Verilog.AST +import VeriFuzz.Verilog.CodeGen -- | Common type alias for synthesis results type UResult = Result Failed () @@ -171,11 +172,16 @@ instance Monoid FuzzResult where -- read from and the current state of all the results. type Fuzz m = StateT FuzzResult (ReaderT FuzzEnv m) -runFuzz :: (Monad m) => [SynthTool] -> [SimTool] -> Yosys -> Fuzz m b -> m b -runFuzz synth sim yos m = +runFuzz + :: MonadIO m => + [SynthTool] -> [SimTool] -> Yosys -> Fuzz Sh a -> m a +runFuzz synth sim yos m = shelly $ runFuzz' synth sim yos m + +runFuzz' :: Monad m => [SynthTool] -> [SimTool] -> Yosys -> Fuzz m b -> m b +runFuzz' synth sim yos m = runReaderT (evalStateT m (FuzzResult [] [] [])) (FuzzEnv synth sim yos) -synthesisers :: (Monad m) => Fuzz m [SynthTool] +synthesisers :: Monad m => Fuzz m [SynthTool] synthesisers = lift $ asks getSynthesisers --simulators :: (Monad m) => Fuzz () m [SimTool] @@ -184,71 +190,80 @@ synthesisers = lift $ asks getSynthesisers combinations :: [a] -> [b] -> [(a, b)] combinations l1 l2 = [ (x, y) | x <- l1, y <- l2 ] -runInTmp :: (MonadSh m) => m a -> m a -runInTmp a = liftSh (withTmpDir $ (\dir -> cd dir)) >> a - -mkAndRun :: (MonadSh m) => FilePath -> Sh a -> m a -mkAndRun a = liftSh . chdir_p a - -liftWith' - :: (MonadIO m) - => (Sh (Result a b) -> Sh (Result a b)) - -> ResultT a Sh b - -> m (Result a b) -liftWith' a = liftIO . shellyFailDir . a . runResultT - ---lift' :: (MonadIO m) => ResultT a Sh b -> m (Result a b) ---lift' = liftWith' id - -logT :: (MonadIO m) => Text -> m () -logT = liftIO . shelly . echoP +logT :: MonadSh m => Text -> m () +logT = liftSh . echoP -timeit :: (MonadIO m) => m a -> m (NominalDiffTime, a) +timeit :: (MonadIO m, MonadSh m) => m a -> m (NominalDiffTime, a) timeit a = do start <- liftIO getCurrentTime result <- a end <- liftIO getCurrentTime return (diffUTCTime end start, result) -synthesis :: (MonadIO m) => SourceInfo -> Fuzz m () +synthesis :: MonadSh m => SourceInfo -> Fuzz m () synthesis src = do synth <- synthesisers - results <- mapM - (\a -> liftWith' (mkAndRun . fromText $ showT a) - $ runSynth a src (fromText $ "syn_" <> showT a <> ".v") - ) - synth + results <- liftSh $ mapM exec synth synthStatus .= zipWith SynthStatus synth results - liftIO $ print results + liftSh $ inspect results + where + exec a = runResultT $ do + liftSh . mkdir_p . fromText $ toText a + pop (fromText $ toText a) $ runSynth a src -generateSample :: (MonadIO m) => Gen SourceInfo -> Fuzz m SourceInfo +generateSample :: (MonadIO m, MonadSh m) => Gen SourceInfo -> Fuzz m SourceInfo generateSample gen = do logT "Sampling Verilog from generator" (t, src) <- timeit $ Hog.sample gen logT $ "Generated Verilog (" <> showT t <> ")" return src -passedSynthesis :: (MonadIO m) => Fuzz m [SynthTool] +passedSynthesis :: MonadSh m => Fuzz m [SynthTool] passedSynthesis = fmap toSynth . filter passed . _synthStatus <$> get where passed (SynthStatus _ (Pass _)) = True + passed _ = False toSynth (SynthStatus s _) = s -fuzz :: (MonadIO m) => Gen SourceInfo -> Fuzz m FuzzResult -fuzz gen = do +make :: MonadSh m => FilePath -> m () +make f = liftSh $ do + mkdir_p f + cp_r "data" $ f fromText "data" + +pop :: MonadSh m => FilePath -> m a -> m a +pop f a = do + dir <- liftSh pwd + liftSh $ cd f + ret <- a + liftSh $ cd dir + return ret + +equivalence :: MonadSh m => SourceInfo -> Fuzz m () +equivalence src = do yos <- lift $ asks yosysInstance - src <- generateSample gen - synthesis src synth <- passedSynthesis let synthComb = nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth - results <- mapM (uncurry $ equivalence yos src) synthComb - liftIO $ print results + results <- liftSh $ mapM (uncurry $ equiv yos) synthComb + liftSh $ inspect results + where + tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a') + equiv yos a 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 yos a (Just b) src + where + dir = fromText $ "equiv_" <> toText a <> "_" <> toText b + +fuzz :: (MonadIO m, MonadSh m) => Gen SourceInfo -> Fuzz m FuzzResult +fuzz gen = do + make "output" + pop "output" $ do + src <- generateSample gen + synthesis src + equivalence src return mempty - where - tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a') - equivalence yos src a b = - liftIO . shellyFailDir . runInTmp . runResultT $ runEquiv yos - a - (Just b) - src diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs index 2d06819..6e02482 100644 --- a/src/VeriFuzz/Sim/Internal.hs +++ b/src/VeriFuzz/Sim/Internal.hs @@ -80,7 +80,6 @@ instance Monoid Failed where class Tool a => Synthesiser a where runSynth :: a -- ^ Synthesiser tool instance -> SourceInfo -- ^ Run information - -> FilePath -- ^ Output verilog file for the module -> ResultSh () -- ^ does not return any values synthOutput :: a -> FilePath setSynthOutput :: a -> FilePath -> a diff --git a/src/VeriFuzz/Sim/Quartus.hs b/src/VeriFuzz/Sim/Quartus.hs index beb7f10..5bda0be 100644 --- a/src/VeriFuzz/Sim/Quartus.hs +++ b/src/VeriFuzz/Sim/Quartus.hs @@ -37,13 +37,13 @@ instance Tool Quartus where instance Synthesiser Quartus where runSynth = runSynthQuartus synthOutput = quartusOutput - setSynthOutput (Quartus a _) f = Quartus a f + setSynthOutput (Quartus a _) = Quartus a defaultQuartus :: Quartus -defaultQuartus = Quartus Nothing "quartus/syn_quartus.v" +defaultQuartus = Quartus Nothing "syn_quartus.v" -runSynthQuartus :: Quartus -> SourceInfo -> FilePath -> ResultSh () -runSynthQuartus sim (SourceInfo top src) outf = do +runSynthQuartus :: Quartus -> SourceInfo -> ResultSh () +runSynthQuartus sim (SourceInfo top src) = do dir <- liftSh pwd let ex = execute_ SynthFail dir "quartus" liftSh $ do @@ -54,7 +54,7 @@ runSynthQuartus sim (SourceInfo top src) outf = do ex (exec "quartus_fit") [top, "--part=5CGXFC7D6F31C6"] ex (exec "quartus_eda") [top, "--simulation", "--tool=vcs"] liftSh $ do - cp (fromText "simulation/vcs" fromText top <.> "vo") outf + cp (fromText "simulation/vcs" fromText top <.> "vo") $ synthOutput sim echoP "Quartus synthesis done" where inpf = "rtl.v" diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs index f630ea6..93f24a3 100644 --- a/src/VeriFuzz/Sim/Template.hs +++ b/src/VeriFuzz/Sim/Template.hs @@ -43,16 +43,18 @@ doubleName :: Text -> Text doubleName n = n <> " " <> n {-# INLINE doubleName #-} +outputText :: Synthesiser a => a -> Text +outputText = toTextIgnore . synthOutput + -- brittany-disable-next-binding -yosysSatConfig :: (Tool a, Tool b) => a -> Maybe b -> SourceInfo -> Text -yosysSatConfig sim1 sim2 (SourceInfo top src) = [st|read_verilog syn_#{toText sim1}.v +yosysSatConfig :: (Synthesiser a, Synthesiser b) => a -> Maybe b -> SourceInfo -> Text +yosysSatConfig sim1 sim2 (SourceInfo top src) = [st|read_verilog #{outputText sim1} #{rename "_1" mis} read_verilog syn_#{idSim2}.v #{rename "_2" mis} read_verilog #{top}.v proc; opt_clean flatten #{top} -! touch test.#{toText sim1}.#{idSim2}.input_ok sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{top} |] where @@ -86,7 +88,7 @@ write_verilog -force #{outf} |] -- brittany-disable-next-binding -sbyConfig :: (Tool a, Tool b) => FilePath -> a -> Maybe b -> SourceInfo -> Text +sbyConfig :: (Synthesiser a, Synthesiser b) => FilePath -> a -> Maybe b -> SourceInfo -> Text sbyConfig bd sim1 sim2 (SourceInfo top src) = [st|[options] mode prove @@ -95,17 +97,17 @@ smtbmc z3 [script] #{readL} -read -formal syn_#{toText sim1}.v +read -formal #{outputText sim1} #{rename "_1" mis} -read -formal syn_#{maybe "rtl" toText sim2}.v +read -formal #{maybe "rtl.v" outputText sim2} #{rename "_2" mis} read -formal top.v prep -top #{top} [files] #{depList} -syn_#{maybe "rtl" toText sim2}.v -syn_#{toText sim1}.v +#{maybe "rtl.v" outputText sim2} +#{outputText sim1} top.v |] where diff --git a/src/VeriFuzz/Sim/Vivado.hs b/src/VeriFuzz/Sim/Vivado.hs index 7cf6d4b..d213a12 100644 --- a/src/VeriFuzz/Sim/Vivado.hs +++ b/src/VeriFuzz/Sim/Vivado.hs @@ -38,16 +38,16 @@ instance Tool Vivado where instance Synthesiser Vivado where runSynth = runSynthVivado synthOutput = vivadoOutput - setSynthOutput (Vivado a _) f = Vivado a f + setSynthOutput (Vivado a _) = Vivado a defaultVivado :: Vivado -defaultVivado = Vivado "vivado" "vivado/syn_vivado.v" +defaultVivado = Vivado "vivado" "syn_vivado.v" -runSynthVivado :: Vivado -> SourceInfo -> FilePath -> ResultSh () -runSynthVivado sim (SourceInfo top src) outf = do +runSynthVivado :: Vivado -> SourceInfo -> ResultSh () +runSynthVivado sim (SourceInfo top src) = do dir <- liftSh pwd liftSh $ do - writefile vivadoTcl . vivadoSynthConfig top $ toTextIgnore outf + writefile vivadoTcl . vivadoSynthConfig top . toTextIgnore $ synthOutput sim writefile "rtl.v" $ genSource src run_ "sed" ["s/^module/(* use_dsp48=\"no\" *) module/;", "-i", "rtl.v"] echoP "Vivado: run" diff --git a/src/VeriFuzz/Sim/XST.hs b/src/VeriFuzz/Sim/XST.hs index b5b1b8b..e5e3e06 100644 --- a/src/VeriFuzz/Sim/XST.hs +++ b/src/VeriFuzz/Sim/XST.hs @@ -42,13 +42,13 @@ instance Tool XST where instance Synthesiser XST where runSynth = runSynthXST synthOutput = xstOutput - setSynthOutput (XST a b _) f = XST a b f + setSynthOutput (XST a b _) = XST a b defaultXST :: XST -defaultXST = XST "xst" "netgen" "xst/syn_xst.v" +defaultXST = XST "xst" "netgen" "syn_xst.v" -runSynthXST :: XST -> SourceInfo -> FilePath -> ResultSh () -runSynthXST sim (SourceInfo top src) outf = do +runSynthXST :: XST -> SourceInfo -> ResultSh () +runSynthXST sim (SourceInfo top src) = do dir <- liftSh pwd let exec = execute_ SynthFail dir "xst" liftSh $ do @@ -64,7 +64,7 @@ runSynthXST sim (SourceInfo top src) outf = do , "-ofmt" , "verilog" , toTextIgnore $ modFile <.> "ngc" - , toTextIgnore outf + , toTextIgnore $ synthOutput sim ] liftSh $ do echoP "XST: clean" @@ -72,7 +72,7 @@ runSynthXST sim (SourceInfo top src) outf = do "sed" [ "-i" , "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;" - , toTextIgnore outf + , toTextIgnore $ synthOutput sim ] echoP "XST: done" where diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs index 98244a6..f219e01 100644 --- a/src/VeriFuzz/Sim/Yosys.hs +++ b/src/VeriFuzz/Sim/Yosys.hs @@ -42,16 +42,16 @@ instance Tool Yosys where instance Synthesiser Yosys where runSynth = runSynthYosys synthOutput = yosysOutput - setSynthOutput (Yosys a _) f = Yosys a f + setSynthOutput (Yosys a _) = Yosys a instance Show Yosys where show _ = "yosys" defaultYosys :: Yosys -defaultYosys = Yosys "yosys" "yosys/syn_yosys.v" +defaultYosys = Yosys "yosys" "syn_yosys.v" -runSynthYosys :: Yosys -> SourceInfo -> FilePath -> ResultSh () -runSynthYosys sim (SourceInfo _ src) outf = ( SynthFail) . liftSh $ do +runSynthYosys :: Yosys -> SourceInfo -> ResultSh () +runSynthYosys sim (SourceInfo _ src) = ( SynthFail) . liftSh $ do dir <- pwd writefile inpf $ genSource src echoP "Yosys: synthesis" @@ -63,13 +63,13 @@ runSynthYosys sim (SourceInfo _ src) outf = ( SynthFail) . liftSh $ do where inpf = "rtl.v" inp = toTextIgnore inpf - out = toTextIgnore outf + out = toTextIgnore $ synthOutput sim runMaybeSynth :: (Synthesiser a) => Maybe a -> SourceInfo -> ResultSh () runMaybeSynth (Just sim) srcInfo = - runSynth sim srcInfo $ fromText [st|syn_#{toText sim}.v|] + runSynth sim srcInfo runMaybeSynth Nothing (SourceInfo _ src) = - liftSh . writefile "syn_rtl.v" $ genSource src + liftSh . writefile "rtl.v" $ genSource src runEquivYosys :: (Synthesiser a, Synthesiser b) @@ -87,7 +87,7 @@ runEquivYosys yosys sim1 sim2 srcInfo = do $ srcInfo ^. mainModule writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo - runSynth sim1 srcInfo $ fromText [st|syn_#{toText sim1}.v|] + runSynth sim1 srcInfo runMaybeSynth sim2 srcInfo liftSh $ do echoP "Yosys: equivalence check" @@ -108,7 +108,6 @@ runEquiv _ sim1 sim2 srcInfo = do root <- liftSh rootPath dir <- liftSh pwd liftSh $ do - echoP "SymbiYosys: setup" writefile "top.v" . genSource . initMod @@ -116,6 +115,6 @@ runEquiv _ sim1 sim2 srcInfo = do $ srcInfo ^. mainModule writefile "test.sby" $ sbyConfig root sim1 sim2 srcInfo - liftSh $ echoP "SymbiYosys: run" + liftSh $ echoP "Running SymbiYosys" execute_ EquivFail dir "symbiyosys" "sby" ["-f", "test.sby"] - liftSh $ echoP "SymbiYosys: done" + liftSh $ echoP "SymbiYosys equivalence check passed" -- cgit