From 24cf9ce5bf673615ebe36f5ab5d0ff7685dfada6 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 25 Jun 2019 22:32:21 +0100 Subject: Add back the simulation --- README.md | 7 ++++-- data/cells_xilinx_7.v | 13 ----------- src/VeriFuzz/Fuzz.hs | 49 +++++++++++++++++++++++------------------ src/VeriFuzz/Sim/Icarus.hs | 52 ++++++++++++++++++++++---------------------- src/VeriFuzz/Sim/Template.hs | 2 +- 5 files changed, 60 insertions(+), 63 deletions(-) diff --git a/README.md b/README.md index 2d0588e..829f3b0 100644 --- a/README.md +++ b/README.md @@ -3,14 +3,17 @@ Verilog Fuzzer to test the major verilog compilers by generating random, valid verilog. -It currently supports the following simulators: +It currently supports the following synthesisers: - [Yosys](http://www.clifford.at/yosys/) -- [Icarus Verilog](http://iverilog.icarus.com) - [Xst](https://www.xilinx.com/support/documentation/sw_manuals/xilinx11/ise_c_using_xst_for_synthesis.htm) - [Vivado](https://www.xilinx.com/products/design-tools/ise-design-suite.html) - [Quartus](https://www.intel.com/content/www/us/en/programmable/downloads/download-center.html) +and the following simulator: + +- [Icarus Verilog](http://iverilog.icarus.com) + ## Build the Fuzzer The fuzzer is split into an executable (in the [app](/app) folder) and a diff --git a/data/cells_xilinx_7.v b/data/cells_xilinx_7.v index c757c2f..cc72893 100644 --- a/data/cells_xilinx_7.v +++ b/data/cells_xilinx_7.v @@ -971,19 +971,6 @@ module BUFGCTRL (O, CE0, CE1, I0, I1, IGNORE0, IGNORE1, S0, S1); end endmodule // BUFGCTRL -module BUFGDLL (O, I); - output O; - input I; - parameter DUTY_CYCLE_CORRECTION = "TRUE"; - wire clkin_int; - wire clk0_out, clk180_out, clk270_out, clk2x_out; - wire clk90_out, clkdv_out, locked_out; - CLKDLL clkdll_inst (.CLK0(clk0_out), .CLK180(clk180_out), .CLK270(clk270_out), .CLK2X(clk2x_out), .CLK90(clk90_out), .CLKDV(clkdv_out), .LOCKED(locked_out), .CLKFB(O), .CLKIN(clkin_int), .RST(1'b0)); - defparam clkdll_inst.DUTY_CYCLE_CORRECTION = DUTY_CYCLE_CORRECTION; - IBUFG ibufg_inst (.O(clkin_int), .I(I)); - BUFG bufg_inst (.O(O), .I(clk0_out)); -endmodule // BUFGDLL - module BUFG_LB ( CLKOUT, CLKIN diff --git a/src/VeriFuzz/Fuzz.hs b/src/VeriFuzz/Fuzz.hs index 3aeb0e0..181207c 100644 --- a/src/VeriFuzz/Fuzz.hs +++ b/src/VeriFuzz/Fuzz.hs @@ -37,6 +37,11 @@ import Control.Monad.Trans.Control (MonadBaseControl) import Control.Monad.Trans.Maybe (runMaybeT) import Control.Monad.Trans.Reader hiding (local) import Control.Monad.Trans.State.Strict +import qualified Crypto.Random.DRBG as C +import Data.ByteString (ByteString) +import Data.ByteString.Builder (byteStringHex, + toLazyByteString) +import qualified Data.ByteString.Lazy as L import Data.List (nubBy, sort) import Data.Maybe (isNothing) import Data.Text (Text) @@ -57,6 +62,7 @@ import VeriFuzz.Internal import VeriFuzz.Reduce import VeriFuzz.Report import VeriFuzz.Result +import VeriFuzz.Sim.Icarus import VeriFuzz.Sim.Internal import VeriFuzz.Sim.Yosys import VeriFuzz.Verilog.AST @@ -211,23 +217,17 @@ equivalence src = do runEquiv a b src where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b -simulation :: (MonadBaseControl IO m, MonadSh m) => SourceInfo -> Fuzz m () +simulation :: (MonadIO m, MonadSh m) => SourceInfo -> Fuzz m () simulation src = do synth <- passEquiv --- let synthComb = --- nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth - let synthComb = - nubBy tupEq - . filter (uncurry (/=)) - $ (,) defaultIdentitySynth - <$> synth - resTimes <- liftSh $ mapM (uncurry equiv) synthComb - fuzzSynthResults .= toSynthResult synthComb resTimes + vals <- liftIO $ generateByteString 20 + resTimes <- liftSh $ mapM (equiv vals) $ conv <$> synth liftSh $ inspect resTimes where tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a') - equiv a b = - toolRun ("equivalence check for " <> toText a <> " and " <> toText b) + conv (SynthResult a _ _ _) = a + equiv b a = + toolRun ("simulation for " <> toText a) . runResultT $ do make dir @@ -239,15 +239,22 @@ simulation src = do synthOutput a ) $ synthOutput a - cp - ( fromText ".." - fromText (toText b) - synthOutput b - ) - $ synthOutput b writefile "rtl.v" $ genSource src - runEquiv a b src - where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b + runSimIc defaultIcarus a src b + where dir = fromText $ "simulation_" <> toText a + +-- | Generate a specific number of random bytestrings of size 256. +randomByteString :: C.CtrDRBG -> Int -> [ByteString] -> [ByteString] +randomByteString gen n bytes + | n == 0 = ranBytes : bytes + | otherwise = randomByteString newGen (n - 1) $ ranBytes : bytes + where Right (ranBytes, newGen) = C.genBytes 32 gen + +-- | generates the specific number of bytestring with a random seed. +generateByteString :: Int -> IO [ByteString] +generateByteString n = do + gen <- C.newGenIO :: IO C.CtrDRBG + return $ randomByteString gen n [] failEquivWithIdentity :: (MonadSh m) => Fuzz m [SynthResult] failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get @@ -364,7 +371,7 @@ fuzz gen conf = do ?~ seed' (tsynth, _) <- titleRun "Synthesis" $ synthesis src (tequiv, _) <- titleRun "Equivalence Check" $ equivalence src - (tsim, _) <- titleRun "Equivalence Check" $ simulation src + (tsim, _) <- titleRun "Simulation" $ simulation src fails <- failEquivWithIdentity synthFails <- failedSynthesis redResult <- diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs index 6df2cf7..a5a3227 100644 --- a/src/VeriFuzz/Sim/Icarus.hs +++ b/src/VeriFuzz/Sim/Icarus.hs @@ -13,18 +13,21 @@ Icarus verilog module. module VeriFuzz.Sim.Icarus ( Icarus(..) , defaultIcarus + , runSimIc ) where import Control.DeepSeq (NFData, rnf, rwhnf) import Control.Lens +import Control.Monad (void) import Crypto.Hash (Digest, hash) import Crypto.Hash.Algorithms (SHA256) -import Data.Binary (encode) +import Data.Binary (decode, encode) +import Data.Bits import qualified Data.ByteArray as BA (convert) import Data.ByteString (ByteString) import qualified Data.ByteString as B -import Data.ByteString.Lazy (toStrict) +import Data.ByteString.Lazy (fromStrict, toStrict) import qualified Data.ByteString.Lazy as L (ByteString) import Data.Char (digitToInt) import Data.Foldable (fold) @@ -37,6 +40,7 @@ import Prelude hiding (FilePath) import Shelly import Shelly.Lifted (liftSh) import VeriFuzz.Sim.Internal +import VeriFuzz.Sim.Template import VeriFuzz.Verilog.AST import VeriFuzz.Verilog.BitVec import VeriFuzz.Verilog.CodeGen @@ -124,13 +128,18 @@ runSimIcarusWithFile sim f _ = annotate SimFail . liftSh $ do "vvp" (runFoldLines (mempty :: ByteString) callback (vvpPath sim) ["main"]) +fromBytes :: ByteString -> Integer +fromBytes = B.foldl' f 0 + where + f a b = a `shiftL` 8 .|. fromIntegral b + runSimIc - :: (Synthesiser a) => a -> SourceInfo -> [ByteString] -> ResultSh ByteString -runSimIc sim1 srcInfo bss = do + :: (Synthesiser b) => Icarus -> b -> SourceInfo -> [ByteString] -> ResultSh ByteString +runSimIc sim1 synth1 srcInfo bss = do dir <- liftSh pwd let top = srcInfo ^. mainModule let inConcat = (RegConcat (Id . fromPort <$> (top ^. modInPorts))) - let tb = ModDecl + let tb = instantiateMod top $ ModDecl "testbench" [] [] @@ -138,28 +147,19 @@ runSimIc sim1 srcInfo bss = do $ fold [ BlockAssign (Assign "clk" Nothing 0) , BlockAssign (Assign inConcat Nothing 0) ] - <> (SysTaskEnable $ Task "finish" []) - , Always . TimeCtrl 5 $ BlockAssign (Assign "clk" Nothing (UnNot (Id "clk"))) - , Always . EventCtrl (EPosEdge "clk") $ SysTaskEnable $ Task "strobe" ["%b", Id "y"] + <> fold ((\r -> TimeCtrl 10 (Just $ BlockAssign (Assign inConcat Nothing r))) + . fromInteger . fromBytes <$> bss) + <> (SysTaskEnable $ Task "finish" []) + , Always . TimeCtrl 5 . Just $ BlockAssign (Assign "clk" Nothing (UnOp UnNot (Id "clk"))) + , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable $ Task "strobe" ["%b", Id "y"] ] [] - liftSh $ do - writefile "top.v" - . genSource - . initMod - . makeTopAssert - $ srcInfo - ^. mainModule - replaceMods (synthOutput sim1) "_1" srcInfo - replaceMods (synthOutput sim2) "_2" srcInfo - writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo - e <- liftSh $ do - exe dir "symbiyosys" "sby" ["-f", "proof.sby"] - lastExitCode - case e of - 0 -> ResultT . return $ Pass () - 2 -> ResultT . return $ Fail EquivFail - 124 -> ResultT . return $ Fail TimeoutError - _ -> ResultT . return $ Fail EquivError + + liftSh . writefile "testbench.v" $ icarusTestbench (Verilog [tb]) synth1 + liftSh $ exe dir "icarus" "iverilog" ["-o", "main", "testbench.v"] + liftSh $ B.take 8 . BA.convert . (hash :: ByteString -> Digest SHA256) <$> logCommand + dir + "vvp" + (runFoldLines (mempty :: ByteString) callback (vvpPath sim1) ["main"]) where exe dir name e = void . errExit False . logCommand dir name . timeout e diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs index 913b220..3be6558 100644 --- a/src/VeriFuzz/Sim/Template.hs +++ b/src/VeriFuzz/Sim/Template.hs @@ -127,7 +127,7 @@ icarusTestbench t synth1 = [st| `include "data/cells_verific.v" `include "data/cells_xilinx_7.v" `include "data/cells_yosys.v" -`include "#{synthOutput synth1}" +`include "#{toTextIgnore $ synthOutput synth1}" #{genSource t} |] -- cgit