diff options
62 files changed, 2202 insertions, 478 deletions
@@ -1,16 +1,61 @@ # VeriFuzz [![Build Status](https://travis-ci.com/ymherklotz/verifuzz.svg?token=qfBKKGwxeWkjDsy7e16x&branch=master)](https://travis-ci.com/ymherklotz/verifuzz) Verilog Fuzzer to test the major verilog compilers by generating random, valid -verilog. +and deterministic Verilog. There is a +[presentation](https://yannherklotz.com/docs/presentation.pdf) about VeriFuzz +and a [thesis](https://yannherklotz.com/docs/thesis.pdf) which goes over all the +details of the implementation and results that were found. -It currently supports the following simulators: +It currently supports the following synthesis tools: - [Yosys](http://www.clifford.at/yosys/) -- [Icarus Verilog](http://iverilog.icarus.com) - [Xst](https://www.xilinx.com/support/documentation/sw_manuals/xilinx11/ise_c_using_xst_for_synthesis.htm) - [Vivado](https://www.xilinx.com/products/design-tools/ise-design-suite.html) - [Quartus](https://www.intel.com/content/www/us/en/programmable/downloads/download-center.html) +and the following simulator: + +- [Icarus Verilog](http://iverilog.icarus.com) + +## Supported Verilog Constructs + +The fuzzer generates combinational and behavioural Verilog to test the various +tools. The most notable constructs that are supported and generated are the +following: + +- module definitions with parameter definitions, inputs and outputs +- module items, such as instantiations, continuous assignment, always blocks, + initial blocks, parameter and local parameter declarations +- most expressions, for example concatenation, arithmetic operations, ternary + conditional operator +- behavioural code in sequential always blocks +- behavioural control flow such as if-else and for loops +- declaration of wires and variables of any size, signed or unsigned +- bit selection from wires and variables + +## Reported bugs + +21 bugs were found in total over the course of a month. 8 of those bugs were +reported and 3 were fixed. + +### Yosys + +| Type | Issue | Confirmed | Fixed | +|---------------|------------------------------------------------------------|-----------|-------| +| Mis-synthesis | [Issue 1047](https://github.com/YosysHQ/yosys/issues/1047) | ✓ | ✓ | +| Mis-synthesis | [Issue 997](https://github.com/YosysHQ/yosys/issues/997) | ✓ | ✓ | +| Crash | [Issue 993](https://github.com/YosysHQ/yosys/issues/993) | ✓ | ✓ | + +### Vivado + +| Type | Issue | Confirmed | Fixed | +|---------------|-------------------------------------------------------------------------------------------------------------------------------------|-----------|-------| +| Crash | [Forum 981787](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Verilog-If-statement-nesting-crash/td-p/981787) | ✓ | 𐄂 | +| Crash | [Forum 981136](https://forums.xilinx.com/t5/Synthesis/Vivado-2018-3-synthesis-crash/td-p/981136) | ✓ | 𐄂 | +| Mis-synthesis | [Forum 981789](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Unsigned-bit-extension-in-if-statement/td-p/981789) | ✓ | 𐄂 | +| Mis-synthesis | [Forum 982518](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Signed-with-shift-in-condition-synthesis-mistmatch/td-p/982518) | ✓ | 𐄂 | +| Mis-synthesis | [Forum 982419](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Bit-selection-synthesis-mismatch/td-p/982419) | ✓ | 𐄂 | + ## Build the Fuzzer The fuzzer is split into an executable (in the [app](/app) folder) and a @@ -49,3 +94,54 @@ To run the test-suites: ``` stack test ``` + +## Configuration + +VeriFuzz can be configured using a [TOML](https://github.com/toml-lang/toml) +file. There are four main sections in the configuration file, an example can be +seen [here](/examples/config.toml). + +### Information section + +Contains information about the command line tool being used, such as the hash of +the commit it was compiled with and the version of the tool. The tool then +verifies that these match the current configuration, and will emit a warning if +they do not. This ensures that if one wants a deterministic run and is therefore +passing a seed to the generation, that it will always give the same +result. Different versions might change some aspects of the Verilog generation, +which would affect how a seed would generate Verilog. + +### Probability section + +Provides a way to assign frequency values to each of the nodes in the +AST. During the state-based generation, each node is chosen randomly based on +those probabilities. This provides a simple way to drastically change the +Verilog that is generated, by changing how often a construct is chosen or by not +generating a construct at all. + +### Property section + +Changes properties of the generated Verilog code, such as the size of the +output, maximum statement or module depth and sampling method of Verilog +programs. This section also allows a seed to be specified, which would mean that +only that particular seed will be used in the fuzz run. This is extremely useful +when wanting to replay a specific failure and the output is missing. + +### Synthesiser section + +Accepts a list of synthesisers which will be fuzzed. These have to first be +defined in the code and implement the required interface. They can then be +configured by having a name assigned to them and the name of the output Verilog +file. By each having a different name, multiple instances of the same +synthesiser can be included in a fuzz run. The instances might differ in the +optimisations that are performed, or in the version of the synthesiser. + +## Acknowledgement + +Clifford Wolf's [VlogHammer](http://www.clifford.at/yosys/vloghammer.html) is an +existing Verilog fuzzer that generates random Verilog expressions. It was the +inspiration for the general structure of this fuzzer, which extends the fuzzing +to the behavioural parts of Verilog. + +Tom Hawkins' Verilog parser was used to write the lexer, the parser was then +rewritten using [Parsec](https://hackage.haskell.org/package/parsec). diff --git a/data/README.md b/data/README.md new file mode 100644 index 0000000..def3ad3 --- /dev/null +++ b/data/README.md @@ -0,0 +1,5 @@ +# Cells + +The implementation of the cells were initially taken from [VlogHammer +scripts](https://github.com/YosysHQ/VlogHammer/tree/master/testbench/scripts). Additions +were then implemented manually. diff --git a/data/cells_cyclone_v.v b/data/cells_cyclone_v.v index be465d8..5bcb32f 100644 --- a/data/cells_cyclone_v.v +++ b/data/cells_cyclone_v.v @@ -8,7 +8,7 @@ module cyclonev_lcell_comb ( ); input dataa, datab, datac, datad, datae, dataf, datag, cin, sharein; - output reg combout, sumout, cout, shareout; + output reg combout = 0, sumout = 0, cout = 0, shareout = 0; parameter lut_mask = 64'hFFFFFFFFFFFFFFFF; parameter shared_arith = "off"; @@ -63,25 +63,8 @@ module cyclonev_lcell_comb ( begin e0_mask = mask[15:0]; e1_mask = mask[31:16]; - begin - e0_lut = lut4(e0_mask, dataa, datab, datac, datad); - e1_lut = lut4(e1_mask, dataa, datab, datac, datad); - if (datae === 1'bX) // X propogation - begin - if (e0_lut == e1_lut) - begin - lut5 = e0_lut; - end - else - begin - lut5 = 1'bX; - end - end - else - begin - lut5 = (datae == 1'b1) ? e1_lut : e0_lut; - end - end + e0_lut = lut4(e0_mask, dataa, datab, datac, datad); + e1_lut = lut4(e1_mask, dataa, datab, datac, datad); end endfunction @@ -101,29 +84,7 @@ module cyclonev_lcell_comb ( begin f0_mask = mask[31:0]; f1_mask = mask[63:32]; - begin - lut6 = mask[{dataf, datae, datad, datac, datab, dataa}]; - if (lut6 === 1'bX) - begin - f0_lut = lut5(f0_mask, dataa, datab, datac, datad, datae); - f1_lut = lut5(f1_mask, dataa, datab, datac, datad, datae); - if (dataf === 1'bX) // X propogation - begin - if (f0_lut == f1_lut) - begin - lut6 = f0_lut; - end - else - begin - lut6 = 1'bX; - end - end - else - begin - lut6 = (dataf == 1'b1) ? f1_lut : f0_lut; - end - end - end + lut6 = mask[{dataf, datae, datad, datac, datab, dataa}]; end endfunction @@ -257,10 +218,15 @@ module dffeas (d, clk, ena, clrn, prn, aload, asdata, sclr, sload, devclrn, devp input devclrn; input devpor; - output reg q; + output reg q = 0; - always @(posedge clk) begin - q <= d; + always @(posedge clk or posedge aload) begin + if (aload == 1'b1) + q <= asdata; + else if (sload == 1'b1) + q <= asdata; + else + q <= d; end endmodule diff --git a/data/cells_xilinx_7.v b/data/cells_xilinx_7.v index c757c2f..cc72893 100644 --- a/data/cells_xilinx_7.v +++ b/data/cells_xilinx_7.v @@ -971,19 +971,6 @@ module BUFGCTRL (O, CE0, CE1, I0, I1, IGNORE0, IGNORE1, S0, S1); end endmodule // BUFGCTRL -module BUFGDLL (O, I); - output O; - input I; - parameter DUTY_CYCLE_CORRECTION = "TRUE"; - wire clkin_int; - wire clk0_out, clk180_out, clk270_out, clk2x_out; - wire clk90_out, clkdv_out, locked_out; - CLKDLL clkdll_inst (.CLK0(clk0_out), .CLK180(clk180_out), .CLK270(clk270_out), .CLK2X(clk2x_out), .CLK90(clk90_out), .CLKDV(clkdv_out), .LOCKED(locked_out), .CLKFB(O), .CLKIN(clkin_int), .RST(1'b0)); - defparam clkdll_inst.DUTY_CYCLE_CORRECTION = DUTY_CYCLE_CORRECTION; - IBUFG ibufg_inst (.O(clkin_int), .I(I)); - BUFG bufg_inst (.O(O), .I(clk0_out)); -endmodule // BUFGDLL - module BUFG_LB ( CLKOUT, CLKIN diff --git a/examples/config.toml b/examples/config.toml index 497afe2..7f030d7 100644 --- a/examples/config.toml +++ b/examples/config.toml @@ -1,11 +1,43 @@ +[info] + commit = "d32f4cc45bc8c0670fb788b1fcd4c2f2b15fa094" + version = "0.3.0.0" + [probability] - moditem.always = 1 - moditem.assign = 10 - statement.blocking = 5 + expr.binary = 5 + expr.concatenation = 3 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 5 + moditem.combinational = 1 + moditem.instantiation = 1 + moditem.sequential = 1 + statement.blocking = 0 statement.conditional = 1 - statement.nonblocking = 1 + statement.forloop = 0 + statement.nonblocking = 3 [property] - depth = 3 - size = 50 + module.depth = 2 + module.max = 5 + output.combine = false + sample.method = "random" + sample.size = 10 + size = 20 + statement.depth = 3 + +[[synthesiser]] + description = "yosys" + name = "yosys" + output = "syn_yosys.v" + +[[synthesiser]] + description = "vivado" + name = "vivado" + output = "syn_vivado.v" diff --git a/examples/shift.v b/examples/shift.v new file mode 100644 index 0000000..ad1c1fd --- /dev/null +++ b/examples/shift.v @@ -0,0 +1,103 @@ +module shift1(input clk, in, output [3:0] q); + reg q0 = 0, q1 = 0, q2 = 0, q3 = 0; + + always @(posedge clk) begin + q0 = in; + end + always @(posedge clk) begin + q1 = q0; + end + always @(posedge clk) begin + q2 = q1; + end + always @(posedge clk) begin + q3 = q2; + end + + assign q = {q0, q1, q2, q3}; +endmodule // shift1 + +module shift2(input clk, in, output [3:0] q); + reg q0 = 0, q1 = 0, q2 = 0, q3 = 0; + + always @(*) begin + q2 = q1; + q3 = q2; + q1 = q0; + q0 = in; + end + + assign q = {q0, q1, q2, q3}; +endmodule // shift2 + +module shift3(input clk, in, output [3:0] q); + reg q0 = 0, q1 = 0, q2 = 0, q3 = 0; + + always @(posedge clk) begin + q3 <= q2; + q2 <= q1; + q1 <= q0; + q0 <= in; + end + + assign q = {q0, q1, q2, q3}; +endmodule // shift3 + +module shift4(input clk, in, output [3:0] q); + reg q0 = 0, q1 = 0, q2 = 0, q3 = 0; + + always @(posedge clk) begin + q0 <= in; + end + always @(posedge clk) begin + q1 <= q0; + end + always @(posedge clk) begin + q2 <= q1; + end + always @(posedge clk) begin + q3 <= q2; + end + + assign q = {q0, q1, q2, q3}; +endmodule // shift4 + +`ifdef FORMAL +module top(input clk, in); + wire [3:0] q1, q2, q3, q4; + + shift1 shift1(.clk(clk), .in(in), .q(q1)); + shift2 shift2(.clk(clk), .in(in), .q(q2)); + shift3 shift3(.clk(clk), .in(in), .q(q3)); + shift4 shift4(.clk(clk), .in(in), .q(q4)); + + always @(posedge clk) begin + assert(q1 == q2); + assert(q2 == q3); + assert(q3 == q4); + end +endmodule // top +`endif + +`ifndef SYNTHESIS +module main; + reg clk = 0, qin = 0; + wire [256:0] val = 256'h73a27383942819780a5765c741b2949712384778493895283249178574; + reg [5:0] count = 0; + wire [3:0] q1out, q2out, q3out, q4out; + + shift1 shift1(.clk(clk), .in(qin), .q(q1out)); + shift2 shift2(.clk(clk), .in(qin), .q(q2out)); + shift3 shift3(.clk(clk), .in(qin), .q(q3out)); + shift4 shift4(.clk(clk), .in(qin), .q(q4out)); + + always #10 clk = ~clk; + + always @(posedge clk) begin + count <= count + 1; + qin <= val >> count; + if(q1out !== q2out || q2out !== q3out || q3out !== q4out) + $strobe("q: %b\n q1: %b\n q2: %b\n q3: %b\n q4: %b\n\n", qin, q1out, q2out, q3out, q4out); + end +endmodule // main +`endif diff --git a/experiments/config_all.toml b/experiments/config_all.toml new file mode 100644 index 0000000..06d399e --- /dev/null +++ b/experiments/config_all.toml @@ -0,0 +1,45 @@ +[probability] + expr.binary = 5 + expr.concatenation = 5 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 2 + moditem.combinational = 0 + moditem.instantiation = 0 + moditem.sequential = 3 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 0 + statement.nonblocking = 2 + +[property] + module.depth = 2 + module.max = 5 + size = 20 + statement.depth = 7 + sample.method = "hat" + sample.size = 10 + +[[synthesiser]] + description = "yosys" + name = "yosys" + output = "syn_yosys.v" + bin = "/home/ymh15/.local/bin" + +[[synthesiser]] + description = "vivado" + name = "vivado" + output = "syn_vivado.v" + bin = "/usr/local/Xilinx/Vivado/2018.2/bin" + +[[synthesiser]] + description = "xst" + name = "xst" + output = "syn_xst.v" + bin = "/usr/local/Xilinx/ise/ISE/bin/lin64" diff --git a/experiments/config_extra_large.toml b/experiments/config_extra_large.toml new file mode 100644 index 0000000..03469f7 --- /dev/null +++ b/experiments/config_extra_large.toml @@ -0,0 +1,45 @@ +[probability] + expr.binary = 5 + expr.concatenation = 5 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 2 + moditem.combinational = 0 + moditem.instantiation = 0 + moditem.sequential = 3 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 0 + statement.nonblocking = 2 + +[property] + module.depth = 2 + module.max = 5 + size = 20 + statement.depth = 6 + sample.method = "hat" + sample.size = 10 + +[[synthesiser]] + description = "yosys" + name = "yosys" + output = "syn_yosys.v" + bin = "/home/ymh15/.local/bin" + +[[synthesiser]] + description = "vivado" + name = "vivado" + output = "syn_vivado.v" + bin = "/usr/local/Xilinx/Vivado/2018.2/bin" + +[[synthesiser]] + description = "xst" + name = "xst" + output = "syn_xst.v" + bin = "/usr/local/Xilinx/ise/ISE/bin/lin64" diff --git a/experiments/config_large.toml b/experiments/config_large.toml new file mode 100644 index 0000000..06d399e --- /dev/null +++ b/experiments/config_large.toml @@ -0,0 +1,45 @@ +[probability] + expr.binary = 5 + expr.concatenation = 5 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 2 + moditem.combinational = 0 + moditem.instantiation = 0 + moditem.sequential = 3 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 0 + statement.nonblocking = 2 + +[property] + module.depth = 2 + module.max = 5 + size = 20 + statement.depth = 7 + sample.method = "hat" + sample.size = 10 + +[[synthesiser]] + description = "yosys" + name = "yosys" + output = "syn_yosys.v" + bin = "/home/ymh15/.local/bin" + +[[synthesiser]] + description = "vivado" + name = "vivado" + output = "syn_vivado.v" + bin = "/usr/local/Xilinx/Vivado/2018.2/bin" + +[[synthesiser]] + description = "xst" + name = "xst" + output = "syn_xst.v" + bin = "/usr/local/Xilinx/ise/ISE/bin/lin64" diff --git a/experiments/config_large_yosys.toml b/experiments/config_large_yosys.toml new file mode 100644 index 0000000..c1f4837 --- /dev/null +++ b/experiments/config_large_yosys.toml @@ -0,0 +1,33 @@ +[probability] + expr.binary = 5 + expr.concatenation = 5 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 2 + moditem.combinational = 0 + moditem.instantiation = 0 + moditem.sequential = 3 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 0 + statement.nonblocking = 2 + +[property] + module.depth = 2 + module.max = 5 + size = 20 + statement.depth = 7 + sample.method = "hat" + sample.size = 10 + +[[synthesiser]] + description = "yosys" + name = "yosys" + output = "syn_yosys.v" + bin = "/home/ymh15/.local/bin" diff --git a/experiments/config_medium.toml b/experiments/config_medium.toml new file mode 100644 index 0000000..1f3ae0d --- /dev/null +++ b/experiments/config_medium.toml @@ -0,0 +1,45 @@ +[probability] + expr.binary = 5 + expr.concatenation = 5 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 2 + moditem.combinational = 0 + moditem.instantiation = 0 + moditem.sequential = 3 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 0 + statement.nonblocking = 2 + +[property] + module.depth = 2 + module.max = 5 + size = 20 + statement.depth = 5 + sample.method = "hat" + sample.size = 10 + +[[synthesiser]] + description = "yosys" + name = "yosys" + output = "syn_yosys.v" + bin = "/home/ymh15/.local/bin" + +[[synthesiser]] + description = "vivado" + name = "vivado" + output = "syn_vivado.v" + bin = "/usr/local/Xilinx/Vivado/2018.2/bin" + +[[synthesiser]] + description = "xst" + name = "xst" + output = "syn_xst.v" + bin = "/usr/local/Xilinx/ise/ISE/bin/lin64" diff --git a/experiments/config_medium_rand.toml b/experiments/config_medium_rand.toml new file mode 100644 index 0000000..905b904 --- /dev/null +++ b/experiments/config_medium_rand.toml @@ -0,0 +1,50 @@ + +[info] + commit = "d14ec7f57e678fdf478d3c138fe74b03cf8f0523" + version = "0.3.0.0" + +[probability] + expr.binary = 5 + expr.concatenation = 0 + expr.number = 1 + expr.rangeselect = 0 + expr.signed = 0 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 2 + moditem.combinational = 0 + moditem.instantiation = 0 + moditem.sequential = 3 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 0 + statement.nonblocking = 2 + +[property] + module.depth = 2 + module.max = 5 + sample.method = "hat" + sample.size = 10 + size = 20 + statement.depth = 5 + +[[synthesiser]] + bin = "/home/ymh15/.local/bin" + description = "yosys" + name = "yosys" + output = "syn_yosys.v" + +[[synthesiser]] + bin = "/usr/local/Xilinx/Vivado/2018.2/bin" + description = "vivado" + name = "vivado" + output = "syn_vivado.v" + +[[synthesiser]] + bin = "/usr/local/Xilinx/ise/ISE/bin/lin64" + description = "xst" + name = "xst" + output = "syn_xst.v" diff --git a/experiments/config_size_l.toml b/experiments/config_size_l.toml new file mode 100644 index 0000000..535d745 --- /dev/null +++ b/experiments/config_size_l.toml @@ -0,0 +1,45 @@ +[probability] + expr.binary = 5 + expr.concatenation = 5 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 2 + moditem.combinational = 0 + moditem.instantiation = 0 + moditem.sequential = 3 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 0 + statement.nonblocking = 2 + +[property] + module.depth = 2 + module.max = 5 + size = 25 + statement.depth = 2 + sample.method = "hat" + sample.size = 10 + +[[synthesiser]] + description = "yosys" + name = "yosys" + output = "syn_yosys.v" + bin = "/home/ymh15/.local/bin" + +[[synthesiser]] + description = "vivado" + name = "vivado" + output = "syn_vivado.v" + bin = "/usr/local/Xilinx/Vivado/2018.2/bin" + +[[synthesiser]] + description = "xst" + name = "xst" + output = "syn_xst.v" + bin = "/usr/local/Xilinx/ise/ISE/bin/lin64" diff --git a/experiments/config_size_m.toml b/experiments/config_size_m.toml new file mode 100644 index 0000000..e0d1333 --- /dev/null +++ b/experiments/config_size_m.toml @@ -0,0 +1,45 @@ +[probability] + expr.binary = 5 + expr.concatenation = 5 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 2 + moditem.combinational = 0 + moditem.instantiation = 0 + moditem.sequential = 3 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 0 + statement.nonblocking = 2 + +[property] + module.depth = 2 + module.max = 5 + size = 20 + statement.depth = 2 + sample.method = "hat" + sample.size = 10 + +[[synthesiser]] + description = "yosys" + name = "yosys" + output = "syn_yosys.v" + bin = "/home/ymh15/.local/bin" + +[[synthesiser]] + description = "vivado" + name = "vivado" + output = "syn_vivado.v" + bin = "/usr/local/Xilinx/Vivado/2018.2/bin" + +[[synthesiser]] + description = "xst" + name = "xst" + output = "syn_xst.v" + bin = "/usr/local/Xilinx/ise/ISE/bin/lin64" diff --git a/experiments/config_size_s.toml b/experiments/config_size_s.toml new file mode 100644 index 0000000..c512253 --- /dev/null +++ b/experiments/config_size_s.toml @@ -0,0 +1,45 @@ +[probability] + expr.binary = 5 + expr.concatenation = 5 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 2 + moditem.combinational = 0 + moditem.instantiation = 0 + moditem.sequential = 3 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 0 + statement.nonblocking = 2 + +[property] + module.depth = 2 + module.max = 5 + size = 15 + statement.depth = 2 + sample.method = "hat" + sample.size = 10 + +[[synthesiser]] + description = "yosys" + name = "yosys" + output = "syn_yosys.v" + bin = "/home/ymh15/.local/bin" + +[[synthesiser]] + description = "vivado" + name = "vivado" + output = "syn_vivado.v" + bin = "/usr/local/Xilinx/Vivado/2018.2/bin" + +[[synthesiser]] + description = "xst" + name = "xst" + output = "syn_xst.v" + bin = "/usr/local/Xilinx/ise/ISE/bin/lin64" diff --git a/experiments/config_size_xl.toml b/experiments/config_size_xl.toml new file mode 100644 index 0000000..52906c2 --- /dev/null +++ b/experiments/config_size_xl.toml @@ -0,0 +1,45 @@ +[probability] + expr.binary = 5 + expr.concatenation = 5 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 2 + moditem.combinational = 0 + moditem.instantiation = 0 + moditem.sequential = 3 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 0 + statement.nonblocking = 2 + +[property] + module.depth = 2 + module.max = 5 + size = 30 + statement.depth = 2 + sample.method = "hat" + sample.size = 10 + +[[synthesiser]] + description = "yosys" + name = "yosys" + output = "syn_yosys.v" + bin = "/home/ymh15/.local/bin" + +[[synthesiser]] + description = "vivado" + name = "vivado" + output = "syn_vivado.v" + bin = "/usr/local/Xilinx/Vivado/2018.2/bin" + +[[synthesiser]] + description = "xst" + name = "xst" + output = "syn_xst.v" + bin = "/usr/local/Xilinx/ise/ISE/bin/lin64" diff --git a/experiments/config_small.toml b/experiments/config_small.toml new file mode 100644 index 0000000..9cad0a0 --- /dev/null +++ b/experiments/config_small.toml @@ -0,0 +1,45 @@ +[probability] + expr.binary = 5 + expr.concatenation = 5 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 2 + moditem.combinational = 0 + moditem.instantiation = 0 + moditem.sequential = 3 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 0 + statement.nonblocking = 2 + +[property] + module.depth = 2 + module.max = 5 + size = 20 + statement.depth = 3 + sample.method = "hat" + sample.size = 10 + +[[synthesiser]] + description = "yosys" + name = "yosys" + output = "syn_yosys.v" + bin = "/home/ymh15/.local/bin" + +[[synthesiser]] + description = "vivado" + name = "vivado" + output = "syn_vivado.v" + bin = "/usr/local/Xilinx/Vivado/2018.2/bin" + +[[synthesiser]] + description = "xst" + name = "xst" + output = "syn_xst.v" + bin = "/usr/local/Xilinx/ise/ISE/bin/lin64" diff --git a/experiments/config_tiny.toml b/experiments/config_tiny.toml new file mode 100644 index 0000000..9cad0a0 --- /dev/null +++ b/experiments/config_tiny.toml @@ -0,0 +1,45 @@ +[probability] + expr.binary = 5 + expr.concatenation = 5 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 2 + moditem.combinational = 0 + moditem.instantiation = 0 + moditem.sequential = 3 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 0 + statement.nonblocking = 2 + +[property] + module.depth = 2 + module.max = 5 + size = 20 + statement.depth = 3 + sample.method = "hat" + sample.size = 10 + +[[synthesiser]] + description = "yosys" + name = "yosys" + output = "syn_yosys.v" + bin = "/home/ymh15/.local/bin" + +[[synthesiser]] + description = "vivado" + name = "vivado" + output = "syn_vivado.v" + bin = "/usr/local/Xilinx/Vivado/2018.2/bin" + +[[synthesiser]] + description = "xst" + name = "xst" + output = "syn_xst.v" + bin = "/usr/local/Xilinx/ise/ISE/bin/lin64" diff --git a/experiments/config_yosys.toml b/experiments/config_yosys.toml new file mode 100644 index 0000000..487ca2e --- /dev/null +++ b/experiments/config_yosys.toml @@ -0,0 +1,33 @@ +[probability] + expr.binary = 5 + expr.concatenation = 5 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 2 + moditem.combinational = 0 + moditem.instantiation = 0 + moditem.sequential = 3 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 0 + statement.nonblocking = 2 + +[property] + module.depth = 2 + module.max = 5 + size = 20 + statement.depth = 5 + sample.method = "hat" + sample.size = 10 + +[[synthesiser]] + description = "yosys" + name = "yosys" + output = "syn_yosys.v" + bin = "/home/ymh15/.local/bin" diff --git a/experiments/quartus_all.toml b/experiments/quartus_all.toml new file mode 100644 index 0000000..b6a7373 --- /dev/null +++ b/experiments/quartus_all.toml @@ -0,0 +1,33 @@ +[probability] + expr.binary = 5 + expr.concatenation = 5 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 2 + moditem.combinational = 0 + moditem.instantiation = 0 + moditem.sequential = 3 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 0 + statement.nonblocking = 2 + +[property] + module.depth = 2 + module.max = 5 + size = 20 + statement.depth = 3 + sample.method = "hat" + sample.size = 10 + +[[synthesiser]] + description = "quartus" + name = "quartus" + output = "syn_quartus.v" + bin = "/usr/local/altera/18.1/quartus/bin" diff --git a/experiments/vivado_all.toml b/experiments/vivado_all.toml new file mode 100644 index 0000000..5e575ec --- /dev/null +++ b/experiments/vivado_all.toml @@ -0,0 +1,51 @@ +[probability] + expr.binary = 5 + expr.concatenation = 5 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 2 + moditem.combinational = 0 + moditem.instantiation = 0 + moditem.sequential = 3 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 0 + statement.nonblocking = 2 + +[property] + module.depth = 2 + module.max = 5 + size = 20 + statement.depth = 5 + sample.method = "hat" + sample.size = 10 + +[[synthesiser]] + name = "vivado" + description = "vivado_2018.2" + output = "syn_vivado_2018_2.v" + bin = "/usr/local/Xilinx/Vivado/2018.2/bin" + +[[synthesiser]] + name = "vivado" + description = "vivado_2017.4" + output = "syn_vivado_2017_4.v" + bin = "/usr/local/Xilinx/Vivado/2017.4/bin" + +[[synthesiser]] + name = "vivado" + description = "vivado_2016.2" + output = "syn_vivado_2016_2.v" + bin = "/usr/local/Xilinx/Vivado/2016.2/bin" + +[[synthesiser]] + name = "vivado" + description = "vivado_2016.1" + output = "syn_vivado_2016_1.v" + bin = "/usr/local/Xilinx/Vivado/2016.1/bin" diff --git a/experiments/yosys_all.toml b/experiments/yosys_all.toml new file mode 100644 index 0000000..2a425d1 --- /dev/null +++ b/experiments/yosys_all.toml @@ -0,0 +1,39 @@ +[probability] + expr.binary = 5 + expr.concatenation = 5 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 2 + moditem.combinational = 0 + moditem.instantiation = 0 + moditem.sequential = 3 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 0 + statement.nonblocking = 2 + +[property] + module.depth = 2 + module.max = 5 + size = 20 + statement.depth = 7 + sample.method = "hat" + sample.size = 10 + +[[synthesiser]] + name = "yosys" + description = "yosys_0.8" + output = "yosys_0_8.v" + bin = "/home/ymh15/opt/yosys0.8/bin" + +[[synthesiser]] + name = "yosys" + description = "yosys_master" + output = "yosys_master.v" + bin = "/home/ymh15/.local/bin" diff --git a/scripts/convert.py b/scripts/convert.py new file mode 100755 index 0000000..d592fd6 --- /dev/null +++ b/scripts/convert.py @@ -0,0 +1,31 @@ +#!/usr/bin/env python3 + +import sys +from bs4 import BeautifulSoup +import csv +import re + +def main(file_, output): + with open(file_, "r") as f: + file_contents = f.read() + + sec = re.compile(r"([0-9.]+)s") + + soup = BeautifulSoup(file_contents, "html.parser") + table = soup.select_one("table.table") + headers = [th.text for th in table.select("tr th")] + vals = [[td.text for td in row.find_all("td")] for row in table.select("tr + tr")][:-2] + + headers = map(lambda x: "Size" if x == "Size (loc)" else x, headers) + + vals = map(lambda l: map(lambda s: sec.sub(r"\1", s), l), vals) + vals = map(lambda l: map(lambda s: re.sub(r"Failed", r"1", s), l), vals) + vals = map(lambda l: map(lambda s: re.sub(r"Passed", r"0", s), l), vals) + + with open(output, "w") as f: + wr = csv.writer(f) + wr.writerow(headers) + wr.writerows(vals) + +if __name__ == '__main__': + main(sys.argv[1], sys.argv[2]) diff --git a/scripts/exclude.sh b/scripts/exclude.sh new file mode 100644 index 0000000..cfaf514 --- /dev/null +++ b/scripts/exclude.sh @@ -0,0 +1,37 @@ +#!/usr/bin/env bash + +# bug0: ./output_vivado_all2/fuzz_8/vivado_2018.2/hs_err_pid108202.log +bug0="HOptGenControl::updateConst\(UConst\*, int, URange const&, UConst::Type, UConst::Type\)\+0x8d" + +# bug1: ./output_vivado_all2/fuzz_18/vivado_2016.2/hs_err_pid128529.log +bug1="HOptDfg::reconnectLoadPinToSource\(DFPin\*, DFPin\*\)\+0x247" + +# bug2: ./output_vivado_all2/fuzz_1/vivado_2016.2/hs_err_pid99371.log +bug2="HOptDfg::reconnectLoadPinToSource\(DFPin\*, DFPin\*\)\+0x2c0" + +# bug3: ./output_vivado_all2/fuzz_1/vivado_2018.2/hs_err_pid99120.log +bug3="HOptDfg::reconnectLoadPinToSource\(DFPin\*, DFPin\*\)\+0x23b" + +# bug4: ./size_test_length_no_combine/1/output5/fuzz_20/reduce_vivado/hs_err_pid52393.log +bug4="HOptDfg::mergeReconvergentPartitions\(DFPin\*, DFGraph\*, UHashSet<DFPin\*, DFPin\*, UEKey<DFPin\*>, UHashSetNode<DFPin\*>, DFPin\*, UEValue<DFPin\*, UHashSetNode<DFPin\*> > > const&, UHashMap<DFNode\*, DFPin\*, DFNode\*, UEKey<DFNode\*> >&, UHashMap<DFGraph\*, DFGraphInfo, DFGraph\*, UEKey<DFGraph\*> >&, DFGraph::DFGraphType, UHashMapList<DFGraph\*, UHashList<DFPin\*, DFPin\*, UEKey<DFPin\*>, UHashListNode<DFPin\*>, DFPin\*>, DFGraph\*, UEKey<DFGraph\*> >&\)\+0x1c6" + +# bug5: ./swarm/medium95/fuzz_14/reduce_vivado/hs_err_pid126430.log +bug5="HOptDfg::mergeReconvergentPartitions\(DFPin\*, DFGraph\*, UHashSet<DFPin\*, DFPin\*, UEKey<DFPin\*>, UHashSetNode<DFPin\*>, DFPin\*, UEValue<DFPin\*, UHashSetNode<DFPin\*> > > const&, UHashMap<DFNode\*, DFPin\*, DFNode\*, UEKey<DFNode\*> >&, UHashMap<DFGraph\*, DFGraphInfo, DFGraph\*, UEKey<DFGraph\*> >&, DFGraph::DFGraphType, UHashMapList<DFGraph\*, UHashList<DFPin\*, DFPin\*, UEKey<DFPin\*>, UHashListNode<DFPin\*>, DFPin\*>, DFGraph\*, UEKey<DFGraph\*> >&\)\+0x2e8" + +# bug6: ./swarm/medium108/fuzz_3/reduce_vivado/hs_err_pid95577.log +bug6="DD::DD\(Cudd\*, DdNode\*\)\+0x2a" + +# bug7: ./output_vivado/medium13/fuzz_12/vivado_2016.2/hs_err_pid47970.log +bug7="HOptDfg::mergeReconvergentPartitions\(DFPin\*, DFGraph\*, UHashSet<DFPin\*, DFPin\*, UEKey<DFPin\*>, UHashSetNode<DFPin\*>, DFPin\*, UEValue<DFPin\*, UHashSetNode<DFPin\*> > > const&, UHashMap<DFNode\*, DFPin\*, DFNode\*, UEKey<DFNode\*> >&, UHashMap<DFGraph\*, DFGraphInfo, DFGraph\*, UEKey<DFGraph\*> >&, DFGraph::DFGraphType, UHashMapList<DFGraph\*, UHashList<DFPin\*, DFPin\*, UEKey<DFPin\*>, UHashListNode<DFPin\*>, DFPin\*>, DFGraph\*, UEKey<DFGraph\*> >&\)\+0x241" + +# bug8: ./output_vivado/medium10/fuzz_5/vivado_2016.2/hs_err_pid50009.log +bug8="HOptGenControl::extractSyncRSForWireOrMerge\(DFGraph\*, DFNode\*, URange const&, DFEdge\*, DFPin\*\*, UConst\*, int, UConst\*, int, bool, DFPin\*&, UHashSet<DFNode\*, DFNode\*, UEKey<DFNode\*>, UHashSetNode<DFNode\*>, DFNode\*, UEValue<DFNode\*, UHashSetNode<DFNode\*> > >&, bool\)\+0xc33" + +grep -E "$bug0|$bug1|$bug2|$bug3|$bug4|$bug5|$bug6|$bug7|$bug8" $1 >/dev/null 2>&1 +exitcode=$? + +if [[ $exitcode -ne 0 ]]; then + echo $1 + head $1 + echo +fi diff --git a/scripts/run.py b/scripts/run.py new file mode 100755 index 0000000..63295af --- /dev/null +++ b/scripts/run.py @@ -0,0 +1,22 @@ +#!/usr/bin/env python3 + +import subprocess +import os + +def main(): + i = 0 + name = "mediumB" + config = "experiments/config_yosys.toml" + iterations = 50 + directory = "yosys_all" + if not os.path.exists(directory): + os.makedirs(directory) + while True: + subprocess.call(["verifuzz", "fuzz" + , "-o", directory + "/" + name + str(i) + , "-c", config + , "-n", str(iterations)]) + i += 1 + +if __name__ == '__main__': + main() diff --git a/scripts/size b/scripts/size.py index d6d7466..d6d7466 100755 --- a/scripts/size +++ b/scripts/size.py diff --git a/scripts/swarm.py b/scripts/swarm.py new file mode 100755 index 0000000..99b0c54 --- /dev/null +++ b/scripts/swarm.py @@ -0,0 +1,26 @@ +#!/usr/bin/env python3 + +import subprocess +import os + +def main(): + i = 0 + name = "medium" + config = "experiments/config_medium.toml" + iterations = 20 + directory = "swarm" + if not os.path.exists(directory): + os.makedirs(directory) + while True: + subprocess.call(["verifuzz", "config" + , "-c", config + , "-o", directory + "/config_medium_random.toml" + , "--randomise"]) + subprocess.call([ "verifuzz", "fuzz" + , "-o", directory + "/" + name + str(i) + , "-c", directory + "/config_medium_random.toml" + , "-n", str(iterations)]) + i += 1 + +if __name__ == '__main__': + main() diff --git a/src/VeriFuzz.hs b/src/VeriFuzz.hs index 66c795f..0bbdc4f 100644 --- a/src/VeriFuzz.hs +++ b/src/VeriFuzz.hs @@ -28,27 +28,29 @@ module VeriFuzz where import Control.Concurrent -import Control.Lens -import Control.Monad.IO.Class (liftIO) -import qualified Crypto.Random.DRBG as C -import Data.ByteString (ByteString) -import Data.ByteString.Builder (byteStringHex, toLazyByteString) -import qualified Data.ByteString.Lazy as L -import qualified Data.Graph.Inductive as G -import qualified Data.Graph.Inductive.Dot as G -import Data.Maybe (isNothing) -import Data.Text (Text) -import qualified Data.Text as T -import Data.Text.Encoding (decodeUtf8) -import qualified Data.Text.IO as T -import Hedgehog (Gen) -import qualified Hedgehog.Gen as Hog -import Hedgehog.Internal.Seed (Seed) +import Control.Lens hiding ( (<.>) ) +import Control.Monad.IO.Class ( liftIO ) +import qualified Crypto.Random.DRBG as C +import Data.ByteString ( ByteString ) +import Data.ByteString.Builder ( byteStringHex + , toLazyByteString + ) +import qualified Data.ByteString.Lazy as L +import qualified Data.Graph.Inductive as G +import qualified Data.Graph.Inductive.Dot as G +import Data.Maybe ( isNothing ) +import Data.Text ( Text ) +import qualified Data.Text as T +import Data.Text.Encoding ( decodeUtf8 ) +import qualified Data.Text.IO as T +import Hedgehog ( Gen ) +import qualified Hedgehog.Gen as Hog +import Hedgehog.Internal.Seed ( Seed ) import Options.Applicative -import Prelude hiding (FilePath) -import Shelly hiding (command) -import Shelly.Lifted (liftSh) -import System.Random (randomIO) +import Prelude hiding ( FilePath ) +import Shelly hiding ( command ) +import Shelly.Lifted ( liftSh ) +import System.Random ( randomIO ) import VeriFuzz.Circuit import VeriFuzz.Config import VeriFuzz.Fuzz @@ -58,6 +60,7 @@ import VeriFuzz.Result import VeriFuzz.Sim import VeriFuzz.Sim.Internal import VeriFuzz.Verilog +import VeriFuzz.Verilog.Parser ( parseSourceInfoFile ) data OptTool = TYosys | TXST @@ -79,9 +82,11 @@ data Opts = Fuzz { fuzzOutput :: {-# UNPACK #-} !Text } | Parse { fileName :: {-# UNPACK #-} !FilePath } - | Reduce { fileName :: {-# UNPACK #-} !FilePath - , top :: {-# UNPACK #-} !Text - , reduceScript :: {-# UNPACK #-} !FilePath + | Reduce { fileName :: {-# UNPACK #-} !FilePath + , top :: {-# UNPACK #-} !Text + , reduceScript :: {-# UNPACK #-} !(Maybe FilePath) + , synthesiserDesc :: ![SynthDescription] + , rerun :: Bool } | ConfigOpt { writeConfig :: !(Maybe FilePath) , configFile :: !(Maybe FilePath) @@ -107,6 +112,17 @@ parseSynth val | val == "yosys" = Just TYosys | val == "xst" = Just TXST | otherwise = Nothing +parseSynthDesc :: String -> Maybe SynthDescription +parseSynthDesc val + | val == "yosys" = Just $ SynthDescription "yosys" Nothing Nothing Nothing + | val == "vivado" = Just $ SynthDescription "vivado" Nothing Nothing Nothing + | val == "xst" = Just $ SynthDescription "xst" Nothing Nothing Nothing + | val == "quartus" = Just + $ SynthDescription "quartus" Nothing Nothing Nothing + | val == "identity" = Just + $ SynthDescription "identity" Nothing Nothing Nothing + | otherwise = Nothing + parseSim :: String -> Maybe OptTool parseSim val | val == "icarus" = Just TIcarus | otherwise = Nothing @@ -180,13 +196,26 @@ reduceOpts = <> showDefault <> value "top" ) - <*> ( strOption + <*> ( optional + . strOption $ long "script" - <> short 's' <> metavar "SCRIPT" <> help "Script that determines if the current file is interesting, which is determined by the script returning 0." ) + <*> ( many + . option (optReader parseSynthDesc) + $ short 's' + <> long "synth" + <> metavar "SYNTH" + <> help "Specify synthesiser to use." + ) + <*> ( switch + $ short 'r' + <> long "rerun" + <> help + "Only rerun the current synthesis file with all the synthesisers." + ) configOpts :: Parser Opts configOpts = @@ -346,7 +375,49 @@ handleOpts (Parse f) = do Left l -> print l Right v -> print $ GenVerilog v where file = T.unpack . toTextIgnore $ f -handleOpts (Reduce f t s) = shelly $ reduceWithScript t s f +handleOpts (Reduce f t _ ls' False) = do + src <- parseSourceInfoFile t (toTextIgnore f) + case descriptionToSynth <$> ls' of + a : b : _ -> do + putStrLn "Reduce with equivalence check" + shelly $ do + make dir + pop dir $ do + src' <- reduceSynth a b src + writefile (fromText ".." </> dir <.> "v") $ genSource src' + a : _ -> do + putStrLn "Reduce with synthesis failure" + shelly $ do + make dir + pop dir $ do + src' <- reduceSynthesis a src + writefile (fromText ".." </> dir <.> "v") $ genSource src' + _ -> do + putStrLn "Not reducing because no synthesiser was specified" + return () + where dir = fromText "reduce" +handleOpts (Reduce f t _ ls' True) = do + src <- parseSourceInfoFile t (toTextIgnore f) + case descriptionToSynth <$> ls' of + a : b : _ -> do + putStrLn "Starting equivalence check" + res <- shelly . runResultT $ do + make dir + pop dir $ do + runSynth a src + runSynth b src + runEquiv a b src + case res of + 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" + _ <- shelly . runResultT $ mapM (flip runSynth src) as + return () + where dir = fromText "equiv" handleOpts (ConfigOpt c conf r) = do config <- if r then getConfig conf >>= randomise else getConfig conf maybe (T.putStrLn . encodeConfig $ config) (`encodeConfigFile` config) diff --git a/src/VeriFuzz/Circuit.hs b/src/VeriFuzz/Circuit.hs index 58027b1..9ee601f 100644 --- a/src/VeriFuzz/Circuit.hs +++ b/src/VeriFuzz/Circuit.hs @@ -26,8 +26,8 @@ module VeriFuzz.Circuit where import Control.Lens -import Hedgehog (Gen) -import qualified Hedgehog.Gen as Hog +import Hedgehog ( Gen ) +import qualified Hedgehog.Gen as Hog import VeriFuzz.Circuit.Base import VeriFuzz.Circuit.Gen import VeriFuzz.Circuit.Random diff --git a/src/VeriFuzz/Circuit/Base.hs b/src/VeriFuzz/Circuit/Base.hs index ed63105..adc7d52 100644 --- a/src/VeriFuzz/Circuit/Base.hs +++ b/src/VeriFuzz/Circuit/Base.hs @@ -18,7 +18,10 @@ module VeriFuzz.Circuit.Base ) where -import Data.Graph.Inductive (Gr, LEdge, LNode) +import Data.Graph.Inductive ( Gr + , LEdge + , LNode + ) import System.Random -- | The types for all the gates. diff --git a/src/VeriFuzz/Circuit/Gen.hs b/src/VeriFuzz/Circuit/Gen.hs index 0b13ece..323d8bb 100644 --- a/src/VeriFuzz/Circuit/Gen.hs +++ b/src/VeriFuzz/Circuit/Gen.hs @@ -15,9 +15,11 @@ module VeriFuzz.Circuit.Gen ) where -import Data.Graph.Inductive (LNode, Node) -import qualified Data.Graph.Inductive as G -import Data.Maybe (catMaybes) +import Data.Graph.Inductive ( LNode + , Node + ) +import qualified Data.Graph.Inductive as G +import Data.Maybe ( catMaybes ) import VeriFuzz.Circuit.Base import VeriFuzz.Circuit.Internal import VeriFuzz.Verilog.AST diff --git a/src/VeriFuzz/Circuit/Internal.hs b/src/VeriFuzz/Circuit/Internal.hs index 3a7346f..5220f4d 100644 --- a/src/VeriFuzz/Circuit/Internal.hs +++ b/src/VeriFuzz/Circuit/Internal.hs @@ -19,9 +19,11 @@ module VeriFuzz.Circuit.Internal ) where -import Data.Graph.Inductive (Graph, Node) -import qualified Data.Graph.Inductive as G -import qualified Data.Text as T +import Data.Graph.Inductive ( Graph + , Node + ) +import qualified Data.Graph.Inductive as G +import qualified Data.Text as T -- | Convert an integer into a label. -- diff --git a/src/VeriFuzz/Circuit/Random.hs b/src/VeriFuzz/Circuit/Random.hs index 58e855c..2750de8 100644 --- a/src/VeriFuzz/Circuit/Random.hs +++ b/src/VeriFuzz/Circuit/Random.hs @@ -18,13 +18,14 @@ module VeriFuzz.Circuit.Random ) where -import Data.Graph.Inductive (Context) -import qualified Data.Graph.Inductive as G -import Data.Graph.Inductive.PatriciaTree (Gr) -import Data.List (nub) -import Hedgehog (Gen) -import qualified Hedgehog.Gen as Hog -import qualified Hedgehog.Range as Hog +import Data.Graph.Inductive ( Context ) +import qualified Data.Graph.Inductive as G +import Data.Graph.Inductive.PatriciaTree + ( Gr ) +import Data.List ( nub ) +import Hedgehog ( Gen ) +import qualified Hedgehog.Gen as Hog +import qualified Hedgehog.Range as Hog import VeriFuzz.Circuit.Base dupFolder :: (Eq a, Eq b) => Context a b -> [Context a b] -> [Context a b] diff --git a/src/VeriFuzz/Config.hs b/src/VeriFuzz/Config.hs index 9295f71..0fc9435 100644 --- a/src/VeriFuzz/Config.hs +++ b/src/VeriFuzz/Config.hs @@ -61,11 +61,14 @@ module VeriFuzz.Config , probStmntNonBlock , probStmntCond , probStmntFor + , propSampleSize + , propSampleMethod , propSize , propSeed , propStmntDepth , propModDepth , propMaxModules + , propCombine , parseConfigFile , parseConfig , encodeConfig @@ -74,18 +77,22 @@ module VeriFuzz.Config ) where -import Control.Applicative (Alternative) -import Control.Lens hiding ((.=)) -import Data.List.NonEmpty (NonEmpty (..)) -import Data.Maybe (fromMaybe) -import Data.Text (Text, pack) -import qualified Data.Text.IO as T -import Data.Version (showVersion) +import Control.Applicative ( Alternative ) +import Control.Lens hiding ( (.=) ) +import Data.List.NonEmpty ( NonEmpty(..) ) +import Data.Maybe ( fromMaybe ) +import Data.Text ( Text + , pack + ) +import qualified Data.Text.IO as T +import Data.Version ( showVersion ) import Development.GitRev -import Hedgehog.Internal.Seed (Seed) -import Paths_verifuzz (version) -import Shelly (toTextIgnore) -import Toml (TomlCodec, (.=)) +import Hedgehog.Internal.Seed ( Seed ) +import Paths_verifuzz ( version ) +import Shelly ( toTextIgnore ) +import Toml ( TomlCodec + , (.=) + ) import qualified Toml import VeriFuzz.Sim.Quartus import VeriFuzz.Sim.Vivado @@ -189,11 +196,14 @@ data Probability = Probability { _probModItem :: {-# UNPACK #-} !ProbModItem } deriving (Eq, Show) -data ConfProperty = ConfProperty { _propSize :: {-# UNPACK #-} !Int - , _propSeed :: !(Maybe Seed) - , _propStmntDepth :: {-# UNPACK #-} !Int - , _propModDepth :: {-# UNPACK #-} !Int - , _propMaxModules :: {-# UNPACK #-} !Int +data ConfProperty = ConfProperty { _propSize :: {-# UNPACK #-} !Int + , _propSeed :: !(Maybe Seed) + , _propStmntDepth :: {-# UNPACK #-} !Int + , _propModDepth :: {-# UNPACK #-} !Int + , _propMaxModules :: {-# UNPACK #-} !Int + , _propSampleMethod :: !Text + , _propSampleSize :: {-# UNPACK #-} !Int + , _propCombine :: {-# UNPACK #-} !Bool } deriving (Eq, Show) @@ -261,7 +271,7 @@ defaultConfig :: Config defaultConfig = Config (Info (pack $(gitHash)) (pack $ showVersion version)) (Probability defModItem defStmnt defExpr) - (ConfProperty 20 Nothing 3 2 5) + (ConfProperty 20 Nothing 3 2 5 "random" 10 False) [] [fromYosys defaultYosys, fromVivado defaultVivado] where @@ -374,6 +384,14 @@ propCodec = .= _propModDepth <*> defaultValue (defProp propMaxModules) (int "module" "max") .= _propMaxModules + <*> defaultValue (defProp propSampleMethod) + (Toml.text (twoKey "sample" "method")) + .= _propSampleMethod + <*> defaultValue (defProp propSampleSize) (int "sample" "size") + .= _propSampleSize + <*> defaultValue (defProp propCombine) + (Toml.bool (twoKey "output" "combine")) + .= _propCombine where defProp i = defaultConfig ^. configProperty . i simulator :: TomlCodec SimDescription diff --git a/src/VeriFuzz/Fuzz.hs b/src/VeriFuzz/Fuzz.hs index 77962b5..dd7fe7b 100644 --- a/src/VeriFuzz/Fuzz.hs +++ b/src/VeriFuzz/Fuzz.hs @@ -21,38 +21,52 @@ module VeriFuzz.Fuzz , fuzzMultiple , runFuzz , sampleSeed + -- * Helpers + , make + , pop ) where -import Control.DeepSeq (force) -import Control.Exception.Lifted (finally) -import Control.Lens hiding ((<.>)) -import Control.Monad (forM, void) +import Control.DeepSeq ( force ) +import Control.Exception.Lifted ( finally ) +import Control.Lens hiding ( (<.>) ) +import Control.Monad ( forM + , replicateM + ) import Control.Monad.IO.Class -import Control.Monad.Trans.Class (lift) -import Control.Monad.Trans.Control (MonadBaseControl) -import Control.Monad.Trans.Maybe (runMaybeT) -import Control.Monad.Trans.Reader hiding (local) +import Control.Monad.Trans.Class ( lift ) +import Control.Monad.Trans.Control ( MonadBaseControl ) +import Control.Monad.Trans.Maybe ( runMaybeT ) +import Control.Monad.Trans.Reader + hiding ( local ) import Control.Monad.Trans.State.Strict -import Data.List (nubBy) -import Data.Maybe (isNothing) -import Data.Text (Text) -import qualified Data.Text as T +import qualified Crypto.Random.DRBG as C +import Data.ByteString ( ByteString ) +import Data.List ( nubBy + , sort + ) +import Data.Maybe ( isNothing ) +import Data.Text ( Text ) +import qualified Data.Text as T import Data.Time -import Hedgehog (Gen) -import qualified Hedgehog.Internal.Gen as Hog -import Hedgehog.Internal.Seed (Seed) -import qualified Hedgehog.Internal.Seed as Hog -import qualified Hedgehog.Internal.Tree as Hog -import Prelude hiding (FilePath) -import Shelly hiding (get) -import Shelly.Lifted (MonadSh, liftSh) -import System.FilePath.Posix (takeBaseName) +import Data.Tuple ( swap ) +import Hedgehog ( Gen ) +import qualified Hedgehog.Internal.Gen as Hog +import Hedgehog.Internal.Seed ( Seed ) +import qualified Hedgehog.Internal.Seed as Hog +import qualified Hedgehog.Internal.Tree as Hog +import Prelude hiding ( FilePath ) +import Shelly hiding ( get ) +import Shelly.Lifted ( MonadSh + , liftSh + ) +import System.FilePath.Posix ( takeBaseName ) import VeriFuzz.Config import VeriFuzz.Internal import VeriFuzz.Reduce import VeriFuzz.Report import VeriFuzz.Result +import VeriFuzz.Sim.Icarus import VeriFuzz.Sim.Internal import VeriFuzz.Sim.Yosys import VeriFuzz.Verilog.AST @@ -64,9 +78,19 @@ data FuzzEnv = FuzzEnv { getSynthesisers :: ![SynthTool] } deriving (Eq, Show) +data FuzzState = FuzzState { _fuzzSynthResults :: ![SynthResult] + , _fuzzSimResults :: ![SimResult] + , _fuzzSynthStatus :: ![SynthStatus] + } + deriving (Eq, Show) + +$(makeLenses ''FuzzState) + +type Frequency a = [(Seed, a)] -> [(Int, Gen (Seed, a))] + -- | The main type for the fuzzing, which contains an environment that can be -- read from and the current state of all the results. -type Fuzz m = StateT FuzzReport (ReaderT FuzzEnv m) +type Fuzz m = StateT FuzzState (ReaderT FuzzEnv m) type MonadFuzz m = (MonadBaseControl IO m, MonadIO m, MonadSh m) @@ -75,7 +99,7 @@ runFuzz conf yos m = shelly $ runFuzz' conf yos m runFuzz' :: Monad m => Config -> Yosys -> (Config -> Fuzz m b) -> m b runFuzz' conf yos m = runReaderT - (evalStateT (m conf) (FuzzReport [] [] [])) + (evalStateT (m conf) (FuzzState [] [] [])) (FuzzEnv ( force $ defaultIdentitySynth @@ -106,32 +130,29 @@ timeit a = do synthesis :: (MonadBaseControl IO m, MonadSh m) => SourceInfo -> Fuzz m () synthesis src = do - synth <- synthesisers - results <- liftSh $ mapM exec synth - synthStatus .= zipWith SynthStatus synth results - liftSh $ inspect results + synth <- synthesisers + resTimes <- liftSh $ mapM exec synth + fuzzSynthStatus + .= applyList (uncurry . SynthStatus <$> synth) (fmap swap resTimes) + liftSh $ inspect resTimes where - exec a = runResultT $ do + exec a = toolRun ("synthesis with " <> toText a) . runResultT $ do liftSh . mkdir_p . fromText $ toText a pop (fromText $ toText a) $ runSynth a src -generateSample - :: (MonadIO m, MonadSh m) - => Maybe Seed - -> Gen SourceInfo - -> Fuzz m (Seed, SourceInfo) -generateSample seed gen = do - logT "Sampling Verilog from generator" - (t, v) <- timeit $ sampleSeed seed gen - logT $ "Generated Verilog (" <> showT t <> ")" - return v - passedSynthesis :: MonadSh m => Fuzz m [SynthTool] -passedSynthesis = fmap toSynth . filter passed . _synthStatus <$> get +passedSynthesis = fmap toSynth . filter passed . _fuzzSynthStatus <$> get + where + passed (SynthStatus _ (Pass _) _) = True + passed _ = False + toSynth (SynthStatus s _ _) = s + +failedSynthesis :: MonadSh m => Fuzz m [SynthTool] +failedSynthesis = fmap toSynth . filter failed . _fuzzSynthStatus <$> get where - passed (SynthStatus _ (Pass _)) = True - passed _ = False - toSynth (SynthStatus s _) = s + failed (SynthStatus _ (Fail SynthFail) _) = True + failed _ = False + toSynth (SynthStatus s _ _) = s make :: MonadSh m => FilePath -> m () make f = liftSh $ do @@ -146,8 +167,21 @@ pop f a = do applyList :: [a -> b] -> [a] -> [b] applyList a b = apply' <$> zip a b where apply' (a', b') = a' b' -toSynthResult :: [(SynthTool, SynthTool)] -> [Result Failed ()] -> [SynthResult] -toSynthResult a b = flip applyList b $ uncurry SynthResult <$> a +applyLots :: (a -> b -> c -> d -> e) -> [(a, b)] -> [(c, d)] -> [e] +applyLots func a b = applyList (uncurry . uncurry func <$> a) b + +toSynthResult + :: [(SynthTool, SynthTool)] + -> [(NominalDiffTime, Result Failed ())] + -> [SynthResult] +toSynthResult a b = applyLots SynthResult a $ fmap swap b + +toolRun :: (MonadIO m, MonadSh m) => Text -> m a -> m (NominalDiffTime, a) +toolRun t m = do + logT $ "Running " <> t + (diff, res) <- timeit m + logT $ "Finished " <> t <> " (" <> showT diff <> ")" + return (diff, res) equivalence :: (MonadBaseControl IO m, MonadSh m) => SourceInfo -> Fuzz m () equivalence src = do @@ -159,71 +193,233 @@ equivalence src = do . filter (uncurry (/=)) $ (,) defaultIdentitySynth <$> synth - results <- liftSh $ mapM (uncurry equiv) synthComb - synthResults .= toSynthResult synthComb results - liftSh $ inspect results + resTimes <- liftSh $ mapM (uncurry equiv) synthComb + fuzzSynthResults .= toSynthResult synthComb resTimes + liftSh $ inspect resTimes where tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a') - equiv a b = runResultT $ do + equiv a b = + toolRun ("equivalence check for " <> toText a <> " and " <> toText b) + . runResultT + $ do + make dir + pop dir $ do + liftSh $ do + cp + ( fromText ".." + </> fromText (toText a) + </> synthOutput a + ) + $ synthOutput a + cp + ( fromText ".." + </> fromText (toText b) + </> synthOutput b + ) + $ synthOutput b + writefile "rtl.v" $ genSource src + runEquiv a b src + where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b + +simulation :: (MonadIO m, MonadSh m) => SourceInfo -> Fuzz m () +simulation src = do + synth <- passEquiv + vals <- liftIO $ generateByteString 20 + ident <- liftSh $ equiv vals defaultIdentitySynth + resTimes <- liftSh $ mapM (equiv vals) $ conv <$> synth + liftSh + . inspect + $ (\(_, r) -> bimap show (T.unpack . T.take 10 . showBS) r) + <$> (ident : resTimes) + where + conv (SynthResult _ a _ _) = a + equiv b a = toolRun ("simulation for " <> toText a) . runResultT $ do make dir pop dir $ do liftSh $ do cp (fromText ".." </> fromText (toText a) </> synthOutput a) $ synthOutput a - cp (fromText ".." </> fromText (toText b) </> synthOutput b) - $ synthOutput b writefile "rtl.v" $ genSource src - runEquiv a b src - where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b + runSimIc defaultIcarus a src b + where dir = fromText $ "simulation_" <> toText a + +-- | Generate a specific number of random bytestrings of size 256. +randomByteString :: C.CtrDRBG -> Int -> [ByteString] -> [ByteString] +randomByteString gen n bytes + | n == 0 = ranBytes : bytes + | otherwise = randomByteString newGen (n - 1) $ ranBytes : bytes + where Right (ranBytes, newGen) = C.genBytes 32 gen + +-- | generates the specific number of bytestring with a random seed. +generateByteString :: Int -> IO [ByteString] +generateByteString n = do + gen <- C.newGenIO :: IO C.CtrDRBG + return $ randomByteString gen n [] failEquivWithIdentity :: (MonadSh m) => Fuzz m [SynthResult] -failEquivWithIdentity = filter withIdentity . _synthResults <$> get +failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get + where + withIdentity (SynthResult (IdentitySynth _) _ (Fail EquivFail) _) = True + withIdentity (SynthResult _ (IdentitySynth _) (Fail EquivFail) _) = True + withIdentity _ = False + +passEquiv :: (MonadSh m) => Fuzz m [SynthResult] +passEquiv = filter withIdentity . _fuzzSynthResults <$> get where - withIdentity (SynthResult (IdentitySynth _) _ (Fail EquivFail)) = True - withIdentity (SynthResult _ (IdentitySynth _) (Fail EquivFail)) = True - withIdentity _ = False + withIdentity (SynthResult _ _ (Pass _) _) = True + withIdentity _ = False -- | Always reduces with respect to 'Identity'. reduction :: (MonadSh m) => SourceInfo -> Fuzz m () reduction src = do - fails <- failEquivWithIdentity - _ <- liftSh $ mapM red fails + fails <- failEquivWithIdentity + synthFails <- failedSynthesis + _ <- liftSh $ mapM red fails + _ <- liftSh $ mapM redSynth synthFails return () where - red (SynthResult a b _) = do + red (SynthResult a b _ _) = do make dir pop dir $ do s <- reduceSynth a b src writefile (fromText ".." </> dir <.> "v") $ genSource s return s where dir = fromText $ "reduce_" <> toText a <> "_" <> toText b + redSynth a = do + make dir + pop dir $ do + s <- reduceSynthesis a src + writefile (fromText ".." </> dir <.> "v") $ genSource s + return s + where dir = fromText $ "reduce_" <> toText a + +titleRun + :: (MonadIO m, MonadSh m) => Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a) +titleRun t f = do + logT $ "### Starting " <> t <> " ###" + (diff, res) <- timeit f + logT $ "### Finished " <> t <> " (" <> showT diff <> ") ###" + return (diff, res) + +whenMaybe :: Applicative m => Bool -> m a -> m (Maybe a) +whenMaybe b x = if b then Just <$> x else pure Nothing + +getTime :: (Num n) => Maybe (n, a) -> n +getTime = maybe 0 fst + +generateSample + :: (MonadIO m, MonadSh m) + => Fuzz m (Seed, SourceInfo) + -> Fuzz m (Seed, SourceInfo) +generateSample f = do + logT "Sampling Verilog from generator" + (t, v@(s, _)) <- timeit f + logT $ "Chose " <> showT s + logT $ "Generated Verilog (" <> showT t <> ")" + return v + +verilogSize :: (Source a) => a -> Int +verilogSize = length . lines . T.unpack . genSource + +sampleVerilog + :: (MonadSh m, MonadIO m, Source a, Ord a) + => Frequency a + -> Int + -> Maybe Seed + -> Gen a + -> m (Seed, a) +sampleVerilog _ _ seed@(Just _) gen = sampleSeed seed gen +sampleVerilog freq n Nothing gen = do + res <- replicateM n $ sampleSeed Nothing gen + let sizes = fmap getSize res + let samples = fmap snd . sort $ zip sizes res + liftIO $ Hog.sample . Hog.frequency $ freq samples + where getSize (_, s) = verilogSize s + +hatFreqs :: Frequency a +hatFreqs l = zip hat (return <$> l) + where + h = length l `div` 2 + hat = (+ h) . negate . abs . (h -) <$> [1 .. length l] + +meanFreqs :: Source a => Frequency a +meanFreqs l = zip hat (return <$> l) + where + hat = calc <$> sizes + calc i = if abs (mean - i) == min_ then 1 else 0 + mean = sum sizes `div` length l + min_ = minimum $ abs . (mean -) <$> sizes + sizes = verilogSize . snd <$> l + +medianFreqs :: Frequency a +medianFreqs l = zip hat (return <$> l) + where + h = length l `div` 2 + hat = set_ <$> [1 .. length l] + set_ n = if n == h then 1 else 0 fuzz :: MonadFuzz m => Gen SourceInfo -> Config -> Fuzz m FuzzReport fuzz gen conf = do - (seed', src) <- generateSample seed gen + (seed', src) <- generateSample genMethod + let size = length . lines . T.unpack $ genSource src liftSh . writefile "config.toml" . encodeConfig $ conf & configProperty . propSeed - .~ Just seed' - synthesis src - equivalence src - reduction src - report <- get + ?~ seed' + (tsynth, _) <- titleRun "Synthesis" $ synthesis src + (tequiv, _) <- titleRun "Equivalence Check" $ equivalence src + (_ , _) <- titleRun "Simulation" $ simulation src + fails <- failEquivWithIdentity + synthFails <- failedSynthesis + redResult <- + whenMaybe (not $ null fails && null synthFails) + . titleRun "Reduction" + $ reduction src + state_ <- get currdir <- liftSh pwd + let vi = flip view state_ + let report = FuzzReport currdir + (vi fuzzSynthResults) + (vi fuzzSimResults) + (vi fuzzSynthStatus) + size + tsynth + tequiv + (getTime redResult) liftSh . writefile "index.html" $ printResultReport (bname currdir) report return report where - seed = conf ^. configProperty . propSeed - bname = T.pack . takeBaseName . T.unpack . toTextIgnore + seed = conf ^. configProperty . propSeed + bname = T.pack . takeBaseName . T.unpack . toTextIgnore + genMethod = case T.toLower $ conf ^. configProperty . propSampleMethod of + "hat" -> do + logT "Using the hat function" + sv hatFreqs + "mean" -> do + logT "Using the mean function" + sv meanFreqs + "median" -> do + logT "Using the median function" + sv medianFreqs + _ -> do + logT "Using first seed" + sampleSeed seed gen + sv a = sampleVerilog a (conf ^. configProperty . propSampleSize) seed gen + +relativeFuzzReport :: (MonadSh m) => FuzzReport -> m FuzzReport +relativeFuzzReport fr@(FuzzReport dir _ _ _ _ _ _ _) = liftSh $ do + newPath <- relPath dir + return $ (fuzzDir .~ newPath) fr fuzzInDir :: MonadFuzz m => FilePath -> Gen SourceInfo -> Config -> Fuzz m FuzzReport fuzzInDir fp src conf = do make fp - pop fp $ fuzz src conf + res <- pop fp $ fuzz src conf + relativeFuzzReport res fuzzMultiple :: MonadFuzz m @@ -231,7 +427,7 @@ fuzzMultiple -> Maybe FilePath -> Gen SourceInfo -> Config - -> Fuzz m FuzzReport + -> Fuzz m [FuzzReport] fuzzMultiple n fp src conf = do x <- case fp of Nothing -> do @@ -243,11 +439,16 @@ fuzzMultiple n fp src conf = do <> formatTime defaultTimeLocale "%Y-%m-%d_%H-%M-%S" ct Just f -> return f make x - when (isNothing seed) . void . pop x . forM [1 .. n] $ fuzzDir - unless (isNothing seed) . void . pop x $ fuzzDir (1 :: Int) - return mempty + pop x $ do + results <- if isNothing seed + then forM [1 .. n] fuzzDir' + else (: []) <$> fuzzDir' (1 :: Int) + liftSh . writefile (fromText "index" <.> "html") $ printSummary + "Fuzz Summary" + results + return results where - fuzzDir n' = fuzzInDir (fromText $ "fuzz_" <> showT n') src conf + fuzzDir' n' = fuzzInDir (fromText $ "fuzz_" <> showT n') src conf seed = conf ^. configProperty . propSeed sampleSeed :: MonadSh m => Maybe Seed -> Gen a -> m (Seed, a) @@ -267,7 +468,5 @@ sampleSeed s gen = $ Hog.runGenT 30 seed gen of Nothing -> loop (n - 1) - Just x -> do - liftSh . logT $ showT seed - return (seed, Hog.nodeValue x) + Just x -> return (seed, Hog.nodeValue x) in loop (100 :: Int) diff --git a/src/VeriFuzz/Internal.hs b/src/VeriFuzz/Internal.hs index 22efa92..b5ce3ba 100644 --- a/src/VeriFuzz/Internal.hs +++ b/src/VeriFuzz/Internal.hs @@ -14,13 +14,24 @@ module VeriFuzz.Internal ( -- * Useful functions safe , showT + , showBS , comma , commaNL ) where -import Data.Text (Text) -import qualified Data.Text as T +import Data.ByteString ( ByteString ) +import Data.ByteString.Builder ( byteStringHex + , toLazyByteString + ) +import qualified Data.ByteString.Lazy as L +import Data.Text ( Text ) +import qualified Data.Text as T +import Data.Text.Encoding ( decodeUtf8 ) + +-- | Function to show a bytestring in a hex format. +showBS :: ByteString -> Text +showBS = decodeUtf8 . L.toStrict . toLazyByteString . byteStringHex -- | Converts unsafe list functions in the Prelude to a safe version. safe :: ([a] -> b) -> [a] -> Maybe b diff --git a/src/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs index 33cb648..6bae371 100644 --- a/src/VeriFuzz/Reduce.hs +++ b/src/VeriFuzz/Reduce.hs @@ -17,6 +17,7 @@ module VeriFuzz.Reduce ( -- $strategy reduceWithScript , reduceSynth + , reduceSynthesis , reduce , reduce_ , Replacement(..) @@ -34,27 +35,32 @@ 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 @@ -111,7 +117,7 @@ instance Traversable Replacement where -- | Split a list in two halves. halve :: Replace [a] -halve [] = None +halve [] = Single [] halve [_] = Single [] halve l = Dual a b where (a, b) = splitAt (length l `div` 2) l @@ -254,6 +260,12 @@ exprId (VecSelect i _) = Just i exprId (RangeSelect i _) = Just i exprId _ = Nothing +eventId :: Event -> Maybe Identifier +eventId (EId i) = Just i +eventId (EPosEdge i) = Just i +eventId (ENegEdge i) = Just i +eventId _ = Nothing + portToId :: Port -> Identifier portToId (Port _ _ _ i) = i @@ -327,6 +339,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 @@ -396,8 +409,11 @@ toIds = nub . mapMaybe exprId . concatMap universe toIdsConst :: [ConstExpr] -> [Identifier] toIdsConst = toIds . fmap constToExpr +toIdsEvent :: [Event] -> [Identifier] +toIdsEvent = nub . mapMaybe eventId . concatMap universe + allStatIds' :: Statement -> [Identifier] -allStatIds' s = nub $ assignIds <> otherExpr +allStatIds' s = nub $ assignIds <> otherExpr <> eventProcessedIds where assignIds = toIds @@ -405,7 +421,8 @@ allStatIds' s = nub $ assignIds <> otherExpr <> (s ^.. stmntNBA . assignExpr) <> (s ^.. forAssign . assignExpr) <> (s ^.. forIncr . assignExpr) - otherExpr = toIds $ (s ^.. forExpr) <> (s ^.. stmntCondExpr) + otherExpr = toIds $ (s ^.. forExpr) <> (s ^.. stmntCondExpr) + eventProcessedIds = toIdsEvent $ s ^.. statEvent allStatIds :: Statement -> [Identifier] allStatIds s = nub . concat $ allStatIds' <$> universe s @@ -502,28 +519,27 @@ reduce_ title repl bot eval src = do (src ^.. infoSrc . _Wrapped . traverse . modItems . traverse) ) <> ")" - replAnswer <- sequenceA $ evalIfNotEmpty <$> replacement - case (replacement, replAnswer) of - (Single s, Single True ) -> runIf s - (Dual _ r, Dual False True) -> runIf r - (Dual l _, Dual True False) -> runIf l - (Dual l r, Dual True True ) -> check l r - _ -> return src + if bot src + then return src + else case repl src of + Single s -> do + red <- eval s + if red + then if cond s then recReduction s else return s + else return src + Dual l r -> do + red <- eval l + if red + then if cond l then recReduction l else return l + else do + red' <- eval r + if red' + then if cond r then recReduction r else return r + else return src + None -> return src where - replacement = repl src - runIf s = if s /= src && not (bot s) - then reduce_ title repl bot eval s - else return s - evalIfNotEmpty = eval - check l r - | bot l = return l - | bot r = return r - | otherwise = do - lreduced <- runIf l - rreduced <- runIf r - if _infoSrc lreduced < _infoSrc rreduced - then return lreduced - else return rreduced + cond s = s /= src + recReduction = reduce_ title repl bot eval -- | Reduce an input to a minimal representation. It follows the reduction -- strategy mentioned above. @@ -537,7 +553,7 @@ reduce eval src = $ red "Modules" moduleBot halveModules src >>= redAll "Module Items" modItemBot halveModItems >>= redAll "Statements" (const defaultBot) halveStatements - >>= redAll "Expressions" (const defaultBot) halveExpr + -- >>= redAll "Expressions" (const defaultBot) halveExpr where red s bot a = reduce_ s a bot eval red' s bot a t = reduce_ s (a t) (bot t) eval @@ -585,3 +601,13 @@ reduceSynth a b = reduce synth Fail EquivFail -> True Fail _ -> False Pass _ -> False + +reduceSynthesis :: (Synthesiser a, MonadSh m) => a -> SourceInfo -> m SourceInfo +reduceSynthesis a = reduce synth + where + synth src = liftSh $ do + r <- runResultT $ runSynth a src + return $ case r of + Fail SynthFail -> True + Fail _ -> False + Pass _ -> False diff --git a/src/VeriFuzz/Report.hs b/src/VeriFuzz/Report.hs index 2edd31e..3037b34 100644 --- a/src/VeriFuzz/Report.hs +++ b/src/VeriFuzz/Report.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE RankNTypes #-} {-| Module : VeriFuzz.Report Description : Generate a report from a fuzz run. @@ -16,12 +17,19 @@ module VeriFuzz.Report ( SynthTool(..) , SynthStatus(..) , SynthResult(..) + , SimResult(..) , SimTool(..) , FuzzReport(..) , printResultReport + , printSummary , synthResults , simResults , synthStatus + , equivTime + , fuzzDir + , fileLines + , reducTime + , synthTime , defaultIcarusSim , defaultVivadoSynth , defaultYosysSynth @@ -33,19 +41,37 @@ module VeriFuzz.Report ) where -import Control.DeepSeq (NFData, rnf) -import Control.Lens hiding (Identity) -import Data.ByteString (ByteString) -import Data.Maybe (fromMaybe) -import Data.Text (Text) -import Data.Text.Lazy (toStrict) -import Prelude hiding (FilePath) -import Shelly (fromText) -import Text.Blaze.Html (Html, (!)) -import Text.Blaze.Html.Renderer.Text (renderHtml) +import Control.DeepSeq ( NFData + , rnf + ) +import Control.Lens hiding ( Identity + , (<.>) + ) +import Data.Bifunctor ( bimap ) +import Data.ByteString ( ByteString ) +import Data.Maybe ( fromMaybe ) +import Data.Monoid ( Endo ) +import Data.Text ( Text ) +import qualified Data.Text as T +import Data.Text.Lazy ( toStrict ) +import Data.Time +import Data.Vector ( fromList ) +import Prelude hiding ( FilePath ) +import Shelly ( FilePath + , fromText + , toTextIgnore + , (<.>) + , (</>) + ) +import Statistics.Sample ( meanVariance ) +import Text.Blaze.Html ( Html + , (!) + ) +import Text.Blaze.Html.Renderer.Text ( renderHtml ) import qualified Text.Blaze.Html5 as H import qualified Text.Blaze.Html5.Attributes as A import VeriFuzz.Config +import VeriFuzz.Internal import VeriFuzz.Result import VeriFuzz.Sim import VeriFuzz.Sim.Internal @@ -139,46 +165,55 @@ defaultIcarusSim = IcarusSim defaultIcarus -- | The results from running a tool through a simulator. It can either fail or -- return a result, which is most likely a 'ByteString'. -data SimResult = SimResult !SynthTool !SimTool !BResult +data SimResult = SimResult !SynthTool !SimTool !BResult !NominalDiffTime deriving (Eq) instance Show SimResult where - show (SimResult synth sim r) = show synth <> ", " <> show sim <> ": " <> show r + show (SimResult synth sim r d) = show synth <> ", " <> show sim <> ": " <> show (bimap show (T.unpack . showBS) r) <> " (" <> show d <> ")" + +getSimResult :: SimResult -> UResult +getSimResult (SimResult _ _ (Pass _) _) = Pass () +getSimResult (SimResult _ _ (Fail b) _) = Fail b -- | The results of comparing the synthesised outputs of two files using a -- formal equivalence checker. This will either return a failure or an output -- which is most likely '()'. -data SynthResult = SynthResult !SynthTool !SynthTool !UResult +data SynthResult = SynthResult !SynthTool !SynthTool !UResult !NominalDiffTime deriving (Eq) instance Show SynthResult where - show (SynthResult synth synth2 r) = show synth <> ", " <> show synth2 <> ": " <> show r + show (SynthResult synth synth2 r d) = show synth <> ", " <> show synth2 <> ": " <> show r <> " (" <> show d <> ")" + +getSynthResult :: SynthResult -> UResult +getSynthResult (SynthResult _ _ a _) = a -- | The status of the synthesis using a simulator. This will be checked before -- attempting to run the equivalence checks on the simulator, as that would be -- unnecessary otherwise. -data SynthStatus = SynthStatus !SynthTool !UResult +data SynthStatus = SynthStatus !SynthTool !UResult !NominalDiffTime deriving (Eq) +getSynthStatus :: SynthStatus -> UResult +getSynthStatus (SynthStatus _ a _) = a + instance Show SynthStatus where - show (SynthStatus synth r) = "synthesis " <> show synth <> ": " <> show r + show (SynthStatus synth r d) = "synthesis " <> show synth <> ": " <> show r <> " (" <> show d <> ")" -- | The complete state that will be used during fuzzing, which contains the -- results from all the operations. -data FuzzReport = FuzzReport { _synthResults :: ![SynthResult] +data FuzzReport = FuzzReport { _fuzzDir :: !FilePath + , _synthResults :: ![SynthResult] , _simResults :: ![SimResult] , _synthStatus :: ![SynthStatus] + , _fileLines :: {-# UNPACK #-} !Int + , _synthTime :: {-# UNPACK #-} !NominalDiffTime + , _equivTime :: {-# UNPACK #-} !NominalDiffTime + , _reducTime :: {-# UNPACK #-} !NominalDiffTime } deriving (Eq, Show) $(makeLenses ''FuzzReport) -instance Semigroup FuzzReport where - FuzzReport a1 b1 c1 <> FuzzReport a2 b2 c2 = FuzzReport (a1 <> a2) (b1 <> b2) (c1 <> c2) - -instance Monoid FuzzReport where - mempty = FuzzReport [] [] [] - descriptionToSim :: SimDescription -> SimTool descriptionToSim (SimDescription "icarus") = defaultIcarusSim descriptionToSim s = @@ -201,11 +236,11 @@ descriptionToSynth (SynthDescription "xst" bin desc out) = descriptionToSynth (SynthDescription "quartus" bin desc out) = QuartusSynth . Quartus (fromText <$> bin) - (fromMaybe (quartusDesc defaultQuartus) $ desc) + (fromMaybe (quartusDesc defaultQuartus) desc) $ maybe (quartusOutput defaultQuartus) fromText out descriptionToSynth (SynthDescription "identity" _ desc out) = IdentitySynth - . Identity (fromMaybe (identityDesc defaultIdentity) $ desc) + . Identity (fromMaybe (identityDesc defaultIdentity) desc) $ maybe (identityOutput defaultIdentity) fromText out descriptionToSynth s = error $ "Could not find implementation for synthesiser '" <> show s <> "'" @@ -220,42 +255,46 @@ status (Fail EquivError ) = H.td ! A.class_ "is-danger" $ "Equivalence error" status (Fail TimeoutError) = H.td ! A.class_ "is-warning" $ "Time out" synthStatusHtml :: SynthStatus -> Html -synthStatusHtml (SynthStatus synth res) = H.tr $ do +synthStatusHtml (SynthStatus synth res diff) = H.tr $ do H.td . H.toHtml $ toText synth status res + H.td . H.toHtml $ showT diff synthResultHtml :: SynthResult -> Html -synthResultHtml (SynthResult synth1 synth2 res) = H.tr $ do +synthResultHtml (SynthResult synth1 synth2 res diff) = H.tr $ do H.td . H.toHtml $ toText synth1 H.td . H.toHtml $ toText synth2 status res + H.td . H.toHtml $ showT diff + +resultHead :: Text -> Html +resultHead name = H.head $ do + H.title $ "Fuzz Report - " <> H.toHtml name + H.meta ! A.name "viewport" ! A.content "width=device-width, initial-scale=1" + H.meta ! A.charset "utf8" + H.link + ! A.rel "stylesheet" + ! A.href + "https://cdnjs.cloudflare.com/ajax/libs/bulma/0.7.4/css/bulma.min.css" resultReport :: Text -> FuzzReport -> Html -resultReport name (FuzzReport synth _ stat) = H.docTypeHtml $ do - H.head $ do - H.title $ "Fuzz Report - " <> H.toHtml name - H.meta ! A.name "viewport" ! A.content - "width=device-width, initial-scale=1" - H.meta ! A.charset "utf8" - H.link - ! A.rel "stylesheet" - ! A.href - "https://cdnjs.cloudflare.com/ajax/libs/bulma/0.7.4/css/bulma.min.css" +resultReport name (FuzzReport _ synth _ stat _ _ _ _) = H.docTypeHtml $ do + resultHead name H.body . (H.section ! A.class_ "section") . (H.div ! A.class_ "container") $ do - H.h1 ! A.class_ "title" $ "Fuzz Report - " <> H.toHtml name - H.h2 ! A.class_ "subtitle" $ "Synthesis Failure" + H.h1 ! A.class_ "title is-1" $ "Fuzz Report - " <> H.toHtml name + H.h2 ! A.class_ "title is-2" $ "Synthesis" H.table ! A.class_ "table" $ do H.thead . H.toHtml $ ( H.tr . H.toHtml - $ [H.th "Synthesis tool", H.th "Synthesis Status"] + $ [H.th "Tool", H.th "Status", H.th "Run time"] ) H.tbody . H.toHtml $ fmap synthStatusHtml stat - H.h2 ! A.class_ "subtitle" $ "Equivalence Check Status" + H.h2 ! A.class_ "title is-2" $ "Equivalence Check" H.table ! A.class_ "table" $ do H.thead . H.toHtml @@ -263,10 +302,107 @@ resultReport name (FuzzReport synth _ stat) = H.docTypeHtml $ do . H.toHtml $ [ H.th "First tool" , H.th "Second tool" - , H.th "Equivalence Status" + , H.th "Status" + , H.th "Run time" ] ) H.tbody . H.toHtml $ fmap synthResultHtml synth +resultStatus :: Result a b -> Html +resultStatus (Pass _) = H.td ! A.class_ "is-success" $ "Passed" +resultStatus (Fail _) = H.td ! A.class_ "is-danger" $ "Failed" + +fuzzStats + :: (Real a1, Traversable t) + => ((a1 -> Const (Endo [a1]) a1) -> a2 -> Const (Endo [a1]) a2) + -> t a2 + -> (Double, Double) +fuzzStats sel fr = meanVariance converted + where converted = fromList . fmap realToFrac $ fr ^.. traverse . sel + +fuzzStatus :: Text -> FuzzReport -> Html +fuzzStatus name (FuzzReport dir s1 s2 s3 sz t1 t2 t3) = H.tr $ do + H.td + . ( H.a + ! A.href + ( H.textValue + $ toTextIgnore (dir </> fromText "index" <.> "html") + ) + ) + $ H.toHtml name + resultStatus + $ mconcat (fmap getSynthResult s1) + <> mconcat (fmap getSimResult s2) + <> mconcat (fmap getSynthStatus s3) + H.td . H.string $ show sz + H.td . H.string $ show t1 + H.td . H.string $ show t2 + H.td . H.string $ show t3 + +summary :: Text -> [FuzzReport] -> Html +summary name fuzz = H.docTypeHtml $ do + resultHead name + H.body + . (H.section ! A.class_ "section") + . (H.div ! A.class_ "container") + $ do + H.h1 ! A.class_ "title is-1" $ "FuzzReport - " <> H.toHtml name + H.table ! A.class_ "table" $ do + H.thead . H.tr $ H.toHtml + [ H.th "Name" + , H.th "Status" + , H.th "Size (loc)" + , H.th "Synthesis time" + , H.th "Equivalence check time" + , H.th "Reduction time" + ] + H.tbody + . H.toHtml + . fmap + (\(i, r) -> + fuzzStatus ("Fuzz " <> showT (i :: Int)) r + ) + $ zip [1 ..] fuzz + H.tfoot . H.toHtml $ do + H.tr $ H.toHtml + [ H.td $ H.strong "Total" + , H.td mempty + , H.td + . H.string + . show + . sum + $ fuzz + ^.. traverse + . fileLines + , sumUp synthTime + , sumUp equivTime + , sumUp reducTime + ] + H.tr $ H.toHtml + [ H.td $ H.strong "Mean" + , H.td mempty + , fst $ bimap d2I d2I $ fuzzStats fileLines fuzz + , fst $ meanVar synthTime + , fst $ meanVar equivTime + , fst $ meanVar reducTime + ] + H.tr $ H.toHtml + [ H.td $ H.strong "Variance" + , H.td mempty + , snd $ bimap d2I d2I $ fuzzStats fileLines fuzz + , snd $ meanVar synthTime + , snd $ meanVar equivTime + , snd $ meanVar reducTime + ] + where + sumUp s = showHtml . sum $ fuzz ^.. traverse . s + meanVar s = bimap d2T d2T $ fuzzStats s fuzz + showHtml = H.td . H.string . show + d2T = showHtml . (realToFrac :: Double -> NominalDiffTime) + d2I = H.td . H.string . show + printResultReport :: Text -> FuzzReport -> Text printResultReport t f = toStrict . renderHtml $ resultReport t f + +printSummary :: Text -> [FuzzReport] -> Text +printSummary t f = toStrict . renderHtml $ summary t f diff --git a/src/VeriFuzz/Result.hs b/src/VeriFuzz/Result.hs index 4d1f5b8..4ea7988 100644 --- a/src/VeriFuzz/Result.hs +++ b/src/VeriFuzz/Result.hs @@ -31,8 +31,14 @@ import Control.Monad.Base import Control.Monad.IO.Class import Control.Monad.Trans.Class import Control.Monad.Trans.Control -import Shelly (RunFailed (..), Sh, catch_sh) -import Shelly.Lifted (MonadSh, liftSh) +import Data.Bifunctor ( Bifunctor(..) ) +import Shelly ( RunFailed(..) + , Sh + , catch_sh + ) +import Shelly.Lifted ( MonadSh + , liftSh + ) -- | Result type which is equivalent to 'Either' or 'Error'. This is -- reimplemented so that there is full control over the 'Monad' definition and @@ -42,7 +48,7 @@ data Result a b = Fail a deriving (Eq, Show) instance Semigroup (Result a b) where - Fail _ <> b = b + Pass _ <> a = a a <> _ = a instance (Monoid b) => Monoid (Result a b) where @@ -64,6 +70,10 @@ instance Monad (Result a) where instance MonadBase (Result a) (Result a) where liftBase = id +instance Bifunctor Result where + bimap a _ (Fail c) = Fail $ a c + bimap _ b (Pass c) = Pass $ b c + -- | The transformer for the 'Result' type. This newtype ResultT a m b = ResultT { runResultT :: m (Result a b) } diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs index 423d51b..8e62136 100644 --- a/src/VeriFuzz/Sim/Icarus.hs +++ b/src/VeriFuzz/Sim/Icarus.hs @@ -13,30 +13,41 @@ Icarus verilog module. module VeriFuzz.Sim.Icarus ( Icarus(..) , defaultIcarus + , runSimIc ) where -import Control.DeepSeq (NFData, rnf, rwhnf) +import Control.DeepSeq ( NFData + , rnf + , rwhnf + ) import Control.Lens -import Crypto.Hash (Digest, hash) -import Crypto.Hash.Algorithms (SHA256) -import Data.Binary (encode) -import qualified Data.ByteArray as BA (convert) -import Data.ByteString (ByteString) -import qualified Data.ByteString as B -import Data.ByteString.Lazy (toStrict) -import qualified Data.ByteString.Lazy as L (ByteString) -import Data.Char (digitToInt) -import Data.Foldable (fold) -import Data.List (transpose) -import Data.Maybe (listToMaybe) -import Data.Text (Text) -import qualified Data.Text as T -import Numeric (readInt) -import Prelude hiding (FilePath) +import Control.Monad ( void ) +import Crypto.Hash ( Digest + , hash + ) +import Crypto.Hash.Algorithms ( SHA256 ) +import Data.Binary ( encode ) +import Data.Bits +import qualified Data.ByteArray as BA + ( convert ) +import Data.ByteString ( ByteString ) +import qualified Data.ByteString as B +import Data.ByteString.Lazy ( toStrict ) +import qualified Data.ByteString.Lazy as L + ( ByteString ) +import Data.Char ( digitToInt ) +import Data.Foldable ( fold ) +import Data.List ( transpose ) +import Data.Maybe ( listToMaybe ) +import Data.Text ( Text ) +import qualified Data.Text as T +import Numeric ( readInt ) +import Prelude hiding ( FilePath ) import Shelly -import Shelly.Lifted (liftSh) +import Shelly.Lifted ( liftSh ) import VeriFuzz.Sim.Internal +import VeriFuzz.Sim.Template import VeriFuzz.Verilog.AST import VeriFuzz.Verilog.BitVec import VeriFuzz.Verilog.CodeGen @@ -117,11 +128,68 @@ runSimIcarusWithFile :: Icarus -> FilePath -> [ByteString] -> ResultSh ByteString runSimIcarusWithFile sim f _ = annotate SimFail . liftSh $ do dir <- pwd - logger "Icarus: Compile" logCommand_ dir "icarus" $ run (icarusPath sim) ["-o", "main", toTextIgnore f] - logger "Icarus: Run" B.take 8 . BA.convert . (hash :: ByteString -> Digest SHA256) <$> logCommand dir "vvp" (runFoldLines (mempty :: ByteString) callback (vvpPath sim) ["main"]) + +fromBytes :: ByteString -> Integer +fromBytes = B.foldl' f 0 where f a b = a `shiftL` 8 .|. fromIntegral b + +runSimIc + :: (Synthesiser b) + => Icarus + -> b + -> SourceInfo + -> [ByteString] + -> ResultSh ByteString +runSimIc sim1 synth1 srcInfo bss = do + dir <- liftSh pwd + let top = srcInfo ^. mainModule + let inConcat = (RegConcat (Id . fromPort <$> (top ^. modInPorts))) + let + tb = instantiateMod top $ ModDecl + "testbench" + [] + [] + [ Initial + $ fold + [ BlockAssign (Assign "clk" Nothing 0) + , BlockAssign (Assign inConcat Nothing 0) + ] + <> fold + ( (\r -> TimeCtrl + 10 + (Just $ BlockAssign (Assign inConcat Nothing r)) + ) + . fromInteger + . fromBytes + <$> bss + ) + <> (SysTaskEnable $ Task "finish" []) + , Always . TimeCtrl 5 . Just $ BlockAssign + (Assign "clk" Nothing (UnOp UnNot (Id "clk"))) + , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable $ Task + "strobe" + ["%b", Id "y"] + ] + [] + + liftSh . writefile "testbench.v" $ icarusTestbench (Verilog [tb]) synth1 + liftSh $ exe dir "icarus" "iverilog" ["-o", "main", "testbench.v"] + liftSh + $ B.take 8 + . BA.convert + . (hash :: ByteString -> Digest SHA256) + <$> logCommand + dir + "vvp" + (runFoldLines (mempty :: ByteString) + callback + (vvpPath sim1) + ["main"] + ) + where + exe dir name e = void . errExit False . logCommand dir name . timeout e diff --git a/src/VeriFuzz/Sim/Identity.hs b/src/VeriFuzz/Sim/Identity.hs index bfded0b..95b4097 100644 --- a/src/VeriFuzz/Sim/Identity.hs +++ b/src/VeriFuzz/Sim/Identity.hs @@ -16,11 +16,16 @@ module VeriFuzz.Sim.Identity ) where -import Control.DeepSeq (NFData, rnf, rwhnf) -import Data.Text (Text, unpack) -import Prelude hiding (FilePath) -import Shelly (FilePath) -import Shelly.Lifted (writefile) +import Control.DeepSeq ( NFData + , rnf + , rwhnf + ) +import Data.Text ( Text + , unpack + ) +import Prelude hiding ( FilePath ) +import Shelly ( FilePath ) +import Shelly.Lifted ( writefile ) import VeriFuzz.Sim.Internal import VeriFuzz.Verilog.AST import VeriFuzz.Verilog.CodeGen diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs index 5c58e1a..a05a96f 100644 --- a/src/VeriFuzz/Sim/Internal.hs +++ b/src/VeriFuzz/Sim/Internal.hs @@ -40,20 +40,26 @@ module VeriFuzz.Sim.Internal where import Control.Lens -import Control.Monad (forM, void) -import Control.Monad.Catch (throwM) -import Data.Bits (shiftL) -import Data.ByteString (ByteString) -import qualified Data.ByteString as B -import Data.Maybe (catMaybes) -import Data.Text (Text) -import qualified Data.Text as T -import Data.Time.Format (defaultTimeLocale, formatTime) -import Data.Time.LocalTime (getZonedTime) -import Prelude hiding (FilePath) +import Control.Monad ( forM + , void + ) +import Control.Monad.Catch ( throwM ) +import Data.Bits ( shiftL ) +import Data.ByteString ( ByteString ) +import qualified Data.ByteString as B +import Data.Maybe ( catMaybes ) +import Data.Text ( Text ) +import qualified Data.Text as T +import Data.Time.Format ( defaultTimeLocale + , formatTime + ) +import Data.Time.LocalTime ( getZonedTime ) +import Prelude hiding ( FilePath ) import Shelly -import Shelly.Lifted (MonadSh, liftSh) -import System.FilePath.Posix (takeBaseName) +import Shelly.Lifted ( MonadSh + , liftSh + ) +import System.FilePath.Posix ( takeBaseName ) import VeriFuzz.Internal import VeriFuzz.Result import VeriFuzz.Verilog.AST @@ -188,21 +194,28 @@ logCommand_ :: FilePath -> Text -> Sh a -> Sh () logCommand_ fp name = void . logCommand fp name execute - :: (MonadSh m, Monad m, Monoid a) - => a + :: (MonadSh m, Monad m) + => Failed -> FilePath -> Text -> FilePath -> [Text] - -> ResultT a m Text -execute f dir name e = annotate f . liftSh . logCommand dir name . timeout e + -> ResultT Failed m Text +execute f dir name e cs = do + (res, exitCode) <- liftSh $ do + res <- errExit False . logCommand dir name $ timeout e cs + (,) res <$> lastExitCode + case exitCode of + 0 -> ResultT . return $ Pass res + 124 -> ResultT . return $ Fail TimeoutError + _ -> ResultT . return $ Fail f execute_ - :: (MonadSh m, Monad m, Monoid a) - => a + :: (MonadSh m, Monad m) + => Failed -> FilePath -> Text -> FilePath -> [Text] - -> ResultT a m () + -> ResultT Failed m () execute_ a b c d = void . execute a b c d diff --git a/src/VeriFuzz/Sim/Quartus.hs b/src/VeriFuzz/Sim/Quartus.hs index ece00eb..e0fbba5 100644 --- a/src/VeriFuzz/Sim/Quartus.hs +++ b/src/VeriFuzz/Sim/Quartus.hs @@ -16,11 +16,16 @@ module VeriFuzz.Sim.Quartus ) where -import Control.DeepSeq (NFData, rnf, rwhnf) -import Data.Text (Text, unpack) -import Prelude hiding (FilePath) +import Control.DeepSeq ( NFData + , rnf + , rwhnf + ) +import Data.Text ( Text + , unpack + ) +import Prelude hiding ( FilePath ) import Shelly -import Shelly.Lifted (liftSh) +import Shelly.Lifted ( liftSh ) import VeriFuzz.Sim.Internal import VeriFuzz.Verilog.AST import VeriFuzz.Verilog.CodeGen @@ -52,12 +57,16 @@ runSynthQuartus :: Quartus -> SourceInfo -> ResultSh () runSynthQuartus sim (SourceInfo top src) = do dir <- liftSh pwd let ex = execute_ SynthFail dir "quartus" - liftSh $ do - writefile inpf $ genSource src - logger "Running Quartus synthesis" + liftSh . writefile inpf $ genSource src + liftSh . noPrint $ run_ + "sed" + [ "-i" + , "s/^module/(* multstyle = \"logic\" *) module/;" + , toTextIgnore inpf + ] ex (exec "quartus_map") [top, "--source=" <> toTextIgnore inpf, "--family=Cyclone V"] - ex (exec "quartus_fit") [top, "--part=5CGTFD9E5F35C7N"] + ex (exec "quartus_fit") [top, "--part=5CGXFC7D6F31C6"] ex (exec "quartus_eda") [top, "--simulation", "--tool=vcs"] liftSh $ do cp (fromText "simulation/vcs" </> fromText top <.> "vo") @@ -68,7 +77,6 @@ runSynthQuartus sim (SourceInfo top src) = do , "s,^// DATE.*,,; s,^tri1 (.*);,wire \\1 = 1;,; /^\\/\\/ +synopsys/ d;" , toTextIgnore $ synthOutput sim ] - logger "Quartus synthesis done" where inpf = "rtl.v" exec s = maybe (fromText s) (</> fromText s) $ quartusBin sim diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs index 4aa07f6..3be6558 100644 --- a/src/VeriFuzz/Sim/Template.hs +++ b/src/VeriFuzz/Sim/Template.hs @@ -18,17 +18,19 @@ module VeriFuzz.Sim.Template , xstSynthConfig , vivadoSynthConfig , sbyConfig + , icarusTestbench ) where -import Control.Lens ((^..)) -import Data.Text (Text) -import qualified Data.Text as T -import Prelude hiding (FilePath) +import Control.Lens ((^..)) +import Data.Text (Text) +import qualified Data.Text as T +import Prelude hiding (FilePath) import Shelly -import Text.Shakespeare.Text (st) +import Text.Shakespeare.Text (st) import VeriFuzz.Sim.Internal import VeriFuzz.Verilog.AST +import VeriFuzz.Verilog.CodeGen rename :: Text -> [Text] -> Text rename end entries = @@ -117,3 +119,15 @@ top.v . fromText <$> deps readL = T.intercalate "\n" $ mappend "read -formal " <$> deps + +icarusTestbench :: (Synthesiser a) => Verilog -> a -> Text +icarusTestbench t synth1 = [st| +`include "data/cells_cmos.v" +`include "data/cells_cyclone_v.v" +`include "data/cells_verific.v" +`include "data/cells_xilinx_7.v" +`include "data/cells_yosys.v" +`include "#{toTextIgnore $ synthOutput synth1}" + +#{genSource t} +|] diff --git a/src/VeriFuzz/Sim/Vivado.hs b/src/VeriFuzz/Sim/Vivado.hs index ee67a78..8697a0f 100644 --- a/src/VeriFuzz/Sim/Vivado.hs +++ b/src/VeriFuzz/Sim/Vivado.hs @@ -16,11 +16,16 @@ module VeriFuzz.Sim.Vivado ) where -import Control.DeepSeq (NFData, rnf, rwhnf) -import Data.Text (Text, unpack) -import Prelude hiding (FilePath) +import Control.DeepSeq ( NFData + , rnf + , rwhnf + ) +import Data.Text ( Text + , unpack + ) +import Prelude hiding ( FilePath ) import Shelly -import Shelly.Lifted (liftSh) +import Shelly.Lifted ( liftSh ) import VeriFuzz.Sim.Internal import VeriFuzz.Sim.Template import VeriFuzz.Verilog.AST @@ -56,13 +61,16 @@ runSynthVivado sim (SourceInfo top src) = do writefile vivadoTcl . vivadoSynthConfig top . toTextIgnore $ synthOutput sim writefile "rtl.v" $ genSource src - run_ "sed" ["s/^module/(* use_dsp=\"no\" *) module/;", "-i", "rtl.v"] - logger "Vivado: run" + run_ + "sed" + [ "s/^module/(* use_dsp48=\"no\" *) (* use_dsp=\"no\" *) module/;" + , "-i" + , "rtl.v" + ] let exec_ n = execute_ SynthFail dir "vivado" (maybe (fromText n) (</> fromText n) $ vivadoBin sim) exec_ "vivado" ["-mode", "batch", "-source", toTextIgnore vivadoTcl] - liftSh $ logger "Vivado: done" where vivadoTcl = fromText ("vivado_" <> top) <.> "tcl" diff --git a/src/VeriFuzz/Sim/XST.hs b/src/VeriFuzz/Sim/XST.hs index 11be094..f5faae5 100644 --- a/src/VeriFuzz/Sim/XST.hs +++ b/src/VeriFuzz/Sim/XST.hs @@ -18,12 +18,17 @@ module VeriFuzz.Sim.XST ) where -import Control.DeepSeq (NFData, rnf, rwhnf) -import Data.Text (Text, unpack) -import Prelude hiding (FilePath) +import Control.DeepSeq ( NFData + , rnf + , rwhnf + ) +import Data.Text ( Text + , unpack + ) +import Prelude hiding ( FilePath ) import Shelly -import Shelly.Lifted (liftSh) -import Text.Shakespeare.Text (st) +import Shelly.Lifted ( liftSh ) +import Text.Shakespeare.Text ( st ) import VeriFuzz.Sim.Internal import VeriFuzz.Sim.Template import VeriFuzz.Verilog.AST @@ -64,9 +69,7 @@ runSynthXST sim (SourceInfo top src) = do writefile xstFile $ xstSynthConfig top writefile prjFile [st|verilog work "rtl.v"|] writefile "rtl.v" $ genSource src - logger "XST: run" exec "xst" ["-ifn", toTextIgnore xstFile] - liftSh $ logger "XST: netgen" exec "netgen" [ "-w" @@ -75,15 +78,12 @@ runSynthXST sim (SourceInfo top src) = do , toTextIgnore $ modFile <.> "ngc" , toTextIgnore $ synthOutput sim ] - liftSh $ do - logger "XST: clean" - noPrint $ run_ - "sed" - [ "-i" - , "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;" - , toTextIgnore $ synthOutput sim - ] - logger "XST: done" + liftSh . noPrint $ run_ + "sed" + [ "-i" + , "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;" + , toTextIgnore $ synthOutput sim + ] where modFile = fromText top xstFile = modFile <.> "xst" diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs index 3081a65..8f9d4a7 100644 --- a/src/VeriFuzz/Sim/Yosys.hs +++ b/src/VeriFuzz/Sim/Yosys.hs @@ -20,14 +20,19 @@ module VeriFuzz.Sim.Yosys ) where -import Control.DeepSeq (NFData, rnf, rwhnf) +import Control.DeepSeq ( NFData + , rnf + , rwhnf + ) import Control.Lens -import Control.Monad (void) -import Data.Text (Text, unpack) -import Prelude hiding (FilePath) +import Control.Monad ( void ) +import Data.Text ( Text + , unpack + ) +import Prelude hiding ( FilePath ) import Shelly -import Shelly.Lifted (liftSh) -import Text.Shakespeare.Text (st) +import Shelly.Lifted ( liftSh ) +import Text.Shakespeare.Text ( st ) import VeriFuzz.Result import VeriFuzz.Sim.Internal import VeriFuzz.Sim.Template @@ -62,16 +67,19 @@ yosysPath :: Yosys -> FilePath yosysPath sim = maybe (fromText "yosys") (</> fromText "yosys") $ yosysBin sim runSynthYosys :: Yosys -> SourceInfo -> ResultSh () -runSynthYosys sim (SourceInfo _ src) = (<?> SynthFail) . liftSh $ do - dir <- pwd - writefile inpf $ genSource src - logger "Yosys: synthesis" - logCommand_ dir "yosys" $ timeout +runSynthYosys sim (SourceInfo _ src) = do + dir <- liftSh $ do + dir' <- pwd + writefile inpf $ genSource src + return dir' + execute_ + SynthFail + dir + "yosys" (yosysPath sim) [ "-p" , "read -formal " <> inp <> "; synth; write_verilog -noattr " <> out ] - logger "Yosys: synthesis done" where inpf = "rtl.v" inp = toTextIgnore inpf @@ -95,10 +103,7 @@ runEquivYosys yosys sim1 sim2 srcInfo = do writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo runSynth sim1 srcInfo runSynth sim2 srcInfo - liftSh $ do - logger "Yosys: equivalence check" - run_ (yosysPath yosys) [toTextIgnore checkFile] - logger "Yosys: equivalence done" + liftSh $ run_ (yosysPath yosys) [toTextIgnore checkFile] where checkFile = fromText [st|test.#{toText sim1}.#{toText sim2}.ys|] runEquiv @@ -115,12 +120,11 @@ runEquiv sim1 sim2 srcInfo = do replaceMods (synthOutput sim1) "_1" srcInfo replaceMods (synthOutput sim2) "_2" srcInfo writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo - liftSh $ logger "Running SymbiYosys" e <- liftSh $ do exe dir "symbiyosys" "sby" ["-f", "proof.sby"] lastExitCode case e of - 0 -> liftSh $ logger "SymbiYosys equivalence check passed" + 0 -> ResultT . return $ Pass () 2 -> ResultT . return $ Fail EquivFail 124 -> ResultT . return $ Fail TimeoutError _ -> ResultT . return $ Fail EquivError 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/src/VeriFuzz/Verilog/AST.hs b/src/VeriFuzz/Verilog/AST.hs index 306366c..43063e6 100644 --- a/src/VeriFuzz/Verilog/AST.hs +++ b/src/VeriFuzz/Verilog/AST.hs @@ -139,14 +139,18 @@ module VeriFuzz.Verilog.AST ) where -import Control.Lens hiding ((<|)) +import Control.Lens hiding ( (<|) ) import Data.Data import Data.Data.Lens -import Data.Functor.Foldable.TH (makeBaseFunctor) -import Data.List.NonEmpty (NonEmpty (..), (<|)) -import Data.String (IsString, fromString) -import Data.Text (Text) -import Data.Traversable (sequenceA) +import Data.Functor.Foldable.TH ( makeBaseFunctor ) +import Data.List.NonEmpty ( NonEmpty(..) + , (<|) + ) +import Data.String ( IsString + , fromString + ) +import Data.Text ( Text ) +import Data.Traversable ( sequenceA ) import VeriFuzz.Verilog.BitVec -- | Identifier in Verilog. This is just a string of characters that can either @@ -169,6 +173,9 @@ data Event = EId {-# UNPACK #-} !Identifier | EComb !Event !Event deriving (Eq, Show, Ord, Data) +instance Plated Event where + plate = uniplate + -- | Binary operators that are currently supported in the verilog generation. data BinaryOperator = BinPlus -- ^ @+@ | BinMinus -- ^ @-@ @@ -492,7 +499,7 @@ newtype Verilog = Verilog { getVerilog :: [ModDecl] } data SourceInfo = SourceInfo { _infoTop :: {-# UNPACK #-} !Text , _infoSrc :: !Verilog } - deriving (Eq, Show) + deriving (Eq, Ord, Data, Show) $(makeLenses ''Expr) $(makeLenses ''ConstExpr) diff --git a/src/VeriFuzz/Verilog/CodeGen.hs b/src/VeriFuzz/Verilog/CodeGen.hs index a0ec0cc..82945aa 100644 --- a/src/VeriFuzz/Verilog/CodeGen.hs +++ b/src/VeriFuzz/Verilog/CodeGen.hs @@ -17,18 +17,20 @@ This module generates the code from the Verilog AST defined in module VeriFuzz.Verilog.CodeGen ( -- * Code Generation GenVerilog(..) - , genSource + , Source(..) , render ) where -import Data.Data (Data) -import Data.List.NonEmpty (NonEmpty (..), toList) -import Data.Text (Text) -import qualified Data.Text as T +import Data.Data ( Data ) +import Data.List.NonEmpty ( NonEmpty(..) + , toList + ) +import Data.Text ( Text ) +import qualified Data.Text as T import Data.Text.Prettyprint.Doc -import Numeric (showHex) -import VeriFuzz.Internal hiding (comma) +import Numeric ( showHex ) +import VeriFuzz.Internal hiding ( comma ) import VeriFuzz.Verilog.AST import VeriFuzz.Verilog.BitVec diff --git a/src/VeriFuzz/Verilog/Eval.hs b/src/VeriFuzz/Verilog/Eval.hs index 4a43c19..d8840e3 100644 --- a/src/VeriFuzz/Verilog/Eval.hs +++ b/src/VeriFuzz/Verilog/Eval.hs @@ -17,9 +17,9 @@ module VeriFuzz.Verilog.Eval where import Data.Bits -import Data.Foldable (fold) -import Data.Functor.Foldable hiding (fold) -import Data.Maybe (listToMaybe) +import Data.Foldable ( fold ) +import Data.Functor.Foldable hiding ( fold ) +import Data.Maybe ( listToMaybe ) import VeriFuzz.Verilog.AST import VeriFuzz.Verilog.BitVec diff --git a/src/VeriFuzz/Verilog/Gen.hs b/src/VeriFuzz/Verilog/Gen.hs index f2d2b0a..f08e5a6 100644 --- a/src/VeriFuzz/Verilog/Gen.hs +++ b/src/VeriFuzz/Verilog/Gen.hs @@ -237,14 +237,6 @@ someI m f = do amount <- gen $ Hog.int (Hog.linear 1 m) replicateM amount f -some :: StateGen a -> StateGen [a] -some = someI 50 - -many :: StateGen a -> StateGen [a] -many f = do - amount <- gen $ Hog.int (Hog.linear 0 50) - replicateM amount f - makeIdentifier :: T.Text -> StateGen Identifier makeIdentifier prefix = do context <- get @@ -481,10 +473,11 @@ calcRange ps i (Range l r) = eval l - eval r + 1 moduleDef :: Maybe Identifier -> StateGen ModDecl moduleDef top = do name <- moduleName top - portList <- some $ nextPort Wire + portList <- Hog.list (Hog.linear 4 10) $ nextPort Wire mi <- Hog.list (Hog.linear 4 100) modItem - ps <- many parameter + ps <- Hog.list (Hog.linear 0 10) parameter context <- get + config <- lift ask let local = filter (`notElem` portList) $ _variables context let size = @@ -493,12 +486,14 @@ moduleDef top = do $ local ^.. traverse . portSize - let clock = Port Wire False 1 "clk" - let yport = Port Wire False size "y" - let comb = combineAssigns_ yport local + let combine = config ^. configProperty . propCombine + let clock = Port Wire False 1 "clk" + let yport = + if combine then Port Wire False 1 "y" else Port Wire False size "y" + let comb = combineAssigns_ combine yport local return . declareMod local - . ModDecl name [yport] (clock : portList) (mi <> [comb]) + . ModDecl name [yport] (clock : portList) (comb : mi) $ ps -- | Procedural generation method for random Verilog. Uses internal 'Reader' and diff --git a/src/VeriFuzz/Verilog/Internal.hs b/src/VeriFuzz/Verilog/Internal.hs index 8d19c14..16148cf 100644 --- a/src/VeriFuzz/Verilog/Internal.hs +++ b/src/VeriFuzz/Verilog/Internal.hs @@ -29,7 +29,7 @@ module VeriFuzz.Verilog.Internal where import Control.Lens -import Data.Text (Text) +import Data.Text ( Text ) import VeriFuzz.Verilog.AST regDecl :: Identifier -> ModItem diff --git a/src/VeriFuzz/Verilog/Mutate.hs b/src/VeriFuzz/Verilog/Mutate.hs index 66f3c37..e4a10df 100644 --- a/src/VeriFuzz/Verilog/Mutate.hs +++ b/src/VeriFuzz/Verilog/Mutate.hs @@ -41,10 +41,12 @@ module VeriFuzz.Verilog.Mutate where import Control.Lens -import Data.Foldable (fold) -import Data.Maybe (catMaybes, fromMaybe) -import Data.Text (Text) -import qualified Data.Text as T +import Data.Foldable ( fold ) +import Data.Maybe ( catMaybes + , fromMaybe + ) +import Data.Text ( Text ) +import qualified Data.Text as T import VeriFuzz.Circuit.Internal import VeriFuzz.Internal import VeriFuzz.Verilog.AST @@ -337,30 +339,30 @@ declareMod ports = initMod . (modItems %~ (decl ++)) -- >>> GenVerilog . simplify $ (Id "y") + (Id "x") -- (y + x) simplify :: Expr -> Expr -simplify (BinOp (Number (BitVec _ 1)) BinAnd e) = e -simplify (BinOp e BinAnd (Number (BitVec _ 1))) = e -simplify (BinOp (Number (BitVec _ 0)) BinAnd _) = Number 0 -simplify (BinOp _ BinAnd (Number (BitVec _ 0))) = Number 0 -simplify (BinOp e BinPlus (Number (BitVec _ 0))) = e -simplify (BinOp (Number (BitVec _ 0)) BinPlus e) = e +simplify (BinOp (Number (BitVec _ 1)) BinAnd e) = e +simplify (BinOp e BinAnd (Number (BitVec _ 1))) = e +simplify (BinOp (Number (BitVec _ 0)) BinAnd _) = Number 0 +simplify (BinOp _ BinAnd (Number (BitVec _ 0))) = Number 0 +simplify (BinOp e BinPlus (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinPlus e) = e simplify (BinOp e BinMinus (Number (BitVec _ 0))) = e simplify (BinOp (Number (BitVec _ 0)) BinMinus e) = e simplify (BinOp e BinTimes (Number (BitVec _ 1))) = e simplify (BinOp (Number (BitVec _ 1)) BinTimes e) = e simplify (BinOp _ BinTimes (Number (BitVec _ 0))) = Number 0 simplify (BinOp (Number (BitVec _ 0)) BinTimes _) = Number 0 -simplify (BinOp e BinOr (Number (BitVec _ 0))) = e -simplify (BinOp (Number (BitVec _ 0)) BinOr e) = e -simplify (BinOp e BinLSL (Number (BitVec _ 0))) = e -simplify (BinOp (Number (BitVec _ 0)) BinLSL e) = e -simplify (BinOp e BinLSR (Number (BitVec _ 0))) = e -simplify (BinOp (Number (BitVec _ 0)) BinLSR e) = e -simplify (BinOp e BinASL (Number (BitVec _ 0))) = e -simplify (BinOp (Number (BitVec _ 0)) BinASL e) = e -simplify (BinOp e BinASR (Number (BitVec _ 0))) = e -simplify (BinOp (Number (BitVec _ 0)) BinASR e) = e -simplify (UnOp UnPlus e) = e -simplify e = e +simplify (BinOp e BinOr (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinOr e) = e +simplify (BinOp e BinLSL (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinLSL e) = e +simplify (BinOp e BinLSR (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinLSR e) = e +simplify (BinOp e BinASL (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinASL e) = e +simplify (BinOp e BinASR (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinASR e) = e +simplify (UnOp UnPlus e) = e +simplify e = e -- | Remove all 'Identifier' that do not appeare in the input list from an -- 'Expr'. The identifier will be replaced by @1'b0@, which can then later be @@ -377,13 +379,21 @@ removeId i = transform trans combineAssigns :: Port -> [ModItem] -> [ModItem] combineAssigns p a = - a <> [ModCA . ContAssign (p ^. portName) . fold $ Id <$> assigns] + a + <> [ ModCA + . ContAssign (p ^. portName) + . UnOp UnXor + . fold + $ Id + <$> assigns + ] where assigns = a ^.. traverse . modContAssign . contAssignNetLVal -combineAssigns_ :: Port -> [Port] -> ModItem -combineAssigns_ p ps = +combineAssigns_ :: Bool -> Port -> [Port] -> ModItem +combineAssigns_ comb p ps = ModCA . ContAssign (p ^. portName) + . (if comb then UnOp UnXor else id) . fold $ Id <$> ps diff --git a/src/VeriFuzz/Verilog/Parser.hs b/src/VeriFuzz/Verilog/Parser.hs index 68d0ef3..0820e48 100644 --- a/src/VeriFuzz/Verilog/Parser.hs +++ b/src/VeriFuzz/Verilog/Parser.hs @@ -26,17 +26,20 @@ module VeriFuzz.Verilog.Parser where import Control.Lens -import Control.Monad (void) -import Data.Bifunctor (bimap) +import Control.Monad ( void ) +import Data.Bifunctor ( bimap ) import Data.Bits -import Data.Functor (($>)) -import Data.Functor.Identity (Identity) -import Data.List (isInfixOf, isPrefixOf, null) -import Data.List.NonEmpty (NonEmpty (..)) -import Data.Text (Text) -import qualified Data.Text as T -import qualified Data.Text.IO as T -import Text.Parsec hiding (satisfy) +import Data.Functor ( ($>) ) +import Data.Functor.Identity ( Identity ) +import Data.List ( isInfixOf + , isPrefixOf + , null + ) +import Data.List.NonEmpty ( NonEmpty(..) ) +import Data.Text ( Text ) +import qualified Data.Text as T +import qualified Data.Text.IO as T +import Text.Parsec hiding ( satisfy ) import Text.Parsec.Expr import VeriFuzz.Internal import VeriFuzz.Verilog.AST diff --git a/src/VeriFuzz/Verilog/Quote.hs b/src/VeriFuzz/Verilog/Quote.hs index 362cf06..f0b7c96 100644 --- a/src/VeriFuzz/Verilog/Quote.hs +++ b/src/VeriFuzz/Verilog/Quote.hs @@ -18,8 +18,8 @@ module VeriFuzz.Verilog.Quote where import Data.Data -import qualified Data.Text as T -import qualified Language.Haskell.TH as TH +import qualified Data.Text as T +import qualified Language.Haskell.TH as TH import Language.Haskell.TH.Quote import Language.Haskell.TH.Syntax import VeriFuzz.Verilog.Parser diff --git a/test/Doctest.hs b/test/Doctest.hs index 7463dfe..9dc22a4 100644 --- a/test/Doctest.hs +++ b/test/Doctest.hs @@ -1,7 +1,10 @@ module Main where -import Build_doctests (flags, module_sources, pkgs) -import Test.DocTest (doctest) +import Build_doctests ( flags + , module_sources + , pkgs + ) +import Test.DocTest ( doctest ) main :: IO () main = doctest args where args = flags ++ pkgs ++ module_sources diff --git a/test/Parser.hs b/test/Parser.hs index 03cc3a6..84f1906 100644 --- a/test/Parser.hs +++ b/test/Parser.hs @@ -17,10 +17,15 @@ module Parser where import Control.Lens -import Data.Either (either, isRight) -import Hedgehog (Gen, Property, (===)) -import qualified Hedgehog as Hog -import qualified Hedgehog.Gen as Hog +import Data.Either ( either + , isRight + ) +import Hedgehog ( Gen + , Property + , (===) + ) +import qualified Hedgehog as Hog +import qualified Hedgehog.Gen as Hog import Test.Tasty import Test.Tasty.Hedgehog import Test.Tasty.HUnit diff --git a/test/Property.hs b/test/Property.hs index 001c7d3..4e17695 100644 --- a/test/Property.hs +++ b/test/Property.hs @@ -11,16 +11,23 @@ module Property ) where -import Data.Either (either, isRight) -import qualified Data.Graph.Inductive as G -import Data.Text (Text) -import Hedgehog (Gen, Property, (===)) -import qualified Hedgehog as Hog -import Hedgehog.Function (Arg, Vary) -import qualified Hedgehog.Function as Hog -import qualified Hedgehog.Gen as Hog -import qualified Hedgehog.Range as Hog -import Parser (parserTests) +import Data.Either ( either + , isRight + ) +import qualified Data.Graph.Inductive as G +import Data.Text ( Text ) +import Hedgehog ( Gen + , Property + , (===) + ) +import qualified Hedgehog as Hog +import Hedgehog.Function ( Arg + , Vary + ) +import qualified Hedgehog.Function as Hog +import qualified Hedgehog.Gen as Hog +import qualified Hedgehog.Range as Hog +import Parser ( parserTests ) import Test.Tasty import Test.Tasty.Hedgehog import Text.Parsec diff --git a/test/Reduce.hs b/test/Reduce.hs index 9c59e48..bc47d94 100644 --- a/test/Reduce.hs +++ b/test/Reduce.hs @@ -17,7 +17,7 @@ module Reduce ) where -import Data.List ((\\)) +import Data.List ( (\\) ) import Test.Tasty import Test.Tasty.HUnit import VeriFuzz @@ -29,6 +29,7 @@ reduceUnitTests = testGroup [ moduleReducerTest , modItemReduceTest , halveStatementsTest + , statementReducerTest , activeWireTest , cleanTest , cleanAllTest @@ -52,6 +53,7 @@ module top; reg h; wire i; wire j; + wire clk; initial d <= a; always @* begin @@ -62,6 +64,8 @@ module top; end end + always @(posedge clk); + assign b = g; endmodule |] @@ -74,6 +78,7 @@ module top; reg f; reg g; reg h; + wire clk; initial d <= a; always @* begin @@ -84,6 +89,8 @@ module top; end end + always @(posedge clk); + assign b = g; endmodule |] @@ -366,6 +373,94 @@ 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 halveModules srcInfo1 @?= golden1 diff --git a/test/Unit.hs b/test/Unit.hs index 84508c4..aaffe09 100644 --- a/test/Unit.hs +++ b/test/Unit.hs @@ -4,9 +4,9 @@ module Unit where import Control.Lens -import Data.List.NonEmpty (NonEmpty (..)) -import Parser (parseUnitTests) -import Reduce (reduceUnitTests) +import Data.List.NonEmpty ( NonEmpty(..) ) +import Parser ( parseUnitTests ) +import Reduce ( reduceUnitTests ) import Test.Tasty import Test.Tasty.HUnit import VeriFuzz diff --git a/verifuzz.cabal b/verifuzz.cabal index 1b220f3..ef5761b 100644 --- a/verifuzz.cabal +++ b/verifuzz.cabal @@ -1,5 +1,5 @@ name: verifuzz -version: 0.2.0.0 +version: 0.3.0.0 synopsis: Random verilog generation and simulator testing. description: VeriFuzz provides random verilog generation modules @@ -92,6 +92,8 @@ library , optparse-applicative >=0.14 && <0.15 , exceptions >=0.10.0 && <0.11 , blaze-html >=0.9.0.1 && <0.10 + , statistics >=0.14.0.2 && <0.16 + , vector >=0.12.0.1 && <0.13 default-extensions: OverloadedStrings executable verifuzz |