Move simulation into library

1 files changed, 89 insertions, 1 deletions

diff --git a/src/VeriFuzz.hs b/src/VeriFuzz.hs
index d700d6d..5f5d68a 100644
--- a/src/VeriFuzz.hs
+++ b/src/VeriFuzz.hs
@@ -9,7 +9,9 @@ Portability : POSIX
 -}
 
 module VeriFuzz
-  ( module VeriFuzz.AST
+  ( runEquivalence
+  , runSimulation
+  , module VeriFuzz.AST
   , module VeriFuzz.ASTGen
   , module VeriFuzz.Circuit
   , module VeriFuzz.CodeGen
@@ -24,6 +26,21 @@ module VeriFuzz
   , module VeriFuzz.Yosys
   ) where
 
+import           Control.Lens
+import qualified Crypto.Random.DRBG       as C
+import           Data.ByteString          (ByteString)
+import           Data.ByteString.Builder  (byteStringHex, toLazyByteString)
+import qualified Data.ByteString.Lazy     as L
+import qualified Data.Graph.Inductive     as G
+import qualified Data.Graph.Inductive.Dot as G
+import           Data.Text                (Text)
+import qualified Data.Text                as T
+import           Data.Text.Encoding       (decodeUtf8)
+import qualified Data.Text.IO             as T
+import           Prelude                  hiding (FilePath)
+import           Shelly
+import           Test.QuickCheck          (Gen)
+import qualified Test.QuickCheck          as QC
 import           VeriFuzz.AST
 import           VeriFuzz.ASTGen
 import           VeriFuzz.Circuit
@@ -37,3 +54,74 @@ import           VeriFuzz.Mutate
 import           VeriFuzz.Random
 import           VeriFuzz.XST
 import           VeriFuzz.Yosys
+
+genRand :: C.CtrDRBG -> Int -> [ByteString] -> [ByteString]
+genRand gen n bytes | n == 0    = ranBytes : bytes
+                    | otherwise = genRand newGen (n - 1) $ ranBytes : bytes
+  where Right (ranBytes, newGen) = C.genBytes 32 gen
+
+genRandom :: Int -> IO [ByteString]
+genRandom n = do
+  gen <- C.newGenIO :: IO C.CtrDRBG
+  return $ genRand gen n []
+
+draw :: IO ()
+draw = do
+  gr <- QC.generate $ rDups <$> QC.resize 10 (randomDAG :: QC.Gen (G.Gr Gate ()))
+  let dot = G.showDot . G.fglToDotString $ G.nemap show (const "") gr
+  writeFile "file.dot" dot
+  shelly $ run_ "dot" ["-Tpng", "-o", "file.png", "file.dot"]
+
+showBS :: ByteString -> Text
+showBS = decodeUtf8 . L.toStrict . toLazyByteString . byteStringHex
+
+runSimulation :: IO ()
+runSimulation = do
+  gr <- QC.generate $ rDups <$> QC.resize 100 (randomDAG :: QC.Gen (G.Gr Gate ()))
+  -- let dot = G.showDot . G.fglToDotString $ G.nemap show (const "") gr
+  -- writeFile "file.dot" dot
+  -- shelly $ run_ "dot" ["-Tpng", "-o", "file.png", "file.dot"]
+  let circ =
+        head $ (nestUpTo 30 . generateAST $ Circuit gr) ^.. getVerilogSrc . traverse . getDescription
+  rand <- genRandom 20
+  rand2 <- QC.generate (randomMod 10 100)
+  val  <- shelly $ runSim defaultIcarus (rand2) rand
+  T.putStrLn $ showBS val
+
+onFailure :: Text -> RunFailed -> Sh ()
+onFailure t _ = do
+  ex <- lastExitCode
+  case ex of
+    124 -> do
+      echoP "Test TIMEOUT"
+      chdir ".." $ cp_r (fromText t) $ fromText (t <> "_timeout")
+    _ -> do
+      echoP "Test FAIL"
+      chdir ".." $ cp_r (fromText t) $ fromText (t <> "_failed")
+
+runEquivalence :: Gen ModDecl -> Text -> Int -> IO ()
+runEquivalence gm t i = do
+  m <- QC.generate gm
+  rand <- genRandom 20
+  shellyFailDir $ do
+    mkdir_p (fromText "output" </> fromText n)
+    curr <- toTextIgnore <$> pwd
+    setenv "VERIFUZZ_ROOT" curr
+    cd (fromText "output" </> fromText n)
+    catch_sh (runEquiv defaultYosys defaultYosys
+              (Just defaultXst) m >> echoP "Test OK") $
+      onFailure n
+    catch_sh (runSim (Icarus "iverilog" "vvp") m rand
+              >>= (\b -> echoP ("RTL Sim: " <> showBS b))) $
+      onFailure n
+--    catch_sh (runSimWithFile (Icarus "iverilog" "vvp") "syn_yosys.v" rand
+--              >>= (\b -> echoP ("Yosys Sim: " <> showBS b))) $
+--      onFailure n
+--    catch_sh (runSimWithFile (Icarus "iverilog" "vvp") "syn_xst.v" rand
+--              >>= (\b -> echoP ("XST Sim: " <> showBS b))) $
+--      onFailure n
+    cd ".."
+    rm_rf $ fromText n
+  when (i < 5) (runEquivalence gm t $ i+1)
+  where
+    n = t <> "_" <> T.pack (show i)