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.org | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'experiments/instructions.org') 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