From 5025a43948a682bc40d5c91606ec97cd8d6c3897 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Grave Date: Sat, 16 Feb 2019 20:19:00 +0000 Subject: Change Port type, adding signed info --- src/VeriFuzz/AST.hs | 22 +++++++++++----------- src/VeriFuzz/ASTGen.hs | 4 ++-- src/VeriFuzz/CodeGen.hs | 12 ++++++++---- src/VeriFuzz/Gen.hs | 17 +++++++++-------- src/VeriFuzz/Internal/AST.hs | 17 +++++++++++++---- src/VeriFuzz/Mutate.hs | 8 ++++---- 6 files changed, 47 insertions(+), 33 deletions(-) (limited to 'src') diff --git a/src/VeriFuzz/AST.hs b/src/VeriFuzz/AST.hs index f5d1824..34d9327 100644 --- a/src/VeriFuzz/AST.hs +++ b/src/VeriFuzz/AST.hs @@ -47,9 +47,9 @@ module VeriFuzz.AST -- ** Ports , PortDir(..) , PortType(..) - , regSigned , Port(..) , portType + , portSigned , portSize , portName -- * Expression @@ -411,11 +411,11 @@ instance QC.Arbitrary PortDir where -- | Currently, only @wire@ and @reg@ are supported, as the other net types are -- not that common and not a priority. data PortType = Wire - | Reg { _regSigned :: Bool } + | Reg deriving (Eq, Show, Data) instance QC.Arbitrary PortType where - arbitrary = QC.oneof [pure Wire, Reg <$> QC.arbitrary] + arbitrary = QC.elements [Wire, Reg] makeLenses ''PortType @@ -427,15 +427,17 @@ makeLenses ''PortType -- -- This is now implemented inside 'ModDecl' itself, which uses a list of output -- and input ports. -data Port = Port { _portType :: PortType - , _portSize :: Int - , _portName :: Identifier +data Port = Port { _portType :: PortType + , _portSigned :: Bool + , _portSize :: Int + , _portName :: Identifier } deriving (Eq, Show, Data) makeLenses ''Port instance QC.Arbitrary Port where - arbitrary = Port <$> QC.arbitrary <*> positiveArb <*> QC.arbitrary + arbitrary = Port <$> QC.arbitrary <*> QC.arbitrary + <*> positiveArb <*> QC.arbitrary -- | This is currently a type because direct module declaration should also be -- added: @@ -565,10 +567,8 @@ traverseModItem _ e = pure e makeLenses ''ModDecl modPortGen :: QC.Gen Port -modPortGen = QC.oneof - [ Port Wire <$> positiveArb <*> QC.arbitrary - , Port <$> (Reg <$> QC.arbitrary) <*> positiveArb <*> QC.arbitrary - ] +modPortGen = Port <$> QC.arbitrary <*> QC.arbitrary + <*> QC.arbitrary <*> QC.arbitrary instance QC.Arbitrary ModDecl where arbitrary = ModDecl <$> QC.arbitrary <*> QC.arbitrary <*> QC.listOf1 modPortGen <*> QC.arbitrary diff --git a/src/VeriFuzz/ASTGen.hs b/src/VeriFuzz/ASTGen.hs index 6bac157..ff948c3 100644 --- a/src/VeriFuzz/ASTGen.hs +++ b/src/VeriFuzz/ASTGen.hs @@ -38,7 +38,7 @@ inputsC :: Circuit -> [Node] inputsC c = inputs (getCircuit c) genPortsAST :: (Circuit -> [Node]) -> Circuit -> [Port] -genPortsAST f c = port . frNode <$> f c where port = Port Wire 4 +genPortsAST f c = port . frNode <$> f c where port = Port Wire False 4 -- | Generates the nested expression AST, so that it can then generate the -- assignment expressions. @@ -71,7 +71,7 @@ genModuleDeclAST c = ModDecl i output ports items where i = Identifier "gen_module" ports = genPortsAST inputsC c - output = [Port Wire 90 "y"] + output = [Port Wire False 90 "y"] a = genAssignAST c items = a ++ [ModCA . ContAssign "y" . fold $ Id <$> assigns] assigns = a ^.. traverse . modContAssign . contAssignNetLVal diff --git a/src/VeriFuzz/CodeGen.hs b/src/VeriFuzz/CodeGen.hs index f35eff7..3e36cf5 100644 --- a/src/VeriFuzz/CodeGen.hs +++ b/src/VeriFuzz/CodeGen.hs @@ -68,12 +68,17 @@ genModPort port = port ^. portName . getIdentifier -- | Generate the 'Port' description. genPort :: Port -> Text -genPort port = t <> size <> name +genPort port = t <> sign <> size <> name where - t = (<> " ") . genPortType $ port ^. portType + t = flip mappend " " . genPortType $ port ^. portType size | port ^. portSize > 1 = "[" <> showT (port ^. portSize - 1) <> ":0] " | otherwise = "" name = port ^. portName . getIdentifier + sign = genSigned $ port ^. portSigned + +genSigned :: Bool -> Text +genSigned True = "signed " +genSigned _ = "" -- | Convert the 'PortDir' type to 'Text'. genPortDir :: PortDir -> Text @@ -188,8 +193,7 @@ genConstExpr (ConstExpr num) = showT num genPortType :: PortType -> Text genPortType Wire = "wire" -genPortType (Reg signed) | signed = "reg signed" - | otherwise = "reg" +genPortType Reg = "reg" genAssign :: Text -> Assign -> Text genAssign op (Assign r d e) = genLVal r <> op <> maybe "" genDelay d <> genExpr e diff --git a/src/VeriFuzz/Gen.hs b/src/VeriFuzz/Gen.hs index c246e4e..6eb8723 100644 --- a/src/VeriFuzz/Gen.hs +++ b/src/VeriFuzz/Gen.hs @@ -13,12 +13,13 @@ Various useful generators. module VeriFuzz.Gen where import Control.Lens -import Data.Foldable (fold) -import qualified Data.Text as T -import Test.QuickCheck (Gen) -import qualified Test.QuickCheck as QC +import Data.Foldable (fold) +import qualified Data.Text as T +import Test.QuickCheck (Gen) +import qualified Test.QuickCheck as QC import VeriFuzz.AST import VeriFuzz.ASTGen +import VeriFuzz.Internal import VeriFuzz.Mutate import VeriFuzz.Random @@ -28,7 +29,7 @@ toId = Identifier . ("w"<>) . T.pack . show toPort :: Identifier -> Gen Port toPort ident = do i <- abs <$> QC.arbitrary - return $ Port Wire i ident + return $ wire i ident sumSize :: [Port] -> Int sumSize ports = @@ -52,11 +53,11 @@ randomMod :: Int -> Int -> Gen ModDecl randomMod inps total = do x <- sequence $ randomOrdAssigns start end ident <- sequence $ toPort <$> ids - let inputs = take inps ident + let inputs_ = take inps ident let other = drop inps ident let y = ModCA . ContAssign "y" . fold $ Id <$> drop inps ids - let yport = [Port Wire (sumSize other) "y"] - return . initMod . declareMod other . ModDecl "test_module" yport inputs $ x ++ [y] + let yport = [wire (sumSize other) "y"] + return . initMod . declareMod other . ModDecl "test_module" yport inputs_ $ x ++ [y] where ids = toId <$> [1..total] end = drop inps ids diff --git a/src/VeriFuzz/Internal/AST.hs b/src/VeriFuzz/Internal/AST.hs index b8f569b..95f3bfc 100644 --- a/src/VeriFuzz/Internal/AST.hs +++ b/src/VeriFuzz/Internal/AST.hs @@ -17,10 +17,10 @@ import Data.Text (Text) import VeriFuzz.AST regDecl :: Identifier -> ModItem -regDecl = Decl Nothing . Port (Reg False) 1 +regDecl = Decl Nothing . Port Reg False 1 wireDecl :: Identifier -> ModItem -wireDecl = Decl Nothing . Port Wire 1 +wireDecl = Decl Nothing . Port Wire False 1 -- | Create an empty module. emptyMod :: ModDecl @@ -63,10 +63,19 @@ addTestBench :: VerilogSrc -> VerilogSrc addTestBench = addDescription $ Description testBench defaultPort :: Identifier -> Port -defaultPort = Port Wire 1 +defaultPort = Port Wire False 1 portToExpr :: Port -> Expr -portToExpr (Port _ _ i) = Id i +portToExpr (Port _ _ _ i) = Id i modName :: ModDecl -> Text modName = view $ modId . getIdentifier + +yPort :: Identifier -> Port +yPort = Port Wire False 90 + +wire :: Int -> Identifier -> Port +wire = Port Wire False + +reg :: Int -> Identifier -> Port +reg = Port Reg False diff --git a/src/VeriFuzz/Mutate.hs b/src/VeriFuzz/Mutate.hs index b8b1f59..15eac90 100644 --- a/src/VeriFuzz/Mutate.hs +++ b/src/VeriFuzz/Mutate.hs @@ -97,7 +97,7 @@ instantiateMod :: ModDecl -> ModDecl -> ModDecl instantiateMod m main = main & modItems %~ ((out ++ regIn ++ [inst]) ++) where out = Decl Nothing <$> m ^. modOutPorts - regIn = Decl Nothing <$> (m ^. modInPorts & traverse . portType .~ Reg False) + regIn = Decl Nothing <$> (m ^. modInPorts & traverse . portType .~ Reg) 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 @@ -160,9 +160,9 @@ makeIdFrom a i = (i <>) . Identifier . ("_" <>) $ showT a makeTop :: Int -> ModDecl -> ModDecl makeTop i m = ModDecl (m ^. modId) ys (m ^. modInPorts) modIt where - ys = Port Wire 90 . flip makeIdFrom "y" <$> [1 .. i] + ys = yPort . flip makeIdFrom "y" <$> [1 .. i] modIt = instantiateModSpec_ "_" . modN <$> [1 .. i] - modN n = m & modId %~ makeIdFrom n & modOutPorts .~ [Port Wire 90 (makeIdFrom n "y")] + modN n = m & modId %~ makeIdFrom n & modOutPorts .~ [yPort (makeIdFrom n "y")] -- | 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. @@ -172,7 +172,7 @@ makeTopAssert = (modItems %~ (++ [assert])) . (modInPorts %~ addClk) . makeTop 2 assert = Always . EventCtrl e . Just $ SeqBlock [TaskEnable $ Task "assert" [BinOp (Id "y_1") BinEq (Id "y_2")]] e = EPosEdge "clk" - addClk = (Port Wire 1 "clk" :) + addClk = (defaultPort "clk" :) -- | Provide declarations for all the ports that are passed to it. declareMod :: [Port] -> ModDecl -> ModDecl -- cgit