search

d-kfmnn / amulet2

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

Verification hung #5

Closed vkrao100 closed 3 years ago

vkrao100 commented 3 years ago

Hi @d-kfmnn,

I was trying to verify an SP-AR-RC format (optimized using resyn+dc2 in abc ) 128-bit correct multiplier. However, the verification gets stuck while reducing slice 244 for a long time. The amulet1.0 and amulet1.5 versions verify it within seconds.

Attaching the test case. map-sp-ar-rc-128-opt-dc2.zip

Thanks, Vikas

d-kfmnn commented 3 years ago

Hi Vikas,

sorry for taking so long on this bugfix. Again many thanks for providing the benchmark!

In Amulet2.0 I apply a variable elimination step before sorting the gates, which I did not do in amulet1.x. However, I did not consider a corner case for XOR-gates, which caused a hickup in the variable ordering.

Best, Daniela