diff options
Diffstat (limited to 'src/VeriFuzz')
-rw-r--r-- | src/VeriFuzz/Config.hs | 2 | ||||
-rw-r--r-- | src/VeriFuzz/Fuzz.hs | 60 | ||||
-rw-r--r-- | src/VeriFuzz/Reduce.hs | 6 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/CodeGen.hs | 4 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/Eval.hs | 21 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/Gen.hs | 38 |
6 files changed, 82 insertions, 49 deletions
diff --git a/src/VeriFuzz/Config.hs b/src/VeriFuzz/Config.hs index 9961667..fa06e46 100644 --- a/src/VeriFuzz/Config.hs +++ b/src/VeriFuzz/Config.hs @@ -287,7 +287,7 @@ exprCodec = <*> defaultValue (defProb probExprId) (intE "variable") .= _probExprId <*> defaultValue (defProb probExprRangeSelect) (intE "rangeselect") - .= _probExprRangeSelect + .= _probExprRangeSelect <*> defaultValue (defProb probExprUnOp) (intE "unary") .= _probExprUnOp <*> defaultValue (defProb probExprBinOp) (intE "binary") diff --git a/src/VeriFuzz/Fuzz.hs b/src/VeriFuzz/Fuzz.hs index 4680a03..57928b4 100644 --- a/src/VeriFuzz/Fuzz.hs +++ b/src/VeriFuzz/Fuzz.hs @@ -116,7 +116,11 @@ synthesis src = do liftSh . mkdir_p . fromText $ toText a pop (fromText $ toText a) $ runSynth a src -generateSample :: (MonadIO m, MonadSh m) => Maybe Seed -> Gen SourceInfo -> Fuzz m (Seed, SourceInfo) +generateSample + :: (MonadIO m, MonadSh m) + => Maybe Seed + -> Gen SourceInfo + -> Fuzz m (Seed, SourceInfo) generateSample seed gen = do logT "Sampling Verilog from generator" (t, v) <- timeit $ sampleSeed seed gen @@ -165,13 +169,20 @@ equivalence src = do fuzz :: MonadFuzz m => Gen SourceInfo -> Config -> Fuzz m FuzzReport fuzz gen conf = do (seed', src) <- generateSample seed gen - liftSh . writefile "config.toml" . encodeConfig $ conf & configProperty . propSeed .~ Just seed' + liftSh + . writefile "config.toml" + . encodeConfig + $ conf + & configProperty + . propSeed + .~ Just seed' synthesis src equivalence src return mempty where seed = conf ^. configProperty . propSeed -fuzzInDir :: MonadFuzz m => FilePath -> Gen SourceInfo -> Config -> Fuzz m FuzzReport +fuzzInDir + :: MonadFuzz m => FilePath -> Gen SourceInfo -> Config -> Fuzz m FuzzReport fuzzInDir fp src conf = do make fp pop fp $ fuzz src conf @@ -197,23 +208,32 @@ fuzzMultiple n fp src conf = do when (isNothing seed) . void . pop x . forM [1 .. n] $ fuzzDir unless (isNothing seed) . void . pop x $ fuzzDir (1 :: Int) return mempty - where fuzzDir n' = fuzzInDir (fromText $ "fuzz_" <> showT n') src conf - seed = conf ^. configProperty . propSeed + where + fuzzDir n' = fuzzInDir (fromText $ "fuzz_" <> showT n') src conf + seed = conf ^. configProperty . propSeed sampleSeed :: MonadIO m => Maybe Seed -> Gen a -> m (Seed, a) sampleSeed s gen = - liftIO $ - let - loop n = - if n <= 0 then - error "Hedgehog.Gen.sample: too many discards, could not generate a sample" - else do - seed <- maybe Hog.random return s - case runIdentity . runMaybeT . Hog.runTree $ Hog.runGenT 30 seed gen of - Nothing -> - loop (n - 1) - Just x -> do - liftIO . putStrLn $ "VeriFuzz: Chosen seed was '" <> show seed <> "'" - pure $ (seed, Hog.nodeValue x) - in - loop (100 :: Int) + liftIO + $ let + loop n = if n <= 0 + then + error + "Hedgehog.Gen.sample: too many discards, could not generate a sample" + else do + seed <- maybe Hog.random return s + case + runIdentity + . runMaybeT + . Hog.runTree + $ Hog.runGenT 30 seed gen + of + Nothing -> loop (n - 1) + Just x -> do + liftIO + . putStrLn + $ "VeriFuzz: Chosen seed was '" + <> show seed + <> "'" + pure $ (seed, Hog.nodeValue x) + in loop (100 :: Int) diff --git a/src/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs index cf7a302..e666f38 100644 --- a/src/VeriFuzz/Reduce.hs +++ b/src/VeriFuzz/Reduce.hs @@ -103,10 +103,10 @@ cleanMod m newm = modify . change <$> newm ^. modItems halveStatements :: Statement -> Replacement Statement -halveStatements (SeqBlock l) = SeqBlock <$> halve l +halveStatements (SeqBlock l ) = SeqBlock <$> halve l halveStatements (CondStmnt _ (Just a) b) = maybe (Single a) (Dual a) b -halveStatements (CondStmnt _ Nothing b) = maybe None Single b -halveStatements (ForLoop _ _ _ s) = Single s +halveStatements (CondStmnt _ Nothing b) = maybe None Single b +halveStatements (ForLoop _ _ _ s ) = Single s halveStatements _ = None -- | Split a module declaration in half by trying to remove assign statements. diff --git a/src/VeriFuzz/Verilog/CodeGen.hs b/src/VeriFuzz/Verilog/CodeGen.hs index af255a2..f20d959 100644 --- a/src/VeriFuzz/Verilog/CodeGen.hs +++ b/src/VeriFuzz/Verilog/CodeGen.hs @@ -138,8 +138,8 @@ expr (BinOp eRhs bin eLhs) = "(" <> expr eRhs <> binaryOp bin <> expr eLhs <> ")" expr (Number b ) = showNum b expr (Id i ) = getIdentifier i -expr (VecSelect i e) = getIdentifier i <> "[" <> expr e <> "]" -expr (RangeSelect i r) = getIdentifier i <> range r +expr (VecSelect i e ) = getIdentifier i <> "[" <> expr e <> "]" +expr (RangeSelect i r ) = getIdentifier i <> range r expr (Concat c ) = "{" <> comma (expr <$> c) <> "}" expr (UnOp u e ) = "(" <> unaryOp u <> expr e <> ")" expr (Cond l t f) = "(" <> expr l <> " ? " <> expr t <> " : " <> expr f <> ")" diff --git a/src/VeriFuzz/Verilog/Eval.hs b/src/VeriFuzz/Verilog/Eval.hs index 5dbee8c..4a43c19 100644 --- a/src/VeriFuzz/Verilog/Eval.hs +++ b/src/VeriFuzz/Verilog/Eval.hs @@ -92,10 +92,9 @@ applyBinary BinASR = toInt shiftR evaluateConst :: Bindings -> ConstExprF BitVec -> BitVec evaluateConst _ (ConstNumF b) = b evaluateConst p (ParamIdF i) = - cata (evaluateConst p) - . maybe 0 paramValue_ - . listToMaybe - $ filter ((== i) . paramIdent_) p + cata (evaluateConst p) . maybe 0 paramValue_ . listToMaybe $ filter + ((== i) . paramIdent_) + p evaluateConst _ (ConstConcatF c ) = fold c evaluateConst _ (ConstUnOpF unop c ) = applyUnary unop c evaluateConst _ (ConstBinOpF a binop b) = applyBinary binop a b @@ -105,16 +104,16 @@ evaluateConst _ (ConstStrF _ ) = 0 -- | Apply a function to all the bitvectors. Would be fixed by having a -- 'Functor' instance for a polymorphic 'ConstExpr'. applyBitVec :: (BitVec -> BitVec) -> ConstExpr -> ConstExpr -applyBitVec f (ConstNum b) = ConstNum $ f b -applyBitVec f (ConstConcat c) = ConstConcat $ fmap (applyBitVec f) c +applyBitVec f (ConstNum b ) = ConstNum $ f b +applyBitVec f (ConstConcat c ) = ConstConcat $ fmap (applyBitVec f) c applyBitVec f (ConstUnOp unop c) = ConstUnOp unop $ applyBitVec f c -applyBitVec f (ConstBinOp a binop b) = ConstBinOp (applyBitVec f a) binop (applyBitVec f b) -applyBitVec f (ConstCond a b c) = ConstCond (abv a) (abv b) (abv c) where abv = applyBitVec f +applyBitVec f (ConstBinOp a binop b) = + ConstBinOp (applyBitVec f a) binop (applyBitVec f b) +applyBitVec f (ConstCond a b c) = ConstCond (abv a) (abv b) (abv c) + where abv = applyBitVec f applyBitVec _ a = a -- | This probably could be implemented using some recursion scheme in the -- future. It would also be fixed by having a polymorphic expression type. resize :: Int -> ConstExpr -> ConstExpr -resize n = applyBitVec (resize' n) - where - resize' n' (BitVec _ a) = BitVec n' a +resize n = applyBitVec (resize' n) where resize' n' (BitVec _ a) = BitVec n' a diff --git a/src/VeriFuzz/Verilog/Gen.hs b/src/VeriFuzz/Verilog/Gen.hs index bc5d329..5306d83 100644 --- a/src/VeriFuzz/Verilog/Gen.hs +++ b/src/VeriFuzz/Verilog/Gen.hs @@ -75,7 +75,8 @@ random ctx fun = do randomOrdAssigns :: [Port] -> [Port] -> [Gen ModItem] randomOrdAssigns inp ids = snd $ foldr generate (inp, []) ids - where generate cid (i, o) = (cid : i, random i (ContAssign (_portName cid)) : o) + where + generate cid (i, o) = (cid : i, random i (ContAssign (_portName cid)) : o) randomMod :: Int -> Int -> Gen ModDecl randomMod inps total = do @@ -186,7 +187,7 @@ constExprWithContext ps prob size where subexpr y = constExprWithContext ps prob $ size `div` y exprSafeList :: ProbExpr -> [(Int, Gen Expr)] -exprSafeList prob = [ (prob ^. probExprNum, Number <$> genBitVec)] +exprSafeList prob = [(prob ^. probExprNum, Number <$> genBitVec)] exprRecList :: ProbExpr -> (Hog.Size -> Gen Expr) -> [(Int, Gen Expr)] exprRecList prob subexpr = @@ -206,11 +207,12 @@ rangeSelect ps ports = do let s = calcRange ps (Just 32) $ _portSize p msb <- Hog.int (Hog.constantFrom (s `div` 2) 0 (s - 1)) lsb <- Hog.int (Hog.constantFrom (msb `div` 2) 0 msb) - return . RangeSelect (_portName p) $ Range (fromIntegral msb) (fromIntegral lsb) + return . RangeSelect (_portName p) $ Range (fromIntegral msb) + (fromIntegral lsb) exprWithContext :: ProbExpr -> [Parameter] -> [Port] -> Hog.Size -> Gen Expr -exprWithContext prob ps [] n | n == 0 = Hog.frequency $ exprSafeList prob - | n > 0 = Hog.frequency $ exprRecList prob subexpr +exprWithContext prob ps [] n | n == 0 = Hog.frequency $ exprSafeList prob + | n > 0 = Hog.frequency $ exprRecList prob subexpr | otherwise = exprWithContext prob ps [] 0 where subexpr y = exprWithContext prob ps [] $ n `div` y exprWithContext prob ps l n @@ -220,7 +222,7 @@ exprWithContext prob ps l n : exprSafeList prob | n > 0 = Hog.frequency - $ (prob ^. probExprId, Id . fromPort <$> Hog.element l) + $ (prob ^. probExprId , Id . fromPort <$> Hog.element l) : (prob ^. probExprRangeSelect, rangeSelect ps l) : exprRecList prob subexpr | otherwise @@ -255,7 +257,10 @@ scopedExpr :: StateGen Expr scopedExpr = do context <- get prob <- askProbability - gen . Hog.sized . exprWithContext (_probExpr prob) (_parameters context) $ _variables context + gen + . Hog.sized + . exprWithContext (_probExpr prob) (_parameters context) + $ _variables context contAssign :: StateGen ContAssign contAssign = do @@ -455,7 +460,8 @@ evalRange ps n (Range l r) = Range (eval l) (eval r) calcRange :: [Parameter] -> Maybe Int -> Range -> Int calcRange ps i (Range l r) = eval l - eval r + 1 - where eval a = fromIntegral . cata (evaluateConst ps) $ maybe a (flip resize a) i + where + eval a = fromIntegral . cata (evaluateConst ps) $ maybe a (flip resize a) i -- | Generates a module definition randomly. It always has one output port which -- is set to @y@. The size of @y@ is the total combination of all the locally @@ -466,15 +472,23 @@ moduleDef top = do name <- moduleName top portList <- some $ newPort Wire mi <- Hog.list (Hog.linear 4 100) modItem - ps <- many parameter + ps <- many parameter context <- get let local = filter (`notElem` portList) $ _variables context - let size = evalRange (_parameters context) 32 . sum $ local ^.. traverse . portSize + let + size = + evalRange (_parameters context) 32 + . sum + $ local + ^.. traverse + . portSize let clock = Port Wire False 1 "clk" let yport = Port Wire False size "y" let comb = combineAssigns_ yport local - return . declareMod local - . ModDecl name [yport] (clock : portList) (mi <> [comb]) $ ps + return + . declareMod local + . ModDecl name [yport] (clock : portList) (mi <> [comb]) + $ ps -- | Procedural generation method for random Verilog. Uses internal 'Reader' and -- 'State' to keep track of the current Verilog code structure. |