ABC Performance Analysis

Overview

SAW 0.8 includes a linked-in version of ABC and uses the saw-core-aig package plus a bit blaster in the aig package to construct AIGs using the C API to ABC when using the abc proof tactic. This caused numerous maintenance headaches, so after the 0.8 release we removed the linked-in ABC version. In its place, we have four new ways to interact with ABC.

• The sbv_abc tactic converts the goal to SMT-Lib2 using SBV and sends it to an external ABC process.
• The w4_abc_smtlib2 tactic converts the goal to SMT-Lib2 using What4 and sends it to an external ABC process.
• The w4_abc_verilog tactic converts the goal to Verilog using What4 and sends it to an external ABC process.
• The w4_abc_aiger tactic converts the goal to AIGER format and sends it to an external ABC process. I just realized while writing this that it doesn't use What4, and therefore is misleadingly named.

Benchmarks

One set of benchmarks, written to exist as props.saw in some arbitrary sub-directory of the saw-script repo:

import "../deps/cryptol-specs/Primitive/Symmetric/Cipher/Block/simon.cry";
// correctSimon32_64, uniqueExpandSimon32_64

import "../deps/cryptol-specs/Primitive/Symmetric/Cipher/Block/speck.cry";
// correctSpeck32_64

import "../deps/cryptol-specs/Primitive/Symmetric/Cipher/Block/PRINCE.cry";
// princeCorrect, princeCorrect'

import "../deps/cryptol-specs/Primitive/Symmetric/Cipher/Block/TEA.cry";
// teaCorrect, teaCorrect'

import "../deps/cryptol-specs/Primitive/Symmetric/Cipher/Block/GOST.cry";
// gostCorrect

import "../deps/cryptol-specs/Primitive/Symmetric/Cipher/Block/DES.cry";
// DESCorrect

import "../deps/cryptol-specs/Primitive/Symmetric/Cipher/Stream/Salsa20.cry";
// Salsa20_has_no_collisions

import "../deps/cryptol-specs/Primitive/Symmetric/Cipher/Stream/ZUC.cry";
// ZUC_isResistantToCollisionAttack

prove_term "uniqueExpandSimon32_64" {{ uniqueExpandSimon32_64 }};
prove_term "correctSimon32_64" {{ correctSimon32_64 }};
prove_term "correctSpeck32_64" {{ correctSpeck32_64 }};
//prove_term "princeCorrect" {{ princeCorrect }};
//prove_term "princeCorrect'" {{ princeCorrect' }};
//prove_term "gostCorrect" {{ gostCorrect }};
prove_term "DESCorrect" {{ DESCorrect }};
prove_term "Salsa20_has_no_collisions" {{ Salsa20_has_no_collisions }};
prove_term "ZUC_isResistantToCollisionAttack" {{ ZUC_isResistantToCollisionAttack }};

This file can then be included in scripts that define prove_term to use different tactics, and intended to run with different SAW versions. For example, this one just times w4_abc_aiger:

enable_experimental;
let prove_term msg t = do {
  print "SAW 0.9 w4_abc_aiger";
  time (prove w4_abc_aiger t);
};

include "props.saw";

To check the proof tactics that exist in SAW 0.8, intended for use with SAW 0.8:

enable_experimental;
let prove_term msg t = do {
  print (str_concat "== Proving " msg);
  print "SAW 0.8 abc";
  time (prove abc t);
  print "SAW 0.8 sbv_abc";
  time (prove sbv_abc t);
  print "SAW 0.8 w4_abc_smtlib2";
  time (prove w4_abc_smtlib2 t);
  print "SAW 0.8 w4_abc_verilog";
  time (prove w4_abc_verilog t);
  print "SAW 0.8 offline_aig";
  time (prove (offline_aig "foo") t);
  print "SAW 0.8 offline_cnf";
  time (prove (offline_cnf "foo") t);
  print "SAW 0.8 offline_verilog";
  time (prove (offline_verilog "foo") t);
  exec "rm" ["foo.prove0.aig"] "";
  exec "rm" ["foo.prove0.cnf"] "";
  exec "rm" ["foo.prove0.v"] "";
};

include "props.saw";

And then to prove a goal using the newer tactics, intended for use with SAW 0.9 or newer:

enable_experimental;
let prove_term msg t = do {
  print (str_concat "== Proving " msg);
  print "SAW 0.9 sbv_abc";
  time (prove sbv_abc t);
  //print "SAW 0.9 w4_abc_aiger";
  //time (prove w4_abc_aiger t);
  print "SAW 0.9 w4_abc_smtlib2";
  time (prove w4_abc_smtlib2 t);
  print "SAW 0.9 w4_abc_verilog";
  time (prove w4_abc_verilog t);
  print "SAW 0.9 offline_aig";
  time (prove (offline_aig "foo") t);
  print "SAW 0.9 offline_cnf";
  time (prove (offline_cnf "foo") t);
  print "SAW 0.9 offline_verilog";
  time (prove (offline_verilog "foo") t);
  exec "rm" ["foo.prove0.aig"] "";
  exec "rm" ["foo.prove0.cnf"] "";
  exec "rm" ["foo.prove0.v"] "";
};

include "props.saw";

In this case, w4_abc_aiger is commented out because it often runs for an extremely long time. I've checked the offline AIGER mode, which uses the same bit-blaster and AIGER writer, and it's fast. So the problem is in the encoding of the formula as an AIG.

Early Conclusions

It seems, unfortunately, that most of these benchmarks are slower when going through What4. The sbv_abc tactic is usually faster than w4_abc_smtlib2 or w4_abc_verilog. The old abc tactic is also usually faster than the new w4_abc_aiger (sometimes drastically so), but given that they use very similar execution paths, this is somewhat mysterious.