diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-01-01 21:33:29 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-01-01 21:33:29 +0100 |
commit | ff8f80651015556aa8f2d49a8fcbceccb7a5be8e (patch) | |
tree | 2b4606aadf18da9e3e7a6701b3bafc53019a391e /experiments/instructions.org | |
parent | f37727468db7fa9e84c0a7b6b4f4c008214ad70b (diff) | |
download | verismith-ff8f80651015556aa8f2d49a8fcbceccb7a5be8e.tar.gz verismith-ff8f80651015556aa8f2d49a8fcbceccb7a5be8e.zip |
Update instructions
Diffstat (limited to 'experiments/instructions.org')
-rw-r--r-- | experiments/instructions.org | 16 |
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. |