diff options
Diffstat (limited to 'src/VeriFuzz/Sim/Yosys.hs')
| -rw-r--r-- | src/VeriFuzz/Sim/Yosys.hs | 40 |
1 files changed, 22 insertions, 18 deletions
diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs index 3081a65..8f9d4a7 100644 --- a/src/VeriFuzz/Sim/Yosys.hs +++ b/src/VeriFuzz/Sim/Yosys.hs @@ -20,14 +20,19 @@ module VeriFuzz.Sim.Yosys ) where -import Control.DeepSeq (NFData, rnf, rwhnf) +import Control.DeepSeq ( NFData + , rnf + , rwhnf + ) import Control.Lens -import Control.Monad (void) -import Data.Text (Text, unpack) -import Prelude hiding (FilePath) +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 Shelly.Lifted ( liftSh ) +import Text.Shakespeare.Text ( st ) import VeriFuzz.Result import VeriFuzz.Sim.Internal import VeriFuzz.Sim.Template @@ -62,16 +67,19 @@ yosysPath :: Yosys -> FilePath yosysPath sim = maybe (fromText "yosys") (</> fromText "yosys") $ yosysBin sim runSynthYosys :: Yosys -> SourceInfo -> ResultSh () -runSynthYosys sim (SourceInfo _ src) = (<?> SynthFail) . liftSh $ do - dir <- pwd - writefile inpf $ genSource src - logger "Yosys: synthesis" - logCommand_ dir "yosys" $ timeout +runSynthYosys sim (SourceInfo _ src) = do + dir <- liftSh $ do + dir' <- pwd + writefile inpf $ genSource src + return dir' + execute_ + SynthFail + dir + "yosys" (yosysPath sim) [ "-p" , "read -formal " <> inp <> "; synth; write_verilog -noattr " <> out ] - logger "Yosys: synthesis done" where inpf = "rtl.v" inp = toTextIgnore inpf @@ -95,10 +103,7 @@ runEquivYosys yosys sim1 sim2 srcInfo = do writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo runSynth sim1 srcInfo runSynth sim2 srcInfo - liftSh $ do - logger "Yosys: equivalence check" - run_ (yosysPath yosys) [toTextIgnore checkFile] - logger "Yosys: equivalence done" + liftSh $ run_ (yosysPath yosys) [toTextIgnore checkFile] where checkFile = fromText [st|test.#{toText sim1}.#{toText sim2}.ys|] runEquiv @@ -115,12 +120,11 @@ runEquiv sim1 sim2 srcInfo = do replaceMods (synthOutput sim1) "_1" srcInfo replaceMods (synthOutput sim2) "_2" srcInfo writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo - liftSh $ logger "Running SymbiYosys" e <- liftSh $ do exe dir "symbiyosys" "sby" ["-f", "proof.sby"] lastExitCode case e of - 0 -> liftSh $ logger "SymbiYosys equivalence check passed" + 0 -> ResultT . return $ Pass () 2 -> ResultT . return $ Fail EquivFail 124 -> ResultT . return $ Fail TimeoutError _ -> ResultT . return $ Fail EquivError |