diff options
-rw-r--r-- | app/Main.hs | 5 | ||||
-rw-r--r-- | src/VeriFuzz/Simulator/Internal/Template.hs | 5 | ||||
-rw-r--r-- | src/VeriFuzz/Simulator/Xst.hs | 12 | ||||
-rw-r--r-- | src/VeriFuzz/Simulator/Yosys.hs | 28 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/AST.hs | 2 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/CodeGen.hs | 2 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/Mutate.hs | 7 | ||||
-rw-r--r-- | test/Property.hs | 16 | ||||
-rw-r--r-- | test/Unit.hs | 95 |
9 files changed, 117 insertions, 55 deletions
diff --git a/app/Main.hs b/app/Main.hs index c13d4c2..aeda625 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -43,7 +43,10 @@ runEquivalence t = do ^.. getVerilogSrc . traverse . getDescription - shelly . chdir_p (fromText "equiv" </> fromText t) . verbosely $ runEquiv defaultYosys defaultYosys (Just defaultXst) circ + shelly . chdir_p (fromText "equiv" </> fromText t) . verbosely $ runEquiv defaultYosys + defaultYosys + (Just defaultXst) + circ main :: IO () --main = sample (arbitrary :: Gen (Circuit Input)) 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" diff --git a/test/Property.hs b/test/Property.hs index 80c6f68..c6ca390 100644 --- a/test/Property.hs +++ b/test/Property.hs @@ -1,4 +1,7 @@ -module Property (propertyTests) where +module Property + ( propertyTests + ) +where import qualified Data.Graph.Inductive as G import Data.Graph.Inductive.PatriciaTree (Gr) @@ -19,16 +22,11 @@ instance QC.Arbitrary TestGraph where instance QC.Arbitrary AltTestGraph where arbitrary = AltTestGraph <$> QC.resize 100 V.randomDAG -simpleGraph = QC.testProperty "simple graph generation check" $ - \graph -> simp graph +simpleGraph = QC.testProperty "simple graph generation check" $ \graph -> simp graph where simp = G.isSimple . getGraph -simpleAltGraph = QC.testProperty "simple alternative graph generation check" $ - \graph -> simp graph +simpleAltGraph = QC.testProperty "simple alternative graph generation check" $ \graph -> simp graph where simp = G.isSimple . getAltGraph propertyTests :: TestTree -propertyTests = testGroup "Property Tests" - [ simpleGraph - , simpleAltGraph - ] +propertyTests = testGroup "Property Tests" [simpleGraph, simpleAltGraph] diff --git a/test/Unit.hs b/test/Unit.hs index 8bcc702..a72e188 100644 --- a/test/Unit.hs +++ b/test/Unit.hs @@ -1,4 +1,7 @@ -module Unit (unitTests) where +module Unit + ( unitTests + ) +where import Control.Lens import qualified Data.Graph.Inductive as G @@ -8,35 +11,75 @@ import Test.Tasty import Test.Tasty.HUnit import VeriFuzz -unitTests = testGroup "Unit tests" - [ testCase "Transformation of AST" $ - assertEqual "Successful transformation" transformExpectedResult +unitTests = testGroup + "Unit tests" + [ testCase "Transformation of AST" $ assertEqual + "Successful transformation" + transformExpectedResult (transformOf traverseExpr trans transformTestData) ] transformTestData :: Expr -transformTestData = BinOp (BinOp (BinOp (Id "id1") BinAnd (Id "id2")) BinAnd - (BinOp (Id "id1") BinAnd (Id "id2"))) BinAnd - (BinOp (BinOp (BinOp (Id "id1") BinAnd (Id "id2")) BinAnd - (BinOp (Id "id1") BinAnd (BinOp (BinOp (Id "id1") BinAnd (Id "id2")) BinAnd - (BinOp (Id "id1") BinAnd (Id "id2"))))) BinOr - (Concat [Concat [ Concat [Id "id1", Id "id2", Id "id2"], Id "id2", Id "id2" - , Concat [Id "id2", Id "id2", Concat [Id "id1", Id "id2"]] - , Id "id2"], Id "id1", Id "id2"])) +transformTestData = BinOp + (BinOp (BinOp (Id "id1") BinAnd (Id "id2")) BinAnd (BinOp (Id "id1") BinAnd (Id "id2"))) + BinAnd + (BinOp + (BinOp + (BinOp (Id "id1") BinAnd (Id "id2")) + BinAnd + (BinOp + (Id "id1") + BinAnd + (BinOp (BinOp (Id "id1") BinAnd (Id "id2")) BinAnd (BinOp (Id "id1") BinAnd (Id "id2"))) + ) + ) + BinOr + (Concat + [ Concat + [ Concat [Id "id1", Id "id2", Id "id2"] + , Id "id2" + , Id "id2" + , Concat [Id "id2", Id "id2", Concat [Id "id1", Id "id2"]] + , Id "id2" + ] + , Id "id1" + , Id "id2" + ] + ) + ) transformExpectedResult :: Expr -transformExpectedResult = BinOp (BinOp (BinOp (Id "id1") BinAnd (Id "Replaced")) BinAnd - (BinOp (Id "id1") BinAnd (Id "Replaced"))) BinAnd - (BinOp (BinOp (BinOp (Id "id1") BinAnd (Id "Replaced")) BinAnd - (BinOp (Id "id1") BinAnd (BinOp (BinOp (Id "id1") BinAnd (Id "Replaced")) BinAnd - (BinOp (Id "id1") BinAnd (Id "Replaced"))))) BinOr - (Concat [Concat [ Concat [Id "id1", Id "Replaced", Id "Replaced"], Id "Replaced", Id "Replaced" - , Concat [Id "Replaced", Id "Replaced", Concat [Id "id1", Id "Replaced"]] - , Id "Replaced"], Id "id1", Id "Replaced"])) +transformExpectedResult = BinOp + (BinOp (BinOp (Id "id1") BinAnd (Id "Replaced")) BinAnd (BinOp (Id "id1") BinAnd (Id "Replaced"))) + BinAnd + (BinOp + (BinOp + (BinOp (Id "id1") BinAnd (Id "Replaced")) + BinAnd + (BinOp + (Id "id1") + BinAnd + (BinOp (BinOp (Id "id1") BinAnd (Id "Replaced")) + BinAnd + (BinOp (Id "id1") BinAnd (Id "Replaced")) + ) + ) + ) + BinOr + (Concat + [ Concat + [ Concat [Id "id1", Id "Replaced", Id "Replaced"] + , Id "Replaced" + , Id "Replaced" + , Concat [Id "Replaced", Id "Replaced", Concat [Id "id1", Id "Replaced"]] + , Id "Replaced" + ] + , Id "id1" + , Id "Replaced" + ] + ) + ) -trans e = - case e of - Id id -> if id == Identifier "id2" then - Id $ Identifier "Replaced" - else Id id - _ -> e +trans e = case e of + Id id -> if id == Identifier "id2" then Id $ Identifier "Replaced" else Id id + _ -> e |