aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-05-19 22:13:22 +0100
committerYann Herklotz <git@yannherklotz.com>2021-05-19 22:13:22 +0100
commitfeaf70849a93c60379104a6b4c1e7ee05afab340 (patch)
tree1f83318a9e0157ab963e4909ab4a1b7839c1ed92
parent17796b3ff9bcab6547f49a62b47ed244a8b01571 (diff)
downloadverismith-feaf70849a93c60379104a6b4c1e7ee05afab340.tar.gz
verismith-feaf70849a93c60379104a6b4c1e7ee05afab340.zip
Add new simulation for EMI
-rw-r--r--src/Verismith/Fuzz.hs46
-rw-r--r--src/Verismith/Tool/Icarus.hs67
2 files changed, 91 insertions, 22 deletions
diff --git a/src/Verismith/Fuzz.hs b/src/Verismith/Fuzz.hs
index 42c667e..c2c30a9 100644
--- a/src/Verismith/Fuzz.hs
+++ b/src/Verismith/Fuzz.hs
@@ -324,10 +324,6 @@ equivalence src = do
where
dir = fromText $ "equiv_" <> toText a <> "_" <> toText b
-equivalenceEMI :: (MonadBaseControl IO m, MonadSh m, Show ann) => (SourceInfo ann) -> Fuzz m ()
-equivalenceEMI src = do
- datadir <- fmap _fuzzDataDir askOpts
-
simulation :: (MonadIO m, MonadSh m, Show ann) => (SourceInfo ann) -> Fuzz m ()
simulation src = do
datadir <- fmap _fuzzDataDir askOpts
@@ -365,6 +361,31 @@ simulation src = do
where
dir = fromText $ "countereg_sim_" <> toText a
+simulationEMI :: (MonadIO m, MonadSh m, Show ann) => (SourceInfo ann) -> Fuzz m ()
+simulationEMI src = do
+ datadir <- fmap _fuzzDataDir askOpts
+ synth <- passedSynthesis
+ counterEgs <- failEquivWithIdentityCE
+ vals <- liftIO $ generateByteString Nothing 32 20
+ ident <- liftSh $ sim datadir vals Nothing defaultIdentitySynth
+ resTimes <- liftSh $ mapM (sim datadir vals (justPass $ snd ident)) synth
+ fuzzSimResults .= toSimResult defaultIcarusSim vals synth resTimes
+ liftSh
+ . inspect
+ $ (\(_, r) -> bimap show (T.unpack . T.take 10 . showBS) r)
+ <$> (ident : resTimes)
+ where
+ sim datadir b i a = toolRun ("simulation for " <> toText a) . runResultT $ do
+ make dir
+ pop dir $ do
+ liftSh $ do
+ cp (fromText ".." </> fromText (toText a) </> synthOutput a) $
+ synthOutput a
+ writefile "rtl.v" $ genSource src
+ runSimIc datadir defaultIcarus a src b i
+ where
+ dir = fromText $ "countereg_sim_" <> toText a
+
failEquivWithIdentity :: (MonadSh m) => Fuzz m [SynthResult]
failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get
where
@@ -610,24 +631,13 @@ fuzzEMI gen = do
. propSeed
?~ seed'
(tsynth, _) <- titleRun "Synthesis" $ synthesis src
- (tequiv, _) <-
- if (_fuzzOptsNoEquiv opts)
- then return (0, mempty)
- else titleRun "Equivalence Check" $ equivalenceEMI src
(_, _) <-
if (_fuzzOptsNoSim opts)
then return (0, mempty)
- else titleRun "Simulation" $ simulation src
+ else titleRun "Simulation" $ simulationEMI src
fails <- failEquivWithIdentity
failedSim <- failedSimulations
synthFails <- failedSynthesis
- redResult <-
- whenMaybe
- ( not (null failedSim && null fails && null synthFails)
- && not (_fuzzOptsNoReduction opts)
- )
- . titleRun "Reduction"
- $ reduction src
state_ <- get
currdir <- liftSh pwd
let vi = flip view state_
@@ -639,6 +649,6 @@ fuzzEMI gen = do
(vi fuzzSynthStatus)
size
tsynth
- tequiv
- (getTime redResult)
+ 0
+ 0
return report
diff --git a/src/Verismith/Tool/Icarus.hs b/src/Verismith/Tool/Icarus.hs
index 8504640..da387dc 100644
--- a/src/Verismith/Tool/Icarus.hs
+++ b/src/Verismith/Tool/Icarus.hs
@@ -12,6 +12,7 @@ module Verismith.Tool.Icarus
( Icarus (..),
defaultIcarus,
runSimIc,
+ runSimIcEMI,
runSimIcEC,
)
where
@@ -175,6 +176,45 @@ tbModule bss top =
where
inConcat = (RegConcat . filter (/= (Id "clk")) $ (Id . fromPort <$> (top ^. modInPorts)))
+tbModule' :: [Identifier] -> [ByteString] -> (ModDecl ann) -> (Verilog ann)
+tbModule' ids bss top =
+ Verilog
+ [ instantiateMod top $
+ ModDecl
+ "testbench"
+ []
+ []
+ [ Initial $
+ fold
+ [ BlockAssign (Assign "clk" Nothing 0),
+ BlockAssign (Assign inConcat Nothing 0),
+ BlockAssign (Assign inIds Nothing 0)
+ ]
+ <> fold
+ ( ( \r ->
+ TimeCtrl
+ 10
+ (Just $ BlockAssign (Assign inConcat Nothing r))
+ )
+ . fromInteger
+ . fromBytes <$> bss
+ )
+ <> (TimeCtrl 10 . Just . 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"]
+ ]
+ []
+ ]
+ where
+ inConcat = (RegConcat
+ . filter (flip notElem $ fmap Id ids)
+ . filter (/= (Id "clk"))
+ $ (Id . fromPort <$> (top ^. modInPorts)))
+ inIds = RegConcat $ fmap Id ids
+
counterTestBench :: CounterEg -> (ModDecl ann) -> (Verilog ann)
counterTestBench (CounterEg _ states) m = tbModule filtered m
where
@@ -230,16 +270,35 @@ runSimIc ::
-- | Synthesis tool to be tested.
b ->
-- | Original generated program to test.
- (SourceInfo ann) ->
+ SourceInfo ann ->
-- | Test vectors to be passed as inputs to the generated Verilog.
[ByteString] ->
- -- | What the correct output should be. If
- -- 'Nothing' is passed, then just return 'Pass
- -- ByteString' with the answer.
+ -- | What the correct output should be. If 'Nothing' is passed, then just return 'Pass ByteString'
+ -- with the answer.
Maybe ByteString ->
ResultSh ByteString
runSimIc = runSimIc' tbModule
+runSimIcEMI ::
+ (Synthesiser b, Show ann) =>
+ -- | EMI Ids
+ [Identifier] ->
+ -- | Data directory.
+ FilePath ->
+ -- | Icarus simulator.
+ Icarus ->
+ -- | Synthesis tool to be tested.
+ b ->
+ -- | Original generated program to test.
+ SourceInfo ann ->
+ -- | Test vectors to be passed as inputs to the generated Verilog.
+ [ByteString] ->
+ -- | What the correct output should be. If 'Nothing' is passed, then just return 'Pass ByteString'
+ -- with the answer.
+ Maybe ByteString ->
+ ResultSh ByteString
+runSimIcEMI ids = runSimIc' (tbModule' ids)
+
runSimIcEC ::
(Synthesiser b, Show ann) =>
FilePath ->