search

berkeley-abc / abc

ABC: System for Sequential Logic Synthesis and Formal Verification
Other
885 stars 553 forks source link

Is there a parallel version for CEC? Thanks! #325

Open dezhangxd opened 2 weeks ago

dezhangxd commented 2 weeks ago

We noticed the paper "Parallel combinational equivalence checking" at TCAD (2019) , and the parallel version was developed on 'ABC &cec'.

So, is there a parallel CEC command in the current ABC?

Many thanks!

bojle commented 2 weeks ago

+1 i am interested in knowing this too

weaversa commented 1 week ago

There is! Though, I don't know if it's the same as in the referenced paper.

abc 01> &splitprove -h
usage: &splitprove [-PTIL num] [-svwh]
             proves CEC problem by case-splitting
    -P num : the number of concurrent processes [default = 1]
    -T num : runtime limit in seconds per subproblem [default = 10]
    -I num : the max number of iterations (0 = infinity) [default = 0]
    -L num : maximum look-ahead during cofactoring [default = 1]
    -s     : enable silent computation (no reporting) [default = no]
    -v     : toggle printing verbose information [default = no]
    -w     : toggle printing more verbose information [default = no]
    -h     : print the command usage