Implement circuit reduction

[mgudemann]

• find / eliminate equivalent latches (or negation-equivalent ones)
• reduction of combinatorial nodes
• find implications

While SAT simplification can reduce the query size a help a lot, already creating smaller circuit representations / netlists has shown to be very beneficial in addition. For IC3 reducing the number of latches leads to smaller cubes, for induction/BMC all reductions are beneficial, either by reducing the circuit or by strengthening the properties. Finding implications might only be beneficial for induction/BMC.

[mgudemann]

a sensible place to add seems to be netlist creation, in particular in aig mode and then passing the reduced circuit / strengthened properties to the back-end solver

[eigold]

Sorry for the late reply. (I have been working hard on writing and debugging extra code for the paper version of iC3.) I agree that adding circuit optimization techniques is quite beneficial. This is definitely should be done after some urgent stuff is finished which is a) paper related coding and collecting experimental data b) debugging the SMV input (I will comment more on this topic in a reply to your other email) c) adding the ability to specify initial states of latches symbolically (via constraints). I realized the importance of the latter item, when Rajdeep pointed out that IC3-db "refused" to verify a simple Verilog example because the initial value of a register was specified by an input variable. (Currently, IC3-db assumes that every latch is initialized by 0,1 or a don't-care). This can be easily fixed by specifying initial states as a set of constraints. I have actually written the necessary code in one of my numerous variations of IC3 I experimented with.

…

On Sat, Jul 22, 2017 at 8:02 AM, Matthias Güdemann ***@***.*** > wrote: - find / eliminate equivalent latches (or negation-equivalent ones) - reduction of combinatorial nodes - find implications While SAT simplification can reduce the query size a help a lot, already creating smaller circuit representations / netlists has shown to be very beneficial in addition. For IC3 reducing the number of latches leads to smaller cubes, for induction/BMC all reductions are beneficial, either by reducing the circuit or by strengthening the properties. Finding implications might only be beneficial for induction/BMC. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#28>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AS5pCsqvLVGG3nLCXX_c9-iCHs1Kvhilks5sQeTugaJpZM4OgJ3e> .