cec: Adding new algorithm for generating simulation vectors for SAT sweeping (SimGen)

[Carmine50]

Overview

The following pull request adds a new function in ABC. You can call this new function by using the command "&fraigSimGen." This algorithm relates to this work.

CLI arguments

The command &fraigSimGen has the following arguments:

• -E num sets the experiment ID. There are 5 possible experiment types: 1) reverse simulation, 2) simple implication, 3) advanced implication, 4) advanced implication + count DCs, 5) advanced implication + count DCs + FFC;
• -O num sets the bitwidth of the output gold which defines the number of LUTs whose output value is targeted by SimGen;
• -S num sets the bitwidth of the simulation vectors which defines the number of bits used during simulation;
• -t num sets the timeout value for SimGen;
• -i num sets the maximum number of iterations;
• -v toggles verbose outputs;
• -V toggles very verbose outputs.

Please look at the paper for more information related to the experiments' meanings.

General Code Structure

The file src/proof/cec/cecSatG2.c contains the main algorithm Cec_SimGenRun. The main function is divided in the following steps:

1. If the AIG is not LUT-mapped, apply LUT technology mapping. Then, extract the LUTs' SOPs.
2. Compute the MFFCs.
3. Execute a set of random simulations. The number of the simulations can be specified with the argument -i.
4. Remove non-LUT nodes from the equivalence classes.
5. Execute SimGen's main algorithm using the methodology specified by experiment ID. SimGen is run for multiple iterations until the timeout specified by the -t option is reached. The -O parameter specifies the number of parallel LUTs targeted during each run of SimGen.
6. Call the SAT solver on the remaining nodes in the equivalence classes.
7. Evaluate results achieved.

For all simulations, the bitwidth used is specified by the option -S.

Main Algo Structure

The core function of SimGen is executeControlledSim. This function is divided into the following steps:

1. Generate output gold values.
2. Select an equivalence class.
3. Compute the fanin cones of the selected LUTs.
4. Compute the input vectors for which these LUTs achieve the selected output gold values.
5. If there are still equivalence classes and the timeout has not been reached yet, go to step 2.
6. If the previous condition is not respected, terminate the execution of the core function.