• Top
    • Documentation
    • Books
    • Boolean-reasoning
      • Ipasir
      • Aignet
      • Aig
        • Aig-constructors
        • Aig-vars
        • Aig-sat
        • Bddify
        • Aig-substitution
        • Aig-other
          • Best-aig
          • Aig2c
            • Aig2c-config-p
            • Aig2c-compile
            • Aig2c-maketemps
            • Aig2c-main
            • Aig2c-prologue
            • Aig2c-maketemps-list
            • Aig2c-epilogue
            • Aig2c-main-list
          • Expr-to-aig
          • Aiger-write
          • Aig-random-sim
          • Aiger-read
          • Aig-print
          • Aig-cases
        • Aig-semantics
        • Aig-and-count
      • Satlink
      • Truth
      • Ubdds
      • Bdd
      • Faig
      • Bed
      • 4v
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Aig-other

Aig2c

Naive compiler from Hons AIGs into C/C++ code fragments.

The idea here is to be able to take an AIG and embed it in a C or C++ program. You can tweak various aspects of the code that gets generated, but some basic example output is:

const uint32_t n_8 = inputs.a;     // prologue: initializes temp variables
const uint32_t n_2 = inputs.b;     //   you can control the rhs'es here
const uint32_t n_4 = inputs.c;

const uint32_t n_3 = ~n_4;         // main aig contents
const uint32_t n_1 = n_2 & n_3;    //   never try to understand this
const uint32_t n_7 = ~n_8;
const uint32_t n_6 = n_4 & n_7;
const uint32_t n_5 = n_6 & n_1;

out1 = n_1;                        // epilogue: extracts aigs to outputs
out2 = n_5;                        //   you can control the lhs'es here

We try to make relatively few assumptions about how you might actually use this code. Toward that goal, you may configure, e.g., the names and types of the temporary variables, and the operators used to carry out each AND and NOT operation.

Some high level notes:

  • We basically turn each AIG node into one line of C/C++ code.
  • We do at least take advantage of shared structure in the AIG, and avoid recomputing an AND node just because it has multiple fanouts.
  • We don't even do basic optimizations like using | or ^ operators, but doing so might be useful.
  • We do nothing to smartly collapse the AIG into vectors to take advantage of, e.g., 32-bit bitwise ANDs, or anything like that.

The top-level function is aig2c-compile.

Subtopics

Aig2c-config-p
Configuration object that governs how we translate an AIG into C/C++.
Aig2c-compile
Compile an alist of AIGs into a C code fragment.
Aig2c-maketemps
Create the temporary C code variable names that will be used for each each AIG node, for a single AIG.
Aig2c-main
Create the assignments for a single AIG.
Aig2c-prologue
Create the assignments for AIG constant and variable nodes.
Aig2c-maketemps-list
Create the temporary C code variable names for a whole list of AIGs.
Aig2c-epilogue
Create the assignments from AIG nodes to outputs.
Aig2c-main-list
Create the assignments for a list of AIGs.