aboutsummaryrefslogtreecommitdiffstats
path: root/src/VeriFuzz/Sim
diff options
context:
space:
mode:
Diffstat (limited to 'src/VeriFuzz/Sim')
-rw-r--r--src/VeriFuzz/Sim/Icarus.hs108
-rw-r--r--src/VeriFuzz/Sim/Identity.hs15
-rw-r--r--src/VeriFuzz/Sim/Internal.hs53
-rw-r--r--src/VeriFuzz/Sim/Quartus.hs26
-rw-r--r--src/VeriFuzz/Sim/Template.hs24
-rw-r--r--src/VeriFuzz/Sim/Vivado.hs22
-rw-r--r--src/VeriFuzz/Sim/XST.hs32
-rw-r--r--src/VeriFuzz/Sim/Yosys.hs40
8 files changed, 220 insertions, 100 deletions
diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs
index 423d51b..8e62136 100644
--- a/src/VeriFuzz/Sim/Icarus.hs
+++ b/src/VeriFuzz/Sim/Icarus.hs
@@ -13,30 +13,41 @@ Icarus verilog module.
module VeriFuzz.Sim.Icarus
( Icarus(..)
, defaultIcarus
+ , runSimIc
)
where
-import Control.DeepSeq (NFData, rnf, rwhnf)
+import Control.DeepSeq ( NFData
+ , rnf
+ , rwhnf
+ )
import Control.Lens
-import Crypto.Hash (Digest, hash)
-import Crypto.Hash.Algorithms (SHA256)
-import Data.Binary (encode)
-import qualified Data.ByteArray as BA (convert)
-import Data.ByteString (ByteString)
-import qualified Data.ByteString as B
-import Data.ByteString.Lazy (toStrict)
-import qualified Data.ByteString.Lazy as L (ByteString)
-import Data.Char (digitToInt)
-import Data.Foldable (fold)
-import Data.List (transpose)
-import Data.Maybe (listToMaybe)
-import Data.Text (Text)
-import qualified Data.Text as T
-import Numeric (readInt)
-import Prelude hiding (FilePath)
+import Control.Monad ( void )
+import Crypto.Hash ( Digest
+ , hash
+ )
+import Crypto.Hash.Algorithms ( SHA256 )
+import Data.Binary ( encode )
+import Data.Bits
+import qualified Data.ByteArray as BA
+ ( convert )
+import Data.ByteString ( ByteString )
+import qualified Data.ByteString as B
+import Data.ByteString.Lazy ( toStrict )
+import qualified Data.ByteString.Lazy as L
+ ( ByteString )
+import Data.Char ( digitToInt )
+import Data.Foldable ( fold )
+import Data.List ( transpose )
+import Data.Maybe ( listToMaybe )
+import Data.Text ( Text )
+import qualified Data.Text as T
+import Numeric ( readInt )
+import Prelude hiding ( FilePath )
import Shelly
-import Shelly.Lifted (liftSh)
+import Shelly.Lifted ( liftSh )
import VeriFuzz.Sim.Internal
+import VeriFuzz.Sim.Template
import VeriFuzz.Verilog.AST
import VeriFuzz.Verilog.BitVec
import VeriFuzz.Verilog.CodeGen
@@ -117,11 +128,68 @@ runSimIcarusWithFile
:: Icarus -> FilePath -> [ByteString] -> ResultSh ByteString
runSimIcarusWithFile sim f _ = annotate SimFail . liftSh $ do
dir <- pwd
- logger "Icarus: Compile"
logCommand_ dir "icarus"
$ run (icarusPath sim) ["-o", "main", toTextIgnore f]
- logger "Icarus: Run"
B.take 8 . BA.convert . (hash :: ByteString -> Digest SHA256) <$> logCommand
dir
"vvp"
(runFoldLines (mempty :: ByteString) callback (vvpPath sim) ["main"])
+
+fromBytes :: ByteString -> Integer
+fromBytes = B.foldl' f 0 where f a b = a `shiftL` 8 .|. fromIntegral b
+
+runSimIc
+ :: (Synthesiser b)
+ => Icarus
+ -> b
+ -> SourceInfo
+ -> [ByteString]
+ -> ResultSh ByteString
+runSimIc sim1 synth1 srcInfo bss = do
+ dir <- liftSh pwd
+ let top = srcInfo ^. mainModule
+ let inConcat = (RegConcat (Id . fromPort <$> (top ^. modInPorts)))
+ let
+ tb = instantiateMod top $ ModDecl
+ "testbench"
+ []
+ []
+ [ Initial
+ $ fold
+ [ BlockAssign (Assign "clk" Nothing 0)
+ , BlockAssign (Assign inConcat Nothing 0)
+ ]
+ <> fold
+ ( (\r -> TimeCtrl
+ 10
+ (Just $ BlockAssign (Assign inConcat Nothing r))
+ )
+ . fromInteger
+ . fromBytes
+ <$> bss
+ )
+ <> (SysTaskEnable $ Task "finish" [])
+ , Always . TimeCtrl 5 . Just $ BlockAssign
+ (Assign "clk" Nothing (UnOp UnNot (Id "clk")))
+ , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable $ Task
+ "strobe"
+ ["%b", Id "y"]
+ ]
+ []
+
+ liftSh . writefile "testbench.v" $ icarusTestbench (Verilog [tb]) synth1
+ liftSh $ exe dir "icarus" "iverilog" ["-o", "main", "testbench.v"]
+ liftSh
+ $ B.take 8
+ . BA.convert
+ . (hash :: ByteString -> Digest SHA256)
+ <$> logCommand
+ dir
+ "vvp"
+ (runFoldLines (mempty :: ByteString)
+ callback
+ (vvpPath sim1)
+ ["main"]
+ )
+ where
+ exe dir name e = void . errExit False . logCommand dir name . timeout e
diff --git a/src/VeriFuzz/Sim/Identity.hs b/src/VeriFuzz/Sim/Identity.hs
index bfded0b..95b4097 100644
--- a/src/VeriFuzz/Sim/Identity.hs
+++ b/src/VeriFuzz/Sim/Identity.hs
@@ -16,11 +16,16 @@ module VeriFuzz.Sim.Identity
)
where
-import Control.DeepSeq (NFData, rnf, rwhnf)
-import Data.Text (Text, unpack)
-import Prelude hiding (FilePath)
-import Shelly (FilePath)
-import Shelly.Lifted (writefile)
+import Control.DeepSeq ( NFData
+ , rnf
+ , rwhnf
+ )
+import Data.Text ( Text
+ , unpack
+ )
+import Prelude hiding ( FilePath )
+import Shelly ( FilePath )
+import Shelly.Lifted ( writefile )
import VeriFuzz.Sim.Internal
import VeriFuzz.Verilog.AST
import VeriFuzz.Verilog.CodeGen
diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs
index 5c58e1a..a05a96f 100644
--- a/src/VeriFuzz/Sim/Internal.hs
+++ b/src/VeriFuzz/Sim/Internal.hs
@@ -40,20 +40,26 @@ module VeriFuzz.Sim.Internal
where
import Control.Lens
-import Control.Monad (forM, void)
-import Control.Monad.Catch (throwM)
-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.Format (defaultTimeLocale, formatTime)
-import Data.Time.LocalTime (getZonedTime)
-import Prelude hiding (FilePath)
+import Control.Monad ( forM
+ , void
+ )
+import Control.Monad.Catch ( throwM )
+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.Format ( defaultTimeLocale
+ , formatTime
+ )
+import Data.Time.LocalTime ( getZonedTime )
+import Prelude hiding ( FilePath )
import Shelly
-import Shelly.Lifted (MonadSh, liftSh)
-import System.FilePath.Posix (takeBaseName)
+import Shelly.Lifted ( MonadSh
+ , liftSh
+ )
+import System.FilePath.Posix ( takeBaseName )
import VeriFuzz.Internal
import VeriFuzz.Result
import VeriFuzz.Verilog.AST
@@ -188,21 +194,28 @@ logCommand_ :: FilePath -> Text -> Sh a -> Sh ()
logCommand_ fp name = void . logCommand fp name
execute
- :: (MonadSh m, Monad m, Monoid a)
- => a
+ :: (MonadSh m, Monad m)
+ => Failed
-> FilePath
-> Text
-> FilePath
-> [Text]
- -> ResultT a m Text
-execute f dir name e = annotate f . liftSh . logCommand dir name . timeout e
+ -> ResultT Failed m Text
+execute f dir name e cs = do
+ (res, exitCode) <- liftSh $ do
+ res <- errExit False . logCommand dir name $ timeout e cs
+ (,) res <$> lastExitCode
+ case exitCode of
+ 0 -> ResultT . return $ Pass res
+ 124 -> ResultT . return $ Fail TimeoutError
+ _ -> ResultT . return $ Fail f
execute_
- :: (MonadSh m, Monad m, Monoid a)
- => a
+ :: (MonadSh m, Monad m)
+ => Failed
-> FilePath
-> Text
-> FilePath
-> [Text]
- -> ResultT a m ()
+ -> ResultT Failed m ()
execute_ a b c d = void . execute a b c d
diff --git a/src/VeriFuzz/Sim/Quartus.hs b/src/VeriFuzz/Sim/Quartus.hs
index ece00eb..e0fbba5 100644
--- a/src/VeriFuzz/Sim/Quartus.hs
+++ b/src/VeriFuzz/Sim/Quartus.hs
@@ -16,11 +16,16 @@ module VeriFuzz.Sim.Quartus
)
where
-import Control.DeepSeq (NFData, rnf, rwhnf)
-import Data.Text (Text, unpack)
-import Prelude hiding (FilePath)
+import Control.DeepSeq ( NFData
+ , rnf
+ , rwhnf
+ )
+import Data.Text ( Text
+ , unpack
+ )
+import Prelude hiding ( FilePath )
import Shelly
-import Shelly.Lifted (liftSh)
+import Shelly.Lifted ( liftSh )
import VeriFuzz.Sim.Internal
import VeriFuzz.Verilog.AST
import VeriFuzz.Verilog.CodeGen
@@ -52,12 +57,16 @@ runSynthQuartus :: Quartus -> SourceInfo -> ResultSh ()
runSynthQuartus sim (SourceInfo top src) = do
dir <- liftSh pwd
let ex = execute_ SynthFail dir "quartus"
- liftSh $ do
- writefile inpf $ genSource src
- logger "Running Quartus synthesis"
+ liftSh . writefile inpf $ genSource src
+ liftSh . noPrint $ run_
+ "sed"
+ [ "-i"
+ , "s/^module/(* multstyle = \"logic\" *) module/;"
+ , toTextIgnore inpf
+ ]
ex (exec "quartus_map")
[top, "--source=" <> toTextIgnore inpf, "--family=Cyclone V"]
- ex (exec "quartus_fit") [top, "--part=5CGTFD9E5F35C7N"]
+ ex (exec "quartus_fit") [top, "--part=5CGXFC7D6F31C6"]
ex (exec "quartus_eda") [top, "--simulation", "--tool=vcs"]
liftSh $ do
cp (fromText "simulation/vcs" </> fromText top <.> "vo")
@@ -68,7 +77,6 @@ runSynthQuartus sim (SourceInfo top src) = do
, "s,^// DATE.*,,; s,^tri1 (.*);,wire \\1 = 1;,; /^\\/\\/ +synopsys/ d;"
, toTextIgnore $ synthOutput sim
]
- logger "Quartus synthesis done"
where
inpf = "rtl.v"
exec s = maybe (fromText s) (</> fromText s) $ quartusBin sim
diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs
index 4aa07f6..3be6558 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 "#{toTextIgnore $ synthOutput synth1}"
+
+#{genSource t}
+|]
diff --git a/src/VeriFuzz/Sim/Vivado.hs b/src/VeriFuzz/Sim/Vivado.hs
index ee67a78..8697a0f 100644
--- a/src/VeriFuzz/Sim/Vivado.hs
+++ b/src/VeriFuzz/Sim/Vivado.hs
@@ -16,11 +16,16 @@ module VeriFuzz.Sim.Vivado
)
where
-import Control.DeepSeq (NFData, rnf, rwhnf)
-import Data.Text (Text, unpack)
-import Prelude hiding (FilePath)
+import Control.DeepSeq ( NFData
+ , rnf
+ , rwhnf
+ )
+import Data.Text ( Text
+ , unpack
+ )
+import Prelude hiding ( FilePath )
import Shelly
-import Shelly.Lifted (liftSh)
+import Shelly.Lifted ( liftSh )
import VeriFuzz.Sim.Internal
import VeriFuzz.Sim.Template
import VeriFuzz.Verilog.AST
@@ -56,13 +61,16 @@ runSynthVivado sim (SourceInfo top src) = do
writefile vivadoTcl . vivadoSynthConfig top . toTextIgnore $ synthOutput
sim
writefile "rtl.v" $ genSource src
- run_ "sed" ["s/^module/(* use_dsp=\"no\" *) module/;", "-i", "rtl.v"]
- logger "Vivado: run"
+ run_
+ "sed"
+ [ "s/^module/(* use_dsp48=\"no\" *) (* use_dsp=\"no\" *) module/;"
+ , "-i"
+ , "rtl.v"
+ ]
let exec_ n = execute_
SynthFail
dir
"vivado"
(maybe (fromText n) (</> fromText n) $ vivadoBin sim)
exec_ "vivado" ["-mode", "batch", "-source", toTextIgnore vivadoTcl]
- liftSh $ logger "Vivado: done"
where vivadoTcl = fromText ("vivado_" <> top) <.> "tcl"
diff --git a/src/VeriFuzz/Sim/XST.hs b/src/VeriFuzz/Sim/XST.hs
index 11be094..f5faae5 100644
--- a/src/VeriFuzz/Sim/XST.hs
+++ b/src/VeriFuzz/Sim/XST.hs
@@ -18,12 +18,17 @@ module VeriFuzz.Sim.XST
)
where
-import Control.DeepSeq (NFData, rnf, rwhnf)
-import Data.Text (Text, unpack)
-import Prelude hiding (FilePath)
+import Control.DeepSeq ( NFData
+ , rnf
+ , rwhnf
+ )
+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.Sim.Internal
import VeriFuzz.Sim.Template
import VeriFuzz.Verilog.AST
@@ -64,9 +69,7 @@ runSynthXST sim (SourceInfo top src) = do
writefile xstFile $ xstSynthConfig top
writefile prjFile [st|verilog work "rtl.v"|]
writefile "rtl.v" $ genSource src
- logger "XST: run"
exec "xst" ["-ifn", toTextIgnore xstFile]
- liftSh $ logger "XST: netgen"
exec
"netgen"
[ "-w"
@@ -75,15 +78,12 @@ runSynthXST sim (SourceInfo top src) = do
, toTextIgnore $ modFile <.> "ngc"
, toTextIgnore $ synthOutput sim
]
- liftSh $ do
- logger "XST: clean"
- noPrint $ run_
- "sed"
- [ "-i"
- , "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;"
- , toTextIgnore $ synthOutput sim
- ]
- logger "XST: done"
+ liftSh . noPrint $ run_
+ "sed"
+ [ "-i"
+ , "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;"
+ , toTextIgnore $ synthOutput sim
+ ]
where
modFile = fromText top
xstFile = modFile <.> "xst"
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
generated by cgit (git 2.34.1) at 2024-06-26 03:20:27 +0000