berkeley-abc / abc

ABC: System for Sequential Logic Synthesis and Formal Verification
Other
891 stars 582 forks source link

"Hard limit on the number of nodes (2^29) is reached." Lacks justification #106

Open TomMD opened 3 years ago

TomMD commented 3 years ago

I see the AIG generation has a hard limit of 2^29. This limit is lower than I'd desire. Is there a rational here (ex: AIG specification) or is this bound arbitrary and for pragmatic reasons?

alanminko commented 3 years ago

This was partially a matter of convenience but also an oversight to some extent. If I designed an AIG package now, it would have a 2^31 hard limit.  This may also not be enough.  if so, it would not be difficult to have a 64-bit AIG package, which the limit of 2^63 nodes.  The only problem with this, is that almost 50% of memory used will be wasted.

In general, my suggestion is to rethink the problem to make it fit into 2^29.  For example, I am aware of several research projects, which build AIGs representing quantized neural networks.  It is easy to generate a one trillion node AIG this way (2^40 nodes).  However, what is often overlooked, is that in addition to using a lot of memory, the computation is very slow. It is much more efficieint to keep the AIG in a hierarchical form.  Everything (simulation, traversal, computation of various functional properties) can be done on such a hierarchical AIG without building its gigantic flat version.

On 11/13/2020 11:11 AM, Thomas M. DuBuisson wrote:

I see the AIG generation has a hard limit of 2^29. This limit is lower than I'd desire. Is there a rational here (ex: AIG specification) or is this bound arbitrary and for pragmatic reasons?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/berkeley-abc/abc/issues/106, or unsubscribe https://github.com/notifications/unsubscribe-auth/AI4DBXVOYZUF36EUDBBWZKLSPWAHDANCNFSM4TU6O3AQ.

TomMD commented 3 years ago

My use of ABC is only incidentally via SAW (saw.galois.com). It seems difficult to move to a hierarchical form as that would require changes throughout the stack. Am I correct in reading that using a 64 bit int to count the nodes in AIG would be objectionable only in so far as the memory used to store the upper 32 bits is mostly wasted (most of the time, entirely wasted)?

alanminko commented 3 years ago

Yes, this is what I meant.  If we have a 1T node AIG, we use 40 bits out of 64. Thus we waste 100(64-40)/64 = 37%.  Perhaps it not too bad. My other concern is that manipulating AIG whose memory footprint is 162^40 bytes = 16 TB (terabytes) will be very slow.

On 11/14/2020 2:39 PM, Thomas M. DuBuisson wrote:

My use of ABC is only incidentally via SAW (saw.galois.com). It seems difficult to move to a hierarchical form as that would require changes throughout the stack. Am I correct in reading that using a 64 bit int to count the nodes in AIG would be objectionable only in so far as the memory used to store the upper 32 bits is mostly wasted (most of the time, entirely wasted)?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/berkeley-abc/abc/issues/106#issuecomment-727275180, or unsubscribe https://github.com/notifications/unsubscribe-auth/AI4DBXX6A4TBALNYWCW7GG3SP4BJJANCNFSM4TU6O3AQ.