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 using the bit blaster in the aig library applied to TODO.

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.