search

d-kfmnn / amulet2

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

Amulet2.0 gets stuck in reduce but 1.5 works fine #6

Open ravipr72 opened 2 years ago

ravipr72 commented 2 years ago

I have a test which unfortunately I cannot share at the moment. In this case on a 22bit wide MUL, 2.1 gets stuck, while 1.5 is able to quickly prove the MUL. I think the issue is in the difference in merge_all routine in slicing step. It seems in 2.x a gate is not merged even if it has a single input in its fanin. However in 1.5, the gate is rejected when both the arguments of the AND gate are input. This leads to a different/heavy logic in slices leading to non-convergence.

d-kfmnn commented 2 years ago

Hey, I just made a new release to AMulet 2.2, where I fixed several issues of the slicing routine. Could you try your test case again and let me know whether the issue is still present? Thanks.

ravipr72 commented 2 years ago

Hi, Thanks for the quick response. I am afraid this does not solve the issue. For this to work, we have to force the slicing to 1.5 based (slicing_non_xor), but as I have reported in my observation, we end up merging very few gates due to the issue I have indicated. 2.2 when forced to run slicing_non_xor based slicing: [amulet2] totally merged 449 variable(s) [amulet2] totally promoted 24 variable(s)

1.5/1.0 (which works) [amulet] totally merged 2691 variable(s) [amulet] totally promoted 16 variable(s)

ravipr72 commented 2 years ago

Don't want to overdo this, but will share the change that when made fixes my issue atleast.

diff amulet2-main/src/slicing.cpp x/amulet2-main/src/slicing.cpp 461d460 < bool all_inp = true; 465,466c464 < if (n_child->get_input()) < continue;

    if (n_child->get_input()) flag = 1;

469d466 < all_inp=false; 472c469 < if (flag || all_inp) continue;

  if (flag) continue;