search

d-kfmnn / amulet2

AMulet 2. - A better AIG Multiplier Examination Tool
MIT License
20 stars 4 forks source link

-substitute sometimes produces an AAG #1

Closed mfernan2 closed 3 years ago

mfernan2 commented 3 years ago

Very nice work!

I haven't quite narrowed down why, but sometimes amulet -substitute ... produces an AAG instead of an AIG. E.g. using the input 32bit-BP-AR-BL.aig from https://github.com/amahzoon/RevSCA-2.0 results in an AAG output. Looking at the AMulet source it looks like, contrary to the --help output, it always outputs an AAG:

...
 if (!aiger_write_to_file(rewritten, aiger_ascii_mode, f2))
...

But this is not the case. Other AIGs I have tried result in AIG output from -substitute. Maybe this is some known behavior of the aiger lib?

mfernan2 commented 3 years ago

Ah I think I figured out the differentiating factor. The ones that produce AIG output instead of AAG output have an FSA that is not a GP adder, so no substitution is performed. I.e. the output is identical to the original AIG.

d-kfmnn commented 3 years ago

I don't know why I've overlooked your issue for so long. Sorry about that.

Yes you are right, there was a inconsistency in printing the AIGs, which used 'aiger_ascii_mode' for the rewritten AIGs, and 'aiger_binary_mode' when no substitution is performed.

Thank you for spotting this issue, it is now fixed.