From 24cf9ce5bf673615ebe36f5ab5d0ff7685dfada6 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 25 Jun 2019 22:32:21 +0100 Subject: Add back the simulation --- README.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'README.md') diff --git a/README.md b/README.md index 2d0588e..829f3b0 100644 --- a/README.md +++ b/README.md @@ -3,14 +3,17 @@ Verilog Fuzzer to test the major verilog compilers by generating random, valid verilog. -It currently supports the following simulators: +It currently supports the following synthesisers: - [Yosys](http://www.clifford.at/yosys/) -- [Icarus Verilog](http://iverilog.icarus.com) - [Xst](https://www.xilinx.com/support/documentation/sw_manuals/xilinx11/ise_c_using_xst_for_synthesis.htm) - [Vivado](https://www.xilinx.com/products/design-tools/ise-design-suite.html) - [Quartus](https://www.intel.com/content/www/us/en/programmable/downloads/download-center.html) +and the following simulator: + +- [Icarus Verilog](http://iverilog.icarus.com) + ## Build the Fuzzer The fuzzer is split into an executable (in the [app](/app) folder) and a -- cgit From 1dd3aa0e68bd836dca4b522a922ed494092e46ba Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 29 Jun 2019 16:12:07 +0100 Subject: Add found bugs --- README.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'README.md') diff --git a/README.md b/README.md index 829f3b0..0159d94 100644 --- a/README.md +++ b/README.md @@ -14,6 +14,25 @@ and the following simulator: - [Icarus Verilog](http://iverilog.icarus.com) +## Reported bugs + +- **MS** :: Mis-synthesis +- **C** :: Crash + +### Yosys + +| Type | Issue | Confirmed | Fixed | | +|------|------------------------------------------------------------|-----------|-------|---| +| MS | [Issue 1047](https://github.com/YosysHQ/yosys/issues/1047) | ✓ | ✓ | | +| MS | [Issue 997](https://github.com/YosysHQ/yosys/issues/997) | ✓ | ✓ | | +| C | [Issue 993](https://github.com/YosysHQ/yosys/issues/993) | ✓ | ✓ | | + +### Vivado + +| Type | Issue | Confirmed | Fixed | +|------|-----------------------------------------------------------------------------------------------------|-----------|-------| +| C | https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Verilog-If-statement-nesting-crash/td-p/981787 | | | + ## Build the Fuzzer The fuzzer is split into an executable (in the [app](/app) folder) and a -- cgit From e4ee48cf1077c0698cd7659ebf3bc84ba9596c79 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 29 Jun 2019 16:17:14 +0100 Subject: Add reported bugs --- README.md | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) (limited to 'README.md') diff --git a/README.md b/README.md index 0159d94..2853f29 100644 --- a/README.md +++ b/README.md @@ -21,17 +21,21 @@ and the following simulator: ### Yosys -| Type | Issue | Confirmed | Fixed | | -|------|------------------------------------------------------------|-----------|-------|---| -| MS | [Issue 1047](https://github.com/YosysHQ/yosys/issues/1047) | ✓ | ✓ | | -| MS | [Issue 997](https://github.com/YosysHQ/yosys/issues/997) | ✓ | ✓ | | -| C | [Issue 993](https://github.com/YosysHQ/yosys/issues/993) | ✓ | ✓ | | +| Type | Issue | Confirmed | Fixed | +|------|------------------------------------------------------------|-----------|-------| +| MS | [Issue 1047](https://github.com/YosysHQ/yosys/issues/1047) | ✓ | ✓ | +| MS | [Issue 997](https://github.com/YosysHQ/yosys/issues/997) | ✓ | ✓ | +| C | [Issue 993](https://github.com/YosysHQ/yosys/issues/993) | ✓ | ✓ | ### Vivado -| Type | Issue | Confirmed | Fixed | -|------|-----------------------------------------------------------------------------------------------------|-----------|-------| -| C | https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Verilog-If-statement-nesting-crash/td-p/981787 | | | +| Type | Issue | Confirmed | Fixed | +|------|---------------------------------------------------------------------------------------------------------------------|-----------|-------| +| C | [Forum 981787](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Verilog-If-statement-nesting-crash/td-p/981787) | ✓ | 𐄂 | +| C | [Forum 981136](https://forums.xilinx.com/t5/Synthesis/Vivado-2018-3-synthesis-crash/td-p/981136) | ✓ | 𐄂 | +| MS | [Forum 981789](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Unsigned-bit-extension-in-if-statement/td-p/981789) | ✓ | 𐄂 | +| MS | [Forum 982518](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Signed-with-shift-in-condition-synthesis-mistmatch/td-p/982518) | ✓ | 𐄂 | +| MS | [Forum 982419](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Bit-selection-synthesis-mismatch/td-p/982419) | ✓ | 𐄂 | ## Build the Fuzzer -- cgit From 4be7974ae71eb024977198b146f6052a1854541c Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 29 Jun 2019 16:18:32 +0100 Subject: Add some more stats --- README.md | 3 +++ 1 file changed, 3 insertions(+) (limited to 'README.md') diff --git a/README.md b/README.md index 2853f29..13addac 100644 --- a/README.md +++ b/README.md @@ -16,6 +16,9 @@ and the following simulator: ## Reported bugs +21 bugs were found in total over the course of a month. 8 of those bugs were +reported and 3 were fixed. + - **MS** :: Mis-synthesis - **C** :: Crash -- cgit From 9d72391db16f0e0c46c4db510d07a585cb1bf3e9 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 29 Jun 2019 20:05:36 +0100 Subject: Add links to presentation and thesis --- README.md | 33 ++++++++++++++++++++++++++------- 1 file changed, 26 insertions(+), 7 deletions(-) (limited to 'README.md') diff --git a/README.md b/README.md index 13addac..6e2cbac 100644 --- a/README.md +++ b/README.md @@ -14,6 +14,15 @@ 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. + +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. + ## Reported bugs 21 bugs were found in total over the course of a month. 8 of those bugs were @@ -32,13 +41,13 @@ reported and 3 were fixed. ### Vivado -| Type | Issue | Confirmed | Fixed | -|------|---------------------------------------------------------------------------------------------------------------------|-----------|-------| -| C | [Forum 981787](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Verilog-If-statement-nesting-crash/td-p/981787) | ✓ | 𐄂 | -| C | [Forum 981136](https://forums.xilinx.com/t5/Synthesis/Vivado-2018-3-synthesis-crash/td-p/981136) | ✓ | 𐄂 | -| MS | [Forum 981789](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Unsigned-bit-extension-in-if-statement/td-p/981789) | ✓ | 𐄂 | -| MS | [Forum 982518](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Signed-with-shift-in-condition-synthesis-mistmatch/td-p/982518) | ✓ | 𐄂 | -| MS | [Forum 982419](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Bit-selection-synthesis-mismatch/td-p/982419) | ✓ | 𐄂 | +| Type | Issue | Confirmed | Fixed | +|------|-------------------------------------------------------------------------------------------------------------------------------------|-----------|-------| +| C | [Forum 981787](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Verilog-If-statement-nesting-crash/td-p/981787) | ✓ | 𐄂 | +| C | [Forum 981136](https://forums.xilinx.com/t5/Synthesis/Vivado-2018-3-synthesis-crash/td-p/981136) | ✓ | 𐄂 | +| MS | [Forum 981789](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Unsigned-bit-extension-in-if-statement/td-p/981789) | ✓ | 𐄂 | +| MS | [Forum 982518](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Signed-with-shift-in-condition-synthesis-mistmatch/td-p/982518) | ✓ | 𐄂 | +| MS | [Forum 982419](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Bit-selection-synthesis-mismatch/td-p/982419) | ✓ | 𐄂 | ## Build the Fuzzer @@ -78,3 +87,13 @@ To run the test-suites: ``` stack test ``` + +## 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). -- cgit From 8734d40f4842065ce5a579eb0cc77171bbd436b0 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 29 Jun 2019 20:08:48 +0100 Subject: Add generated constructs --- README.md | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) (limited to 'README.md') diff --git a/README.md b/README.md index 6e2cbac..6901f69 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,10 @@ # 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. +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 synthesisers: @@ -17,11 +20,18 @@ and the following simulator: ## Supported Verilog Constructs The fuzzer generates combinational and behavioural Verilog to test the various -tools. - -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. +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 -- cgit From e41bb1cddbaf20f96a03e86ba5f0afb47983301d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 5 Jul 2019 13:52:46 +0200 Subject: Small changes to the documentation --- README.md | 31 ++++++++++++++----------------- 1 file changed, 14 insertions(+), 17 deletions(-) (limited to 'README.md') diff --git a/README.md b/README.md index 6901f69..30b4593 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,12 @@ # 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. There is a +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 synthesisers: +It currently supports the following synthesis tools: - [Yosys](http://www.clifford.at/yosys/) - [Xst](https://www.xilinx.com/support/documentation/sw_manuals/xilinx11/ise_c_using_xst_for_synthesis.htm) @@ -38,26 +38,23 @@ following: 21 bugs were found in total over the course of a month. 8 of those bugs were reported and 3 were fixed. -- **MS** :: Mis-synthesis -- **C** :: Crash - ### Yosys -| Type | Issue | Confirmed | Fixed | -|------|------------------------------------------------------------|-----------|-------| -| MS | [Issue 1047](https://github.com/YosysHQ/yosys/issues/1047) | ✓ | ✓ | -| MS | [Issue 997](https://github.com/YosysHQ/yosys/issues/997) | ✓ | ✓ | -| C | [Issue 993](https://github.com/YosysHQ/yosys/issues/993) | ✓ | ✓ | +| 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 | -|------|-------------------------------------------------------------------------------------------------------------------------------------|-----------|-------| -| C | [Forum 981787](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Verilog-If-statement-nesting-crash/td-p/981787) | ✓ | 𐄂 | -| C | [Forum 981136](https://forums.xilinx.com/t5/Synthesis/Vivado-2018-3-synthesis-crash/td-p/981136) | ✓ | 𐄂 | -| MS | [Forum 981789](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Unsigned-bit-extension-in-if-statement/td-p/981789) | ✓ | 𐄂 | -| MS | [Forum 982518](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Signed-with-shift-in-condition-synthesis-mistmatch/td-p/982518) | ✓ | 𐄂 | -| MS | [Forum 982419](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Bit-selection-synthesis-mismatch/td-p/982419) | ✓ | 𐄂 | +| 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 -- cgit From c19a51a8156bbcaee13d9819c8fe54ed0ca5c4cc Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 5 Jul 2019 15:17:39 +0200 Subject: Add section about configuration file --- README.md | 41 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) (limited to 'README.md') diff --git a/README.md b/README.md index 30b4593..6c0eb1a 100644 --- a/README.md +++ b/README.md @@ -95,6 +95,47 @@ 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 -- cgit