diff options
author | Yann Herklotz <git@yannherklotz.com> | 2019-06-17 16:13:00 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2019-06-29 16:12:46 +0100 |
commit | a3cf56b7e2edef87181c534dea099a884ac99306 (patch) | |
tree | 8c56694a6dea8b5aa832e8df6fb2eec1620c72f4 /src/VeriFuzz/Sim/Icarus.hs | |
parent | 54c2072ac4b92bb3db3fcd0208cbb877f1abbf8d (diff) | |
download | verismith-a3cf56b7e2edef87181c534dea099a884ac99306.tar.gz verismith-a3cf56b7e2edef87181c534dea099a884ac99306.zip |
Add part of the simulator implementation
Diffstat (limited to 'src/VeriFuzz/Sim/Icarus.hs')
-rw-r--r-- | src/VeriFuzz/Sim/Icarus.hs | 40 |
1 files changed, 40 insertions, 0 deletions
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 |