Is there a parallel version for CEC? Thanks!

[dezhangxd]

Is there a parallel version for CEC? Thanks!

[dezhangxd]

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]

+1 i am interested in knowing this too

[weaversa]

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

[jfliasdjlasjg]

&splitprove need download kissat