aboutsummaryrefslogtreecommitdiffstats
path: root/experiments/instructions.org
diff options
context:
space:
mode:
Diffstat (limited to 'experiments/instructions.org')
-rw-r--r--experiments/instructions.org16
1 files changed, 16 insertions, 0 deletions
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.