From d60fc9c882f6ce668123fbfbfd9a0f02dd832f7b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 20 Jan 2019 16:49:17 +0000 Subject: Prettify files --- src/VeriFuzz/Simulator/Internal/Template.hs | 5 ++++- src/VeriFuzz/Simulator/Xst.hs | 12 ++++++------ src/VeriFuzz/Simulator/Yosys.hs | 28 ++++++++++++++++------------ src/VeriFuzz/Verilog/AST.hs | 2 ++ src/VeriFuzz/Verilog/CodeGen.hs | 2 ++ src/VeriFuzz/Verilog/Mutate.hs | 7 +++++++ 6 files changed, 37 insertions(+), 19 deletions(-) (limited to 'src') diff --git a/src/VeriFuzz/Simulator/Internal/Template.hs b/src/VeriFuzz/Simulator/Internal/Template.hs index 6813e72..4b9cc4e 100644 --- a/src/VeriFuzz/Simulator/Internal/Template.hs +++ b/src/VeriFuzz/Simulator/Internal/Template.hs @@ -22,6 +22,7 @@ import Text.Shakespeare.Text (st) import VeriFuzz.Simulator.General import VeriFuzz.Verilog +-- brittany-disable-next-binding yosysSatConfig :: (Simulator a, Simulator b) => a -> Maybe b -> ModDecl -> Text yosysSatConfig sim1 sim2 m = [st|read_verilog syn_#{toText sim1}.v rename #{mi} #{mi}_1 @@ -37,11 +38,13 @@ sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 idSim2 = maybe "rtl" toText sim2 mi = modName m +-- brittany-disable-next-binding yosysSimConfig :: Text yosysSimConfig = [st|read_verilog rtl.v; proc;; rename mod mod_rtl |] +-- brittany-disable-next-binding xstSynthConfig :: ModDecl -> Text xstSynthConfig m = [st|run -ifn #{mi}.prj -ofn #{mi} -p artix7 -top #{mi} @@ -52,6 +55,7 @@ xstSynthConfig m = [st|run where mi = modName m +-- brittany-disable-next-binding sbyConfig :: (Simulator a, Simulator b) => FilePath -> a -> Maybe b -> ModDecl -> Text sbyConfig bd sim1 sim2 m = [st|[options] mode prove @@ -79,7 +83,6 @@ top.v deps = ["cells_cmos.v", "cells_cyclone_v.v", "cells_verific.v", "cells_xilinx_7.v"] depList = T.intercalate "\n" - . zipWith mappend ((<>" ") <$> deps) $ toTextIgnore . ((bd fromText "data") ) . fromText diff --git a/src/VeriFuzz/Simulator/Xst.hs b/src/VeriFuzz/Simulator/Xst.hs index 2314dd1..415a45e 100644 --- a/src/VeriFuzz/Simulator/Xst.hs +++ b/src/VeriFuzz/Simulator/Xst.hs @@ -37,16 +37,16 @@ defaultXst :: Xst defaultXst = Xst "/opt/Xilinx/14.7/ISE_DS/ISE/bin/lin64/xst" "/opt/Xilinx/14.7/ISE_DS/ISE/bin/lin64/netgen" --- brittany-disable-next-binding runSynthXst :: Xst -> ModDecl -> FilePath -> Sh () runSynthXst sim m outf = do writefile xstFile $ xstSynthConfig m writefile prjFile [st|verilog work "rtl.v"|] writefile "rtl.v" $ genSource m timeout_ (xstPath sim) ["-ifn", toTextIgnore xstFile] - run_ (netgenPath sim) ["-w", "-ofmt", "verilog", toTextIgnore $ modFile <.> "ngc", toTextIgnore outf] + run_ (netgenPath sim) + ["-w", "-ofmt", "verilog", toTextIgnore $ modFile <.> "ngc", toTextIgnore outf] run_ "sed" ["-i", "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;", toTextIgnore outf] - where - modFile = fromText $ modName m - xstFile = modFile <.> "xst" - prjFile = modFile <.> "prj" + where + modFile = fromText $ modName m + xstFile = modFile <.> "xst" + prjFile = modFile <.> "prj" diff --git a/src/VeriFuzz/Simulator/Yosys.hs b/src/VeriFuzz/Simulator/Yosys.hs index 4c2e0ad..ec5a284 100644 --- a/src/VeriFuzz/Simulator/Yosys.hs +++ b/src/VeriFuzz/Simulator/Yosys.hs @@ -35,10 +35,11 @@ instance Synthesize Yosys where defaultYosys :: Yosys defaultYosys = Yosys "/usr/bin/yosys" -writeSimFile :: Yosys -- ^ Simulator instance - -> ModDecl -- ^ Current module - -> FilePath -- ^ Output sim file - -> Sh () +writeSimFile + :: Yosys -- ^ Simulator instance + -> ModDecl -- ^ Current module + -> FilePath -- ^ Output sim file + -> Sh () writeSimFile _ m file = do writefile "rtl.v" $ genSource m writefile file yosysSimConfig @@ -53,16 +54,19 @@ runSynthYosys sim m outf = do out = toTextIgnore outf -- ids = T.intercalate "," $ allVars m ^.. traverse . getIdentifier -runOtherSynth :: (Synthesize a) => Maybe a -> ModDecl -> Sh () -runOtherSynth (Just sim) m = runSynth sim m $ fromText [st|syn_#{toText sim}.v|] -runOtherSynth Nothing m = writefile "syn_rtl.v" $ genSource m +runMaybeSynth :: (Synthesize a) => Maybe a -> ModDecl -> Sh () +runMaybeSynth (Just sim) m = runSynth sim m $ fromText [st|syn_#{toText sim}.v|] +runMaybeSynth Nothing m = writefile "syn_rtl.v" $ genSource m -runEquiv :: (Synthesize a, Synthesize b) => Yosys -> a -> Maybe b -> ModDecl -> Sh () -runEquiv yosys sim1 sim2 m = do +runEquivYosys :: (Synthesize a, Synthesize b) => Yosys -> a -> Maybe b -> ModDecl -> Sh () +runEquivYosys yosys sim1 sim2 m = do writefile "top.v" . genSource . initMod $ makeTop 2 m writefile checkFile $ yosysSatConfig sim1 sim2 m runSynth sim1 m $ fromText [st|syn_#{toText sim1}.v|] - runOtherSynth sim2 m + runMaybeSynth sim2 m run_ (yosysPath yosys) [toTextIgnore checkFile] - where - checkFile = fromText [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|] + where checkFile = fromText [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|] + +runEquiv :: (Synthesize a, Synthesize b) => Yosys -> a -> Maybe b -> ModDecl -> Sh () +runEquiv yosys sim1 sim2 m = do + writefile "top.v" . genSource . initMod $ makeTopAssert m diff --git a/src/VeriFuzz/Verilog/AST.hs b/src/VeriFuzz/Verilog/AST.hs index f940281..1b2cb19 100644 --- a/src/VeriFuzz/Verilog/AST.hs +++ b/src/VeriFuzz/Verilog/AST.hs @@ -144,6 +144,8 @@ instance QC.Arbitrary Delay where data Event = EId Identifier | EExpr Expr | EAll + | EPosEdge Identifier + | ENegEdge Identifier deriving (Eq, Show) instance QC.Arbitrary Event where diff --git a/src/VeriFuzz/Verilog/CodeGen.hs b/src/VeriFuzz/Verilog/CodeGen.hs index 58b1d16..0b7f422 100644 --- a/src/VeriFuzz/Verilog/CodeGen.hs +++ b/src/VeriFuzz/Verilog/CodeGen.hs @@ -155,6 +155,8 @@ genEvent :: Event -> Text genEvent (EId i ) = "@(" <> i ^. getIdentifier <> ")" genEvent (EExpr expr) = "@(" <> genExpr expr <> ")" genEvent EAll = "@*" +genEvent (EPosEdge i) = "@(posedge " <> i ^. getIdentifier <> ")" +genEvent (ENegEdge i) = "@(negedge " <> i ^. getIdentifier <> ")" -- | Generates verilog code for a 'Delay'. genDelay :: Delay -> Text diff --git a/src/VeriFuzz/Verilog/Mutate.hs b/src/VeriFuzz/Verilog/Mutate.hs index dca0dd9..0e68419 100644 --- a/src/VeriFuzz/Verilog/Mutate.hs +++ b/src/VeriFuzz/Verilog/Mutate.hs @@ -136,3 +136,10 @@ makeTop i m = ModDecl (m ^. modId) ys (m ^. modInPorts) modIt ys = Port Wire 90 . flip makeIdFrom "y" <$> [1 .. i] modIt = instantiateMod_ . modN <$> [1 .. i] modN n = m & modId %~ makeIdFrom n & modOutPorts .~ [Port Wire 90 (makeIdFrom n "y")] + +makeTopAssert :: ModDecl -> ModDecl +makeTopAssert = (modItems %~ (++ [assert])) . (modInPorts %~ ((Port Wire 1 "clk") :)) . makeTop 2 + where + assert = Always . EventCtrl e . Just $ SeqBlock + [TaskEnable $ Task "assert" [BinOp (Id "y_1") BinEq (Id "y_2")]] + e = EPosEdge "clk" -- cgit