From a3cf56b7e2edef87181c534dea099a884ac99306 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 17 Jun 2019 16:13:00 +0100 Subject: Add part of the simulator implementation --- src/VeriFuzz/Fuzz.hs | 45 ++++++++++++++++++++++++++++++++++++++++++++ src/VeriFuzz/Sim/Icarus.hs | 40 +++++++++++++++++++++++++++++++++++++++ src/VeriFuzz/Sim/Template.hs | 24 ++++++++++++++++++----- 3 files changed, 104 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/VeriFuzz/Fuzz.hs b/src/VeriFuzz/Fuzz.hs index dadae90..3aeb0e0 100644 --- a/src/VeriFuzz/Fuzz.hs +++ b/src/VeriFuzz/Fuzz.hs @@ -211,6 +211,44 @@ equivalence src = do runEquiv a b src where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b +simulation :: (MonadBaseControl IO m, MonadSh m) => SourceInfo -> Fuzz m () +simulation src = do + synth <- passEquiv +-- let synthComb = +-- nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth + let synthComb = + nubBy tupEq + . filter (uncurry (/=)) + $ (,) defaultIdentitySynth + <$> synth + resTimes <- liftSh $ mapM (uncurry equiv) synthComb + fuzzSynthResults .= toSynthResult synthComb resTimes + liftSh $ inspect resTimes + where + tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a') + equiv a b = + toolRun ("equivalence check for " <> toText a <> " and " <> toText 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 a b src + where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b + failEquivWithIdentity :: (MonadSh m) => Fuzz m [SynthResult] failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get where @@ -218,6 +256,12 @@ failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get withIdentity (SynthResult _ (IdentitySynth _) (Fail EquivFail) _) = True withIdentity _ = False +passEquiv :: (MonadSh m) => Fuzz m [SynthResult] +passEquiv = filter withIdentity . _fuzzSynthResults <$> get + where + withIdentity (SynthResult _ _ (Pass _) _) = True + withIdentity _ = False + -- | Always reduces with respect to 'Identity'. reduction :: (MonadSh m) => SourceInfo -> Fuzz m () reduction src = do @@ -320,6 +364,7 @@ fuzz gen conf = do ?~ seed' (tsynth, _) <- titleRun "Synthesis" $ synthesis src (tequiv, _) <- titleRun "Equivalence Check" $ equivalence src + (tsim, _) <- titleRun "Equivalence Check" $ simulation src fails <- failEquivWithIdentity synthFails <- failedSynthesis redResult <- diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs index 6c5751a..6df2cf7 100644 --- a/src/VeriFuzz/Sim/Icarus.hs +++ b/src/VeriFuzz/Sim/Icarus.hs @@ -123,3 +123,43 @@ runSimIcarusWithFile sim f _ = annotate SimFail . liftSh $ do dir "vvp" (runFoldLines (mempty :: ByteString) callback (vvpPath sim) ["main"]) + +runSimIc + :: (Synthesiser a) => a -> SourceInfo -> [ByteString] -> ResultSh ByteString +runSimIc sim1 srcInfo bss = do + dir <- liftSh pwd + let top = srcInfo ^. mainModule + let inConcat = (RegConcat (Id . fromPort <$> (top ^. modInPorts))) + let tb = ModDecl + "testbench" + [] + [] + [ Initial + $ fold [ BlockAssign (Assign "clk" Nothing 0) + , BlockAssign (Assign inConcat Nothing 0) + ] + <> (SysTaskEnable $ Task "finish" []) + , Always . TimeCtrl 5 $ BlockAssign (Assign "clk" Nothing (UnNot (Id "clk"))) + , Always . EventCtrl (EPosEdge "clk") $ SysTaskEnable $ Task "strobe" ["%b", Id "y"] + ] + [] + liftSh $ do + writefile "top.v" + . genSource + . initMod + . makeTopAssert + $ srcInfo + ^. mainModule + replaceMods (synthOutput sim1) "_1" srcInfo + replaceMods (synthOutput sim2) "_2" srcInfo + writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo + e <- liftSh $ do + exe dir "symbiyosys" "sby" ["-f", "proof.sby"] + lastExitCode + case e of + 0 -> ResultT . return $ Pass () + 2 -> ResultT . return $ Fail EquivFail + 124 -> ResultT . return $ Fail TimeoutError + _ -> ResultT . return $ Fail EquivError + where + exe dir name e = void . errExit False . logCommand dir name . timeout e diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs index 4aa07f6..913b220 100644 --- a/src/VeriFuzz/Sim/Template.hs +++ b/src/VeriFuzz/Sim/Template.hs @@ -18,17 +18,19 @@ module VeriFuzz.Sim.Template , xstSynthConfig , vivadoSynthConfig , sbyConfig + , icarusTestbench ) where -import Control.Lens ((^..)) -import Data.Text (Text) -import qualified Data.Text as T -import Prelude hiding (FilePath) +import Control.Lens ((^..)) +import Data.Text (Text) +import qualified Data.Text as T +import Prelude hiding (FilePath) import Shelly -import Text.Shakespeare.Text (st) +import Text.Shakespeare.Text (st) import VeriFuzz.Sim.Internal import VeriFuzz.Verilog.AST +import VeriFuzz.Verilog.CodeGen rename :: Text -> [Text] -> Text rename end entries = @@ -117,3 +119,15 @@ top.v . fromText <$> deps readL = T.intercalate "\n" $ mappend "read -formal " <$> deps + +icarusTestbench :: (Synthesiser a) => Verilog -> a -> Text +icarusTestbench t synth1 = [st| +`include "data/cells_cmos.v" +`include "data/cells_cyclone_v.v" +`include "data/cells_verific.v" +`include "data/cells_xilinx_7.v" +`include "data/cells_yosys.v" +`include "#{synthOutput synth1}" + +#{genSource t} +|] -- cgit