Update instructions

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)
 
 
 
-<a id="org9d6b8b0"></a>
+<a id="orge1df3bc"></a>
 
 # 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
 
 
-<a id="orga672b58"></a>
+<a id="orgc68ec26"></a>
 
 # 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.
 
 
-<a id="org3567b57"></a>
+<a id="org67c7ee8"></a>
 
 ## 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
 
 
-<a id="orgee88861"></a>
+<a id="org4bea20e"></a>
 
 ## 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
 
 
-<a id="orge10bce6"></a>
+<a id="org3c3ca35"></a>
 
 ## 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.
 
 
-<a id="org9d997ed"></a>
+<a id="orgdaa382c"></a>
 
 # 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](<https://github.com/YosysHQ/yosys/issues/997>). In addition to that, a crash can also be reproduced which was also [reported and fixed in Yosys](<https://github.com/YosysHQ/yosys/issues/993>).
 
 
-<a id="org5c11cde"></a>
+<a id="org83f41ec"></a>
 
 ## 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
 
 
-<a id="org959d3a9"></a>
+<a id="org13ba29f"></a>
 
 ## 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`.
 
-<a id="org868d612"></a>
+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.
+
+
+<a id="org049a99a"></a>
 
 ## 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.