From 11bd73faa516cde0af74e5359c36c8f1fa4e816a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 25 May 2019 23:26:27 +0100 Subject: Fix reduction for statements --- src/VeriFuzz.hs | 7 ++-- src/VeriFuzz/Reduce.hs | 26 ++++++++------- src/VeriFuzz/Verilog.hs | 2 ++ test/Reduce.hs | 89 +++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 109 insertions(+), 15 deletions(-) diff --git a/src/VeriFuzz.hs b/src/VeriFuzz.hs index 6d4f839..4b9878d 100644 --- a/src/VeriFuzz.hs +++ b/src/VeriFuzz.hs @@ -400,9 +400,10 @@ handleOpts (Reduce f t _ ls' True) = do runSynth b src runEquiv a b src case res of - Pass _ -> putStrLn "Equivalence check passed" - Fail EquivFail -> error "Equivalence check failed" - Fail _ -> error "Equivalence check errored out" + Pass _ -> putStrLn "Equivalence check passed" + Fail EquivFail -> putStrLn "Equivalence check failed" + Fail TimeoutError -> putStrLn "Equivalence check timed out" + Fail _ -> putStrLn "Equivalence check error" return () as -> do putStrLn "Synthesis check" diff --git a/src/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs index b025a42..2f44c07 100644 --- a/src/VeriFuzz/Reduce.hs +++ b/src/VeriFuzz/Reduce.hs @@ -35,27 +35,28 @@ module VeriFuzz.Reduce ) where -import Control.Lens hiding ((<.>)) -import Control.Monad (void) -import Control.Monad.IO.Class (MonadIO, liftIO) -import Data.Foldable (foldrM) -import Data.List (nub) -import Data.List.NonEmpty (NonEmpty (..)) -import qualified Data.List.NonEmpty as NonEmpty -import Data.Maybe (mapMaybe) -import Data.Text (Text) -import Shelly ((<.>)) +import Control.Lens hiding ((<.>)) +import Control.Monad (void) +import Control.Monad.IO.Class (MonadIO, liftIO) +import Data.Foldable (foldrM) +import Data.List (nub) +import Data.List.NonEmpty (NonEmpty (..)) +import qualified Data.List.NonEmpty as NonEmpty +import Data.Maybe (mapMaybe) +import Data.Text (Text) +import Shelly ((<.>)) import qualified Shelly -import Shelly.Lifted (MonadSh, liftSh) +import Shelly.Lifted (MonadSh, liftSh) import VeriFuzz.Internal import VeriFuzz.Result import VeriFuzz.Sim import VeriFuzz.Sim.Internal +import VeriFuzz.Verilog import VeriFuzz.Verilog.AST -import VeriFuzz.Verilog.CodeGen import VeriFuzz.Verilog.Mutate import VeriFuzz.Verilog.Parser + -- $strategy -- The reduction strategy has multiple different steps. 'reduce' will run these -- strategies one after another, starting at the most coarse grained one. The @@ -334,6 +335,7 @@ matchesModName :: Identifier -> ModDecl -> Bool matchesModName top (ModDecl i _ _ _ _) = top == i halveStatement :: Replace Statement +halveStatement (SeqBlock [s]) = halveStatement s halveStatement (SeqBlock s) = SeqBlock <$> halve s halveStatement (CondStmnt _ (Just s1) (Just s2)) = Dual s1 s2 halveStatement (CondStmnt _ (Just s1) Nothing) = Single s1 diff --git a/src/VeriFuzz/Verilog.hs b/src/VeriFuzz/Verilog.hs index 3e8d2c7..628b00a 100644 --- a/src/VeriFuzz/Verilog.hs +++ b/src/VeriFuzz/Verilog.hs @@ -10,6 +10,8 @@ Portability : POSIX Verilog implementation with random generation and mutations. -} +{-# LANGUAGE QuasiQuotes #-} + module VeriFuzz.Verilog ( SourceInfo(..) , Verilog(..) diff --git a/test/Reduce.hs b/test/Reduce.hs index bc4bbc3..be5ead3 100644 --- a/test/Reduce.hs +++ b/test/Reduce.hs @@ -29,6 +29,7 @@ reduceUnitTests = testGroup [ moduleReducerTest , modItemReduceTest , halveStatementsTest + , statementReducerTest , activeWireTest , cleanTest , cleanAllTest @@ -371,6 +372,94 @@ module top(y, x); endmodule |]) +-- brittany-disable-next-binding +statementReducerTest :: TestTree +statementReducerTest = testCase "Statement reducer" $ do + GenVerilog <$> halveStatements "top" srcInfo1 @?= fmap GenVerilog golden1 + GenVerilog <$> halveStatements "top" srcInfo2 @?= fmap GenVerilog golden2 + where + srcInfo1 = SourceInfo "top" [verilog| +module top(y, x); + output wire [4:0] y; + input wire [4:0] x; + + always @(posedge clk) begin + a <= 1; + b <= 2; + c <= 3; + d <= 4; + end + + always @(posedge clk) begin + a <= 1; + b <= 2; + c <= 3; + d <= 4; + end +endmodule +|] + golden1 = Dual (SourceInfo "top" [verilog| +module top(y, x); + output wire [4:0] y; + input wire [4:0] x; + + always @(posedge clk) begin + a <= 1; + b <= 2; + end + + always @(posedge clk) begin + a <= 1; + b <= 2; + end +endmodule +|]) $ SourceInfo "top" [verilog| +module top(y, x); + output wire [4:0] y; + input wire [4:0] x; + + always @(posedge clk) begin + c <= 3; + d <= 4; + end + + always @(posedge clk) begin + c <= 3; + d <= 4; + end +endmodule +|] + srcInfo2 = SourceInfo "top" [verilog| +module top(y, x); + output wire [4:0] y; + input wire [4:0] x; + + always @(posedge clk) begin + if (x) + y <= 2; + else + y <= 3; + end +endmodule +|] + golden2 = Dual (SourceInfo "top" [verilog| +module top(y, x); + output wire [4:0] y; + input wire [4:0] x; + + always @(posedge clk) + y <= 2; +endmodule +|]) $ SourceInfo "top" [verilog| +module top(y, x); + output wire [4:0] y; + input wire [4:0] x; + + always @(posedge clk) + y <= 3; +endmodule +|] + -- brittany-disable-next-binding moduleReducerTest :: TestTree moduleReducerTest = testCase "Module reducer" $ do -- cgit