From 99fe59abc997ba6f65896a2377881409e257faf9 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 20 Jan 2019 15:33:13 +0000 Subject: Rename moduleId to modId --- app/Main.hs | 8 +++++--- src/VeriFuzz/Simulator.hs | 14 +++++++++++--- src/VeriFuzz/Simulator/Xst.hs | 2 +- src/VeriFuzz/Simulator/Yosys.hs | 18 +++++++++--------- src/VeriFuzz/Verilog/AST.hs | 4 ++-- src/VeriFuzz/Verilog/CodeGen.hs | 2 +- src/VeriFuzz/Verilog/Helpers.hs | 5 ++++- src/VeriFuzz/Verilog/Mutate.hs | 10 +++++----- test/Unit.hs | 1 + 9 files changed, 39 insertions(+), 25 deletions(-) diff --git a/app/Main.hs b/app/Main.hs index 632e0f1..c13d4c2 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -4,7 +4,9 @@ import Control.Lens import qualified Crypto.Random.DRBG as C import Data.ByteString (ByteString) import qualified Data.Graph.Inductive as G +import Data.Text (Text) import Numeric (showHex) +import Prelude hiding (FilePath) import Shelly import qualified Test.QuickCheck as QC import VeriFuzz @@ -31,8 +33,8 @@ runSimulation = do val <- shelly $ runSim defaultIcarus (initMod circ) rand putStrLn $ showHex (abs val) "" -runEquivalence :: IO () -runEquivalence = do +runEquivalence :: Text -> IO () +runEquivalence t = do gr <- QC.generate $ rDups <$> QC.resize 100 (randomDAG :: QC.Gen (G.Gr Gate ())) let circ = initMod @@ -41,7 +43,7 @@ runEquivalence = do ^.. getVerilogSrc . traverse . getDescription - shelly . 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.hs b/src/VeriFuzz/Simulator.hs index 24365fd..a84cd5f 100644 --- a/src/VeriFuzz/Simulator.hs +++ b/src/VeriFuzz/Simulator.hs @@ -11,23 +11,31 @@ Simulator module. -} module VeriFuzz.Simulator - ( module VeriFuzz.Simulator.General + ( SimMatrix + , module VeriFuzz.Simulator.General , module VeriFuzz.Simulator.Yosys , module VeriFuzz.Simulator.Xst , module VeriFuzz.Simulator.Icarus ) where -import Control.Monad.Trans.Reader (ReaderT) +import Control.Monad.Trans.Reader +import Prelude hiding (FilePath) import Shelly import VeriFuzz.Simulator.General import VeriFuzz.Simulator.Icarus import VeriFuzz.Simulator.Xst import VeriFuzz.Simulator.Yosys +-- | Environment used to run the main data SimMatrix = SimMatrix { yosys :: Yosys , xst :: Maybe Xst , icarus :: Maybe Icarus } -type SimEnv = ReaderT SimMatrix Sh +type SimEnv = ReaderT SimMatrix IO + +runAll :: SimEnv () +runAll = do + val <- asks xst + shelly $ run_ "echo" ["Hello World"] diff --git a/src/VeriFuzz/Simulator/Xst.hs b/src/VeriFuzz/Simulator/Xst.hs index 29d1e4a..7b6608b 100644 --- a/src/VeriFuzz/Simulator/Xst.hs +++ b/src/VeriFuzz/Simulator/Xst.hs @@ -51,7 +51,7 @@ runSynthXst sim m outf = do run_ (netgenPath sim) ["-w", "-ofmt", "verilog", toTextIgnore $ modFile <.> "ngc", toTextIgnore outf] run_ "sed" ["-i", "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;", toTextIgnore outf] where - modName = m ^. moduleId . getIdentifier + modName = m ^. modId . getIdentifier modFile = fromText modName xstFile = modFile <.> "xst" prjFile = modFile <.> "prj" diff --git a/src/VeriFuzz/Simulator/Yosys.hs b/src/VeriFuzz/Simulator/Yosys.hs index 8f40ea9..90c40bf 100644 --- a/src/VeriFuzz/Simulator/Yosys.hs +++ b/src/VeriFuzz/Simulator/Yosys.hs @@ -14,8 +14,9 @@ Yosys simulator implementation. module VeriFuzz.Simulator.Yosys where -import Control.Lens +import Data.Maybe (fromMaybe) import Data.Text (Text) +import qualified Data.Text as T import Prelude hiding (FilePath) import Shelly import Text.Shakespeare.Text (st) @@ -54,21 +55,20 @@ runSynthYosys sim m outf = do out = toTextIgnore outf -- brittany-disable-next-binding -writeSatFile :: (Synthesize a, Synthesize b) => Text -> a -> Maybe b -> ModDecl -> Sh () +writeSatFile :: (Synthesize a, Synthesize b) => FilePath -> a -> Maybe b -> ModDecl -> Sh () writeSatFile checkFile sim1 sim2 m = - writefile (fromText checkFile) [st|read_verilog syn_#{toText sim1}.v -rename #{modName} #{modName}_1 -read_verilog syn_#{idSim2}.v -rename #{modName} #{modName}_2 + writefile checkFile [st|read_ilang syn_#{toText sim1}.il +rename #{modName m} #{modName m}_1 +read_ilang syn_#{idSim2}.il +rename #{modName m} #{modName m}_2 read_verilog top.v proc; opt_clean -flatten #{modName} +flatten #{modName m} ! touch test.#{toText sim1}.#{idSim2}.input_ok -sat -timeout 20 -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{modName} +sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{modName m} |] where idSim2 = maybe "rtl" toText sim2 - modName = m ^. moduleId . getIdentifier -- ids = T.intercalate "," $ allVars m ^.. traverse . getIdentifier runOtherSynth :: (Synthesize a) => Maybe a -> ModDecl -> Sh () diff --git a/src/VeriFuzz/Verilog/AST.hs b/src/VeriFuzz/Verilog/AST.hs index b3754ec..f940281 100644 --- a/src/VeriFuzz/Verilog/AST.hs +++ b/src/VeriFuzz/Verilog/AST.hs @@ -91,7 +91,7 @@ module VeriFuzz.Verilog.AST , stmntSysTask -- * Module , ModDecl(..) - , moduleId + , modId , modOutPorts , modInPorts , modItems @@ -495,7 +495,7 @@ instance QC.Arbitrary ModItem where ] -- | 'module' module_identifier [list_of_ports] ';' { module_item } 'end_module' -data ModDecl = ModDecl { _moduleId :: Identifier +data ModDecl = ModDecl { _modId :: Identifier , _modOutPorts :: [Port] , _modInPorts :: [Port] , _modItems :: [ModItem] diff --git a/src/VeriFuzz/Verilog/CodeGen.hs b/src/VeriFuzz/Verilog/CodeGen.hs index 956472f..58b1d16 100644 --- a/src/VeriFuzz/Verilog/CodeGen.hs +++ b/src/VeriFuzz/Verilog/CodeGen.hs @@ -53,7 +53,7 @@ genDescription desc = genModuleDecl $ desc ^. getDescription -- | Generate the 'ModDecl' for a module and convert it to 'Text'. genModuleDecl :: ModDecl -> Text genModuleDecl m = - "module " <> m ^. moduleId . getIdentifier <> ports <> ";\n" <> modI <> "endmodule\n" + "module " <> m ^. modId . getIdentifier <> ports <> ";\n" <> modI <> "endmodule\n" where ports | noIn && noOut = "" | otherwise = "(" <> comma (genModPort <$> outIn) <> ")" diff --git a/src/VeriFuzz/Verilog/Helpers.hs b/src/VeriFuzz/Verilog/Helpers.hs index 4771329..99e5f38 100644 --- a/src/VeriFuzz/Verilog/Helpers.hs +++ b/src/VeriFuzz/Verilog/Helpers.hs @@ -28,7 +28,7 @@ emptyMod = ModDecl "" [] [] [] -- | Set a module name for a module declaration. setModName :: Text -> ModDecl -> ModDecl -setModName str = moduleId .~ Identifier str +setModName str = modId .~ Identifier str -- | Add a input port to the module declaration. addModPort :: Port -> ModDecl -> ModDecl @@ -67,3 +67,6 @@ defaultPort = Port Wire 1 portToExpr :: Port -> Expr portToExpr (Port _ _ i) = Id i + +modName :: ModDecl -> Text +modName = view $ modId . getIdentifier diff --git a/src/VeriFuzz/Verilog/Mutate.hs b/src/VeriFuzz/Verilog/Mutate.hs index 82d3db9..dca0dd9 100644 --- a/src/VeriFuzz/Verilog/Mutate.hs +++ b/src/VeriFuzz/Verilog/Mutate.hs @@ -92,8 +92,8 @@ instantiateMod m main = main & modItems %~ ((out ++ regIn ++ [inst]) ++) where out = Decl Nothing <$> m ^. modOutPorts regIn = Decl Nothing <$> (m ^. modInPorts & traverse . portType .~ Reg False) - inst = ModInst (m ^. moduleId) (m ^. moduleId <> (Identifier . showT $ count + 1)) conns - count = length . filter (== m ^. moduleId) $ main ^.. modItems . traverse . modInstId + inst = ModInst (m ^. modId) (m ^. modId <> (Identifier . showT $ count + 1)) conns + count = length . filter (== m ^. modId) $ main ^.. modItems . traverse . modInstId conns = ModConn . Id <$> allVars m -- | Instantiate without adding wire declarations. It also does not count the @@ -103,7 +103,7 @@ instantiateMod m main = main & modItems %~ ((out ++ regIn ++ [inst]) ++) -- m m(y, x); -- instantiateMod_ :: ModDecl -> ModItem -instantiateMod_ m = ModInst (m ^. moduleId) (m ^. moduleId) conns +instantiateMod_ m = ModInst (m ^. modId) (m ^. modId) conns where conns = ModConn @@ -131,8 +131,8 @@ makeIdFrom a i = (i <>) . Identifier . ("_" <>) $ showT a -- | Make top level module for equivalence verification. Also takes in how many -- modules to instantiate. makeTop :: Int -> ModDecl -> ModDecl -makeTop i m = ModDecl (m ^. moduleId) ys (m ^. modInPorts) modIt +makeTop i m = ModDecl (m ^. modId) ys (m ^. modInPorts) modIt where ys = Port Wire 90 . flip makeIdFrom "y" <$> [1 .. i] modIt = instantiateMod_ . modN <$> [1 .. i] - modN n = m & moduleId %~ makeIdFrom n & modOutPorts .~ [Port Wire 90 (makeIdFrom n "y")] + modN n = m & modId %~ makeIdFrom n & modOutPorts .~ [Port Wire 90 (makeIdFrom n "y")] diff --git a/test/Unit.hs b/test/Unit.hs index 8bcc702..4570357 100644 --- a/test/Unit.hs +++ b/test/Unit.hs @@ -12,6 +12,7 @@ unitTests = testGroup "Unit tests" [ testCase "Transformation of AST" $ assertEqual "Successful transformation" transformExpectedResult (transformOf traverseExpr trans transformTestData) + , testCase "" ] transformTestData :: Expr -- cgit