diff options
| -rw-r--r-- | src/VeriFuzz/Sim/Internal.hs | 36 | ||||
| -rw-r--r-- | src/VeriFuzz/Sim/Template.hs | 9 | ||||
| -rw-r--r-- | src/VeriFuzz/Sim/Vivado.hs | 2 | ||||
| -rw-r--r-- | src/VeriFuzz/Sim/Yosys.hs | 5 |
4 files changed, 41 insertions, 11 deletions
diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs index 6e02482..6d36348 100644 --- a/src/VeriFuzz/Sim/Internal.hs +++ b/src/VeriFuzz/Sim/Internal.hs @@ -18,6 +18,10 @@ module VeriFuzz.Sim.Internal , Simulator(..) , Synthesiser(..) , Failed(..) + , checkPresent + , checkPresentModules + , replace + , replaceMods , rootPath , timeout , timeout_ @@ -33,10 +37,12 @@ module VeriFuzz.Sim.Internal ) where -import Control.Monad (void) +import Control.Lens +import Control.Monad (forM, void) 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.LocalTime (getZonedTime) @@ -89,6 +95,32 @@ class Tool a => Synthesiser a where -- with also has those instances. type ResultSh = ResultT Failed Sh +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 @@ -108,7 +140,7 @@ bsToI = B.foldl' (\i b -> (i `shiftL` 8) + fromIntegral b) 0 {-# INLINE bsToI #-} noPrint :: Sh a -> Sh a -noPrint = liftSh . print_stdout False . print_stderr False +noPrint = print_stdout False . print_stderr False {-# INLINE noPrint #-} echoP :: Text -> Sh () diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs index 771646d..f6e5a1e 100644 --- a/src/VeriFuzz/Sim/Template.hs +++ b/src/VeriFuzz/Sim/Template.hs @@ -88,8 +88,8 @@ write_verilog -force #{outf} |] -- brittany-disable-next-binding -sbyConfig :: (Synthesiser a, Synthesiser b) => FilePath -> a -> Maybe b -> SourceInfo -> Text -sbyConfig bd sim1 sim2 (SourceInfo top src) = [st|[options] +sbyConfig :: (Synthesiser a, Synthesiser b) => a -> Maybe b -> SourceInfo -> Text +sbyConfig sim1 sim2 (SourceInfo top _) = [st|[options] multiclock on mode prove @@ -99,9 +99,7 @@ smtbmc z3 [script] #{readL} read -formal #{outputText sim1} -#{rename "_1" mis} read -formal #{maybe "rtl.v" outputText sim2} -#{rename "_2" mis} read -formal top.v prep -top #{top} @@ -112,12 +110,11 @@ prep -top #{top} top.v |] where - mis = src ^.. getSourceId deps = ["cells_cmos.v", "cells_cyclone_v.v", "cells_verific.v", "cells_xilinx_7.v", "cells_yosys.v"] depList = T.intercalate "\n" $ toTextIgnore - . ((bd </> fromText "data") </>) + . (fromText "data" </>) . fromText <$> deps readL = T.intercalate "\n" $ mappend "read -formal " <$> deps diff --git a/src/VeriFuzz/Sim/Vivado.hs b/src/VeriFuzz/Sim/Vivado.hs index 6ede8b5..1994a57 100644 --- a/src/VeriFuzz/Sim/Vivado.hs +++ b/src/VeriFuzz/Sim/Vivado.hs @@ -50,7 +50,7 @@ runSynthVivado sim (SourceInfo top src) = do writefile vivadoTcl . vivadoSynthConfig top . toTextIgnore $ synthOutput sim writefile "rtl.v" $ genSource src - run_ "sed" ["s/^module/(* use_dsp48=\"no\" *) module/;", "-i", "rtl.v"] + run_ "sed" ["s/^module/(* use_dsp=\"no\" *) module/;", "-i", "rtl.v"] echoP "Vivado: run" execute_ SynthFail dir diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs index f72fb1a..1bff975 100644 --- a/src/VeriFuzz/Sim/Yosys.hs +++ b/src/VeriFuzz/Sim/Yosys.hs @@ -104,7 +104,6 @@ runEquiv -> SourceInfo -> ResultSh () runEquiv _ sim1 sim2 srcInfo = do - root <- liftSh rootPath dir <- liftSh pwd liftSh $ do writefile "top.v" @@ -113,7 +112,9 @@ runEquiv _ sim1 sim2 srcInfo = do . makeTopAssert $ srcInfo ^. mainModule - writefile "test.sby" $ sbyConfig root sim1 sim2 srcInfo + replaceMods (synthOutput sim1) "_1" srcInfo + replaceMods (maybe "rtl.v" synthOutput sim2) "_2" srcInfo + writefile "test.sby" $ sbyConfig sim1 sim2 srcInfo liftSh $ echoP "Running SymbiYosys" execute_ EquivFail dir "symbiyosys" "sby" ["-f", "test.sby"] liftSh $ echoP "SymbiYosys equivalence check passed" |