Skip to content

Commit 781f8c6

Browse files
authored
Merge pull request #9039 from Pinata-Consulting/sv-bug-point
test/orfs: sv-bugpoint instructions
2 parents 751dfd0 + 68c8a57 commit 781f8c6

File tree

1 file changed

+21
-0
lines changed

1 file changed

+21
-0
lines changed

test/orfs/README.md

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -212,3 +212,24 @@ Running this, we get:
212212
</pre>
213213

214214

215+
## using sv-bugpoint to whittle down test-cases
216+
217+
[sv-bugpoint](https://github.com/antmicro/sv-bugpoint) can be used to whittle down test-cases to a minimum example.
218+
219+
Let's say that `bazelisk test test/orfs/gcd:eqy_synth_test` fails, first create a script that looks for the error string in the output, in this case a false positive `Failed to prove equivalence of partition gcd.req_rdy`.
220+
221+
After compiling sv-bugpoint, we create a check.sh script:
222+
223+
```bash
224+
#!/bin/bash
225+
set -euo pipefail
226+
cp $1 test/orfs/gcd/
227+
(bazelisk test test/orfs/gcd:eqy_synth_test --test_timeout=30 --test_output=streamed || error=$?) | tee /dev/tty | grep "Failed to prove equivalence of partition gcd.req_rdy"
228+
```
229+
230+
- `--test_timeout=30` is a suitable timeout for this test and machine, adjust. Note that the timeout must be handled by Bazel and not a generic `timeout` utility as it would not work correctly with the bazel server.
231+
232+
233+
Next, run sv-bugpoint to whittle `test/orfs/gcd/gcd.v` down to a minimal test case:
234+
235+
~/sv-bugpoint/build/sv-bugpoint fail check.sh test/orfs/gcd/gcd.v

0 commit comments

Comments
 (0)