aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--app/Main.hs8
-rw-r--r--src/VeriFuzz/Simulator.hs14
-rw-r--r--src/VeriFuzz/Simulator/Xst.hs2
-rw-r--r--src/VeriFuzz/Simulator/Yosys.hs18
-rw-r--r--src/VeriFuzz/Verilog/AST.hs4
-rw-r--r--src/VeriFuzz/Verilog/CodeGen.hs2
-rw-r--r--src/VeriFuzz/Verilog/Helpers.hs5
-rw-r--r--src/VeriFuzz/Verilog/Mutate.hs10
-rw-r--r--test/Unit.hs1
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);
-- <BLANKLINE>
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
generated by cgit (git 2.34.1) at 2024-06-28 21:26:15 +0000