Generate flip-flops instead of latches

3 files changed, 5 insertions, 14 deletions

diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs
index 6bde792..0fc74a0 100644
--- a/src/VeriFuzz/Sim/Template.hs
+++ b/src/VeriFuzz/Sim/Template.hs
@@ -89,7 +89,6 @@ write_verilog -force #{outf}
 sbyConfig :: (Tool a, Tool b) => FilePath -> a -> Maybe b -> SourceInfo -> Text
 sbyConfig bd sim1 sim2 (SourceInfo top src) = [st|[options]
 mode prove
-multiclock on
 
 [engines]
 smtbmc
diff --git a/src/VeriFuzz/Verilog/Gen.hs b/src/VeriFuzz/Verilog/Gen.hs
index 1793582..87a0a31 100644
--- a/src/VeriFuzz/Verilog/Gen.hs
+++ b/src/VeriFuzz/Verilog/Gen.hs
@@ -105,13 +105,6 @@ newPort pt = do
 choose :: PortType -> Port -> Bool
 choose ptype (Port a _ _ _) = ptype == a
 
-select :: PortType -> StateGen Port
-select ptype = do
-    context <- get
-    case filter (choose Reg) $ context ^.. variables . traverse of
-        [] -> newPort ptype
-        l  -> Hog.element l
-
 scopedExpr :: StateGen Expr
 scopedExpr = do
     context <- get
@@ -166,9 +159,8 @@ statement = do
 
 always :: StateGen ModItem
 always = do
-    stat     <- SeqBlock <$> some statement
-    eventReg <- select Reg
-    return $ Always (EventCtrl (EId (eventReg ^. portName)) (Just stat))
+    stat <- SeqBlock <$> some statement
+    return $ Always (EventCtrl (EPosEdge "clk") (Just stat))
 
 -- | Generate a random module item.
 modItem :: StateGen ModItem
@@ -204,9 +196,10 @@ moduleDef top = do
     initBlock <- initialBlock
     let local = filter (`notElem` portList) $ context ^. variables
     let size  = sum $ local ^.. traverse . portSize
+    let clock = Port Wire False 1 "clk"
     let yport = Port Wire False size "y"
     let comb = combineAssigns_ yport local
-    return . declareMod local . ModDecl name [yport] portList $ initBlock : mi <> [comb]
+    return . declareMod local . ModDecl name [yport] (clock:portList) $ initBlock : mi <> [comb]
 
 -- | Procedural generation method for random Verilog. Uses internal 'Reader' and
 -- 'State' to keep track of the current Verilog code structure.
diff --git a/src/VeriFuzz/Verilog/Mutate.hs b/src/VeriFuzz/Verilog/Mutate.hs
index eca472f..03ee1d0 100644
--- a/src/VeriFuzz/Verilog/Mutate.hs
+++ b/src/VeriFuzz/Verilog/Mutate.hs
@@ -206,13 +206,12 @@ makeTop i m = ModDecl (m ^. modId) ys (m ^. modInPorts) modIt
 -- | Make a top module with an assert that requires @y_1@ to always be equal to
 -- @y_2@, which can then be proven using a formal verification tool.
 makeTopAssert :: ModDecl -> ModDecl
-makeTopAssert = (modItems %~ (++ [assert])) . (modInPorts %~ addClk) . makeTop
+makeTopAssert = (modItems %~ (++ [assert])) . makeTop
     2
   where
     assert = Always . EventCtrl e . Just $ SeqBlock
         [TaskEnable $ Task "assert" [BinOp (Id "y_1") BinEq (Id "y_2")]]
     e      = EPosEdge "clk"
-    addClk = (defaultPort "clk" :)
 
 -- | Provide declarations for all the ports that are passed to it.
 declareMod :: [Port] -> ModDecl -> ModDecl