diff options
| author | Clifford Wolf <clifford@clifford.at> | 2017-01-30 11:38:43 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2017-01-30 11:38:43 +0100 |
| commit | 18ea65ef04889e5016f007d3a034c8c49709cdb6 (patch) | |
| tree | f8bf155c87ccfae366b71d159396f701ef2d3696 /backends | |
| parent | fe29869ec5104376d7d061e82a7f7be77673e8f1 (diff) | |
| download | yosys-18ea65ef04889e5016f007d3a034c8c49709cdb6.tar.gz yosys-18ea65ef04889e5016f007d3a034c8c49709cdb6.tar.bz2 yosys-18ea65ef04889e5016f007d3a034c8c49709cdb6.zip | |
Add "yosys-smtbmc --aig <aim_filename>:<aiw_filename>" support
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smt2/smtbmc.py | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index ab952786e..10875f523 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -29,7 +29,8 @@ num_steps = 20 append_steps = 0 vcdfile = None cexfile = None -aigprefix = None +aimfile = None +aiwfile = None aigheader = True vlogtbfile = None inconstr = list() @@ -74,6 +75,10 @@ yosys-smtbmc [options] <yosys_smt2_output> and AIGER witness file. The file names are <prefix>.aim for the map file and <prefix>.aiw for the witness file. + --aig <aim_filename>:<aiw_filename> + like above, but for map files and witness files that do not + share a filename prefix (or use differen file extensions). + --aig-noheader the AIGER witness file does not include the status and properties lines. @@ -145,7 +150,11 @@ for o, a in opts: elif o == "--cex": cexfile = a elif o == "--aig": - aigprefix = a + if ":" in a: + aimfile, aiwfile = a.split(":") + else: + aimfile = a + ".aim" + aiwfile = a + ".aiw" elif o == "--aig-noheader": aigheader = False elif o == "--dump-vcd": @@ -382,7 +391,7 @@ if cexfile is not None: skip_steps = max(skip_steps, step) num_steps = max(num_steps, step+1) -if aigprefix is not None: +if aimfile is not None: input_map = dict() init_map = dict() latch_map = dict() @@ -392,7 +401,7 @@ if aigprefix is not None: skip_steps = 0 num_steps = 0 - with open(aigprefix + ".aim", "r") as f: + with open(aimfile, "r") as f: for entry in f.read().splitlines(): entry = entry.split() @@ -413,7 +422,7 @@ if aigprefix is not None: assert False - with open(aigprefix + ".aiw", "r") as f: + with open(aiwfile, "r") as f: got_state = False got_ffinit = False step = 0 |