aboutsummaryrefslogtreecommitdiffstats
path: root/src/VeriFuzz/Sim
diff options
context:
space:
mode:
authorYann Herklotz <git@ymhg.org>2019-04-10 23:42:58 +0100
committerYann Herklotz <git@ymhg.org>2019-04-10 23:42:58 +0100
commit186bb5f37770c150bd8e601e9761211af6a9c277 (patch)
tree33ccc13403d1c9a168909b1e9987f29028834396 /src/VeriFuzz/Sim
parentaefb46596f3f2302540a83b2be8b042232822a2f (diff)
downloadverismith-186bb5f37770c150bd8e601e9761211af6a9c277.tar.gz
verismith-186bb5f37770c150bd8e601e9761211af6a9c277.zip
Fix the generation of modules and add initialisation
Diffstat (limited to 'src/VeriFuzz/Sim')
-rw-r--r--src/VeriFuzz/Sim/Icarus.hs3
-rw-r--r--src/VeriFuzz/Sim/Internal.hs2
-rw-r--r--src/VeriFuzz/Sim/Reduce.hs4
-rw-r--r--src/VeriFuzz/Sim/Template.hs2
4 files changed, 6 insertions, 5 deletions
diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs
index 9b5138f..8876706 100644
--- a/src/VeriFuzz/Sim/Icarus.hs
+++ b/src/VeriFuzz/Sim/Icarus.hs
@@ -92,7 +92,8 @@ runSimIcarus sim rinfo bss = do
[ Initial
$ fold (addDisplay $ assignFunc (_modInPorts m) <$> bss)
<> (SysTaskEnable $ Task "finish" [])
- ] []
+ ]
+ []
let newtb = instantiateMod m tb
let modWithTb = Verilog [newtb, m]
writefile "main.v" $ genSource modWithTb
diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs
index 925b155..145042a 100644
--- a/src/VeriFuzz/Sim/Internal.hs
+++ b/src/VeriFuzz/Sim/Internal.hs
@@ -74,7 +74,7 @@ mainModule = lens get_ set_
set_ (SourceInfo top main) v =
SourceInfo top (main & getModule %~ update top v)
update top v m@(ModDecl (Identifier i) _ _ _ _) | i == top = v
- | otherwise = m
+ | otherwise = m
get_ (SourceInfo top main) = head . filter (f top) $ main ^.. getModule
f top (ModDecl (Identifier i) _ _ _ _) = i == top
diff --git a/src/VeriFuzz/Sim/Reduce.hs b/src/VeriFuzz/Sim/Reduce.hs
index 5684ed5..381a84c 100644
--- a/src/VeriFuzz/Sim/Reduce.hs
+++ b/src/VeriFuzz/Sim/Reduce.hs
@@ -67,8 +67,8 @@ filterExpr ids (Id i) = if i `notElem` ids then Number 1 0 else Id i
filterExpr _ e = e
filterDecl :: [Identifier] -> ModItem -> Bool
-filterDecl ids (Decl Nothing (Port _ _ _ i)) = i `elem` ids
-filterDecl _ _ = True
+filterDecl ids (Decl Nothing (Port _ _ _ i) _) = i `elem` ids
+filterDecl _ _ = True
filterAssigns :: [Port] -> ModItem -> Bool
filterAssigns out (ModCA (ContAssign i _)) =
diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs
index 0fc74a0..f630ea6 100644
--- a/src/VeriFuzz/Sim/Template.hs
+++ b/src/VeriFuzz/Sim/Template.hs
@@ -91,7 +91,7 @@ sbyConfig bd sim1 sim2 (SourceInfo top src) = [st|[options]
mode prove
[engines]
-smtbmc
+smtbmc z3
[script]
#{readL}