aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--app/Main.hs149
-rw-r--r--bugs/vivado/1_generated.v31
-rw-r--r--bugs/vivado/1_minimal.v8
-rw-r--r--bugs/vivado/1_original.v501
-rw-r--r--bugs/vivado/2_minimal.v28
-rw-r--r--bugs/vivado/2_original.v44
-rw-r--r--scripts/setup.sh6
-rw-r--r--src/VeriFuzz.hs21
-rw-r--r--src/VeriFuzz/Circuit.hs1
-rw-r--r--src/VeriFuzz/Circuit/Gen.hs8
-rw-r--r--src/VeriFuzz/Config.hs175
-rw-r--r--src/VeriFuzz/Internal.hs5
-rw-r--r--src/VeriFuzz/RecursionScheme.hs84
-rw-r--r--src/VeriFuzz/Sim/Icarus.hs3
-rw-r--r--src/VeriFuzz/Sim/Internal.hs6
-rw-r--r--src/VeriFuzz/Sim/Reduce.hs4
-rw-r--r--src/VeriFuzz/Sim/Template.hs2
-rw-r--r--src/VeriFuzz/Verilog.hs10
-rw-r--r--src/VeriFuzz/Verilog/AST.hs336
-rw-r--r--src/VeriFuzz/Verilog/CodeGen.hs115
-rw-r--r--src/VeriFuzz/Verilog/Gen.hs336
-rw-r--r--src/VeriFuzz/Verilog/Internal.hs25
-rw-r--r--src/VeriFuzz/Verilog/Mutate.hs46
-rw-r--r--src/VeriFuzz/Verilog/Parser.hs14
-rw-r--r--src/VeriFuzz/Verilog/Preprocess.hs7
-rw-r--r--test/Property.hs10
26 files changed, 1451 insertions, 524 deletions
diff --git a/app/Main.hs b/app/Main.hs
index 8b5605b..f20bc59 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -23,10 +23,8 @@ data Opts = Fuzz { fuzzOutput :: {-# UNPACK #-} !Text
, forced :: !Bool
, keepAll :: !Bool
}
- | Rerun { tools :: [Tool]
- , input :: {-# UNPACK #-} !S.FilePath
- }
- | Generate { fileName :: {-# UNPACK #-} !S.FilePath
+ | Generate { mFileName :: !(Maybe FilePath)
+ , configFile :: !(Maybe FilePath)
}
| Parse { fileName :: {-# UNPACK #-} !S.FilePath
}
@@ -59,70 +57,47 @@ parseSim val | val == "icarus" = Just Icarus
| otherwise = Nothing
fuzzOpts :: Parser Opts
-fuzzOpts = Fuzz <$> textOption
- ( long "output"
- <> short 'o'
- <> metavar "DIR"
- <> help "Output directory that the fuzz run takes place in."
- <> showDefault
- <> value "output"
- ) <*> (optional . strOption $
- long "config"
- <> short 'c'
- <> metavar "FILE"
- <> help "Config file for the current fuzz run."
- )
- <*> (switch $
- long "force"
- <> short 'f'
- <> help "Overwrite the specified directory."
- )
- <*> (switch $
- long "keep"
- <> short 'k'
- <> help "Keep all the directories."
- )
-
-rerunOpts :: Parser Opts
-rerunOpts =
- Rerun
- <$> some
- ( option
- (optReader parseSynth)
- ( long "synth"
- <> metavar "SYNTH"
- <> help "Rerun using a synthesiser (yosys|xst)."
- <> showDefault
- <> value Yosys
- )
- <|> option
- (optReader parseSim)
- ( long "sim"
- <> metavar "SIM"
- <> help "Rerun using a simulator (icarus)."
- <> showDefault
- <> value Icarus
- )
- )
- <*> (S.fromText <$> textOption
- ( long "input"
- <> short 'i'
- <> metavar "FILE"
- <> help "Verilog file input."
+fuzzOpts =
+ Fuzz
+ <$> textOption
+ ( long "output"
+ <> short 'o'
+ <> metavar "DIR"
+ <> help "Output directory that the fuzz run takes place in."
<> showDefault
- <> value "rtl.v"
+ <> value "output"
)
+ <*> ( optional
+ . strOption
+ $ long "config"
+ <> short 'c'
+ <> metavar "FILE"
+ <> help "Config file for the current fuzz run."
+ )
+ <*> (switch $ long "force" <> short 'f' <> help
+ "Overwrite the specified directory."
+ )
+ <*> (switch $ long "keep" <> short 'k' <> help
+ "Keep all the directories."
)
genOpts :: Parser Opts
-genOpts = Generate . S.fromText <$> textOption
- ( long "output"
- <> short 'o'
- <> metavar "FILE"
- <> help "Verilog output file."
- <> showDefault
- <> value "main.v"
- )
+genOpts =
+ Generate
+ <$> ( optional
+ . strOption
+ $ long "output"
+ <> short 'o'
+ <> metavar "FILE"
+ <> help "Output to a verilog file instead."
+ )
+ <*> ( optional
+ . strOption
+ $ long "config"
+ <> short 'c'
+ <> metavar "FILE"
+ <> help "Config file for the generation run."
+ )
parseOpts :: Parser Opts
parseOpts = Parse . S.fromText . T.pack <$> strArgument
@@ -145,12 +120,14 @@ reduceOpts =
configOpts :: Parser Opts
configOpts =
- Config <$> (optional . strOption $
- long "output"
- <> short 'o'
- <> metavar "FILE"
- <> help "Output to a TOML Config file."
- )
+ Config
+ <$> ( optional
+ . strOption
+ $ long "output"
+ <> short 'o'
+ <> metavar "FILE"
+ <> help "Output to a TOML Config file."
+ )
argparse :: Parser Opts
argparse =
@@ -167,17 +144,6 @@ argparse =
)
<|> hsubparser
( command
- "rerun"
- (info
- rerunOpts
- (progDesc
- "Rerun a Verilog file with a simulator or a synthesiser."
- )
- )
- <> metavar "rerun"
- )
- <|> hsubparser
- ( command
"generate"
(info
genOpts
@@ -228,10 +194,13 @@ opts = info
"VeriFuzz - A hardware simulator and synthesiser Verilog fuzzer."
)
+getConfig :: Maybe FilePath -> IO V.Config
+getConfig = maybe (return V.defaultConfig) V.parseConfigFile
+
handleOpts :: Opts -> IO ()
handleOpts (Fuzz out configF force keep) = do
- num <- getNumCapabilities
- config <- maybe (return V.defaultConfig) V.parseConfigFile configF
+ num <- getNumCapabilities
+ config <- getConfig configF
S.shellyFailDir $ do
when force . S.rm_rf $ S.fromText out
S.mkdir_p $ S.fromText out
@@ -245,14 +214,18 @@ handleOpts (Fuzz out configF force keep) = do
)
<$> [1 .. num]
sequence_ $ takeMVar <$> vars
-handleOpts (Generate _) = error "Not implemented"
-handleOpts (Parse f) = do
+handleOpts (Generate f c) = do
+ config <- getConfig c
+ source <- V.proceduralIO config
+ maybe (T.putStrLn $ V.genSource source)
+ (flip T.writeFile (V.genSource source))
+ f
+handleOpts (Parse f) = do
verilogSrc <- readFile file
case V.parseVerilog file verilogSrc of
Left l -> print l
Right v -> print $ V.GenVerilog v
where file = T.unpack . S.toTextIgnore $ f
-handleOpts (Rerun _ _) = undefined
handleOpts (Reduce f t) = do
verilogSrc <- readFile file
case V.parseVerilog file verilogSrc of
@@ -262,8 +235,10 @@ handleOpts (Reduce f t) = do
vreduced <- V.runReduce (V.SourceInfo t v)
writeFile "reduced.v" . T.unpack $ V.genSource vreduced
where file = T.unpack $ S.toTextIgnore f
-handleOpts (Config c) = maybe (T.putStrLn . V.configEncode $ V.defaultConfig)
- (`V.configToFile` V.defaultConfig) c
+handleOpts (Config c) = maybe
+ (T.putStrLn . V.configEncode $ V.defaultConfig)
+ (`V.configToFile` V.defaultConfig)
+ c
main :: IO ()
main = do
diff --git a/bugs/vivado/1_generated.v b/bugs/vivado/1_generated.v
new file mode 100644
index 0000000..de68529
--- /dev/null
+++ b/bugs/vivado/1_generated.v
@@ -0,0 +1,31 @@
+// Copyright 1986-2018 Xilinx, Inc. All Rights Reserved.
+// --------------------------------------------------------------------------------
+// Tool Version: Vivado v.2018.3 (lin64) Build 2405991 Thu Dec 6 23:36:41 MST 2018
+// Date : Thu Apr 11 19:11:05 2019
+// Host : yann-arch running 64-bit unknown
+// Command : write_verilog -force syn_vivado.v
+// Design : top
+// Purpose : This is a Verilog netlist of the current design or from a specific cell of the design. The output is an
+// IEEE 1364-2001 compliant Verilog HDL file that contains netlist information obtained from the input
+// design files.
+// Device : xc7k70tfbg676-3
+// --------------------------------------------------------------------------------
+`timescale 1 ps / 1 ps
+
+(* use_dsp = "no" *)
+(* STRUCTURAL_NETLIST = "yes" *)
+module top
+ (y,
+ wire0);
+ output y;
+ input wire0;
+
+ wire \<const0> ;
+ wire y;
+
+ GND GND
+ (.G(\<const0> ));
+ OBUF y_OBUF_inst
+ (.I(\<const0> ),
+ .O(y));
+endmodule
diff --git a/bugs/vivado/1_minimal.v b/bugs/vivado/1_minimal.v
new file mode 100644
index 0000000..59cec6c
--- /dev/null
+++ b/bugs/vivado/1_minimal.v
@@ -0,0 +1,8 @@
+(* use_dsp48="no" *) module top
+ (y, wire0);
+ output wire y;
+ input wire wire0;
+ wire [1:0] wire4;
+ assign wire4 = 1'b1;
+ assign y = (wire4 <<< 1'h1) && wire0;
+endmodule
diff --git a/bugs/vivado/1_original.v b/bugs/vivado/1_original.v
new file mode 100644
index 0000000..594b361
--- /dev/null
+++ b/bugs/vivado/1_original.v
@@ -0,0 +1,501 @@
+(* use_dsp48="no" *) module top
+#(
+parameter param209 = ((2'ha) ^~ (1'h4)),
+param210 = ((9'hc) ~^ (~^((param209 <<< param209) > (^(9'h9))))),
+param211 = ((((~&(8'h6)) & param210) && param210) ^~ (!((+param209) > (~&param210))))
+)
+(y, clk, wire0, wire1, wire2);
+output wire [1662:0] y;
+input wire clk;
+input wire [2:0] wire0;
+input wire signed [13:0] wire1;
+input wire signed [9:0] wire2;
+reg signed [9:0] reg208 = (32'h0);
+reg signed [2:0] reg207 = (32'h0);
+reg [8:0] reg206 = (32'h0);
+reg signed [4:0] reg205 = (32'h0);
+reg signed [1:0] reg204 = (32'h0);
+reg signed [4:0] reg203 = (32'h0);
+reg signed [3:0] reg202 = (32'h0);
+reg reg201 = (32'h0);
+reg [7:0] reg200 = (32'h0);
+reg [8:0] reg199 = (32'h0);
+reg [14:0] reg198 = (32'h0);
+reg signed [12:0] reg197 = (32'h0);
+reg signed [6:0] reg196 = (32'h0);
+wire signed wire195;
+reg signed [5:0] reg194 = (32'h0);
+reg signed [4:0] reg193 = (32'h0);
+reg signed [1:0] reg192 = (32'h0);
+reg signed [12:0] reg191 = (32'h0);
+reg signed [11:0] reg190 = (32'h0);
+reg signed [7:0] reg189 = (32'h0);
+reg signed reg188 = (32'h0);
+reg signed [5:0] reg187 = (32'h0);
+reg [10:0] reg186 = (32'h0);
+reg signed [9:0] reg185 = (32'h0);
+reg [3:0] reg184 = (32'h0);
+reg signed [6:0] reg183 = (32'h0);
+reg [12:0] reg182 = (32'h0);
+reg reg181 = (32'h0);
+reg signed [7:0] reg180 = (32'h0);
+reg signed [5:0] reg179 = (32'h0);
+reg signed [2:0] reg178 = (32'h0);
+reg signed [5:0] reg177 = (32'h0);
+reg [12:0] reg176 = (32'h0);
+reg [12:0] reg175 = (32'h0);
+reg signed [1:0] reg174 = (32'h0);
+reg signed [14:0] reg173 = (32'h0);
+reg [14:0] reg172 = (32'h0);
+reg [7:0] reg171 = (32'h0);
+reg [10:0] reg170 = (32'h0);
+reg signed [3:0] reg169 = (32'h0);
+reg [12:0] reg168 = (32'h0);
+reg [4:0] reg167 = (32'h0);
+reg [12:0] reg166 = (32'h0);
+reg [4:0] reg165 = (32'h0);
+reg [6:0] reg164 = (32'h0);
+reg signed [8:0] reg163 = (32'h0);
+reg signed [2:0] reg162 = (32'h0);
+reg signed [6:0] reg161 = (32'h0);
+reg signed reg160 = (32'h0);
+reg [14:0] reg159 = (32'h0);
+reg [14:0] reg158 = (32'h0);
+reg signed [8:0] reg157 = (32'h0);
+reg [5:0] reg156 = (32'h0);
+reg [5:0] reg155 = (32'h0);
+reg [2:0] reg154 = (32'h0);
+reg [2:0] reg153 = (32'h0);
+reg [7:0] reg152 = (32'h0);
+reg signed [1:0] reg151 = (32'h0);
+reg signed [9:0] reg150 = (32'h0);
+reg signed [2:0] reg149 = (32'h0);
+reg [10:0] reg148 = (32'h0);
+reg [9:0] reg147 = (32'h0);
+reg signed [14:0] reg146 = (32'h0);
+reg signed [14:0] reg145 = (32'h0);
+reg [14:0] reg144 = (32'h0);
+reg reg143 = (32'h0);
+reg [9:0] reg142 = (32'h0);
+reg [4:0] reg141 = (32'h0);
+reg [12:0] reg140 = (32'h0);
+reg [7:0] reg139 = (32'h0);
+reg [3:0] reg138 = (32'h0);
+reg signed [2:0] reg137 = (32'h0);
+reg [14:0] reg136 = (32'h0);
+reg [8:0] reg135 = (32'h0);
+reg [4:0] reg134 = (32'h0);
+reg [10:0] reg133 = (32'h0);
+reg [9:0] reg132 = (32'h0);
+reg [6:0] reg131 = (32'h0);
+reg [1:0] reg130 = (32'h0);
+reg signed [5:0] reg129 = (32'h0);
+reg [14:0] reg128 = (32'h0);
+reg [5:0] reg127 = (32'h0);
+reg signed [2:0] reg126 = (32'h0);
+reg signed [12:0] reg125 = (32'h0);
+reg signed [7:0] reg124 = (32'h0);
+reg [5:0] reg123 = (32'h0);
+reg signed [3:0] reg122 = (32'h0);
+reg [10:0] reg121 = (32'h0);
+reg [13:0] reg120 = (32'h0);
+reg [5:0] reg119 = (32'h0);
+reg signed [8:0] reg118 = (32'h0);
+reg [5:0] reg117 = (32'h0);
+reg signed [14:0] reg116 = (32'h0);
+reg signed [10:0] reg115 = (32'h0);
+reg reg114 = (32'h0);
+reg signed [10:0] reg113 = (32'h0);
+reg [1:0] reg112 = (32'h0);
+reg [6:0] reg111 = (32'h0);
+reg signed [5:0] reg110 = (32'h0);
+reg signed [10:0] reg109 = (32'h0);
+reg signed [11:0] reg108 = (32'h0);
+reg signed [7:0] reg107 = (32'h0);
+reg signed [1:0] reg106 = (32'h0);
+reg [13:0] reg105 = (32'h0);
+reg signed [4:0] reg104 = (32'h0);
+reg [2:0] reg103 = (32'h0);
+reg signed [10:0] reg102 = (32'h0);
+reg signed [9:0] reg101 = (32'h0);
+reg [9:0] reg100 = (32'h0);
+reg [12:0] reg99 = (32'h0);
+reg [9:0] reg98 = (32'h0);
+reg reg97 = (32'h0);
+reg [1:0] reg96 = (32'h0);
+reg [1:0] reg95 = (32'h0);
+reg [2:0] reg94 = (32'h0);
+reg [6:0] reg93 = (32'h0);
+reg [12:0] reg92 = (32'h0);
+reg signed [13:0] reg91 = (32'h0);
+reg [11:0] reg90 = (32'h0);
+reg signed [13:0] reg89 = (32'h0);
+reg signed [12:0] reg88 = (32'h0);
+reg [13:0] reg87 = (32'h0);
+reg [13:0] reg86 = (32'h0);
+reg [3:0] reg85 = (32'h0);
+reg [5:0] reg84 = (32'h0);
+reg signed [11:0] reg83 = (32'h0);
+reg signed [10:0] reg82 = (32'h0);
+reg signed [7:0] reg81 = (32'h0);
+reg [8:0] reg80 = (32'h0);
+reg signed [9:0] reg79 = (32'h0);
+reg signed [4:0] reg78 = (32'h0);
+reg signed [7:0] reg77 = (32'h0);
+reg [5:0] reg76 = (32'h0);
+reg signed [7:0] reg75 = (32'h0);
+reg signed [5:0] reg74 = (32'h0);
+reg [9:0] reg73 = (32'h0);
+reg signed [6:0] reg72 = (32'h0);
+reg [5:0] reg71 = (32'h0);
+reg [5:0] reg70 = (32'h0);
+reg signed [10:0] reg69 = (32'h0);
+reg signed [2:0] reg68 = (32'h0);
+reg [10:0] reg67 = (32'h0);
+reg signed [14:0] reg66 = (32'h0);
+reg [4:0] reg65 = (32'h0);
+reg signed reg64 = (32'h0);
+reg [12:0] reg63 = (32'h0);
+reg [7:0] reg62 = (32'h0);
+reg [14:0] reg61 = (32'h0);
+reg [14:0] reg60 = (32'h0);
+reg signed [9:0] reg59 = (32'h0);
+reg signed reg58 = (32'h0);
+reg signed [4:0] reg57 = (32'h0);
+reg signed [3:0] reg56 = (32'h0);
+reg [2:0] reg55 = (32'h0);
+reg [8:0] reg54 = (32'h0);
+reg signed [13:0] reg53 = (32'h0);
+reg signed [8:0] reg52 = (32'h0);
+reg [10:0] reg51 = (32'h0);
+reg [13:0] reg50 = (32'h0);
+reg signed [12:0] reg49 = (32'h0);
+reg [13:0] reg48 = (32'h0);
+reg [4:0] reg47 = (32'h0);
+reg signed [11:0] reg46 = (32'h0);
+reg [10:0] reg45 = (32'h0);
+reg [8:0] reg44 = (32'h0);
+reg [2:0] reg43 = (32'h0);
+reg signed [3:0] reg42 = (32'h0);
+reg signed [8:0] reg41 = (32'h0);
+reg signed [6:0] reg40 = (32'h0);
+reg signed [13:0] reg39 = (32'h0);
+reg [3:0] reg38 = (32'h0);
+reg [3:0] reg37 = (32'h0);
+reg [3:0] reg36 = (32'h0);
+reg signed [7:0] reg35 = (32'h0);
+reg [8:0] reg34 = (32'h0);
+reg signed [10:0] reg33 = (32'h0);
+reg signed [14:0] reg32 = (32'h0);
+reg [13:0] reg31 = (32'h0);
+reg signed [9:0] reg30 = (32'h0);
+reg [13:0] reg29 = (32'h0);
+reg signed [8:0] reg28 = (32'h0);
+reg signed [8:0] reg27 = (32'h0);
+reg [1:0] reg26 = (32'h0);
+reg signed [13:0] reg25 = (32'h0);
+reg [4:0] reg24 = (32'h0);
+reg signed [8:0] reg23 = (32'h0);
+reg signed [8:0] reg22 = (32'h0);
+reg signed [3:0] reg21 = (32'h0);
+reg signed [10:0] reg20 = (32'h0);
+reg signed [3:0] reg19 = (32'h0);
+reg signed [13:0] reg18 = (32'h0);
+reg signed [4:0] reg17 = (32'h0);
+reg [9:0] reg16 = (32'h0);
+reg signed [3:0] reg15 = (32'h0);
+reg signed reg14 = (32'h0);
+reg [8:0] reg13 = (32'h0);
+reg signed [4:0] reg12 = (32'h0);
+reg signed [11:0] reg11 = (32'h0);
+reg signed reg10 = (32'h0);
+reg signed [2:0] reg9 = (32'h0);
+reg signed [10:0] reg8 = (32'h0);
+reg [3:0] reg7 = (32'h0);
+reg [1:0] reg6 = (32'h0);
+wire [3:0] wire5;
+wire signed [13:0] wire4;
+wire [9:0] wire3;
+assign wire3 = (&(~^wire2));
+assign wire4 = $unsigned($signed((+$unsigned((-6'h1)))));
+assign wire5 = (($signed($signed(wire4)) <<< (~(2'h1))) && $signed(wire3));
+always @(posedge clk) begin
+reg6 = wire5;
+reg7 = reg6;
+reg8 = $signed(wire4);
+reg9 = $signed($unsigned((-2'h1)));
+reg10 = $signed((-15'h7));
+reg11 <= wire1;
+reg12 <= (+wire1);
+reg13 = (wire1 ^ (+$signed($signed(reg7))));
+reg14 <= $signed(($unsigned((reg10 - reg7)) ^ $signed($unsigned((9'ha)))));
+reg15 = wire0;
+reg16 = $unsigned($unsigned($unsigned(reg9)));
+reg17 = (reg10 >>> $signed($signed($unsigned((-8'h6)))));
+if(($unsigned((~((-wire4) >>> $unsigned(wire5)))) == (32'h0)))
+begin
+reg18 = ((^~(-15'h3)) ~^ (5'h7));
+reg19 <= $signed($signed(wire1));
+reg20 = (-14'h1);
+reg21 <= ((-6'ha) < $signed($signed(wire5)));
+reg22 <= (-((^~(^reg20)) < $signed($signed(reg10))));
+reg23 = wire0;
+if((((reg20 & reg7) ~^ ((!(9'h8)) >>> $signed((!reg11)))) == (32'h0)))
+begin
+reg24 = $signed((-4'h9));
+reg25 = $signed($signed(reg10));
+reg26 <= (!((!(+reg19)) >= reg6));
+end
+reg27 = ((+reg18) || (^~reg22));
+reg28 <= (($signed((~|reg16)) <= (~&(&reg6))) >>> $signed($unsigned(reg14)));
+reg29 = $signed($signed($unsigned((-8'hd))));
+end
+else
+begin
+reg30 = $signed(reg6);
+reg31 = $unsigned((15'he));
+reg32 <= $signed((reg12 ^~ $unsigned(reg8)));
+reg33 <= (-7'h1);
+reg34 = ((|wire2) >= (reg28 ^ $unsigned($unsigned(reg18))));
+reg35 = $unsigned((10'h8));
+reg36 <= ((~|((12'h1) && reg12)) <= (-3'h4));
+reg37 <= (1'h1);
+reg38 <= (2'h6);
+reg39 <= (~^wire4);
+reg40 <= $unsigned($signed($unsigned($unsigned((-11'hc)))));
+reg41 <= $unsigned((~&$signed($signed((7'h7)))));
+reg42 = $unsigned($unsigned((!(reg25 || reg29))));
+reg43 <= reg31;
+end
+end
+always @(posedge clk) begin
+if((((reg33 << (9'hc)) >> $unsigned((~$unsigned((14'hd))))) == (32'h0)))
+begin
+reg44 <= $signed($unsigned((-14'hc)));
+reg45 = (3'h2);
+reg46 <= $signed($unsigned($signed((^~(-11'hb)))));
+reg47 <= ($unsigned((~(reg8 >= reg38))) < (7'h6));
+reg48 <= (wire3 > reg13);
+reg49 = $signed($signed((~$unsigned((-4'hf)))));
+reg50 <= $unsigned($unsigned($unsigned(((15'he) <= (6'hc)))));
+reg51 = $signed((4'h9));
+reg52 <= $signed((2'h9));
+if(((10'h3) == (32'h0)))
+begin
+if(((~^(~$unsigned($signed(reg33)))) == (32'h0)))
+begin
+reg53 <= (7'ha);
+reg54 <= ((wire2 << $signed((-14'hd))) && $unsigned($unsigned((~(9'h3)))));
+reg55 = (-3'h8);
+reg56 = ((-9'hb) ^ $signed(((~|(-3'hd)) >> $signed(reg28))));
+reg57 <= $signed(reg40);
+reg58 <= (~((&(1'h5)) * $signed($unsigned(reg42))));
+end
+else
+begin
+reg59 = ((&$unsigned($unsigned((1'h4)))) ^ (&($signed((2'h3)) <= $unsigned(wire3))));
+reg60 = $unsigned((-7'h3));
+end
+reg61 <= reg29;
+reg62 = reg12;
+reg63 <= reg10;
+reg64 = (-2'h7);
+reg65 = wire2;
+reg66 = $signed((-6'h6));
+reg67 = $unsigned((-10'he));
+end
+else
+begin
+reg68 = $signed($unsigned(($unsigned(reg44) ^~ $signed((-8'h1)))));
+reg69 = $signed((^~((reg51 <= reg13) || ((3'h4) <= reg8))));
+end
+reg70 = (~|$unsigned((-2'hf)));
+reg71 = (-3'h2);
+end
+else
+begin
+reg72 = wire2;
+reg73 <= ((~|$signed(reg41)) ^~ reg58);
+reg74 <= reg65;
+reg75 = (~^wire1);
+reg76 = $unsigned(reg27);
+reg77 = $signed((7'hc));
+reg78 <= $unsigned(reg8);
+reg79 <= $unsigned($signed(((12'hc) - ((6'hb) == reg36))));
+reg80 = $signed(((~^reg45) << $unsigned($signed((-10'h6)))));
+reg81 = reg75;
+end
+reg82 <= $unsigned((^~wire1));
+reg83 = (-14'h5);
+if(((-15'h9) == (32'h0)))
+begin
+reg84 = reg37;
+reg85 = (7'h9);
+reg86 = ((2'h2) ^~ ($signed($unsigned((4'he))) << reg67));
+end
+else
+begin
+reg87 = $signed(((+$signed(reg80)) < ((-14'h3) > $unsigned((2'h5)))));
+reg88 <= $unsigned($signed(reg30));
+reg89 <= (((!(-10'h4)) ^ reg17) && (+(~reg59)));
+reg90 <= ($signed(((!reg23) - (-5'he))) & ((-$unsigned(reg77)) >>> ($signed((-15'h9)) < $signed(reg27))));
+reg91 <= (-4'h9);
+if(((reg28 | (4'hf)) == (32'h0)))
+begin
+reg92 <= reg87;
+reg93 = (!(~^$unsigned((~|wire5))));
+end
+else
+begin
+reg94 <= $unsigned(reg13);
+reg95 = $signed($unsigned($unsigned(wire5)));
+reg96 = $signed(reg73);
+reg97 <= $unsigned((($unsigned((14'hf)) ^~ (12'hf)) == (((-2'h9) > reg45) || (-9'h4))));
+reg98 = $unsigned($unsigned(reg36));
+reg99 <= $signed(((3'h6) * reg69));
+reg100 = $signed($unsigned((5'hf)));
+reg101 = (-12'h2);
+reg102 <= ((($signed((14'hf)) ^~ reg76) & $unsigned($unsigned((6'h1)))) ~^ $signed(((reg60 >> reg54) ^ $signed(reg70))));
+reg103 = $unsigned((|(-7'he)));
+reg104 = ($unsigned(($unsigned((12'hc)) && (-13'h1))) - (|$unsigned(((-6'ha) <<< reg45))));
+reg105 = ((-11'hb) ~^ (-3'hf));
+reg106 = (~^(+reg75));
+end
+end
+reg107 = reg49;
+reg108 <= reg15;
+reg109 = $signed(reg33);
+if(((~(11'h1)) == (32'h0)))
+begin
+reg110 = $unsigned(reg91);
+reg111 <= (-(-5'h2));
+end
+else
+begin
+reg112 <= $unsigned(($signed($signed(reg58)) ~^ reg20));
+reg113 <= (~^$signed(reg23));
+reg114 <= reg25;
+reg115 <= (-5'h8);
+if(($signed(($unsigned(reg10) >= (4'ha))) == (32'h0)))
+begin
+reg116 = (^((9'h7) == (~reg95)));
+reg117 = (+((10'hd) <= (-3'ha)));
+reg118 <= (~(reg109 & $unsigned((^~reg55))));
+reg119 <= (|$signed(reg69));
+end
+else
+begin
+reg120 = (4'hd);
+reg121 = (&(~^(((-5'h7) * reg92) < $unsigned((11'h2)))));
+reg122 <= $unsigned((&$unsigned(((9'h7) ^ reg68))));
+reg123 <= (-$unsigned((reg91 | $signed((10'ha)))));
+if(($unsigned((-2'hd)) == (32'h0)))
+begin
+reg124 <= $signed((8'h0));
+reg125 <= (-((~&reg41) != $signed((~&(-14'ha)))));
+reg126 <= $unsigned(reg63);
+reg127 <= ((3'hc) ^~ reg80);
+reg128 <= (|(-5'h1));
+reg129 = reg45;
+reg130 <= reg110;
+reg131 <= ((-9'h8) > $unsigned(((9'h8) <= ((-3'h6) && (-14'h2)))));
+reg132 = (14'h2);
+reg133 <= (-(+reg120));
+reg134 = (-8'hf);
+end
+else
+begin
+reg135 = (-1'h1);
+reg136 = reg133;
+reg137 = $signed((-2'h5));
+reg138 <= $unsigned(((-8'h2) * reg84));
+reg139 <= (-((reg119 >> $unsigned((4'h1))) & $unsigned((reg133 << (8'hc)))));
+reg140 <= (12'h1);
+reg141 = $signed(reg100);
+reg142 <= reg85;
+reg143 = $signed(reg103);
+reg144 = (+(~|($signed((14'h9)) + (-15'h8))));
+reg145 = ((-reg34) <= reg125);
+reg146 <= ($signed((-4'h4)) <= (~&(-3'h6)));
+reg147 <= (-(6'h6));
+end
+reg148 <= reg144;
+reg149 = $unsigned((+(6'h1)));
+reg150 <= ($signed(($signed((4'hb)) >>> $unsigned((3'h5)))) <= $signed((~&(reg20 >>> reg111))));
+reg151 = $signed($unsigned(((11'h3) && $signed((7'ha)))));
+reg152 <= reg63;
+end
+reg153 = (-7'h3);
+if(($signed((reg47 | (((-13'hf) ~^ reg129) >>> ((9'hf) - reg18)))) == (32'h0)))
+begin
+reg154 = (-2'h7);
+reg155 <= reg69;
+reg156 <= $signed($signed(((^~(-1'h3)) > (7'he))));
+reg157 <= $signed(reg120);
+reg158 <= (^(12'hc));
+reg159 <= $signed($signed($unsigned((&(12'h3)))));
+reg160 = ((6'h7) || $signed(((|(9'h1)) - $unsigned(reg76))));
+reg161 <= (~(13'hb));
+reg162 = (~|($signed((reg104 * reg59)) ^~ reg151));
+reg163 <= (-14'hd);
+reg164 <= ($signed($signed($unsigned((-11'h8)))) >= (~($signed((3'h8)) ^ $unsigned(reg150))));
+reg165 = $signed($signed(($signed((-9'hd)) >> $signed((-1'he)))));
+reg166 = (|(~&(-6'h6)));
+reg167 = (7'h2);
+reg168 = reg20;
+end
+else
+begin
+reg169 = (1'h9);
+reg170 <= (4'h7);
+reg171 = reg47;
+reg172 <= $unsigned((~$signed((reg81 >>> reg114))));
+reg173 = (~|$unsigned((~(~|(-8'ha)))));
+reg174 = (1'hd);
+reg175 = ((-3'h8) ^ (-1'h6));
+reg176 <= (~|$signed($unsigned((~^(-15'hd)))));
+reg177 = ((((-7'h7) >> (~|reg86)) + (~^reg38)) && (14'h3));
+reg178 <= reg154;
+if(((2'h1) == (32'h0)))
+begin
+reg179 <= $unsigned($signed($signed((^~(11'h2)))));
+reg180 = $unsigned(reg46);
+reg181 = (14'h7);
+reg182 <= (($signed((reg164 * reg143)) > $signed((reg49 < reg7))) << (+$signed(reg66)));
+reg183 = $unsigned((((13'h6) * (reg15 ^ reg124)) >> ((^(11'hb)) <<< $unsigned((-13'h6)))));
+reg184 <= ((1'h5) * $unsigned(reg174));
+end
+else
+begin
+reg185 <= wire4;
+reg186 = reg70;
+reg187 <= reg51;
+reg188 <= $unsigned(reg123);
+reg189 = $signed((^$unsigned(reg163)));
+end
+reg190 = $signed($unsigned((-13'h5)));
+reg191 = $signed((8'h2));
+reg192 <= reg70;
+end
+reg193 = $unsigned($unsigned(reg14));
+reg194 <= $unsigned(($unsigned((reg147 && (5'h9))) & $unsigned($signed((7'he)))));
+end
+end
+assign wire195 = reg108;
+always @(posedge clk) begin
+reg196 = (!(!reg63));
+reg197 = $unsigned((~(&$unsigned((6'hf)))));
+reg198 = (15'h1);
+reg199 <= wire1;
+reg200 = (!reg41);
+reg201 = reg160;
+reg202 <= $unsigned(((^~(~|(9'h9))) ^ (reg104 >= (^(-11'h8)))));
+reg203 <= $unsigned((-(-8'h7)));
+reg204 = (7'h0);
+reg205 = (9'h8);
+reg206 <= (($signed(reg148) ^~ $unsigned($signed(reg65))) <<< $unsigned($signed((!reg176))));
+reg207 = $unsigned(reg205);
+reg208 = wire3;
+end
+assign y = {reg208, reg207, reg206, reg205, reg204, reg203, reg202, reg201, reg200, reg199, reg198, reg197, reg196, wire195, reg194, reg193, reg192, reg191, reg190, reg189, reg188, reg187, reg186, reg185, reg184, reg183, reg182, reg181, reg180, reg179, reg178, reg177, reg176, reg175, reg174, reg173, reg172, reg171, reg170, reg169, reg168, reg167, reg166, reg165, reg164, reg163, reg162, reg161, reg160, reg159, reg158, reg157, reg156, reg155, reg154, reg153, reg152, reg151, reg150, reg149, reg148, reg147, reg146, reg145, reg144, reg143, reg142, reg141, reg140, reg139, reg138, reg137, reg136, reg135, reg134, reg133, reg132, reg131, reg130, reg129, reg128, reg127, reg126, reg125, reg124, reg123, reg122, reg121, reg120, reg119, reg118, reg117, reg116, reg115, reg114, reg113, reg112, reg111, reg110, reg109, reg108, reg107, reg106, reg105, reg104, reg103, reg102, reg101, reg100, reg99, reg98, reg97, reg96, reg95, reg94, reg93, reg92, reg91, reg90, reg89, reg88, reg87, reg86, reg85, reg84, reg83, reg82, reg81, reg80, reg79, reg78, reg77, reg76, reg75, reg74, reg73, reg72, reg71, reg70, reg69, reg68, reg67, reg66, reg65, reg64, reg63, reg62, reg61, reg60, reg59, reg58, reg57, reg56, reg55, reg54, reg53, reg52, reg51, reg50, reg49, reg48, reg47, reg46, reg45, reg44, reg43, reg42, reg41, reg40, reg39, reg38, reg37, reg36, reg35, reg34, reg33, reg32, reg31, reg30, reg29, reg28, reg27, reg26, reg25, reg24, reg23, reg22, reg21, reg20, reg19, reg18, reg17, reg16, reg15, reg14, reg13, reg12, reg11, reg10, reg9, reg8, reg7, reg6, wire5, wire4, wire3};
+endmodule
diff --git a/bugs/vivado/2_minimal.v b/bugs/vivado/2_minimal.v
new file mode 100644
index 0000000..227550e
--- /dev/null
+++ b/bugs/vivado/2_minimal.v
@@ -0,0 +1,28 @@
+(* use_dsp48="no" *) module top
+ (y, clk, wire0, wire1, wire2, wire3);
+ output wire [163:0] y;
+ input wire clk;
+ input wire signed [11:0] wire0;
+ input wire [13:0] wire1;
+ input wire signed [7:0] wire2;
+ input wire signed [3:0] wire3;
+ wire signed [12:0] wire19;
+ wire [6:0] wire18;
+ wire [4:0] wire17;
+ wire signed [12:0] wire16;
+ wire signed [19:0] wire15;
+ wire [7:0] wire14;
+ wire wire13;
+ wire [10:0] wire12;
+ wire signed [9:0] wire11;
+ wire signed [16:0] wire10;
+ reg [15:0] reg9;
+ reg signed [11:0] reg8;
+ wire [6:0] wire7;
+ wire signed [6:0] wire6;
+ wire [10:0] wire5;
+ wire [5:0] wire4;
+ assign wire13 = {wire0, $unsigned(((-17'hd) ? wire0 : (-18'he))), (((9'h8) ? (11'he) : reg8) <<< (~&(-8'h2))), ({reg9, wire1, (3'h12), (-5'hc)} | (&(-1'h12)))};
+ assign wire17 = ((wire13 ? 1'b1 : ( 1'b1 ? (14'he) : wire0)) ? $unsigned($unsigned(((-2'h5)))) : $unsigned($unsigned((wire13 || wire2))));
+ assign y = {wire17};
+endmodule
diff --git a/bugs/vivado/2_original.v b/bugs/vivado/2_original.v
new file mode 100644
index 0000000..f60b789
--- /dev/null
+++ b/bugs/vivado/2_original.v
@@ -0,0 +1,44 @@
+(* use_dsp48="no" *) module top
+ (y, clk, wire0, wire1, wire2, wire3);
+ output wire [163:0] y;
+ input wire clk;
+ input wire signed [11:0] wire0;
+ input wire [13:0] wire1;
+ input wire signed [7:0] wire2;
+ input wire signed [3:0] wire3;
+ wire signed [12:0] wire19;
+ wire [6:0] wire18;
+ wire [4:0] wire17;
+ wire signed [12:0] wire16;
+ wire signed [19:0] wire15;
+ wire [7:0] wire14;
+ wire wire13;
+ wire [10:0] wire12;
+ wire signed [9:0] wire11;
+ wire signed [16:0] wire10;
+ reg [15:0] reg9;
+ reg signed [11:0] reg8;
+ wire [6:0] wire7;
+ wire signed [6:0] wire6;
+ wire [10:0] wire5;
+ wire [5:0] wire4;
+ assign wire4 = $unsigned(($unsigned((-6'h11)) ? ((wire3 ? wire3 : (8'h0)) && $signed(wire2)) : (19'he)));
+ assign wire5 = wire0;
+ assign wire6 = (5'h4);
+ assign wire7 = (wire4 ? {wire2, wire3, wire0, (-9'h6), (20'h10), wire1, (-1'hd), (-2'h10), (6'hc), (-16'hd), wire0} : $unsigned($unsigned((16'h5))));
+ always @(posedge clk) begin
+ reg8 = wire6;
+ reg9 = wire0;
+ end
+ assign wire10 = (+wire0);
+ assign wire11 = $unsigned({(wire6 || (1'h2))});
+ assign wire12 = (12'h7);
+ assign wire13 = {wire5, $unsigned(((-17'hd) ? wire5 : (-18'he))), (((9'h8) ? (11'he) : reg8) <<< (~&(-8'h2))), ({reg9, wire1, (3'h12), (-5'hc)} | (&(-1'h12)))};
+ assign wire14 = ((3'h5) >>> ($unsigned((wire6 ? reg9 : (-16'hb))) > ((wire2 ^ (-20'h1)) ? ((11'h14) ? wire12 : (-10'h13)) : {(-15'h11), wire0, (-3'he), (-12'h14), (-3'hd), (-19'h11)})));
+ assign wire15 = $unsigned(wire14);
+ assign wire16 = ({((-15'hc) >= (2'ha)), (wire15 || reg8), $signed(wire12), {(-10'h12), wire7, wire1, (-19'h14), (5'ha), wire0, wire4, (15'h2), (14'hc), reg9, (19'hb), wire5, (8'h8), wire11, (-11'hc), wire5, wire2, (17'h0), (13'hb), wire2}, (1'h13), (11'hc), (9'h13), (-5'h2), $signed((1'hf)), (reg9 << wire2), {(11'h6), reg8, wire15, wire5, (16'ha), (20'ha), (-5'h8), wire14, (-4'h7), wire4, (4'ha), reg9, (-1'h2)}, $unsigned(reg9), ((-12'h1) ? wire3 : (11'h0)), (|(3'h3)), reg9, {(-13'h2), (-16'h13)}, wire2, (^~wire1), $signed(reg8)} == $signed({(-12'hf), wire11, (-14'h2), (13'he), wire4, reg8, (6'h7), reg9, reg8, wire4, wire3}));
+ assign wire17 = ((wire13 ? ((7'h14) ? (-14'hb) : (-9'h7)) : (wire6 ? (14'he) : wire0)) ? $unsigned($unsigned(((-2'h5) * wire7))) : $unsigned($unsigned((wire13 || wire2))));
+ assign wire18 = wire3;
+ assign wire19 = wire2;
+ assign y = {wire19, wire18, wire17, wire16, wire15, wire14, wire13, wire12, wire11, wire10, reg9, reg8, wire7, wire6, wire5, wire4};
+endmodule
diff --git a/scripts/setup.sh b/scripts/setup.sh
index bd07b12..4006f99 100644
--- a/scripts/setup.sh
+++ b/scripts/setup.sh
@@ -1,19 +1,19 @@
#!/bin/sh
sudo yum -y update
-sudo yum -y install git gcc gcc-c++ tcl-devel python3 \
+sudo yum -y install git gcc gcc-c++ tcl-devel python36 \
graphviz xdot gperf gmp-devel make bison flex autoconf \
tmux
sudo mkdir -p /mnt/tools
-sudo mount /dev/sdf1 /mnt/tools
+sudo mount /dev/nvme2n1p1 /mnt/tools
sudo chown -R $USER:$USER /mnt/tools/home/ec2-user
curl -sSL https://get.haskellstack.org/ | sh
{ cat <<EOF
-export PATH="\${PATH}:/mnt/tools/bin:/mnt/tools/opt/Xilinx/14.7/ISE_DS/ISE/bin/lin64/"
+export PATH="\${PATH}:/mnt/tools/bin:/mnt/tools/opt/Xilinx/14.7/ISE_DS/ISE/bin/lin64/:/mnt/tools/opt/Xilinx/Vivado/2018.3/bin"
EOF
} >> $HOME/.bashrc
diff --git a/src/VeriFuzz.hs b/src/VeriFuzz.hs
index ebedb0d..9486537 100644
--- a/src/VeriFuzz.hs
+++ b/src/VeriFuzz.hs
@@ -55,8 +55,7 @@ generateByteString n = do
return $ randomByteString gen n []
makeSrcInfo :: ModDecl -> SourceInfo
-makeSrcInfo m =
- SourceInfo (m ^. modId . getIdentifier) (Verilog [Description m])
+makeSrcInfo m = SourceInfo (m ^. modId . getIdentifier) (Verilog [m])
-- | Draw a randomly generated DAG to a dot file and compile it to a png so it
-- can be seen.
@@ -107,18 +106,20 @@ checkEquivalence src dir = shellyFailDir $ do
setenv "VERIFUZZ_ROOT" curr
cd (fromText dir)
catch_sh
- (runEquiv defaultYosys defaultYosys (Just defaultVivado) src >> return True
+ ( runEquiv defaultYosys defaultYosys (Just defaultVivado) src
+ >> return True
)
((\_ -> return False) :: RunFailed -> Sh Bool)
-- | Run a fuzz run and check if all of the simulators passed by checking if the
-- generated Verilog files are equivalent.
-runEquivalence :: Gen Verilog -- ^ Generator for the Verilog file.
- -> Text -- ^ Name of the folder on each thread.
- -> Text -- ^ Name of the general folder being used.
- -> Bool -- ^ Keep flag.
- -> Int -- ^ Used to track the recursion.
- -> IO ()
+runEquivalence
+ :: Gen Verilog -- ^ Generator for the Verilog file.
+ -> Text -- ^ Name of the folder on each thread.
+ -> Text -- ^ Name of the general folder being used.
+ -> Bool -- ^ Keep flag.
+ -> Int -- ^ Used to track the recursion.
+ -> IO ()
runEquivalence gm t d k i = do
m <- Hog.sample gm
let srcInfo = SourceInfo "top" m
@@ -129,7 +130,7 @@ runEquivalence gm t d k i = do
setenv "VERIFUZZ_ROOT" curr
cd (fromText "output" </> fromText n)
catch_sh
- ( runEquiv defaultYosys defaultYosys (Just defaultVivado) srcInfo
+ (runEquiv defaultYosys defaultYosys (Just defaultVivado) srcInfo
>> echoP "Test OK"
)
$ onFailure n
diff --git a/src/VeriFuzz/Circuit.hs b/src/VeriFuzz/Circuit.hs
index 37e25ac..d385d32 100644
--- a/src/VeriFuzz/Circuit.hs
+++ b/src/VeriFuzz/Circuit.hs
@@ -43,4 +43,3 @@ fromGraph = do
$ nestUpTo 5 (generateAST gr)
^.. getVerilog
. traverse
- . getDescription
diff --git a/src/VeriFuzz/Circuit/Gen.hs b/src/VeriFuzz/Circuit/Gen.hs
index 817d2f8..1e31e56 100644
--- a/src/VeriFuzz/Circuit/Gen.hs
+++ b/src/VeriFuzz/Circuit/Gen.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 False 4
+genPortsAST f c = port . frNode <$> f c where port = Port Wire False 0 4
-- | Generates the nested expression AST, so that it can then generate the
-- assignment expressions.
@@ -67,13 +67,13 @@ genAssignAST c = catMaybes $ genContAssignAST c <$> nodes
nodes = G.labNodes gr
genModuleDeclAST :: Circuit -> ModDecl
-genModuleDeclAST c = ModDecl i output ports $ combineAssigns yPort a
+genModuleDeclAST c = ModDecl i output ports (combineAssigns yPort a) []
where
i = Identifier "gen_module"
ports = genPortsAST inputsC c
output = []
a = genAssignAST c
- yPort = Port Wire False 90 "y"
+ yPort = Port Wire False 0 90 "y"
generateAST :: Circuit -> Verilog
-generateAST c = Verilog [Description $ genModuleDeclAST c]
+generateAST c = Verilog [genModuleDeclAST c]
diff --git a/src/VeriFuzz/Config.hs b/src/VeriFuzz/Config.hs
index d812248..66c5aa2 100644
--- a/src/VeriFuzz/Config.hs
+++ b/src/VeriFuzz/Config.hs
@@ -15,17 +15,36 @@ Configuration file format and parser.
module VeriFuzz.Config
( Config(..)
, defaultConfig
+ , configProbability
+ , configProperty
, Probability(..)
- , probBlock
- , probNonBlock
- , probAssign
- , probAlways
- , probCond
+ , probModItem
+ , probStmnt
+ , probExpr
+ , ProbExpr(..)
+ , probExprNum
+ , probExprId
+ , probExprUnOp
+ , probExprBinOp
+ , probExprCond
+ , probExprConcat
+ , probExprStr
+ , probExprSigned
+ , probExprUnsigned
+ , ProbModItem(..)
+ , probModItemAssign
+ , probModItemAlways
+ , probModItemInst
+ , ProbStatement(..)
+ , probStmntBlock
+ , probStmntNonBlock
+ , probStmntCond
+ , probStmntFor
, propSize
, propSeed
- , propDepth
- , configProbability
- , configProperty
+ , propStmntDepth
+ , propModDepth
+ , propMaxModules
, parseConfigFile
, parseConfig
, configEncode
@@ -42,29 +61,55 @@ import qualified Data.Text.IO as T (writeFile)
import Toml (TomlCodec, (.=))
import qualified Toml
-data Probability = Probability { _probAssign :: {-# UNPACK #-} !Int
- , _probAlways :: {-# UNPACK #-} !Int
- , _probBlock :: {-# UNPACK #-} !Int
- , _probNonBlock :: {-# UNPACK #-} !Int
- , _probCond :: {-# UNPACK #-} !Int
+data ProbExpr = ProbExpr { _probExprNum :: {-# UNPACK #-} !Int
+ , _probExprId :: {-# UNPACK #-} !Int
+ , _probExprUnOp :: {-# UNPACK #-} !Int
+ , _probExprBinOp :: {-# UNPACK #-} !Int
+ , _probExprCond :: {-# UNPACK #-} !Int
+ , _probExprConcat :: {-# UNPACK #-} !Int
+ , _probExprStr :: {-# UNPACK #-} !Int
+ , _probExprSigned :: {-# UNPACK #-} !Int
+ , _probExprUnsigned :: {-# UNPACK #-} !Int
+ }
+ deriving (Eq, Show)
+
+data ProbModItem = ProbModItem { _probModItemAssign :: {-# UNPACK #-} !Int
+ , _probModItemAlways :: {-# UNPACK #-} !Int
+ , _probModItemInst :: {-# UNPACK #-} !Int
}
deriving (Eq, Show)
-makeLenses ''Probability
+data ProbStatement = ProbStatement { _probStmntBlock :: {-# UNPACK #-} !Int
+ , _probStmntNonBlock :: {-# UNPACK #-} !Int
+ , _probStmntCond :: {-# UNPACK #-} !Int
+ , _probStmntFor :: {-# UNPACK #-} !Int
+ }
+ deriving (Eq, Show)
-data Property = Property { _propSize :: {-# UNPACK #-} !Int
- , _propSeed :: !(Maybe Int)
- , _propDepth :: {-# UNPACK #-} !Int
+data Probability = Probability { _probModItem :: {-# UNPACK #-} !ProbModItem
+ , _probStmnt :: {-# UNPACK #-} !ProbStatement
+ , _probExpr :: {-# UNPACK #-} !ProbExpr
+ }
+ deriving (Eq, Show)
+
+data Property = Property { _propSize :: {-# UNPACK #-} !Int
+ , _propSeed :: !(Maybe Int)
+ , _propStmntDepth :: {-# UNPACK #-} !Int
+ , _propModDepth :: {-# UNPACK #-} !Int
+ , _propMaxModules :: {-# UNPACK #-} !Int
}
deriving (Eq, Show)
-makeLenses ''Property
-
data Config = Config { _configProbability :: {-# UNPACK #-} !Probability
, _configProperty :: {-# UNPACK #-} !Property
}
deriving (Eq, Show)
+makeLenses ''ProbExpr
+makeLenses ''ProbModItem
+makeLenses ''ProbStatement
+makeLenses ''Probability
+makeLenses ''Property
makeLenses ''Config
defaultValue
@@ -75,29 +120,81 @@ defaultValue
defaultValue x = Toml.dimap Just (fromMaybe x) . Toml.dioptional
defaultConfig :: Config
-defaultConfig = Config (Probability 5 1 5 1 1) (Property 20 Nothing 3)
+defaultConfig = Config (Probability defModItem defStmnt defExpr)
+ (Property 20 Nothing 3 2 5)
+ where
+ defModItem = ProbModItem 5 1 1
+ defStmnt = ProbStatement 5 5 1 1
+ defExpr = ProbExpr 1 1 1 1 1 1 0 1 1
twoKey :: Toml.Piece -> Toml.Piece -> Toml.Key
twoKey a b = Toml.Key (a :| [b])
+int :: Toml.Piece -> Toml.Piece -> TomlCodec Int
+int a = Toml.int . twoKey a
+
+exprCodec :: TomlCodec ProbExpr
+exprCodec =
+ ProbExpr
+ <$> defaultValue (defProb probExprNum) (intE "number")
+ .= _probExprNum
+ <*> defaultValue (defProb probExprId) (intE "variable")
+ .= _probExprId
+ <*> defaultValue (defProb probExprUnOp) (intE "unary")
+ .= _probExprUnOp
+ <*> defaultValue (defProb probExprBinOp) (intE "binary")
+ .= _probExprBinOp
+ <*> defaultValue (defProb probExprCond) (intE "ternary")
+ .= _probExprCond
+ <*> defaultValue (defProb probExprConcat) (intE "concatenation")
+ .= _probExprConcat
+ <*> defaultValue (defProb probExprStr) (intE "string")
+ .= _probExprStr
+ <*> defaultValue (defProb probExprSigned) (intE "signed")
+ .= _probExprSigned
+ <*> defaultValue (defProb probExprUnsigned) (intE "unsigned")
+ .= _probExprUnsigned
+ where
+ defProb i = defaultConfig ^. configProbability . probExpr . i
+ intE = int "expr"
+
+stmntCodec :: TomlCodec ProbStatement
+stmntCodec =
+ ProbStatement
+ <$> defaultValue (defProb probStmntBlock) (intS "blocking")
+ .= _probStmntBlock
+ <*> defaultValue (defProb probStmntNonBlock) (intS "nonblocking")
+ .= _probStmntNonBlock
+ <*> defaultValue (defProb probStmntCond) (intS "conditional")
+ .= _probStmntCond
+ <*> defaultValue (defProb probStmntFor) (intS "forloop")
+ .= _probStmntFor
+ where
+ defProb i = defaultConfig ^. configProbability . probStmnt . i
+ intS = int "statement"
+
+modItemCodec :: TomlCodec ProbModItem
+modItemCodec =
+ ProbModItem
+ <$> defaultValue (defProb probModItemAssign) (intM "assign")
+ .= _probModItemAssign
+ <*> defaultValue (defProb probModItemAlways) (intM "always")
+ .= _probModItemAlways
+ <*> defaultValue (defProb probModItemInst) (intM "instantiation")
+ .= _probModItemInst
+ where
+ defProb i = defaultConfig ^. configProbability . probModItem . i
+ intM = int "moditem"
+
probCodec :: TomlCodec Probability
probCodec =
Probability
- <$> defaultValue (defProb probAssign)
- (Toml.int $ twoKey "moditem" "assign")
- .= _probAssign
- <*> defaultValue (defProb probAlways)
- (Toml.int $ twoKey "moditem" "always")
- .= _probAlways
- <*> defaultValue (defProb probBlock)
- (Toml.int $ twoKey "statement" "blocking")
- .= _probBlock
- <*> defaultValue (defProb probNonBlock)
- (Toml.int $ twoKey "statement" "nonblocking")
- .= _probNonBlock
- <*> defaultValue (defProb probNonBlock)
- (Toml.int $ twoKey "statement" "conditional")
- .= _probCond
+ <$> defaultValue (defProb probModItem) modItemCodec
+ .= _probModItem
+ <*> defaultValue (defProb probStmnt) stmntCodec
+ .= _probStmnt
+ <*> defaultValue (defProb probExpr) exprCodec
+ .= _probExpr
where defProb i = defaultConfig ^. configProbability . i
propCodec :: TomlCodec Property
@@ -107,8 +204,12 @@ propCodec =
.= _propSize
<*> Toml.dioptional (Toml.int "seed")
.= _propSeed
- <*> defaultValue (defProp propDepth) (Toml.int "depth")
- .= _propDepth
+ <*> defaultValue (defProp propStmntDepth) (int "statement" "depth")
+ .= _propStmntDepth
+ <*> defaultValue (defProp propModDepth) (int "module" "depth")
+ .= _propModDepth
+ <*> defaultValue (defProp propMaxModules) (int "module" "max")
+ .= _propMaxModules
where defProp i = defaultConfig ^. configProperty . i
configCodec :: TomlCodec Config
diff --git a/src/VeriFuzz/Internal.hs b/src/VeriFuzz/Internal.hs
index 51bb52c..22efa92 100644
--- a/src/VeriFuzz/Internal.hs
+++ b/src/VeriFuzz/Internal.hs
@@ -15,6 +15,7 @@ module VeriFuzz.Internal
safe
, showT
, comma
+ , commaNL
)
where
@@ -33,3 +34,7 @@ showT = T.pack . show
-- | Inserts commas between '[Text]' and except the last one.
comma :: [Text] -> Text
comma = T.intercalate ", "
+
+-- | Inserts commas and newlines between '[Text]' and except the last one.
+commaNL :: [Text] -> Text
+commaNL = T.intercalate ",\n"
diff --git a/src/VeriFuzz/RecursionScheme.hs b/src/VeriFuzz/RecursionScheme.hs
new file mode 100644
index 0000000..7d89498
--- /dev/null
+++ b/src/VeriFuzz/RecursionScheme.hs
@@ -0,0 +1,84 @@
+{-|
+Module : VeriFuzz.RecursionScheme
+Description : Recursion scheme implementation for the AST.
+Copyright : (c) 2019, Yann Herklotz Grave
+License : GPL-3
+Maintainer : ymherklotz [at] gmail [dot] com
+Stability : experimental
+Portability : POSIX
+
+Recursion scheme implementation for the AST.
+-}
+
+module VeriFuzz.RecursionScheme
+ ( Term(..)
+ , Attr(..)
+ , Algebra
+ , bottomUp
+ , topDown
+ , cata
+ , ana
+ , para
+ , apo
+ )
+where
+
+import Control.Arrow ((&&&), (>>>), (|||))
+import Data.Function ((&))
+
+newtype Term f = In { out :: f (Term f) }
+
+data Attr f a = Attr
+ { attribute :: a
+ , hole :: f (Attr f a)
+ }
+
+type Algebra f a = f a -> a
+
+type RAlgebra f a = f (Term f, a) -> a
+
+type RAlgebra' f a = Term f -> f a -> a
+
+type CVAlgebra f a = f (Attr f a) -> a
+
+type Coalgebra f a = a -> f a
+
+type RCoalgebra f a = a -> f (Either (Term f) a)
+
+bottomUp :: Functor a => (Term a -> Term a) -> Term a -> Term a
+bottomUp fn = cata $ In >>> fn
+
+topDown :: Functor a => (Term a -> Term a) -> Term a -> Term a
+topDown fn = ana $ fn >>> out
+
+cata :: Functor f => Algebra f a -> Term f -> a
+cata fn = para' $ const fn
+
+ana :: Functor f => Coalgebra f a -> a -> Term f
+ana fn =
+ fn
+ >>> fmap (ana fn)
+ >>> In
+
+para :: Functor f => RAlgebra f a -> Term f -> a
+para ralg =
+ out
+ >>> fmap (id &&& para ralg)
+ >>> ralg
+
+para' :: Functor f => RAlgebra' f a -> Term f -> a
+para' ralg t = out t & fmap (para' ralg) & ralg t
+
+apo :: Functor f => RCoalgebra f a -> a -> Term f
+apo rcoalg =
+ rcoalg
+ >>> fmap (id ||| apo rcoalg)
+ >>> In
+
+histo :: Functor f => CVAlgebra f a -> Term f -> a
+histo cv =
+ out
+ >>> fmap worker
+ >>> cv
+ where
+ worker t = undefined
diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs
index 14023b7..8876706 100644
--- a/src/VeriFuzz/Sim/Icarus.hs
+++ b/src/VeriFuzz/Sim/Icarus.hs
@@ -93,8 +93,9 @@ runSimIcarus sim rinfo bss = do
$ fold (addDisplay $ assignFunc (_modInPorts m) <$> bss)
<> (SysTaskEnable $ Task "finish" [])
]
+ []
let newtb = instantiateMod m tb
- let modWithTb = Verilog $ Description <$> [newtb, m]
+ let modWithTb = Verilog [newtb, m]
writefile "main.v" $ genSource modWithTb
runSimWithFile sim "main.v" bss
where m = rinfo ^. mainModule
diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs
index 062035c..145042a 100644
--- a/src/VeriFuzz/Sim/Internal.hs
+++ b/src/VeriFuzz/Sim/Internal.hs
@@ -73,10 +73,10 @@ mainModule = lens get_ set_
where
set_ (SourceInfo top main) v =
SourceInfo top (main & getModule %~ update top v)
- update top v m@(ModDecl (Identifier i) _ _ _) | i == top = v
- | otherwise = m
+ update top v m@(ModDecl (Identifier i) _ _ _ _) | i == top = v
+ | otherwise = m
get_ (SourceInfo top main) = head . filter (f top) $ main ^.. getModule
- f top (ModDecl (Identifier i) _ _ _) = i == top
+ f top (ModDecl (Identifier i) _ _ _ _) = i == top
rootPath :: Sh FilePath
rootPath = do
diff --git a/src/VeriFuzz/Sim/Reduce.hs b/src/VeriFuzz/Sim/Reduce.hs
index 5684ed5..361df3e 100644
--- a/src/VeriFuzz/Sim/Reduce.hs
+++ b/src/VeriFuzz/Sim/Reduce.hs
@@ -67,8 +67,8 @@ filterExpr ids (Id i) = if i `notElem` ids then Number 1 0 else Id i
filterExpr _ e = e
filterDecl :: [Identifier] -> ModItem -> Bool
-filterDecl ids (Decl Nothing (Port _ _ _ i)) = i `elem` ids
-filterDecl _ _ = True
+filterDecl ids (Decl Nothing (Port _ _ _ _ i) _) = i `elem` ids
+filterDecl _ _ = True
filterAssigns :: [Port] -> ModItem -> Bool
filterAssigns out (ModCA (ContAssign i _)) =
diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs
index 0fc74a0..f630ea6 100644
--- a/src/VeriFuzz/Sim/Template.hs
+++ b/src/VeriFuzz/Sim/Template.hs
@@ -91,7 +91,7 @@ sbyConfig bd sim1 sim2 (SourceInfo top src) = [st|[options]
mode prove
[engines]
-smtbmc
+smtbmc z3
[script]
#{readL}
diff --git a/src/VeriFuzz/Verilog.hs b/src/VeriFuzz/Verilog.hs
index fdf2ac0..4d3b82c 100644
--- a/src/VeriFuzz/Verilog.hs
+++ b/src/VeriFuzz/Verilog.hs
@@ -14,12 +14,11 @@ module VeriFuzz.Verilog
( Verilog(..)
, parseVerilog
, procedural
+ , proceduralIO
, randomMod
, GenVerilog(..)
, genSource
, getVerilog
- , Description(..)
- , getDescription
-- * Primitives
-- ** Identifier
, Identifier(..)
@@ -69,8 +68,6 @@ module VeriFuzz.Verilog
, exprFunc
, exprBody
, exprStr
- , exprWithContext
- , traverseExpr
, ConstExpr(..)
, constNum
, Function(..)
@@ -91,7 +88,6 @@ module VeriFuzz.Verilog
, statements
, stmntBA
, stmntNBA
- , stmntCA
, stmntTask
, stmntSysTask
, stmntCondExpr
@@ -118,10 +114,6 @@ module VeriFuzz.Verilog
-- * Useful Lenses and Traversals
, getModule
, getSourceId
- -- * Arbitrary
- , Arb
- , arb
- , genPositive
)
where
diff --git a/src/VeriFuzz/Verilog/AST.hs b/src/VeriFuzz/Verilog/AST.hs
index 405b712..007b3b5 100644
--- a/src/VeriFuzz/Verilog/AST.hs
+++ b/src/VeriFuzz/Verilog/AST.hs
@@ -18,8 +18,6 @@ module VeriFuzz.Verilog.AST
( -- * Top level types
Verilog(..)
, getVerilog
- , Description(..)
- , getDescription
-- * Primitives
-- ** Identifier
, Identifier(..)
@@ -50,6 +48,7 @@ module VeriFuzz.Verilog.AST
, Port(..)
, portType
, portSigned
+ , portSizeLower
, portSize
, portName
-- * Expression
@@ -69,10 +68,20 @@ module VeriFuzz.Verilog.AST
, exprFunc
, exprBody
, exprStr
- , exprWithContext
- , traverseExpr
, ConstExpr(..)
+ , constSize
, constNum
+ , constParamId
+ , constConcat
+ , constUnOp
+ , constPrim
+ , constLhs
+ , constBinOp
+ , constRhs
+ , constCond
+ , constTrue
+ , constFalse
+ , constStr
, Function(..)
-- * Assignment
, Assign(..)
@@ -82,6 +91,13 @@ module VeriFuzz.Verilog.AST
, ContAssign(..)
, contAssignNetLVal
, contAssignExpr
+ -- ** Parameters
+ , Parameter(..)
+ , paramIdent
+ , paramValue
+ , LocalParam(..)
+ , localParamIdent
+ , localParamValue
-- * Statment
, Statement(..)
, statDelay
@@ -91,26 +107,33 @@ module VeriFuzz.Verilog.AST
, statements
, stmntBA
, stmntNBA
- , stmntCA
, stmntTask
, stmntSysTask
, stmntCondExpr
, stmntCondTrue
, stmntCondFalse
+ , forAssign
+ , forExpr
+ , forIncr
+ , forStmnt
-- * Module
, ModDecl(..)
, modId
, modOutPorts
, modInPorts
, modItems
+ , modParams
, ModItem(..)
, modContAssign
, modInstId
, modInstName
, modInstConns
+ , paramDecl
+ , localParamDecl
, traverseModItem
, declDir
, declPort
+ , declVal
, ModConn(..)
, modConn
, modConnName
@@ -118,25 +141,16 @@ module VeriFuzz.Verilog.AST
-- * Useful Lenses and Traversals
, getModule
, getSourceId
- -- * Arbitrary
- , Arb
- , arb
- , genPositive
)
where
import Control.Lens
-import Control.Monad (replicateM)
import Data.Data
import Data.Data.Lens
-import Data.List.NonEmpty (toList)
+import Data.List.NonEmpty (NonEmpty)
import Data.String (IsString, fromString)
import Data.Text (Text)
-import qualified Data.Text as T
import Data.Traversable (sequenceA)
-import Hedgehog (Gen)
-import qualified Hedgehog.Gen as Hog
-import qualified Hedgehog.Range as Hog
-- | Identifier in Verilog. This is just a string of characters that can either
-- be lowercase and uppercase for now. This might change in the future though,
@@ -199,7 +213,7 @@ data UnaryOperator = UnPlus -- ^ @+@
deriving (Eq, Show, Ord, Data)
data Function = SignedFunc
- | UnSignedFunc
+ | UnsignedFunc
deriving (Eq, Show, Ord, Data)
-- | Verilog expression, which can either be a primary expression, unary
@@ -250,17 +264,49 @@ instance IsString Expr where
instance Plated Expr where
plate = uniplate
-traverseExpr :: (Applicative f) => (Expr -> f Expr) -> Expr -> f Expr
-traverseExpr f (Concat e ) = Concat <$> sequenceA (f <$> e)
-traverseExpr f (UnOp u e ) = UnOp u <$> f e
-traverseExpr f (BinOp l o r) = BinOp <$> f l <*> pure o <*> f r
-traverseExpr f (Cond c l r) = Cond <$> f c <*> f l <*> f r
-traverseExpr f (Func fn e ) = Func fn <$> f e
-traverseExpr _ e = pure e
+-- | Constant expression, which are known before simulation at compile time.
+data ConstExpr = ConstNum { _constSize :: Int
+ , _constNum :: Integer
+ }
+ | ParamId { _constParamId :: {-# UNPACK #-} !Identifier }
+ | ConstConcat { _constConcat :: [ConstExpr] }
+ | ConstUnOp { _constUnOp :: !UnaryOperator
+ , _constPrim :: ConstExpr
+ }
+ | ConstBinOp { _constLhs :: ConstExpr
+ , _constBinOp :: !BinaryOperator
+ , _constRhs :: ConstExpr
+ }
+ | ConstCond { _constCond :: ConstExpr
+ , _constTrue :: ConstExpr
+ , _constFalse :: ConstExpr
+ }
+ | ConstStr { _constStr :: {-# UNPACK #-} !Text }
+ deriving (Eq, Show, Ord, Data)
+
+instance Num ConstExpr where
+ a + b = ConstBinOp a BinPlus b
+ a - b = ConstBinOp a BinMinus b
+ a * b = ConstBinOp a BinTimes b
+ negate = ConstUnOp UnMinus
+ abs = undefined
+ signum = undefined
+ fromInteger = ConstNum 32 . fromInteger
+
+instance Semigroup ConstExpr where
+ (ConstConcat a) <> (ConstConcat b) = ConstConcat $ a <> b
+ (ConstConcat a) <> b = ConstConcat $ a <> [b]
+ a <> (ConstConcat b) = ConstConcat $ a : b
+ a <> b = ConstConcat [a, b]
--- | Constant expression, which are known before simulation at compilation time.
-newtype ConstExpr = ConstExpr { _constNum :: Int }
- deriving (Eq, Show, Ord, Data, Num)
+instance Monoid ConstExpr where
+ mempty = ConstConcat []
+
+instance IsString ConstExpr where
+ fromString = ConstStr . fromString
+
+instance Plated ConstExpr where
+ plate = uniplate
data Task = Task { _taskName :: {-# UNPACK #-} !Identifier
, _taskExpr :: [Expr]
@@ -306,10 +352,11 @@ data PortType = Wire
--
-- This is now implemented inside 'ModDecl' itself, which uses a list of output
-- and input ports.
-data Port = Port { _portType :: !PortType
- , _portSigned :: !Bool
- , _portSize :: {-# UNPACK #-} !Int
- , _portName :: {-# UNPACK #-} !Identifier
+data Port = Port { _portType :: !PortType
+ , _portSigned :: !Bool
+ , _portSizeLower :: {-# UNPACK #-} !Int
+ , _portSize :: {-# UNPACK #-} !Int
+ , _portName :: {-# UNPACK #-} !Identifier
} deriving (Eq, Show, Ord, Data)
-- | This is currently a type because direct module declaration should also be
@@ -343,13 +390,17 @@ data Statement = TimeCtrl { _statDelay :: {-# UNPACK #-} !Delay
| SeqBlock { _statements :: [Statement] } -- ^ Sequential block (@begin ... end@)
| BlockAssign { _stmntBA :: !Assign } -- ^ blocking assignment (@=@)
| NonBlockAssign { _stmntNBA :: !Assign } -- ^ Non blocking assignment (@<=@)
- | StatCA { _stmntCA :: !ContAssign } -- ^ Statement continuous assignment. May not be correct.
| TaskEnable { _stmntTask :: !Task }
| SysTaskEnable { _stmntSysTask :: !Task }
| CondStmnt { _stmntCondExpr :: Expr
, _stmntCondTrue :: Maybe Statement
, _stmntCondFalse :: Maybe Statement
}
+ | ForLoop { _forAssign :: !Assign
+ , _forExpr :: Expr
+ , _forIncr :: !Assign
+ , _forStmnt :: Statement
+ } -- ^ Loop bounds shall be statically computable for a for loop.
deriving (Eq, Show, Ord, Data)
instance Semigroup Statement where
@@ -361,6 +412,19 @@ instance Semigroup Statement where
instance Monoid Statement where
mempty = SeqBlock []
+-- | Parameter that can be assigned in blocks or modules using @parameter@.
+data Parameter = Parameter { _paramIdent :: {-# UNPACK #-} !Identifier
+ , _paramValue :: ConstExpr
+ }
+ deriving (Eq, Show, Ord, Data)
+
+-- | Local parameter that can be assigned anywhere using @localparam@. It cannot
+-- be changed by initialising the module.
+data LocalParam = LocalParam { _localParamIdent :: {-# UNPACK #-} !Identifier
+ , _localParamValue :: ConstExpr
+ }
+ deriving (Eq, Show, Ord, Data)
+
-- | Module item which is the body of the module expression.
data ModItem = ModCA { _modContAssign :: !ContAssign }
| ModInst { _modInstId :: {-# UNPACK #-} !Identifier
@@ -371,7 +435,10 @@ data ModItem = ModCA { _modContAssign :: !ContAssign }
| Always !Statement
| Decl { _declDir :: !(Maybe PortDir)
, _declPort :: !Port
+ , _declVal :: Maybe ConstExpr
}
+ | ParamDecl { _paramDecl :: NonEmpty Parameter }
+ | LocalParamDecl { _localParamDecl :: NonEmpty LocalParam }
deriving (Eq, Show, Ord, Data)
-- | 'module' module_identifier [list_of_ports] ';' { module_item } 'end_module'
@@ -379,7 +446,9 @@ data ModDecl = ModDecl { _modId :: {-# UNPACK #-} !Identifier
, _modOutPorts :: [Port]
, _modInPorts :: [Port]
, _modItems :: [ModItem]
- } deriving (Eq, Show, Ord, Data)
+ , _modParams :: [Parameter]
+ }
+ deriving (Eq, Show, Ord, Data)
traverseModConn :: (Applicative f) => (Expr -> f Expr) -> ModConn -> f ModConn
traverseModConn f (ModConn e ) = ModConn <$> f e
@@ -391,12 +460,8 @@ traverseModItem f (ModInst a b e) =
ModInst a b <$> sequenceA (traverseModConn f <$> e)
traverseModItem _ e = pure e
--- | Description of the Verilog module.
-newtype Description = Description { _getDescription :: ModDecl }
- deriving (Eq, Show, Ord, Data)
-
-- | The complete sourcetext for the Verilog module.
-newtype Verilog = Verilog { _getVerilog :: [Description] }
+newtype Verilog = Verilog { _getVerilog :: [ModDecl] }
deriving (Eq, Show, Ord, Data, Semigroup, Monoid)
makeLenses ''Identifier
@@ -412,206 +477,15 @@ makeLenses ''Assign
makeLenses ''ContAssign
makeLenses ''Statement
makeLenses ''ModItem
+makeLenses ''Parameter
+makeLenses ''LocalParam
makeLenses ''ModDecl
-makeLenses ''Description
makeLenses ''Verilog
getModule :: Traversal' Verilog ModDecl
-getModule = getVerilog . traverse . getDescription
+getModule = getVerilog . traverse
{-# INLINE getModule #-}
getSourceId :: Traversal' Verilog Text
getSourceId = getModule . modId . getIdentifier
{-# INLINE getSourceId #-}
-
-listOf1 :: Gen a -> Gen [a]
-listOf1 a = toList <$> Hog.nonEmpty (Hog.linear 0 100) a
-
-listOf :: Gen a -> Gen [a]
-listOf = Hog.list (Hog.linear 0 100)
-
-genPositive :: Gen Int
-genPositive = Hog.filter (>= 0) $ Hog.int (Hog.linear 1 99)
-
-integral :: Gen Integer
-integral = Hog.integral (Hog.linear 0 100)
-
-class Arb a where
- arb :: Gen a
-
-instance Arb Identifier where
- arb = do
- l <- genPositive
- Identifier . T.pack <$> replicateM (l + 1) (Hog.element ['a'..'z'])
-
-instance Arb Delay where
- arb = Delay <$> genPositive
-
-instance Arb Event where
- arb = EId <$> arb
-
-instance Arb BinaryOperator where
- arb = Hog.element
- [ BinPlus
- , BinMinus
- , BinTimes
- -- , BinDiv
- -- , BinMod
- , BinEq
- , BinNEq
- -- , BinCEq
- -- , BinCNEq
- , BinLAnd
- , BinLOr
- , BinLT
- , BinLEq
- , BinGT
- , BinGEq
- , BinAnd
- , BinOr
- , BinXor
- , BinXNor
- , BinXNorInv
- -- , BinPower
- , BinLSL
- , BinLSR
- , BinASL
- , BinASR
- ]
-
-instance Arb UnaryOperator where
- arb = Hog.element
- [ UnPlus
- , UnMinus
- , UnNot
- , UnLNot
- , UnAnd
- , UnNand
- , UnOr
- , UnNor
- , UnXor
- , UnNxor
- , UnNxorInv
- ]
-
-instance Arb Function where
- arb = Hog.element
- [ SignedFunc
- , UnSignedFunc
- ]
-
-instance Arb Expr where
- arb = Hog.sized expr
-
-exprSafeList :: [Gen Expr]
-exprSafeList = [Number <$> genPositive <*> integral]
-
-exprRecList :: (Hog.Size -> Gen Expr) -> [Gen Expr]
-exprRecList subexpr =
- [ Number <$> genPositive <*> integral
- , Concat <$> listOf1 (subexpr 8)
- , UnOp
- <$> arb
- <*> subexpr 2
- -- , Str <$> arb
- , BinOp <$> subexpr 2 <*> arb <*> subexpr 2
- , Cond <$> subexpr 3 <*> subexpr 3 <*> subexpr 3
- , Func <$> arb <*> subexpr 2
- ]
-
-expr :: Hog.Size -> Gen Expr
-expr n | n == 0 = Hog.choice $ (Id <$> arb) : exprSafeList
- | n > 0 = Hog.choice $ (Id <$> arb) : exprRecList subexpr
- | otherwise = expr 0
- where subexpr y = expr (n `div` y)
-
-exprWithContext :: [Identifier] -> Hog.Size -> Gen Expr
-exprWithContext [] n | n == 0 = Hog.choice exprSafeList
- | n > 0 = Hog.choice $ exprRecList subexpr
- | otherwise = exprWithContext [] 0
- where subexpr y = exprWithContext [] (n `div` y)
-exprWithContext l n
- | n == 0 = Hog.choice $ (Id <$> Hog.element l) : exprSafeList
- | n > 0 = Hog.choice $ (Id <$> Hog.element l) : exprRecList subexpr
- | otherwise = exprWithContext l 0
- where subexpr y = exprWithContext l (n `div` y)
-
-instance Arb Int where
- arb = Hog.int (Hog.linear 0 100)
-
-instance Arb ConstExpr where
- arb = ConstExpr <$> Hog.int (Hog.linear 0 100)
-
-instance Arb Task where
- arb = Task <$> arb <*> listOf arb
-
-instance Arb LVal where
- arb = Hog.choice [ RegId <$> arb
- , RegExpr <$> arb <*> arb
- , RegSize <$> arb <*> arb <*> arb
- ]
-
-instance Arb PortDir where
- arb = Hog.element [PortIn, PortOut, PortInOut]
-
-instance Arb PortType where
- arb = Hog.element [Wire, Reg]
-
-instance Arb Port where
- arb = Port <$> arb <*> arb <*> genPositive <*> arb
-
-instance Arb ModConn where
- arb = ModConn <$> arb
-
-instance Arb Assign where
- arb = Assign <$> arb <*> Hog.maybe arb <*> arb
-
-instance Arb ContAssign where
- arb = ContAssign <$> arb <*> arb
-
-instance Arb Statement where
- arb = Hog.sized statement
-
-statement :: Hog.Size -> Gen Statement
-statement n
- | n == 0 = Hog.choice
- [ BlockAssign <$> arb
- , NonBlockAssign <$> arb
- -- , StatCA <$> arb
- , TaskEnable <$> arb
- , SysTaskEnable <$> arb
- ]
- | n > 0 = Hog.choice
- [ TimeCtrl <$> arb <*> (Just <$> substat 2)
- , SeqBlock <$> listOf1 (substat 4)
- , BlockAssign <$> arb
- , NonBlockAssign <$> arb
- -- , StatCA <$> arb
- , TaskEnable <$> arb
- , SysTaskEnable <$> arb
- ]
- | otherwise = statement 0
- where substat y = statement (n `div` y)
-
-instance Arb ModItem where
- arb = Hog.choice [ ModCA <$> arb
- , ModInst <$> arb <*> arb <*> listOf arb
- , Initial <$> arb
- , Always <$> (EventCtrl <$> arb <*> Hog.maybe arb)
- , Decl <$> pure Nothing <*> arb
- ]
-
-modPortGen :: Gen Port
-modPortGen = Port <$> arb <*> arb <*> arb <*> arb
-
-instance Arb ModDecl where
- arb = ModDecl <$> arb <*> listOf arb <*> listOf1 modPortGen <*> listOf arb
-
-instance Arb Description where
- arb = Description <$> arb
-
-instance Arb Verilog where
- arb = Verilog <$> listOf1 arb
-
-instance Arb Bool where
- arb = Hog.element [True, False]
diff --git a/src/VeriFuzz/Verilog/CodeGen.hs b/src/VeriFuzz/Verilog/CodeGen.hs
index a05309f..3a8d14a 100644
--- a/src/VeriFuzz/Verilog/CodeGen.hs
+++ b/src/VeriFuzz/Verilog/CodeGen.hs
@@ -23,6 +23,7 @@ where
import Control.Lens (view, (^.))
import Data.Foldable (fold)
+import Data.List.NonEmpty (NonEmpty (..), toList)
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.Text.IO as T
@@ -44,30 +45,44 @@ defMap = maybe ";\n" statement
-- | Convert the 'Verilog' type to 'Text' so that it can be rendered.
verilogSrc :: Verilog -> Text
-verilogSrc source = fold $ description <$> source ^. getVerilog
-
--- | Generate the 'Description' to 'Text'.
-description :: Description -> Text
-description desc = moduleDecl $ desc ^. getDescription
+verilogSrc (Verilog modules) = fold $ moduleDecl <$> modules
-- | Generate the 'ModDecl' for a module and convert it to 'Text'.
moduleDecl :: ModDecl -> Text
-moduleDecl m =
+moduleDecl (ModDecl i outP inP items ps) =
"module "
- <> m
- ^. modId
- . getIdentifier
+ <> identifier i
+ <> params ps
<> ports
<> ";\n"
<> modI
<> "endmodule\n"
where
- ports | noIn && noOut = ""
- | otherwise = "(" <> comma (modPort <$> outIn) <> ")"
- modI = fold $ moduleItem <$> m ^. modItems
- noOut = null $ m ^. modOutPorts
- noIn = null $ m ^. modInPorts
- outIn = (m ^. modOutPorts) ++ (m ^. modInPorts)
+ ports | null outP && null inP = ""
+ | otherwise = "(" <> comma (modPort <$> outIn) <> ")"
+ modI = fold $ moduleItem <$> items
+ outIn = outP ++ inP
+ params [] = ""
+ params (p : pps) = "\n#(\n" <> paramList (p :| pps) <> "\n)\n"
+
+-- | Generates a parameter list. Can only be called with a 'NonEmpty' list.
+paramList :: NonEmpty Parameter -> Text
+paramList ps = "parameter " <> (commaNL . toList $ parameter <$> ps)
+
+-- | Generates a localparam list. Can only be called with a 'NonEmpty' list.
+localParamList :: NonEmpty LocalParam -> Text
+localParamList ps = "localparam " <> (commaNL . toList $ localParam <$> ps)
+
+-- | Generates the assignment for a 'Parameter'.
+parameter :: Parameter -> Text
+parameter (Parameter name val) = identifier name <> " = " <> constExpr val
+
+-- | Generates the assignment for a 'LocalParam'.
+localParam :: LocalParam -> Text
+localParam (LocalParam name val) = identifier name <> " = " <> constExpr val
+
+identifier :: Identifier -> Text
+identifier (Identifier i) = i
-- | Conversts 'Port' to 'Text' for the module list, which means it only
-- generates a list of identifiers.
@@ -76,13 +91,11 @@ modPort p = p ^. portName . getIdentifier
-- | Generate the 'Port' description.
port :: Port -> Text
-port p = t <> sign <> size <> name
+port (Port tp sgn low sz (Identifier name)) = t <> sign <> size <> name
where
- t = flip mappend " " . pType $ p ^. portType
- size | p ^. portSize > 1 = "[" <> showT (p ^. portSize - 1) <> ":0] "
- | otherwise = ""
- name = p ^. portName . getIdentifier
- sign = signed $ p ^. portSigned
+ t = flip mappend " " $ pType tp
+ size = "[" <> showT (low+sz-1) <> ":" <> showT low <> "] "
+ sign = signed sgn
signed :: Bool -> Text
signed True = "signed "
@@ -101,8 +114,13 @@ moduleItem (ModInst (Identifier i) (Identifier name) conn) =
i <> " " <> name <> "(" <> comma (mConn <$> conn) <> ")" <> ";\n"
moduleItem (Initial stat) = "initial " <> statement stat
moduleItem (Always stat) = "always " <> statement stat
-moduleItem (Decl dir p ) = maybe "" makePort dir <> port p <> ";\n"
- where makePort = (<> " ") . portDir
+moduleItem (Decl dir p ini) =
+ maybe "" makePort dir <> port p <> maybe "" makeIni ini <> ";\n"
+ where
+ makePort = (<> " ") . portDir
+ makeIni = (" = " <>) . constExpr
+moduleItem (ParamDecl p) = paramList p <> ";\n"
+moduleItem (LocalParamDecl p) = localParamList p <> ";\n"
mConn :: ModConn -> Text
mConn (ModConn c ) = expr c
@@ -116,17 +134,13 @@ contAssign (ContAssign val e) =
-- | Generate 'Function' to 'Text'
func :: Function -> Text
func SignedFunc = "$signed"
-func UnSignedFunc = "$unsigned"
+func UnsignedFunc = "$unsigned"
-- | Generate 'Expr' to 'Text'.
expr :: Expr -> Text
expr (BinOp eRhs bin eLhs) =
"(" <> expr eRhs <> binaryOp bin <> expr eLhs <> ")"
-expr (Number s n) =
- "(" <> minus <> showT s <> "'h" <> T.pack (showHex (abs n) "") <> ")"
- where
- minus | signum n >= 0 = ""
- | otherwise = "-"
+expr (Number s n) = showNum s n
expr (Id i ) = i ^. getIdentifier
expr (Concat c ) = "{" <> comma (expr <$> c) <> "}"
expr (UnOp u e ) = "(" <> unaryOp u <> expr e <> ")"
@@ -134,6 +148,24 @@ expr (Cond l t f) = "(" <> expr l <> " ? " <> expr t <> " : " <> expr f <> ")"
expr (Func f e ) = func f <> "(" <> expr e <> ")"
expr (Str t ) = "\"" <> t <> "\""
+showNum :: Int -> Integer -> Text
+showNum s n =
+ "(" <> minus <> showT s <> "'h" <> T.pack (showHex (abs n) "") <> ")"
+ where
+ minus | signum n >= 0 = ""
+ | otherwise = "-"
+
+constExpr :: ConstExpr -> Text
+constExpr (ConstNum s n ) = showNum s n
+constExpr (ParamId i) = identifier i
+constExpr (ConstConcat c) = "{" <> comma (constExpr <$> c) <> "}"
+constExpr (ConstUnOp u e) = "(" <> unaryOp u <> constExpr e <> ")"
+constExpr (ConstBinOp eRhs bin eLhs) =
+ "(" <> constExpr eRhs <> binaryOp bin <> constExpr eLhs <> ")"
+constExpr (ConstCond l t f) =
+ "(" <> constExpr l <> " ? " <> constExpr t <> " : " <> constExpr f <> ")"
+constExpr (ConstStr t) = "\"" <> t <> "\""
+
-- | Convert 'BinaryOperator' to 'Text'.
binaryOp :: BinaryOperator -> Text
binaryOp BinPlus = " + "
@@ -196,9 +228,6 @@ lVal (RegSize i msb lsb) =
i ^. getIdentifier <> " [" <> constExpr msb <> ":" <> constExpr lsb <> "]"
lVal (RegConcat e) = "{" <> comma (expr <$> e) <> "}"
-constExpr :: ConstExpr -> Text
-constExpr (ConstExpr num) = showT num
-
pType :: PortType -> Text
pType Wire = "wire"
pType Reg = "reg"
@@ -212,12 +241,20 @@ statement (EventCtrl e stat ) = event e <> " " <> defMap stat
statement (SeqBlock s) = "begin\n" <> fold (statement <$> s) <> "end\n"
statement (BlockAssign a ) = genAssign " = " a <> ";\n"
statement (NonBlockAssign a ) = genAssign " <= " a <> ";\n"
-statement (StatCA a ) = contAssign a
statement (TaskEnable t ) = task t <> ";\n"
statement (SysTaskEnable t ) = "$" <> task t <> ";\n"
statement (CondStmnt e t Nothing) = "if(" <> expr e <> ")\n" <> defMap t
statement (CondStmnt e t f) =
"if(" <> expr e <> ")\n" <> defMap t <> "else\n" <> defMap f
+statement (ForLoop a e incr stmnt) =
+ "for("
+ <> genAssign " = " a
+ <> "; "
+ <> expr e
+ <> "; "
+ <> genAssign " = " incr
+ <> ")\n"
+ <> statement stmnt
task :: Task -> Text
task (Task name e) | null e = i
@@ -275,19 +312,13 @@ instance Source Port where
instance Source ModDecl where
genSource = moduleDecl
-instance Source Description where
- genSource = description
-
instance Source Verilog where
genSource = verilogSrc
+instance Source SourceInfo where
+ genSource (SourceInfo _ src) = genSource src
+
newtype GenVerilog a = GenVerilog { unGenVerilog :: a }
instance (Source a) => Show (GenVerilog a) where
show = T.unpack . genSource . unGenVerilog
-
-instance (Arb a) => Arb (GenVerilog a) where
- arb = GenVerilog <$> arb
-
-instance Source SourceInfo where
- genSource (SourceInfo _ src) = genSource src
diff --git a/src/VeriFuzz/Verilog/Gen.hs b/src/VeriFuzz/Verilog/Gen.hs
index 87a0a31..c325f66 100644
--- a/src/VeriFuzz/Verilog/Gen.hs
+++ b/src/VeriFuzz/Verilog/Gen.hs
@@ -15,6 +15,7 @@ Various useful generators.
module VeriFuzz.Verilog.Gen
( -- * Generation methods
procedural
+ , proceduralIO
, randomMod
)
where
@@ -25,9 +26,11 @@ import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Reader hiding (local)
import Control.Monad.Trans.State.Lazy
import Data.Foldable (fold)
+import Data.List.NonEmpty (toList)
import qualified Data.Text as T
import Hedgehog (Gen)
import qualified Hedgehog.Gen as Hog
+import qualified Hedgehog.Range as Hog
import VeriFuzz.Config
import VeriFuzz.Internal
import VeriFuzz.Verilog.AST
@@ -35,8 +38,11 @@ import VeriFuzz.Verilog.Internal
import VeriFuzz.Verilog.Mutate
data Context = Context { _variables :: [Port]
- , _nameCounter :: Int
- , _stmntDepth :: Int
+ , _parameters :: [Parameter]
+ , _modules :: [ModDecl]
+ , _nameCounter :: {-# UNPACK #-} !Int
+ , _stmntDepth :: {-# UNPACK #-} !Int
+ , _modDepth :: {-# UNPACK #-} !Int
}
makeLenses ''Context
@@ -48,7 +54,7 @@ toId = Identifier . ("w" <>) . T.pack . show
toPort :: Identifier -> Gen Port
toPort ident = do
- i <- genPositive
+ i <- Hog.int $ Hog.linear 1 100
return $ wire i ident
sumSize :: [Port] -> Int
@@ -56,7 +62,7 @@ sumSize ps = sum $ ps ^.. traverse . portSize
random :: [Identifier] -> (Expr -> ContAssign) -> Gen ModItem
random ctx fun = do
- expr <- Hog.sized (exprWithContext ctx)
+ expr <- Hog.sized (exprWithContext (ProbExpr 1 1 1 1 1 1 0 1 1) ctx)
return . ModCA $ fun expr
--randomAssigns :: [Identifier] -> [Gen ModItem]
@@ -74,7 +80,11 @@ randomMod inps total = do
let other = drop inps ident
let y = ModCA . ContAssign "y" . fold $ Id <$> drop inps ids
let yport = [wire (sumSize other) "y"]
- return . declareMod other . ModDecl "test_module" yport inputs_ $ x ++ [y]
+ return . declareMod other $ ModDecl "test_module"
+ yport
+ inputs_
+ (x ++ [y])
+ []
where
ids = toId <$> [1 .. total]
end = drop inps ids
@@ -83,9 +93,136 @@ randomMod inps total = do
gen :: Gen a -> StateGen a
gen = lift . lift
+listOf1 :: Gen a -> Gen [a]
+listOf1 a = toList <$> Hog.nonEmpty (Hog.linear 0 100) a
+
+--listOf :: Gen a -> Gen [a]
+--listOf = Hog.list (Hog.linear 0 100)
+
+largeNum :: Gen Int
+largeNum = Hog.int Hog.linearBounded
+
+wireSize :: Gen Int
+wireSize = Hog.int $ Hog.linear 2 200
+
+binOp :: Gen BinaryOperator
+binOp =
+ Hog.element
+ [ BinPlus
+ , BinMinus
+ , BinTimes
+ -- , BinDiv
+ -- , BinMod
+ , BinEq
+ , BinNEq
+ -- , BinCEq
+ -- , BinCNEq
+ , BinLAnd
+ , BinLOr
+ , BinLT
+ , BinLEq
+ , BinGT
+ , BinGEq
+ , BinAnd
+ , BinOr
+ , BinXor
+ , BinXNor
+ , BinXNorInv
+ -- , BinPower
+ , BinLSL
+ , BinLSR
+ , BinASL
+ , BinASR
+ ]
+
+unOp :: Gen UnaryOperator
+unOp =
+ Hog.element
+ [ UnPlus
+ , UnMinus
+ , UnNot
+ , UnLNot
+ , UnAnd
+ , UnNand
+ , UnOr
+ , UnNor
+ , UnXor
+ , UnNxor
+ , UnNxorInv
+ ]
+
+constExprWithContext :: [Parameter] -> ProbExpr -> Hog.Size -> Gen ConstExpr
+constExprWithContext ps prob size
+ | size == 0 = Hog.frequency
+ [ (prob ^. probExprNum, ConstNum <$> wireSize <*> fmap fromIntegral largeNum)
+ , ( if null ps then 0 else prob ^. probExprId
+ , ParamId . view paramIdent <$> Hog.element ps
+ )
+ ]
+ | size > 0 = Hog.frequency
+ [ (prob ^. probExprNum, ConstNum <$> wireSize <*> fmap fromIntegral largeNum)
+ , ( if null ps then 0 else prob ^. probExprId
+ , ParamId . view paramIdent <$> Hog.element ps
+ )
+ , (prob ^. probExprUnOp, ConstUnOp <$> unOp <*> subexpr 2)
+ , ( prob ^. probExprBinOp
+ , ConstBinOp <$> subexpr 2 <*> binOp <*> subexpr 2
+ )
+ , ( prob ^. probExprCond
+ , ConstCond <$> subexpr 3 <*> subexpr 3 <*> subexpr 3
+ )
+ , (prob ^. probExprConcat, ConstConcat <$> listOf1 (subexpr 8))
+ ]
+ | otherwise = constExprWithContext ps prob 0
+ where subexpr y = constExprWithContext ps prob $ size `div` y
+
+exprSafeList :: ProbExpr -> [(Int, Gen Expr)]
+exprSafeList prob =
+ [ ( prob ^. probExprNum
+ , Number <$> wireSize <*> fmap fromIntegral largeNum
+ )
+ ]
+
+exprRecList :: ProbExpr -> (Hog.Size -> Gen Expr) -> [(Int, Gen Expr)]
+exprRecList prob subexpr =
+ [ ( prob ^. probExprNum
+ , Number <$> wireSize <*> fmap fromIntegral largeNum
+ )
+ , (prob ^. probExprConcat , Concat <$> listOf1 (subexpr 8))
+ , (prob ^. probExprUnOp , UnOp <$> unOp <*> subexpr 2)
+ , (prob ^. probExprStr, Str <$> Hog.text (Hog.linear 0 100) Hog.alphaNum)
+ , (prob ^. probExprBinOp , BinOp <$> subexpr 2 <*> binOp <*> subexpr 2)
+ , (prob ^. probExprCond , Cond <$> subexpr 3 <*> subexpr 3 <*> subexpr 3)
+ , (prob ^. probExprSigned , Func <$> pure SignedFunc <*> subexpr 2)
+ , (prob ^. probExprUnsigned, Func <$> pure UnsignedFunc <*> subexpr 2)
+ ]
+
+exprWithContext :: ProbExpr -> [Identifier] -> Hog.Size -> Gen Expr
+exprWithContext prob [] n | n == 0 = Hog.frequency $ exprSafeList prob
+ | n > 0 = Hog.frequency $ exprRecList prob subexpr
+ | otherwise = exprWithContext prob [] 0
+ where subexpr y = exprWithContext prob [] $ n `div` y
+exprWithContext prob l n
+ | n == 0
+ = Hog.frequency
+ $ (prob ^. probExprId, Id <$> Hog.element l)
+ : exprSafeList prob
+ | n > 0
+ = Hog.frequency
+ $ (prob ^. probExprId, Id <$> Hog.element l)
+ : exprRecList prob subexpr
+ | otherwise
+ = exprWithContext prob l 0
+ where subexpr y = exprWithContext prob l $ n `div` y
+
some :: StateGen a -> StateGen [a]
some f = do
- amount <- gen genPositive
+ amount <- gen $ Hog.int (Hog.linear 1 100)
+ replicateM amount f
+
+many :: StateGen a -> StateGen [a]
+many f = do
+ amount <- gen $ Hog.int (Hog.linear 0 100)
replicateM amount f
makeIdentifier :: T.Text -> StateGen Identifier
@@ -98,32 +235,28 @@ makeIdentifier prefix = do
newPort :: PortType -> StateGen Port
newPort pt = do
ident <- makeIdentifier . T.toLower $ showT pt
- p <- gen $ Port pt <$> arb <*> genPositive <*> pure ident
+ p <- gen $ Port pt <$> Hog.bool <*> pure 0 <*> wireSize <*> pure ident
variables %= (p :)
return p
-choose :: PortType -> Port -> Bool
-choose ptype (Port a _ _ _) = ptype == a
-
scopedExpr :: StateGen Expr
scopedExpr = do
context <- get
- gen
- . Hog.sized
- . exprWithContext
- $ context
- ^.. variables
- . traverse
- . portName
+ prob <- askProbability
+ gen . Hog.sized . exprWithContext (prob ^. probExpr) $ vars context
+ where
+ vars cont =
+ (cont ^.. variables . traverse . portName)
+ <> (cont ^.. parameters . traverse . paramIdent)
contAssign :: StateGen ContAssign
contAssign = do
expr <- scopedExpr
- p <- newPort Wire
+ p <- newPort Wire
return $ ContAssign (p ^. portName) expr
lvalFromPort :: Port -> LVal
-lvalFromPort (Port _ _ _ i) = RegId i
+lvalFromPort (Port _ _ _ _ i) = RegId i
probability :: Config -> Probability
probability c = c ^. configProbability
@@ -137,23 +270,51 @@ assignment = do
lval <- lvalFromPort <$> newPort Reg
return $ Assign lval Nothing expr
-conditional :: StateGen Statement
-conditional = do
- expr <- scopedExpr
+seqBlock :: StateGen Statement
+seqBlock = do
stmntDepth -= 1
tstat <- SeqBlock <$> some statement
- fstat <- Hog.maybe $ SeqBlock <$> some statement
stmntDepth += 1
- return $ CondStmnt (BinOp expr BinEq 0) (Just tstat) fstat
+ return tstat
+
+conditional :: StateGen Statement
+conditional = do
+ expr <- scopedExpr
+ tstat <- seqBlock
+ fstat <- Hog.maybe seqBlock
+ return $ CondStmnt expr (Just tstat) fstat
+
+--constToExpr :: ConstExpr -> Expr
+--constToExpr (ConstNum s n ) = Number s n
+--constToExpr (ParamId i ) = Id i
+--constToExpr (ConstConcat c ) = Concat $ constToExpr <$> c
+--constToExpr (ConstUnOp u p ) = UnOp u (constToExpr p)
+--constToExpr (ConstBinOp a b c) = BinOp (constToExpr a) b (constToExpr c)
+--constToExpr (ConstCond a b c) =
+-- Cond (constToExpr a) (constToExpr b) (constToExpr c)
+--constToExpr (ConstStr s) = Str s
+
+forLoop :: StateGen Statement
+forLoop = do
+ num <- Hog.int (Hog.linear 0 20)
+ var <- lvalFromPort <$> newPort Reg
+ stats <- seqBlock
+ return $ ForLoop (Assign var Nothing 0)
+ (BinOp (varId var) BinLT $ fromIntegral num)
+ (Assign var Nothing $ BinOp (varId var) BinPlus 1)
+ stats
+ where varId v = Id (v ^. regId)
statement :: StateGen Statement
statement = do
prob <- askProbability
cont <- get
+ let defProb i = prob ^. probStmnt . i
Hog.frequency
- [ (prob ^. probBlock , BlockAssign <$> assignment)
- , (prob ^. probNonBlock , NonBlockAssign <$> assignment)
- , (onDepth cont (prob ^. probCond), conditional)
+ [ (defProb probStmntBlock , BlockAssign <$> assignment)
+ , (defProb probStmntNonBlock , NonBlockAssign <$> assignment)
+ , (onDepth cont (defProb probStmntCond), conditional)
+ , (onDepth cont (defProb probStmntFor) , forLoop)
]
where onDepth c n = if c ^. stmntDepth > 0 then n else 0
@@ -162,26 +323,98 @@ always = do
stat <- SeqBlock <$> some statement
return $ Always (EventCtrl (EPosEdge "clk") (Just stat))
+instantiate :: ModDecl -> StateGen ModItem
+instantiate (ModDecl i outP inP _ _) = do
+ context <- get
+ outs <-
+ fmap (Id . view portName) <$> (replicateM (length outP) $ newPort Wire)
+ ins <-
+ (Id "clk" :)
+ . fmap (Id . view portName)
+ . take (length inP - 1)
+ <$> (Hog.shuffle $ context ^. variables)
+ ident <- makeIdentifier "modinst"
+ Hog.choice
+ [ return . ModInst i ident $ ModConn <$> outs <> ins
+ , ModInst i ident <$> Hog.shuffle
+ (zipWith ModConnNamed (view portName <$> outP <> inP) (outs <> ins))
+ ]
+
+-- | Generates a module instance by also generating a new module if there are
+-- not enough modules currently in the context. It keeps generating new modules
+-- for every instance and for every level until either the deepest level is
+-- achieved, or the maximum number of modules are reached.
+--
+-- If the maximum number of levels are reached, it will always pick an instance
+-- from the current context. The problem with this approach is that at the end
+-- there may be many more than the max amount of modules, as the modules are
+-- always set to empty when entering a new level. This is to fix recursive
+-- definitions of modules, which are not defined.
+--
+-- One way to fix that is to also decrement the max modules for every level,
+-- depending on how many modules have already been generated. This would mean
+-- there would be moments when the module cannot generate a new instance but
+-- also not take a module from the current context. A fix for that may be to
+-- have a default definition of a simple module that is used instead.
+--
+-- Another different way to handle this would be to have a probability of taking
+-- a module from a context or generating a new one.
+modInst :: StateGen ModItem
+modInst = do
+ prob <- lift ask
+ context <- get
+ let maxMods = prob ^. configProperty . propMaxModules
+ if length (context ^. modules) < maxMods
+ then do
+ let currMods = context ^. modules
+ let params = context ^. parameters
+ let vars = context ^. variables
+ modules .= []
+ variables .= []
+ parameters .= []
+ modDepth -= 1
+ chosenMod <- moduleDef Nothing
+ ncont <- get
+ let genMods = ncont ^. modules
+ modDepth += 1
+ parameters .= params
+ variables .= vars
+ modules .= chosenMod : currMods <> genMods
+ instantiate chosenMod
+ else Hog.element (context ^. modules) >>= instantiate
+
-- | Generate a random module item.
modItem :: StateGen ModItem
modItem = do
- prob <- askProbability
+ prob <- askProbability
+ context <- get
+ let defProb i = prob ^. probModItem . i
Hog.frequency
- [ (prob ^. probAssign, ModCA <$> contAssign)
- , (prob ^. probAlways, always)
+ [ (defProb probModItemAssign, ModCA <$> contAssign)
+ , (defProb probModItemAlways, always)
+ , ( if context ^. modDepth > 0 then defProb probModItemInst else 0
+ , modInst
+ )
]
moduleName :: Maybe Identifier -> StateGen Identifier
moduleName (Just t) = return t
-moduleName Nothing = gen arb
+moduleName Nothing = makeIdentifier "module"
-initialBlock :: StateGen ModItem
-initialBlock = do
+constExpr :: StateGen ConstExpr
+constExpr = do
+ prob <- askProbability
context <- get
- let l = filter (choose Reg) $ context ^.. variables . traverse
- return . Initial . SeqBlock $ makeAssign <$> l
- where
- makeAssign p = NonBlockAssign $ Assign (lvalFromPort p) Nothing 0
+ gen . Hog.sized $ constExprWithContext (context ^. parameters)
+ (prob ^. probExpr)
+
+parameter :: StateGen Parameter
+parameter = do
+ ident <- makeIdentifier "param"
+ cexpr <- constExpr
+ let param = Parameter ident cexpr
+ parameters %= (param :)
+ return param
-- | 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
@@ -191,22 +424,29 @@ moduleDef :: Maybe Identifier -> StateGen ModDecl
moduleDef top = do
name <- moduleName top
portList <- some $ newPort Wire
- mi <- some modItem
+ mi <- Hog.list (Hog.linear 4 100) modItem
context <- get
- initBlock <- initialBlock
let local = filter (`notElem` portList) $ context ^. variables
let size = 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) $ initBlock : mi <> [comb]
+ let clock = Port Wire False 0 1 "clk"
+ let yport = Port Wire False 0 size "y"
+ let comb = combineAssigns_ yport local
+ declareMod local
+ . ModDecl name [yport] (clock : portList) (mi <> [comb])
+ <$> many parameter
-- | Procedural generation method for random Verilog. Uses internal 'Reader' and
-- 'State' to keep track of the current Verilog code structure.
procedural :: Config -> Gen Verilog
-procedural config = Verilog . (: []) . Description <$> Hog.resize
- num
- (runReaderT (evalStateT (moduleDef (Just "top")) context) config)
+procedural config = do
+ (mainMod, st) <- Hog.resize num
+ $ runReaderT (runStateT (moduleDef (Just "top")) context) config
+ return . Verilog $ mainMod : st ^. modules
where
- context = Context [] 0 $ config ^. configProperty . propDepth
- num = fromIntegral $ config ^. configProperty . propSize
+ context =
+ Context [] [] [] 0 (confProp propStmntDepth) $ confProp propModDepth
+ num = fromIntegral $ confProp propSize
+ confProp i = config ^. configProperty . i
+
+proceduralIO :: Config -> IO Verilog
+proceduralIO = Hog.sample . procedural
diff --git a/src/VeriFuzz/Verilog/Internal.hs b/src/VeriFuzz/Verilog/Internal.hs
index 5999a31..63072b1 100644
--- a/src/VeriFuzz/Verilog/Internal.hs
+++ b/src/VeriFuzz/Verilog/Internal.hs
@@ -16,7 +16,7 @@ module VeriFuzz.Verilog.Internal
, emptyMod
, setModName
, addModPort
- , addDescription
+ , addModDecl
, testBench
, addTestBench
, defaultPort
@@ -33,14 +33,14 @@ import Data.Text (Text)
import VeriFuzz.Verilog.AST
regDecl :: Identifier -> ModItem
-regDecl = Decl Nothing . Port Reg False 1
+regDecl i = Decl Nothing (Port Reg False 0 1 i) Nothing
wireDecl :: Identifier -> ModItem
-wireDecl = Decl Nothing . Port Wire False 1
+wireDecl i = Decl Nothing (Port Wire False 0 1 i) Nothing
-- | Create an empty module.
emptyMod :: ModDecl
-emptyMod = ModDecl "" [] [] []
+emptyMod = ModDecl "" [] [] [] []
-- | Set a module name for a module declaration.
setModName :: Text -> ModDecl -> ModDecl
@@ -50,8 +50,8 @@ setModName str = modId .~ Identifier str
addModPort :: Port -> ModDecl -> ModDecl
addModPort port = modInPorts %~ (:) port
-addDescription :: Description -> Verilog -> Verilog
-addDescription desc = getVerilog %~ (:) desc
+addModDecl :: ModDecl -> Verilog -> Verilog
+addModDecl desc = getVerilog %~ (:) desc
testBench :: ModDecl
testBench = ModDecl
@@ -76,24 +76,25 @@ testBench = ModDecl
-- , SysTaskEnable $ Task "finish" []
]
]
+ []
addTestBench :: Verilog -> Verilog
-addTestBench = addDescription $ Description testBench
+addTestBench = addModDecl testBench
defaultPort :: Identifier -> Port
-defaultPort = Port Wire False 1
+defaultPort = Port Wire False 0 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
+yPort = Port Wire False 0 90
wire :: Int -> Identifier -> Port
-wire = Port Wire False
+wire = Port Wire False 0
reg :: Int -> Identifier -> Port
-reg = Port Reg False
+reg = Port Reg False 0
diff --git a/src/VeriFuzz/Verilog/Mutate.hs b/src/VeriFuzz/Verilog/Mutate.hs
index 03ee1d0..536ebef 100644
--- a/src/VeriFuzz/Verilog/Mutate.hs
+++ b/src/VeriFuzz/Verilog/Mutate.hs
@@ -72,7 +72,7 @@ idTrans _ _ e = e
-- | Replaces the identifier recursively in an expression.
replace :: Identifier -> Expr -> Expr -> Expr
-replace = (transformOf traverseExpr .) . idTrans
+replace = (transform .) . idTrans
-- | Nest expressions for a specific 'Identifier'. If the 'Identifier' is not
-- found, the AST is not changed.
@@ -107,8 +107,8 @@ allVars m =
-- $setup
-- >>> import VeriFuzz.Verilog.CodeGen
--- >>> let m = (ModDecl (Identifier "m") [Port Wire False 5 (Identifier "y")] [Port Wire False 5 "x"] [])
--- >>> let main = (ModDecl "main" [] [] [])
+-- >>> let m = (ModDecl (Identifier "m") [Port Wire False 0 5 (Identifier "y")] [Port Wire False 0 5 "x"] [] [])
+-- >>> let main = (ModDecl "main" [] [] [] [])
-- | Add a Module Instantiation using 'ModInst' from the first module passed to
-- it to the body of the second module. It first has to make all the inputs into
@@ -124,11 +124,14 @@ allVars m =
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)
- inst = ModInst (m ^. modId)
- (m ^. modId <> (Identifier . showT $ count + 1))
- conns
+ out = Decl Nothing <$> m ^. modOutPorts <*> pure Nothing
+ regIn =
+ Decl Nothing
+ <$> (m ^. modInPorts & traverse . portType .~ Reg)
+ <*> pure Nothing
+ inst = ModInst (m ^. modId)
+ (m ^. modId <> (Identifier . showT $ count + 1))
+ conns
count =
length
. filter (== m ^. modId)
@@ -185,8 +188,8 @@ filterChar t ids =
initMod :: ModDecl -> ModDecl
initMod m = m & modItems %~ ((out ++ inp) ++)
where
- out = Decl (Just PortOut) <$> (m ^. modOutPorts)
- inp = Decl (Just PortIn) <$> (m ^. modInPorts)
+ out = Decl (Just PortOut) <$> (m ^. modOutPorts) <*> pure Nothing
+ inp = Decl (Just PortIn) <$> (m ^. modInPorts) <*> pure Nothing
-- | Make an 'Identifier' from and existing Identifier and an object with a
-- 'Show' instance to make it unique.
@@ -196,7 +199,7 @@ 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 ^. modId) ys (m ^. modInPorts) modIt
+makeTop i m = ModDecl (m ^. modId) ys (m ^. modInPorts) modIt []
where
ys = yPort . flip makeIdFrom "y" <$> [1 .. i]
modIt = instantiateModSpec_ "_" . modN <$> [1 .. i]
@@ -206,17 +209,20 @@ makeTop i m = ModDecl (m ^. modId) ys (m ^. modInPorts) modIt
-- | 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.
makeTopAssert :: ModDecl -> ModDecl
-makeTopAssert = (modItems %~ (++ [assert])) . makeTop
- 2
+makeTopAssert = (modItems %~ (++ [assert])) . makeTop 2
where
assert = Always . EventCtrl e . Just $ SeqBlock
[TaskEnable $ Task "assert" [BinOp (Id "y_1") BinEq (Id "y_2")]]
- e = EPosEdge "clk"
+ e = EPosEdge "clk"
--- | Provide declarations for all the ports that are passed to it.
+-- | Provide declarations for all the ports that are passed to it. If they are
+-- registers, it should assign them to 0.
declareMod :: [Port] -> ModDecl -> ModDecl
declareMod ports = initMod . (modItems %~ (decl ++))
- where decl = Decl Nothing <$> ports
+ where
+ decl = declf <$> ports
+ declf p@(Port Reg _ _ _ _) = Decl Nothing p (Just 0)
+ declf p = Decl Nothing p Nothing
-- | Simplify an 'Expr' by using constants to remove 'BinaryOperator' and
-- simplify expressions. To make this work effectively, it should be run until
@@ -273,4 +279,10 @@ combineAssigns p a =
combineAssigns_ :: Port -> [Port] -> ModItem
combineAssigns_ p ps =
- ModCA . ContAssign (p ^. portName) . fold $ Id <$> ps ^.. traverse . portName
+ ModCA
+ . ContAssign (p ^. portName)
+ . fold
+ $ Id
+ <$> ps
+ ^.. traverse
+ . portName
diff --git a/src/VeriFuzz/Verilog/Parser.hs b/src/VeriFuzz/Verilog/Parser.hs
index a072ce8..518bcb9 100644
--- a/src/VeriFuzz/Verilog/Parser.hs
+++ b/src/VeriFuzz/Verilog/Parser.hs
@@ -106,7 +106,7 @@ systemFunc s = satisfy' matchId
parseFunction :: Parser Function
parseFunction =
systemFunc "$unsigned"
- $> UnSignedFunc
+ $> UnsignedFunc
<|> systemFunc "$signed"
$> SignedFunc
@@ -259,7 +259,7 @@ parseNetDecl pd = do
range <- option 1 parseRange
name <- identifier
tok' SymSemi
- return . Decl pd . Port t sign range $ name
+ return $ Decl pd (Port t sign 0 range name) Nothing
where type_ = tok KWWire $> Wire <|> tok KWReg $> Reg
parsePortDir :: Parser PortDir
@@ -281,8 +281,8 @@ parseModList :: Parser [Identifier]
parseModList = list <|> return [] where list = parens $ commaSep identifier
filterDecl :: PortDir -> ModItem -> Bool
-filterDecl p (Decl (Just p') _) = p == p'
-filterDecl _ _ = False
+filterDecl p (Decl (Just p') _ _) = p == p'
+filterDecl _ _ = False
modPorts :: PortDir -> [ModItem] -> [Port]
modPorts p mis = filter (filterDecl p) mis ^.. traverse . declPort
@@ -298,14 +298,12 @@ parseModDecl = do
(modPorts PortOut modItem)
(modPorts PortIn modItem)
modItem
-
-parseDescription :: Parser Description
-parseDescription = Description <$> parseModDecl
+ []
-- | Parses a 'String' into 'Verilog' by skipping any beginning whitespace
-- and then parsing multiple Verilog source.
parseVerilogSrc :: Parser Verilog
-parseVerilogSrc = Verilog <$> many parseDescription
+parseVerilogSrc = Verilog <$> many parseModDecl
-- | Parse a 'String' containing verilog code. The parser currently only supports
-- the subset of Verilog that is being generated randomly.
diff --git a/src/VeriFuzz/Verilog/Preprocess.hs b/src/VeriFuzz/Verilog/Preprocess.hs
index fead5f0..6e9305a 100644
--- a/src/VeriFuzz/Verilog/Preprocess.hs
+++ b/src/VeriFuzz/Verilog/Preprocess.hs
@@ -20,7 +20,9 @@ module VeriFuzz.Verilog.Preprocess
)
where
--- | Remove comments from code.
+-- | Remove comments from code. There is no difference between @(* *)@ and
+-- @/* */@, therefore in this implementation, @*/@ could close @(*@ and vice-versa,
+-- This will be fixed in an upcoming version.
uncomment :: FilePath -> String -> String
uncomment file = uncomment'
where
@@ -28,6 +30,7 @@ uncomment file = uncomment'
"" -> ""
'/' : '/' : rest -> " " ++ removeEOL rest
'/' : '*' : rest -> " " ++ remove rest
+ '(' : '*' : rest -> " " ++ remove rest
'"' : rest -> '"' : ignoreString rest
b : rest -> b : uncomment' rest
@@ -43,6 +46,7 @@ uncomment file = uncomment'
'\n' : rest -> '\n' : remove rest
'\t' : rest -> '\t' : remove rest
'*' : '/' : rest -> " " ++ uncomment' rest
+ '*' : ')' : rest -> " " ++ uncomment' rest
_ : rest -> " " ++ remove rest
removeString a = case a of
@@ -105,4 +109,3 @@ ppLine env ('`' : a) = case lookup name env of
a
rest = drop (length name) a
ppLine env (a : b) = a : ppLine env b
-
diff --git a/test/Property.hs b/test/Property.hs
index ba961cf..431a155 100644
--- a/test/Property.hs
+++ b/test/Property.hs
@@ -3,7 +3,7 @@ module Property
)
where
-import Data.Either (fromRight, isRight)
+import Data.Either (either, isRight)
import qualified Data.Graph.Inductive as G
import Hedgehog (Gen, (===))
import qualified Hedgehog as Hog
@@ -42,11 +42,9 @@ parserIdempotent' = Hog.property $ do
p sv === (p . p) sv
where
vshow = show . GenVerilog
- p =
- vshow
- . fromRight (error "Failed idempotent test")
- . parse parseModDecl "idempotent_test.v"
- . alexScanTokens
+ p sv = either (\x -> show x <> "\n" <> sv) vshow
+ . parse parseModDecl "idempotent_test.v"
+ $ alexScanTokens sv
parserInput :: TestTree
parserInput = testProperty "parser input" parserInput'
generated by cgit (git 2.34.1) at 2024-07-07 17:26:37 +0000