From ff8f80651015556aa8f2d49a8fcbceccb7a5be8e Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 1 Jan 2020 21:33:29 +0100 Subject: Update instructions --- experiments/instructions.md | 52 ++++++++++++++++++++++++++++---------------- experiments/instructions.org | 16 ++++++++++++++ 2 files changed, 49 insertions(+), 19 deletions(-) diff --git a/experiments/instructions.md b/experiments/instructions.md index 95f68da..d84a381 100644 --- a/experiments/instructions.md +++ b/experiments/instructions.md @@ -1,19 +1,19 @@ # Table of Contents -1. [Introduction](#org9d6b8b0) -2. [Finding failures in Yosys 0.8](#orga672b58) - 1. [Installing Yosys master](#org3567b57) - 2. [Running Verismith](#orgee88861) - 3. [Using a pre-existing seed](#orge10bce6) -3. [Better example of reduction and interesting failure](#org9d997ed) - 1. [Build Yosys 3333e002](#org5c11cde) - 2. [Running Verismith for mis-synthesis](#org959d3a9) - 3. [Running Verismith for crash](#org868d612) +1. [Introduction](#orge1df3bc) +2. [Finding failures in Yosys 0.8](#orgc68ec26) + 1. [Installing Yosys master](#org67c7ee8) + 2. [Running Verismith](#org4bea20e) + 3. [Using a pre-existing seed](#org3c3ca35) +3. [Better example of reduction and interesting failure](#orgdaa382c) + 1. [Build Yosys 3333e002](#org83f41ec) + 2. [Running Verismith for mis-synthesis](#org13ba29f) + 3. [Running Verismith for crash](#org049a99a) - + # Introduction @@ -22,7 +22,7 @@ The version of Verismith that is assumed to be used is Verismith 0.6.0.2, which cabal install verismith - + # Finding failures in Yosys 0.8 @@ -33,7 +33,7 @@ However, to find failures in Yosys 0.8, a newer version of Yosys has to be used **Note**: The most common error in Yosys 0.8 is regarding for loops, which are not dealt that well with the reducer at the moment. - + ## Installing Yosys master @@ -53,7 +53,7 @@ Then we want to install Yosys 0.8 (which will be installed to `/opt/yosys/0.8`): sudo make install - + ## Running Verismith @@ -118,7 +118,7 @@ Failures can then either be seen on the output, or a summary can be seen in the firefox yosys_output/index.html - + ## Using a pre-existing seed @@ -181,18 +181,18 @@ Just save the config file in `config.toml` and run the following: Which should find a bug and reduce it to around 200 loc out of 1000. - + # Better example of reduction and interesting failure This bug was found in a development version of Yosys (commit hash 3333e002) and was [reported and fixed in Yosys](). In addition to that, a crash can also be reproduced which was also [reported and fixed in Yosys](). - + ## Build Yosys 3333e002 -First, we need to build Yosys 3333e002, in addition to the version of Yosys master [built earlier](#org3567b57). +First, we need to build Yosys 3333e002, in addition to the version of Yosys master [built earlier](#org67c7ee8). git clean -dfx && git reset --hard HEAD git checkout 3333e002 -b test @@ -201,7 +201,7 @@ First, we need to build Yosys 3333e002, in addition to the version of Yosys mast sudo make install - + ## Running Verismith for mis-synthesis @@ -254,8 +254,22 @@ Then run Verismith with the following: verismith fuzz -c config.toml -o output_ms +The result should be that the equivalence check fails and a reduced testcase should be available in `output_ms/fuzz_1/reduce_identity_yosys.v`. - +Contrary to what is expected, the simulation runs will pass. This is because the bug occurs in the initial values that are assigned to the variables. These are set to 0 in the design, but mistakenly set to x in the synthesised design. The testbench does not check for those values and the error is therefore not found by the testbench. + +To fix this manually, one can add a `$strobe("%b", y);` on line 22 in + + cd output_ms/fuzz_1/simulation_yosys + sed -i '21 a $strobe("%b", y);' yosys_testbench.v + iverilog -o yosys_main yosys_testbench.v + # ./yosys_main | grep 'x' + ./yosys_main + +which should show some `x` in the output which should not be there. + + + ## Running Verismith for crash diff --git a/experiments/instructions.org b/experiments/instructions.org index 869af36..9bc2ea4 100644 --- a/experiments/instructions.org +++ b/experiments/instructions.org @@ -239,6 +239,22 @@ Then run Verismith with the following: verismith fuzz -c config.toml -o output_ms #+end_src +The result should be that the equivalence check fails and a reduced testcase should be available in ~output_ms/fuzz_1/reduce_identity_yosys.v~. + +Contrary to what is expected, the simulation runs will pass. This is because the bug occurs in the initial values that are assigned to the variables. These are set to 0 in the design, but mistakenly set to x in the synthesised design. The testbench does not check for those values and the error is therefore not found by the testbench. + +To fix this manually, one can add a ~$strobe("%b", y);~ on line 22 in + +#+begin_src bash +cd output_ms/fuzz_1/simulation_yosys +sed -i '21 a $strobe("%b", y);' yosys_testbench.v +iverilog -o yosys_main yosys_testbench.v +# ./yosys_main | grep 'x' +./yosys_main +#+end_src + +which should show some ~x~ in the output which should not be there. + *** Running Verismith for crash *Note*: Verismith is not that great at reducing crashes, as is explained in our paper. -- cgit