mirror of
https://github.com/YosysHQ/sby.git
synced 2025-10-07 18:21:56 +00:00
More tests without properties
Used `sby --autotune` to find other engines which fail (though there aren't any other exceptions that I could find). Parse errors from `abc bmc3` and `abc sim3` instead of returning UNKNOWN.
This commit is contained in:
parent
c06d8682cd
commit
db782815f2
2 changed files with 19 additions and 3 deletions
|
@ -246,6 +246,9 @@ def run(mode, task, engine_idx, engine):
|
||||||
else:
|
else:
|
||||||
proc_status = "FAIL"
|
proc_status = "FAIL"
|
||||||
|
|
||||||
|
match = re.match("Error: (Does not work|Only works) for (sequential|combinational) networks.", line)
|
||||||
|
if match: proc_status = "ERROR"
|
||||||
|
|
||||||
return line
|
return line
|
||||||
|
|
||||||
def exit_callback(retcode):
|
def exit_callback(retcode):
|
||||||
|
|
|
@ -1,13 +1,26 @@
|
||||||
[tasks]
|
[tasks]
|
||||||
abc
|
abc prove
|
||||||
abc_keepgoing
|
abc_keepgoing prove
|
||||||
|
|
||||||
|
# "Error: Does not work for combinational networks."
|
||||||
|
abc_bmc3 bmc error
|
||||||
|
# "Error: Only works for sequential networks."
|
||||||
|
abc_sim3 bmc error
|
||||||
|
# "Property index 0 is greater than the number of properties in file model/design_btor_single.btor (0)"
|
||||||
|
btor_pono bmc error
|
||||||
|
|
||||||
[options]
|
[options]
|
||||||
mode prove
|
prove: mode prove
|
||||||
|
bmc: mode bmc
|
||||||
|
cover: mode cover
|
||||||
|
error: expect ERROR
|
||||||
|
|
||||||
[engines]
|
[engines]
|
||||||
abc: abc pdr
|
abc: abc pdr
|
||||||
abc_keepgoing: abc --keep-going pdr
|
abc_keepgoing: abc --keep-going pdr
|
||||||
|
btor_pono: btor pono
|
||||||
|
abc_bmc3: abc bmc3
|
||||||
|
abc_sim3: abc sim3
|
||||||
|
|
||||||
[script]
|
[script]
|
||||||
read -sv test.sv
|
read -sv test.sv
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue