luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #497 from fxreichl/master 

Extend the eSLIM package
This commit is contained in:
alanminko 2026-04-14 10:01:59 -07:00 committed by GitHub
parent 8aa7e12dab 0f6ca59029
commit 2db6ae7848
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
32 changed files with 5738 additions and 2415 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

54
abclib.dsp
View File

@ -4194,6 +4194,26 @@ SOURCE=.\src\opt\sbd\sbdWin.c
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\opt\eslim\areaEngine.cpp
# End Source File
# Begin Source File
SOURCE=.\src\opt\eslim\areaEngine.hpp
# End Source File
# Begin Source File
SOURCE=.\src\opt\eslim\cadicalSolver.hpp
# End Source File
# Begin Source File
SOURCE=.\src\opt\eslim\delayEngine.cpp
# End Source File
# Begin Source File
SOURCE=.\src\opt\eslim\delayEngine.hpp
# End Source File
# Begin Source File
SOURCE=.\src\opt\eslim\eSLIM.cpp
# End Source File
# Begin Source File
@ -4202,6 +4222,14 @@ SOURCE=.\src\opt\eslim\eSLIM.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\eslim\eslimCirMan.cpp
# End Source File
# Begin Source File
SOURCE=.\src\opt\eslim\eslimCirMan.hpp
# End Source File
# Begin Source File
SOURCE=.\src\opt\eslim\eSLIMMan.hpp
# End Source File
# Begin Source File
@ -4214,11 +4242,31 @@ SOURCE=.\src\opt\eslim\relationGeneration.hpp
# End Source File
# Begin Source File
SOURCE=.\src\opt\eslim\satInterfaces.hpp
SOURCE=.\src\opt\eslim\relationSynthesiser.cpp
# End Source File
# Begin Source File
SOURCE=.\src\opt\eslim\selectionStrategy.hpp
SOURCE=.\src\opt\eslim\relationSynthesiser.hpp
# End Source File
# Begin Source File
SOURCE=.\src\opt\eslim\selectionStrategies.hpp
# End Source File
# Begin Source File
SOURCE=.\src\opt\eslim\subcircuit.cpp
# End Source File
# Begin Source File
SOURCE=.\src\opt\eslim\subcircuit.hpp
# End Source File
# Begin Source File
SOURCE=.\src\opt\eslim\synthesisEngines.hpp
# End Source File
# Begin Source File
SOURCE=.\src\opt\eslim\tabooList.hpp
# End Source File
# Begin Source File
@ -4226,7 +4274,7 @@ SOURCE=.\src\opt\eslim\utils.hpp
# End Source File
# Begin Source File
SOURCE=.\src\opt\eslim\synthesisEngine.hpp
SOURCE=.\src\opt\eslim\windowMan.hpp
# End Source File
# End Group
# End Group

349
src/base/abci/abc.c
View File

@ -665,6 +665,7 @@ static int Abc_CommandAbc9Divide ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9eSLIM ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9elSLIM ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9CatBtor ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1517,6 +1518,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&eslim", Abc_CommandAbc9eSLIM, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "elslim", Abc_CommandAbc9elSLIM, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&catbtor", Abc_CommandAbc9CatBtor, 0 );
{
@ -59976,18 +59978,43 @@ int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
int c;
Gia_Man_t * pTemp;
seteSLIMParams(&params);
params.aig = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "DIMPRSTVZdfhns" ) ) != EOF ) {
while ( ( c = Extra_UtilGetopt( argc, argv, "CDIPRSTVWXZcfhistx" ) ) != EOF ) {
switch ( c ) {
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
params.approximate_relation = 1;
params.relation_tfo_bound = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( params.relation_tfo_bound < 0 )
goto usage;
if (globalUtilOptind < argc) {
char *next;
int tfi_bound = strtol (argv[globalUtilOptind], &next, 10);
if (argv[globalUtilOptind] != next && *next == '\0') {
params.generate_relation_with_tfi_limit = 1;
params.relation_tfi_bound = tfi_bound;
globalUtilOptind++;
if (params.relation_tfi_bound < 0) {
goto usage;
}
}
}
break;
case 'D':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
params.timeout_inprocessing = atoi(argv[globalUtilOptind]);
params.synthesis_approach = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( params.timeout_inprocessing < 1 )
if ( params.synthesis_approach < 0 || params.synthesis_approach > 2)
goto usage;
break;
case 'I':
@ -60001,17 +60028,6 @@ int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
if ( params.iterations < 0 )
goto usage;
break;
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
params.mode = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( params.mode < 0 || params.mode > 2)
goto usage;
break;
case 'P':
if ( globalUtilOptind >= argc )
{
@ -60040,9 +60056,9 @@ int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
params.subcircuit_size_bound = atoi(argv[globalUtilOptind]);
params.subcircuit_max_size = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( params.subcircuit_size_bound < 2 )
if ( params.subcircuit_max_size < 2 )
goto usage;
break;
case 'T':
@ -60067,6 +60083,32 @@ int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
if ( params.verbosity_level < 0 || params.verbosity_level > 3 )
goto usage;
break;
case 'W':
if ( globalUtilOptind >= argc + 1)
{
Abc_Print( -1, "Command line switch \"-W\" should be followed by two integers.\n" );
goto usage;
}
params.nWindows = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if (params.nWindows < 0)
goto usage;
params.window_size = atoi(argv[globalUtilOptind]);
if (params.window_size <= 0)
goto usage;
globalUtilOptind++;
break;
case 'X':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
goto usage;
}
params.additional_gates = atoi(argv[globalUtilOptind]);
if ( params.additional_gates < 0 )
goto usage;
globalUtilOptind++;
break;
case 'Z':
if ( globalUtilOptind >= argc )
{
@ -60077,24 +60119,34 @@ int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
params.seed = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'd' :
params.apply_inprocessing ^= 1;
case 'c' :
params.criticial_path_selection_bias ^= 1;
break;
case 'f' :
params.forbidden_pairs ^= 1;
params.forward_search ^= 1;
break;
case 'h':
goto usage;
case 'n' :
params.extended_normality_processing ^= 1;
case 'i' :
params.apply_inprocessing ^= 1;
break;
case 's' :
params.fill_subcircuits ^= 1;
break;
case 't' :
params.use_taboo_list ^= 1;
break;
case 'x' :
params.aig = 0;
break;
default:
goto usage;
}
}
if (params.nWindows > 0 && params.synthesis_approach != 0) {
Abc_Print( -1, "Windows can only be used with area minimization\n" );
return 1;
}
if ( pAbc->pGia == NULL ) {
Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" );
return 1;
@ -60105,26 +60157,265 @@ int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &eslim [-DIMPRSTVZ <num>] [-dfhns]\n" );
Abc_Print( -2, "\t circuit minimization using exact synthesis and the SAT-based local improvement method (SLIM)\n" );
Abc_Print( -2, "\t-D <num> : the timeout in seconds for the individual deepsyn runs [default = %d]\n", params.timeout_inprocessing );
Abc_Print( -2, "usage: &eslim [-CDIPRSTVWXZ <num>] [-cfhistx]\n" );
Abc_Print( -2, "\t circuit optimization using exact synthesis and the SAT-based local improvement method (SLIM)\n" );
Abc_Print( -2, "\t-C <num> : approximate Boolean relations by only considering the frist C levels in the cone \n");
Abc_Print( -2, "\t-D <num> : the delay mode to use [default = %d]\n", params.synthesis_approach );
Abc_Print( -2, "\t-I <num> : the maximal number of iterations (0 = no limit) for the individual eSLIM runs [default = %d]\n", params.iterations );
Abc_Print( -2, "\t-M <num> : the synthesis mode to use [default = %d]\n", params.mode );
Abc_Print( -2, "\t-P <num> : the probability of expanding a node [default = %.2f]\n", params.expansion_probability );
Abc_Print( -2, "\t-R <num> : the number of runs of eSLIM + Inprocessing [default = %d]\n", params.nruns );
Abc_Print( -2, "\t-S <num> : the maximal size of considered subcircuits [default = %d]\n", params.subcircuit_size_bound );
Abc_Print( -2, "\t-S <num> : the maximal size of considered subcircuits [default = %d]\n", params.subcircuit_max_size );
Abc_Print( -2, "\t-T <num> : the timeout in seconds for the individual eSLIM runs [default = %d]\n", params.timeout );
Abc_Print( -2, "\t-V <num> : the verbosity level [default = %d]\n", params.verbosity_level);
Abc_Print( -2, "\t-W <num> <num> : Use m windows of size n [default = %d, %d]\n", params.nWindows, params.window_size);
Abc_Print( -2, "\t-X <num> : the maximal number of additional gates that may be used for depth optimization [default = %d]\n", params.additional_gates);
Abc_Print( -2, "\t-Z <num> : use a fixed seed\n", params.seed);
Abc_Print( -2, "\t-d : toggle inprocessing with deepsyn\n");
Abc_Print( -2, "\t-f : toggle using subcircuits with forbidden pairs\n");
Abc_Print( -2, "\t-c : toggle bias for selection of nodes on the crictical path\n");
Abc_Print( -2, "\t-f : toggle forward expansion of root nodes\n");
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t-n : toggle extended normality processing\n");
Abc_Print( -2, "\t-i : toggle inprocessing\n");
Abc_Print( -2, "\t-s : toggle fill subcircuits\n");
Abc_Print( -2, "\t-t : toggle use taboo list\n");
Abc_Print( -2, "\t-x : allow xor-gates\n");
Abc_Print( -2, "\t\n" );
Abc_Print( -2, "\t This command was contributed by Franz-Xaver Reichl from University of Freiburg.\n" );
return 1;
}
int Abc_CommandAbc9elSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
extern void seteSLIMParams(eSLIM_ParamStruct* params);
extern Abc_Ntk_t* applyelSLIM(Abc_Ntk_t * pGia, const eSLIM_ParamStruct* params);
eSLIM_ParamStruct params;
Abc_Ntk_t* pNtk, *pNtknew;
int c;
seteSLIMParams(&params);
Extra_UtilGetoptReset();
params.subcircuit_max_size = 4;
while ( ( c = Extra_UtilGetopt( argc, argv, "CDGIPRSTVWXZfhist" ) ) != EOF ) {
switch ( c ) {
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
params.approximate_relation = 1;
params.relation_tfo_bound = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( params.relation_tfo_bound < 0 )
goto usage;
if (globalUtilOptind < argc) {
char *next;
int tfi_bound = strtol (argv[globalUtilOptind], &next, 10);
if (argv[globalUtilOptind] != next && *next == '\0') {
params.generate_relation_with_tfi_limit = 1;
params.relation_tfi_bound = tfi_bound;
globalUtilOptind++;
if (params.relation_tfi_bound < 0) {
goto usage;
}
}
}
break;
case 'D':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
params.synthesis_approach = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( params.synthesis_approach < 0 || params.synthesis_approach > 2)
goto usage;
break;
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
params.iterations = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( params.iterations < 0 )
goto usage;
break;
case 'G':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
goto usage;
}
params.gate_size = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( params.gate_size < 1 || params.gate_size > 6 )
goto usage;
break;
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by a float.\n" );
goto usage;
}
params.expansion_probability = atof(argv[globalUtilOptind]);
globalUtilOptind++;
if ( params.expansion_probability <= 0 || params.expansion_probability > 1)
goto usage;
break;
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
params.nruns = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( params.nruns < 1 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
params.subcircuit_max_size = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( params.subcircuit_max_size < 2 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
params.timeout = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( params.timeout < 1 )
goto usage;
break;
case 'V':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-V\" should be followed by an integer.\n" );
goto usage;
}
params.verbosity_level = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( params.verbosity_level < 0 || params.verbosity_level > 3 )
goto usage;
break;
case 'W':
if ( globalUtilOptind >= argc + 1)
{
Abc_Print( -1, "Command line switch \"-W\" should be followed by two integers.\n" );
goto usage;
}
params.nWindows = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if (params.nWindows < 0)
goto usage;
params.window_size = atoi(argv[globalUtilOptind]);
if (params.window_size <= 0)
goto usage;
globalUtilOptind++;
break;
case 'X':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
goto usage;
}
params.additional_gates = atoi(argv[globalUtilOptind]);
if ( params.additional_gates < 0 )
goto usage;
globalUtilOptind++;
break;
case 'Z':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-Z\" should be followed by an integer.\n" );
goto usage;
}
params.fix_seed = 1;
params.seed = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'c' :
params.criticial_path_selection_bias ^= 1;
break;
case 'f' :
params.forward_search ^= 1;
break;
case 'h':
goto usage;
case 'i' :
params.apply_inprocessing ^= 1;
break;
case 's' :
params.fill_subcircuits ^= 1;
break;
case 't' :
params.use_taboo_list ^= 1;
break;
default:
goto usage;
}
}
pNtk = Abc_FrameReadNtk(pAbc);
if ( pNtk == NULL )
{
Abc_Print( -1, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsLogic(pNtk) )
{
Abc_Print( -1, "This command can only be applied to a logic network.\n" );
return 1;
}
if (!Abc_NtkHasSop(pNtk)) {
Abc_NtkToSop( pNtk, -1, ABC_INFINITY );
}
params.aig = 0;
pNtknew = applyelSLIM(pNtk, &params);
Abc_FrameReplaceCurrentNetwork( pAbc, pNtknew );
return 0;
usage:
Abc_Print( -2, "usage: elslim [-CDGIPRSTVWXZ <num>] [-cfhist]\n" );
Abc_Print( -2, "\t Lut optimization using exact synthesis and the SAT-based local improvement method (SLIM)\n" );
Abc_Print( -2, "\t-C <num> : approximate Boolean relations by only considering the frist C levels in the cone \n");
Abc_Print( -2, "\t-D <num> : the delay mode to use [default = %d]\n", params.synthesis_approach );
Abc_Print( -2, "\t-G <num> : the maximal number of fanins gates may use (at most 6) [default = %d]\n", params.gate_size );
Abc_Print( -2, "\t-I <num> : the maximal number of iterations (0 = no limit) for the individual eSLIM runs [default = %d]\n", params.iterations );
Abc_Print( -2, "\t-P <num> : the probability of expanding a node [default = %.2f]\n", params.expansion_probability );
Abc_Print( -2, "\t-R <num> : the number of runs of eSLIM + Inprocessing [default = %d]\n", params.nruns );
Abc_Print( -2, "\t-S <num> : the maximal size of considered subcircuits [default = %d]\n", params.subcircuit_max_size );
Abc_Print( -2, "\t-T <num> : the timeout in seconds for the individual eSLIM runs [default = %d]\n", params.timeout );
Abc_Print( -2, "\t-V <num> : the verbosity level [default = %d]\n", params.verbosity_level);
Abc_Print( -2, "\t-W <num> <num> : Use m windows of size n [default = %d, %d]\n", params.nWindows, params.window_size);
Abc_Print( -2, "\t-X <num> : the maximal number of additional gates that may be used for depth optimization [default = %d]\n", params.additional_gates);
Abc_Print( -2, "\t-Z <num> : use a fixed seed\n", params.seed);
Abc_Print( -2, "\t-c : toggle bias for selection of nodes on the crictical path\n");
Abc_Print( -2, "\t-f : toggle forward expansion of root nodes\n");
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t-i : toggle inprocessing\n");
Abc_Print( -2, "\t-s : toggle fill subcircuits\n");
Abc_Print( -2, "\t-t : toggle use taboo list\n");
Abc_Print( -2, "\t\n" );
Abc_Print( -2, "\t This command was contributed by Franz-Xaver Reichl from University of Freiburg.\n" );
return 1;
}
int Abc_CommandAbc9CatBtor( Abc_Frame_t * pAbc, int argc, char ** argv ) {

163
src/opt/eslim/areaEngine.cpp Normal file
View File

@ -0,0 +1,163 @@
/**CFile****************************************************************
FileName [areaEngine.cpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Implementation of area based SAT encoding.]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#include "areaEngine.hpp"
ABC_NAMESPACE_IMPL_START
namespace eSLIM {
AreaEngine::AreaEngine(const Relation& relation, const Subcircuit& subcir, const eSLIMConfig& cfg, eSLIMLog& log)
: RelationSynthesiser(relation, subcir, subcir.nodes.size(), cfg, log) {
for (int i = 0; i < subcir.inputs.size(); i++) {
input_index_map[subcir.inputs[i]] = i;
}
for (int i = 0; i < subcir.outputs.size(); i++) {
output_index_map[subcir.outputs[i]] = i;
}
if (subcir.forbidden_pairs.size() > 0) {
setupCycleConstraints();
}
}
eSLIMCirMan AreaEngine::synthesiseMinimumSizeCircuit(const Relation& relation, const Subcircuit& subcir, const eSLIMConfig& cfg, eSLIMLog& log) {
AreaEngine synth(relation, subcir, cfg, log);
std::vector<bool> last_model;
int replacement_size = 0;
for (int i = synth.max_size; i>=0; i--) {
double timeout = synth.getDynamicTimeout(i);
int status = synth.checkSize(i, timeout);
if (status == 10) {
last_model = synth.solver.getModel();
i = synth.getSizeFromActivationVars(last_model);
replacement_size = i;
} else {
break;
}
}
if (last_model.empty()) {
// no replacement found
return eSLIMCirMan(0);
} else {
return synth.getReplacement(last_model, replacement_size);
}
}
int AreaEngine::checkSize(unsigned int size) {
return checkSize(size, 0);
}
int AreaEngine::checkSize(unsigned int size, double timeout) {
std::vector<int> assumptions = getSizeAssumption(size);
int status = timeout == 0 ? solver.solve(assumptions) : solver.solve(timeout, assumptions);
logRun(status, size);
return status;
}
void AreaEngine::setupCycleConstraints() {
assert (!subcir.forbidden_pairs.empty());
setupConnectionVariables();
if (subcir.forbidden_pairs.size() > 1) {
connectionVariablesForCombinedCycles();
}
addCycleConstraints();
}
void AreaEngine::addCycleConstraints() {
for (auto const& [outp, inputs] : subcir.forbidden_pairs) {
for (int inp : inputs) {
int output_idx = output_index_map.at(outp);
for (int i = 0; i < max_size; i++) {
solver.addClause({-gate_activation_variables[i], -gate_output_variables[i][output_idx], -connection_variables.at(inp)[i + subcir.inputs.size()]});
}
for (int i = 0; i < subcir.inputs.size(); i++) {
solver.addClause({-gate_output_variables[max_size + i][output_idx], -connection_variables.at(inp)[i]});
}
}
}
}
void AreaEngine::setupConnectionVariables() {
for (auto const& [out, inputs] : subcir.forbidden_pairs) {
for (int in : inputs) {
if (connection_variables.find(in) == connection_variables.end()) {
connection_variables[in] = getNewVariableVector(max_size + subcir.inputs.size());
}
}
}
for (const auto& [input_var, connection_vars] : connection_variables) {
int input_idx = input_index_map.at(input_var);
// An input is connected to itself
solver.addClause({connection_vars[input_idx]});
for (int i = 0; i < max_size; i++) {
int activation_variable = gate_activation_variables[i];
for (int j = 0; j < subcir.inputs.size(); j++) {
// if gate i uses input j and input j is connected to input_var then also gate i is connected to input_var
solver.addClause({-activation_variable, -selection_variables[i][j], -connection_vars[j], connection_vars[subcir.inputs.size() + i]});
}
for (int j = 0; j < i; j++) {
// if gate i uses gate j and gate j is connected to input_var then also gate i is connected to input_var
solver.addClause({-activation_variable, -selection_variables[i][subcir.inputs.size() + j], -connection_vars[subcir.inputs.size() + j], connection_vars[subcir.inputs.size() + i]});
}
}
}
}
void AreaEngine::connectionVariablesForCombinedCycles() {
assert (subcir.forbidden_pairs.size() > 1);
// Inputs are assigned to the outputs on which they depend
std::unordered_map<int, std::unordered_set<int>> inputs_per_output;
// Inputs in pairs
std::unordered_set<int> inputs_in_pairs;
for (auto const& [outp, inputs] : subcir.forbidden_pairs) {
for (int inp : inputs) {
if (inputs_per_output.find(outp) == inputs_per_output.end()) {
inputs_per_output[outp] = {inp};
} else {
inputs_per_output[outp].insert(inp);
}
inputs_in_pairs.insert(inp);
}
}
for (const auto& [ov, inp] : inputs_per_output) {
for (int iv : inputs_in_pairs) {
if (inp.find(iv) == inp.end()) {
for (int k : inputs_per_output.at(ov)) {
for (int i = 0; i < max_size; i++) {
// Input k depends on output ov.
// If gate i represents output ov and gate i is connected to iv then also gate k is connected to iv.
solver.addClause({-gate_activation_variables[i], -gate_output_variables[i][output_index_map.at(ov)],
-connection_variables.at(iv)[subcir.inputs.size() + i], connection_variables.at(iv)[input_index_map.at(k)]});
}
for (int i = 0; i < subcir.inputs.size(); i++) {
// Input k depends on output ov.
// If input i represents output ov and input i is connected to iv then gate k shall be connected to iv too.
solver.addClause({-gate_output_variables[max_size + i][output_index_map.at(ov)], -connection_variables.at(iv)[i], connection_variables.at(iv)[input_index_map.at(k)]});
}
}
}
}
}
}
}
ABC_NAMESPACE_IMPL_END

63
src/opt/eslim/areaEngine.hpp Normal file
View File

@ -0,0 +1,63 @@
/**CFile****************************************************************
FileName [areaEngine.hpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Implementation of area based SAT encoding.]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__OPT__ESLIM__AREAENGINE_hpp
#define ABC__OPT__ESLIM__AREAENGINE_hpp
#include "misc/util/abc_global.h"
#include "relationSynthesiser.hpp"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
class AreaEngine : private RelationSynthesiser {
public:
static eSLIMCirMan synthesiseMinimumSizeCircuit(const Relation& relation, const Subcircuit& subcir, const eSLIMConfig& cfg, eSLIMLog& log);
private:
std::unordered_map<int, std::vector<int>> connection_variables;
std::unordered_map<int,int> input_index_map;
std::unordered_map<int,int> output_index_map;
AreaEngine(const Relation& relation, const Subcircuit& subcir, const eSLIMConfig& cfg, eSLIMLog& log);
int checkSize(unsigned int size, double timeout);
int checkSize(unsigned int size);
void setupCycleConstraints();
void setupConnectionVariables();
// If we have multiple cyclic pairs, different pairs may form form a cycle together
// Assume we have two different pairs (x,y) and (a,b) in potential_cycles.
// It can be the case that x is connected to b and a is connected to y.
// To rule out cycles of this kind we make use of the following idea:
// If (x,y) is in self.potential_cycles then there is a path from x to y that is not part of the current subcircuit.
// Now if b is connected to x, this means that y is also connected to b.
// Thus, all gates that use y as an input are connected to b.
void connectionVariablesForCombinedCycles();
void addCycleConstraints();
};
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

218
src/opt/eslim/cadicalSolver.hpp Normal file
View File

@ -0,0 +1,218 @@
/**CFile****************************************************************
FileName [cadicalSolver.hpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Interface for Cadical SAT solver.]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__OPT__ESLIM__SATINTERFACE_h
#define ABC__OPT__ESLIM__SATINTERFACE_h
#include <vector>
#include <algorithm>
#include <chrono>
#include <iostream>
#include "sat/cadical/cadical.hpp"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
class CadicalSolver {
public:
~CadicalSolver();
void addClause(const std::vector<int>& clause);
void addClause(std::vector<int>&& clause);
void addCombinedClause(const std::vector<int>& cl1, const std::vector<int>& cl2, const std::vector<int>& cl3);
void assume(const std::vector<int>& assumptions);
int solve(double timeout, const std::vector<int>& assumptions);
int solve(const std::vector<int>& assumptions);
int solve(double timeout);
int solve();
std::vector<int> getFailed(const std::vector<int>& assumptions);
bool isFailed(int lit);
std::vector<int> getValues(const std::vector<int>& variables);
bool getValue(int var);
std::vector<bool> getModel();
double getRunTime() const;
private:
void assumeAll(const std::vector<int>& assumptions);
int val(int variable);
double last_runtime;
CaDiCaL::Solver solver;
public:
class TimeoutTerminator : public CaDiCaL::Terminator {
public:
TimeoutTerminator(double max_runtime);
bool terminate();
private:
double max_runtime; //in seconds
std::chrono::time_point<std::chrono::steady_clock> start = std::chrono::steady_clock::now();
};
};
inline CadicalSolver::TimeoutTerminator::TimeoutTerminator(double max_runtime) : max_runtime(max_runtime) {
}
inline bool CadicalSolver::TimeoutTerminator::terminate() {
auto current_time = std::chrono::steady_clock::now();
std::chrono::duration<double> elapsed_seconds = current_time - start;
return elapsed_seconds.count() > max_runtime;
}
inline CadicalSolver::~CadicalSolver()=default;
inline void CadicalSolver::addClause(const std::vector<int>& clause) {
for (auto& l: clause) {
solver.add(l);
}
solver.add(0);
}
inline void CadicalSolver::addClause(std::vector<int>&& clause) {
for (auto& l: clause) {
solver.add(l);
}
solver.add(0);
}
inline void CadicalSolver::addCombinedClause(const std::vector<int>& cl1, const std::vector<int>& cl2, const std::vector<int>& cl3) {
for (auto& l: cl1) {
solver.add(l);
}
for (auto& l: cl2) {
solver.add(l);
}
for (auto& l: cl3) {
solver.add(l);
}
solver.add(0);
}
inline void CadicalSolver::assume(const std::vector<int>& assumptions) {
for (auto& l: assumptions) {
solver.assume(l);
}
}
inline void CadicalSolver::assumeAll(const std::vector<int>& assumptions) {
solver.reset_assumptions();
assume(assumptions);
}
inline int CadicalSolver::solve(double timeout, const std::vector<int>& assumptions) {
assumeAll(assumptions);
std::chrono::time_point<std::chrono::steady_clock> start = std::chrono::steady_clock::now();
TimeoutTerminator terminator(timeout);
solver.connect_terminator(&terminator);
int status = solver.solve();
last_runtime = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::steady_clock::now() - start).count();
if (solver.state() == CaDiCaL::INVALID) {
std::cerr<<"Solver is in invalid state"<<std::endl;
return -1;
}
solver.disconnect_terminator();
return status;
}
inline int CadicalSolver::solve(const std::vector<int>& assumptions) {
assumeAll(assumptions);
std::chrono::time_point<std::chrono::steady_clock> start = std::chrono::steady_clock::now();
int status = solver.solve();
last_runtime = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::steady_clock::now() - start).count();
return status;
}
inline int CadicalSolver::solve(double timeout) {
std::chrono::time_point<std::chrono::steady_clock> start = std::chrono::steady_clock::now();
TimeoutTerminator terminator(timeout);
solver.connect_terminator(&terminator);
int status = solver.solve();
last_runtime = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::steady_clock::now() - start).count();
if (solver.state() == CaDiCaL::INVALID) {
std::cerr<<"Solver is in invalid state"<<std::endl;
return -1;
}
solver.disconnect_terminator();
return status;
}
inline int CadicalSolver::solve() {
std::chrono::time_point<std::chrono::steady_clock> start = std::chrono::steady_clock::now();
int status = solver.solve();
last_runtime = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::steady_clock::now() - start).count();
return status;
}
inline double CadicalSolver::getRunTime() const {
return last_runtime;
}
inline std::vector<int> CadicalSolver::getFailed(const std::vector<int>& assumptions) {
std::vector<int> failed_literals;
for (auto& l: assumptions) {
if (solver.failed(l)) {
failed_literals.push_back(l);
}
}
return failed_literals;
}
inline bool CadicalSolver::isFailed(int lit) {
return solver.failed(lit);
}
inline std::vector<int> CadicalSolver::getValues(const std::vector<int>& variables) {
std::vector<int> assignment;
for (auto& v: variables) {
assignment.push_back(val(v));
}
return assignment;
}
inline bool CadicalSolver::getValue(int var) {
return val(var) > 0;
}
inline std::vector<bool> CadicalSolver::getModel() {
std::vector<bool> assignment;
assignment.push_back(false);
for (int v = 1; v <= solver.vars(); v++) {
assignment.push_back(val(v) > 0);
}
return assignment;
}
inline int CadicalSolver::val(int variable) {
auto l = solver.val(variable);
auto v = abs(l);
if (v == variable) {
return l;
} else {
return variable;
}
}
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

252
src/opt/eslim/delayEngine.cpp Normal file
View File

@ -0,0 +1,252 @@
/**CFile****************************************************************
FileName [delayEngine.cpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Implementation of delay based SAT encoding.]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#include "delayEngine.hpp"
ABC_NAMESPACE_IMPL_START
namespace eSLIM {
DelayEngine::DelayEngine( const Relation& relation, const Subcircuit& subcir, unsigned int max_size, const eSLIMConfig& cfg, eSLIMLog& log)
: RelationSynthesiser(relation, subcir, max_size, cfg, log) {
assert (subcir.forbidden_pairs.empty());
symmetry_selector = getNewVariable();
symmetry_selector_assignment = symmetry_selector;
std::set<int> unique_ats_set (subcir.arrival_times.begin(), subcir.arrival_times.end());
unique_arrival_times = std::vector<int> (unique_ats_set.begin(), unique_ats_set.end());
for (int i : subcir.arrival_times) {
auto it = unique_ats_set.find(i);
int idx = std::distance(unique_ats_set.begin(), it);
inputid2uniqueid.push_back(idx);
}
setupVariables();
constrainDelayVariables();
setupDelayConstraints();
max_delay = delay_selectors.begin()->first;
}
// do not enfore activation variables -> a minimum nof gates might forbid a realization with a certain depth.
eSLIMCirMan DelayEngine::synthesizeMinimumDelayCircuit(const Relation& relation, const Subcircuit& subcir, unsigned int delay, unsigned int max_size, const eSLIMConfig& cfg, eSLIMLog& log) {
DelayEngine synth(relation, subcir, max_size, cfg, log);
std::vector<bool> last_model = synth.reduceDelay(max_size, delay);
if (last_model.empty()) {
// no replacement found
return eSLIMCirMan(0);
} else {
int replacement_size = synth.getSizeFromActivationVars(last_model);
return synth.getReplacement(last_model, replacement_size);
}
}
eSLIMCirMan DelayEngine::synthesizeMinimumDelayAreaCircuit(const Relation& relation, const Subcircuit& subcir, unsigned int delay, unsigned int max_size, const eSLIMConfig& cfg, eSLIMLog& log) {
DelayEngine synth(relation, subcir, max_size, cfg, log);
std::vector<bool> last_model = synth.reduceDelay(max_size, delay);
if (last_model.empty()) {
// We could not even find a replacement with the same delay as the original circuit (timeout)
// Hence, it is unlikely that we find a circuit that has the same delay but fewer gates
return eSLIMCirMan(0);
}
int replacement_size = synth.getSizeFromActivationVars(last_model);
int replacement_delay = synth.getDelayFromDelayVariables(last_model);
std::vector<bool> model = synth.reduceArea(replacement_delay, replacement_size - 1);
if (model.size() > 0) {
replacement_size = synth.getSizeFromActivationVars(model);
std::swap(last_model, model);
}
return synth.getReplacement(last_model, replacement_size);
}
eSLIMCirMan DelayEngine::synthesizeMinimumAreaDelayCircuit(const Relation& relation, const Subcircuit& subcir, const eSLIMConfig& cfg, eSLIMLog& log) {
DelayEngine synth(relation, subcir, subcir.nodes.size(), cfg, log);
std::vector<bool> last_model = synth.reduceArea(synth.max_delay, subcir.nodes.size());
if (last_model.empty()) {
// We could not even find a replacement with the same area as the original circuit (timeout)
// Hence, it is unlikely that we find a circuit that has the same area and a causes a smaller delay
return eSLIMCirMan(0);
}
int replacement_size = synth.getSizeFromActivationVars(last_model);
int replacement_delay = synth.getDelayFromDelayVariables(last_model);
assert (replacement_delay > 0);
std::vector<bool> model = synth.reduceDelay(replacement_size, replacement_delay - 1);
if (model.size() > 0) {
replacement_size = synth.getSizeFromActivationVars(model);
std::swap(last_model, model);
}
return synth.getReplacement(last_model, replacement_size);
}
eSLIMCirMan DelayEngine::synthesizeMinimumAreaDelayConstraintCircuit(const Relation& relation, const Subcircuit& subcir, unsigned int delay, const eSLIMConfig& cfg, eSLIMLog& log) {
DelayEngine synth(relation, subcir, subcir.nodes.size(), cfg, log);
std::vector<bool> last_model = synth.reduceArea(delay, subcir.nodes.size());
if (last_model.empty()) {
return eSLIMCirMan(0);
} else {
int replacement_size = synth.getSizeFromActivationVars(last_model);
return synth.getReplacement(last_model, replacement_size);
}
}
std::vector<bool> DelayEngine::reduceArea(unsigned int max_delay, unsigned int initial_area) {
std::vector<bool> last_model;
for (int i = initial_area; i>=0; i--) {
double timeout = getDynamicTimeout(i);
int status = existsReplacement(i, max_delay, timeout);
if (status == 10) {
last_model = solver.getModel();
i = getSizeFromActivationVars(last_model); // it is possible that more than one gate is reduced in an iteration
} else {
break;
}
}
return last_model;
}
std::vector<bool> DelayEngine::reduceDelay(unsigned int max_size, unsigned int initial_delay) {
assert (delay_selectors.find(initial_delay) != delay_selectors.end());
std::vector<bool> last_model;
for( auto it = delay_selectors.find(initial_delay); it != delay_selectors.end(); ++it ) {
int d = it->first;
double timeout = getDynamicTimeout(max_size);
int status = existsReplacement(max_size, d, timeout);
if (status == 10) {
last_model = solver.getModel();
} else {
break;
}
}
return last_model;
}
std::vector<int> DelayEngine::getAssumptions(unsigned int delay) {
std::vector<int> assumptions;
for (auto const& [d, ds] : delay_selectors) {
if (d > delay) {
assumptions.push_back(-ds);
}
}
return assumptions;
}
std::vector<int> DelayEngine::getAssumptions(unsigned int size, unsigned int delay) {
std::vector<int> assumptions = getAssumptions(delay);
std::vector<int> area_assumptions = getSizeAssumption(size);
assumptions.insert(assumptions.end(), area_assumptions.begin(), area_assumptions.end());
return assumptions;
}
unsigned int DelayEngine::getDelayFromDelayVariables(const std::vector<bool>& model) {
unsigned int delay = 0;
for (auto const& [d, dvars] : delays2delay_variables) {
for (int v : dvars) {
if (model[v]) {
return d;
}
}
}
return delay;
}
int DelayEngine::existsReplacement(unsigned int delay, double timeout) {
std::vector<int> assumptions = getAssumptions(delay);
int status = timeout == 0 ? solver.solve(assumptions) : solver.solve(timeout, assumptions);
unsigned int size = status == 10 ? getSizeFromActivationVars() : max_size;
logRun(status, size);
return status;
}
int DelayEngine::existsReplacement(unsigned int size, unsigned int delay, double timeout) {
std::vector<int> assumptions = getAssumptions(size, delay);
int status = timeout == 0 ? solver.solve(assumptions) : solver.solve(timeout, assumptions);
logRun(status, size);
return status;
}
void DelayEngine::setupVariables() {
for (int i = 0; i < max_size; i++) {
std::vector<std::vector<int>> dvars;
for (int j = 0; j < unique_arrival_times.size(); j++) {
dvars.push_back(getNewVariableVector(i + 1));
}
delay_variables.push_back(dvars);
}
for (int i = 0; i < subcir.outputs.size(); i++) {
std::vector<std::vector<int>> dvars;
for (int j = 0; j < unique_arrival_times.size(); j++) {
dvars.push_back(getNewVariableVector(max_size + 1));
}
output_delays.push_back(dvars);
}
}
int DelayEngine::getDelaySelector(int delay) {
if (delay_selectors.find(delay) == delay_selectors.end()) {
delay_selectors[delay] = getNewVariable();
}
return delay_selectors[delay];
}
void DelayEngine::constrainDelayVariables() {
for (int i = 0; i < max_size; i++) {
int activation_variable = gate_activation_variables[i];
for (int j = 0; j < subcir.inputs.size(); j++) {
solver.addClause({-activation_variable, -selection_variables[i][j], delay_variables[i][inputid2uniqueid[j]][0]});
}
for (int j = 0; j < unique_arrival_times.size(); j++) {
for (int k = 0; k < i; k++) {
int node_id = subcir.inputs.size() + k;
for (int l = 0; l <= k; l++) {
solver.addClause({-activation_variable, -selection_variables[i][node_id], -delay_variables[k][j][l], delay_variables[i][j][l+1]});
}
solver.addClause({-activation_variable, -delay_variables[i][j][k+1], delay_variables[i][j][k]});
}
}
}
for (int i = 0; i < subcir.outputs.size(); i++) {
for (int j = 0; j < subcir.inputs.size(); j++) {
solver.addClause({-gate_output_variables[max_size + j][i], output_delays[i][inputid2uniqueid[j]][0]});
}
for (int j = 0; j < unique_arrival_times.size(); j++) {
for (int k = 0; k < max_size; k++) {
solver.addClause({-output_delays[i][j][k+1], output_delays[i][j][k]});
for (int l = 0; l <= k; l++) {
solver.addClause({-gate_output_variables[k][i], -delay_variables[k][j][l], output_delays[i][j][l+1]});
}
}
}
}
}
void DelayEngine::setupDelayConstraints() {
for (int i = 0; i < unique_arrival_times.size(); i++) {
for (int o = 0; o < subcir.outputs.size(); o++) {
for (int d = 0; d <= max_size; d++) {
int delay = unique_arrival_times[i] + subcir.remaining_times[o] + d;
int ds = getDelaySelector(delay);
solver.addClause({ds, -output_delays[o][i][d]});
delays2delay_variables[delay].push_back(output_delays[o][i][d]);
}
}
}
}
}
ABC_NAMESPACE_IMPL_END

81
src/opt/eslim/delayEngine.hpp Normal file
View File

@ -0,0 +1,81 @@
/**CFile****************************************************************
FileName [delayEngine.hpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Implementation of delay based SAT encoding.]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__OPT__ESLIM__DELAYENGINE_hpp
#define ABC__OPT__ESLIM__DELAYENGINE_hpp
#include <map>
#include "misc/util/abc_global.h"
#include "relationSynthesiser.hpp"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
class DelayEngine : public RelationSynthesiser {
public:
// Find a replacement with at most max_size gates that yields minimum delay
static eSLIMCirMan synthesizeMinimumDelayCircuit(const Relation& relation, const Subcircuit& subcir, unsigned int delay, unsigned int max_size, const eSLIMConfig& cfg, eSLIMLog& log);
// Find a replacement with at most max_size gates that yields minimum delay. Among these circuits find one of minimum size
static eSLIMCirMan synthesizeMinimumDelayAreaCircuit(const Relation& relation, const Subcircuit& subcir, unsigned int delay, unsigned int max_size, const eSLIMConfig& cfg, eSLIMLog& log);
// First minimize area, then minimize delay
static eSLIMCirMan synthesizeMinimumAreaDelayCircuit(const Relation& relation, const Subcircuit& subcir, const eSLIMConfig& cfg, eSLIMLog& log);
// Find a smaller replacement that must not increase delay
static eSLIMCirMan synthesizeMinimumAreaDelayConstraintCircuit(const Relation& relation, const Subcircuit& subcir, unsigned int delay, const eSLIMConfig& cfg, eSLIMLog& log);
private:
std::vector<int> unique_arrival_times;
std::vector<int> inputid2uniqueid;
unsigned int max_delay;
int symmetry_selector;
int symmetry_selector_assignment;
// Indicate the length of the longest paths from inputs to gates
std::vector<std::vector<std::vector<int>>> delay_variables;
std::vector<std::vector<std::vector<int>>> output_delays;
std::map<int, int, std::greater<int>> delay_selectors;
std::map<int, std::vector<int>, std::greater<int>> delays2delay_variables;
DelayEngine(const Relation& relation, const Subcircuit& subcir, unsigned int max_size, const eSLIMConfig& cfg, eSLIMLog& log);
int existsReplacement(unsigned int size, unsigned int delay, double timeout);
int existsReplacement(unsigned int delay, double timeout);
std::vector<int> getAssumptions(unsigned int delay);
std::vector<int> getAssumptions(unsigned int size, unsigned int delay);
void setupVariables();
unsigned int getDelayFromDelayVariables(const std::vector<bool>& model);
std::vector<bool> reduceArea(unsigned int max_delay, unsigned int initial_area);
std::vector<bool> reduceDelay(unsigned int max_size, unsigned int initial_delay);
int getDelaySelector(int delay);
void setupDelayConstraints();
void constrainDelayVariables();
};
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

697
src/opt/eslim/eSLIM.cpp
View File

@ -12,204 +12,611 @@
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - March 2025.]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/03/17 00:00:00 Exp $]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#include "utils.hpp"
#include "eSLIMMan.hpp"
#include "relationGeneration.hpp"
#include "selectionStrategy.hpp"
#include "selectionStrategies.hpp"
#include "windowMan.hpp"
#include "misc/util/abc_namespaces.h"
#include "opt/mfs/mfs.h"
#include "base/main/main.h"
#include "eSLIM.h"
#include "eslimCirMan.hpp"
#include "synthesisEngines.hpp"
#include "selectionStrategies.hpp"
ABC_NAMESPACE_HEADER_START
Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fChoices, int fVerbose );
int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars );
ABC_NAMESPACE_HEADER_END
ABC_NAMESPACE_IMPL_START
eSLIM::eSLIMConfig getCfg(const eSLIM_ParamStruct* params) {
eSLIM::eSLIMConfig config;
config.extended_normality_processing = params->extended_normality_processing;
config.apply_strash = params->apply_strash;
config.fill_subcircuits = params->fill_subcircuits;
config.fix_seed = params->fix_seed;
config.trial_limit_active = params->trial_limit_active;
config.timeout = params->timeout;
config.iterations = params->iterations;
config.subcircuit_size_bound = params->subcircuit_size_bound;
config.subcircuit_max_size = params->subcircuit_max_size;
config.additional_gates = params->additional_gates;
config.strash_intervall = params->strash_intervall;
config.nselection_trials = params->nselection_trials;
config.seed = params->seed;
config.verbosity_level = params->verbosity_level;
config.expansion_probability = params->expansion_probability;
config.approximate_relation = params->approximate_relation;
config.relation_tfo_bound = params->relation_tfo_bound;
config.generate_relation_with_tfi_limit = params->generate_relation_with_tfi_limit;
config.relation_tfi_bound = params->relation_tfi_bound;
config.nwindows = params->nWindows;
config.window_size = params->window_size;
config.aig = params->aig;
config.gate_size = params->gate_size;
if (params->use_taboo_list) {
config.apply_strash = false;
}
return config;
}
void seteSLIMParams(eSLIM_ParamStruct* params) {
params->forbidden_pairs = 1;
params->extended_normality_processing = 0;
params->fill_subcircuits = 0;
params->apply_strash = 1;
params->fix_seed = 0;
params->trial_limit_active = 1;
params->apply_inprocessing = 1;
params->timeout = 1620;
params->timeout_inprocessing = 180;
params->synthesis_approach = 0;
params->seed = 0;
params->verbosity_level = 1;
params->use_taboo_list = 0;
params->forward_search = 0;
params->nWindows = 0;
params->window_size = 500;
params->criticial_path_selection_bias = 0;
params->timeout = 1800;
params->iterations = 0;
params->subcircuit_size_bound = 6;
params->subcircuit_max_size = 6;
params->additional_gates = 0;
params->strash_intervall = 100;
params->nselection_trials = 100;
params->nruns = 1;
params->mode = 0;
params->seed = 0;
params->verbosity_level = 1;
params->expansion_probability = 0.4;
}
Gia_Man_t* selectApproach(Gia_Man_t* pGia, eSLIM::eSLIMConfig params, eSLIM::eSLIMLog& log, int approach, bool allow_forbidden_pairs) {
switch (approach) {
case 0 :
if (allow_forbidden_pairs) {
return eSLIM::eSLIM_Man<eSLIM::CadicalEngine, eSLIM::RelationGeneratorABC, eSLIM::randomizedBFSFP>::applyeSLIM(pGia, params, log);
} else {
return eSLIM::eSLIM_Man<eSLIM::CadicalEngine, eSLIM::RelationGeneratorABC, eSLIM::randomizedBFSnoFP>::applyeSLIM(pGia, params, log);
};
case 1:
if (allow_forbidden_pairs) {
return eSLIM::eSLIM_Man<eSLIM::KissatOneShot, eSLIM::RelationGeneratorABC, eSLIM::randomizedBFSFP>::applyeSLIM(pGia, params, log);
} else {
return eSLIM::eSLIM_Man<eSLIM::KissatOneShot, eSLIM::RelationGeneratorABC, eSLIM::randomizedBFSnoFP>::applyeSLIM(pGia, params, log);
};
case 2:
if (allow_forbidden_pairs) {
return eSLIM::eSLIM_Man<eSLIM::KissatCmdOneShot, eSLIM::RelationGeneratorABC, eSLIM::randomizedBFSFP>::applyeSLIM(pGia, params, log);
} else {
return eSLIM::eSLIM_Man<eSLIM::KissatCmdOneShot, eSLIM::RelationGeneratorABC, eSLIM::randomizedBFSnoFP>::applyeSLIM(pGia, params, log);
};
default:
std::cerr << "eSLIM -- Invalid mode given\n";
assert (false && "Invalid approach selected");
return nullptr;
}
params->expansion_probability = 0.5;
params->approximate_relation = 0;
params->relation_tfo_bound = 0;
params->generate_relation_with_tfi_limit = 0;
params->relation_tfi_bound = 0;
params->aig = 1;
params->gate_size = 2;
}
Gia_Man_t* runInprocessing(Gia_Man_t * pGia, const eSLIM_ParamStruct* params, unsigned int it) {
Gia_Man_t * tmp = Gia_ManDeepSyn( pGia, 1, ABC_INFINITY, params->timeout_inprocessing, 0, params->seed + it, 0, 0, 0);
if ( Gia_ManAndNum(pGia) > Gia_ManAndNum(tmp) ) {
Gia_ManStop( pGia );
pGia = tmp;
} else {
namespace eSLIM {
class DeepsynInprocessor {
public:
DeepsynInprocessor(eSLIMConfig& config);
void setTimeout(int timeout) {this->timeout = timeout;}
void runInprocessing(eSLIMCirMan& es_man);
private:
eSLIMConfig& config;
int timeout;
};
class MfsInprocessor {
public:
MfsInprocessor(eSLIMConfig& config) {}
void runInprocessing(eSLIMCirMan& es_man);
};
class EmptyInprocessor {
public:
EmptyInprocessor(eSLIMConfig& config) {}
void runInprocessing(eSLIMCirMan& es_man) {}
};
template <bool IncreaseSize>
class DelayInprocessor {
public:
DelayInprocessor(eSLIMConfig& config);
void setTimeout(int timeout) {this->timeout = timeout;}
void runInprocessing(eSLIMCirMan& es_man);
private:
eSLIMConfig& config;
int timeout;
};
class Resyn2Inprocessor {
public:
Resyn2Inprocessor(eSLIMConfig& config);
void runInprocessing(eSLIMCirMan& es_man);
private:
// eSLIMConfig& config;
};
template <typename Approach, typename Inprocessor>
class eSLIMRun {
public:
static Gia_Man_t* runeSLIM(Gia_Man_t* cir, const eSLIM_ParamStruct* params);
static Abc_Ntk_t * runeSLIM(Abc_Ntk_t * cir, const eSLIM_ParamStruct* params);
static Abc_Ntk_t * runeSLIMCells(Abc_Ntk_t * cir, const eSLIM_ParamStruct* params);
private:
eSLIMCirMan es_man;
eSLIMConfig config;
eSLIMLog log;
Inprocessor inprocessor;
int initial_area;
int initial_delay;
int area_change_eslim = 0;
int area_change_inprocessing = 0;
int delay_change_eslim = 0;
int delay_change_inprocessing = 0;
int nruns = 0;
eSLIMRun(Gia_Man_t* cir, const eSLIM_ParamStruct* params);
eSLIMRun(Abc_Ntk_t* cir, const eSLIM_ParamStruct* params, bool simplify);
void setUpInprocessor();
void runInprocessing();
void printSettings();
void printLog();
void run();
};
template <typename Approach, typename Inprocessor>
eSLIMRun<Approach, Inprocessor>::eSLIMRun(Abc_Ntk_t* cir, const eSLIM_ParamStruct* params, bool simplify_circuit)
: es_man(cir, simplify_circuit), config(getCfg(params)), log(params->subcircuit_max_size), inprocessor(config) {
nruns = params->nruns;
config.aig = false;
config.apply_strash = false;
}
template <typename Approach, typename Inprocessor>
eSLIMRun<Approach, Inprocessor>::eSLIMRun(Gia_Man_t* cir, const eSLIM_ParamStruct* params)
: es_man(cir), config(getCfg(params)), log(params->subcircuit_max_size), inprocessor(config) {
nruns = params->nruns;
}
template <typename Approach, typename Inprocessor>
Gia_Man_t* eSLIMRun<Approach, Inprocessor>::runeSLIM(Gia_Man_t* cir, const eSLIM_ParamStruct* params) {
eSLIMRun<Approach, Inprocessor> eslim_run(cir, params);
// It seems like the variables are freed by abc during preprocessing. Thus,we copy them
char* name = Abc_UtilStrsav( cir->pName );
char* spec = Abc_UtilStrsav( cir->pSpec );
eslim_run.run();
Gia_Man_t* gia_res = eslim_run.es_man.eSLIMCirManToGia();
gia_res->pName = name;
gia_res->pSpec = spec;
return gia_res;
}
template <typename Approach, typename Inprocessor>
Abc_Ntk_t* eSLIMRun<Approach, Inprocessor>::runeSLIM(Abc_Ntk_t* cir, const eSLIM_ParamStruct* params) {
bool simplify_circuit = true;
eSLIMRun<Approach, Inprocessor> eslim_run(cir, params, simplify_circuit);
eslim_run.config.aig = false;
eslim_run.config.apply_strash = false;
eslim_run.run();
Abc_Ntk_t* ntk_res = eslim_run.es_man.eSLIMCirManToNtk();
ntk_res->pName = Extra_UtilStrsav(cir->pName);
ntk_res->pSpec = Extra_UtilStrsav(cir->pSpec);
return ntk_res;
}
template <typename Approach, typename Inprocessor>
Abc_Ntk_t * eSLIMRun<Approach, Inprocessor>::runeSLIMCells(Abc_Ntk_t * cir, const eSLIM_ParamStruct* params) {
bool simplify_circuit = false;
eSLIMRun<Approach, Inprocessor> eslim_run(cir, params, simplify_circuit);
eslim_run.config.aig = false;
eslim_run.config.apply_strash = false;
eslim_run.run();
Abc_Ntk_t* ntk_res = eslim_run.es_man.eSLIMCirManToMappedNtk();
if (!ntk_res) {
return ntk_res;
}
ntk_res->pName = Extra_UtilStrsav(cir->pName);
ntk_res->pSpec = Extra_UtilStrsav(cir->pSpec);
return ntk_res;
}
template <typename Approach, typename Inprocessor>
void eSLIMRun<Approach, Inprocessor>::run() {
if constexpr ( std::is_same_v<DeepsynInprocessor, Inprocessor> || std::is_same_v<DelayInprocessor<true>, Inprocessor> || std::is_same_v<DelayInprocessor<false>, Inprocessor> ) {
int time_out_inprocessing;
if constexpr ( std::is_same_v<DeepsynInprocessor, Inprocessor> ) {
time_out_inprocessing = config.timeout * 0.1;
} else {
time_out_inprocessing = config.timeout * 0.02;
}
config.timeout -= time_out_inprocessing;
inprocessor.setTimeout(time_out_inprocessing);
}
initial_area = es_man.getNofGates();
initial_delay = es_man.getDepth();
printSettings();
for (int i = 0; i < nruns; i++) {
int size_iteration_start = es_man.getNofGates();
int delay_iteration_start = es_man.getDepth();
if (config.verbosity_level > 0) {
std::cout << "Start eslim run " << i + 1 << "\n";
}
Approach::applyeSLIM(es_man, config, log);
int size_eslim = es_man.getNofGates();
int delay_eslim = es_man.getDepth();
area_change_eslim += size_eslim - size_iteration_start;
delay_change_eslim += delay_eslim - delay_iteration_start;
if (config.verbosity_level > 0) {
std::cout << "eslim -- size: " << size_eslim << " delay: " << delay_eslim << "\n";
}
runInprocessing();
if constexpr ( !std::is_same_v<EmptyInprocessor, Inprocessor> ) {
int size_inprocessing = es_man.getNofGates();
int delay_inprocessing = es_man.getDepth();
area_change_inprocessing += size_inprocessing - size_eslim;
delay_change_inprocessing += delay_inprocessing - delay_eslim;
if (config.verbosity_level > 0) {
std::cout << "inprocessing -- size: " << size_inprocessing << " delay: " << delay_inprocessing << "\n";
}
}
if (config.fix_seed) {
config.seed++;
}
}
printLog();
}
template <typename Approach, typename Inprocessor>
void eSLIMRun<Approach, Inprocessor>::printSettings() {
std::cout << "Apply eSLIM (timeout: " << config.timeout << ") ";
std::cout << nruns << " times.\n";
if constexpr ( !std::is_same_v<EmptyInprocessor, Inprocessor> ) {
std::cout << "Apply inprocessing\n";
}
if (config.iterations > 0) {
std::cout << "Stop eSLIM runs after " << config.iterations << " iterations.\n";
}
std::cout << "Consider subcircuits with up to " << config.subcircuit_max_size << " gates.\n";
printf("When expanding subcircuits, select gates with a probability of %.2f %%.\n", 100 * config.expansion_probability);
}
template <typename Approach, typename Inprocessor>
void eSLIMRun<Approach, Inprocessor>::printLog() {
if (config.verbosity_level > 0) {
int size = es_man.getNofGates();
int delay = es_man.getDepth();
int total_area_change = area_change_eslim + area_change_inprocessing;
int total_delay_change = delay_change_eslim + delay_change_inprocessing;
std::cout << "Final size: " << size << " change: " << total_area_change << "\n";
std::cout << "Final depth: " << delay << " change: " << total_delay_change << "\n";
if constexpr ( !std::is_same_v<EmptyInprocessor, Inprocessor> ) {
if (area_change_eslim <= 0) {
std::cout << "#Gates reduced by eSLIM: " << -area_change_eslim << "\n";
} else {
std::cout << "#Gates introduced by eSLIM: " << area_change_eslim << "\n";
}
if (area_change_inprocessing <= 0) {
std::cout << "#Gates reduced by inprocessing: " << -area_change_inprocessing << "\n";
} else {
std::cout << "#Gates introduced by inprocessing: " << area_change_inprocessing << "\n";
}
if (delay_change_eslim <= 0) {
std::cout << "Delay reduction eSLIM: " << -delay_change_eslim << "\n";
} else {
std::cout << "Delay increase eSLIM: " << delay_change_eslim << "\n";
}
if (delay_change_inprocessing <= 0) {
std::cout << "Delay reduction inprocessing: " << -delay_change_inprocessing << "\n";
} else {
std::cout << "Delay increase inprocessing: " << delay_change_inprocessing << "\n";
}
}
}
if (config.verbosity_level > 1) {
std::cout << "Total #iterations: " << log.iteration_count << "\n";
std::cout << "Total relation generation time (s): " << log.relation_generation_time << "\n";
std::cout << "Total synthesis time (s): " << log.synthesis_time << "\n";
std::cout << "#Iterations with forbidden pairs: " << log.subcircuits_with_forbidden_pairs << "\n";
printf("Relation generation: #SAT-calls: %lu, Total SAT-time: %.2f sec, Max SAT-time: %.4f sec, Avg. SAT-time: %.4f sec\n",
log.nof_sat_calls_relation_generation, log.cummulative_sat_runtime_relation_generation, log.max_sat_runtime_relation_generation,
log.cummulative_sat_runtime_relation_generation/log.nof_sat_calls_relation_generation);
printf("Synthesis: #SAT-calls: %lu, Total SAT-time: %.2f sec, Max SAT-time: %.4f sec, Avg. SAT-time: %.4f sec\n",
log.nof_sat_calls_synthesis, log.cummulative_sat_runtime_synthesis / 1000, log.max_sat_runtime_synthesis / 1000,
log.cummulative_sat_runtime_synthesis / (log.nof_sat_calls_synthesis*1000));
}
if (config.verbosity_level > 2) {
for (int i = 2; i < log.nof_analyzed_circuits_per_size.size(); i++) {
int replaced = log.nof_replaced_circuits_per_size.size() > i ? log.nof_replaced_circuits_per_size[i] : 0;
int reduced = log.nof_reduced_circuits_per_size.size() > i ? log.nof_reduced_circuits_per_size[i] : 0;
std::cout << "#gates: " << i << " - #analysed: " << log.nof_analyzed_circuits_per_size[i] << " - #replaced: " << replaced << " - #reduced: " << reduced;
std::cout << " - avg. relation time: ";
if (log.nof_relation_generations_per_size[i] == 0) {
std::cout << "-";
} else {
printf("%.2f sec", static_cast<double>(log.cummulative_relation_generation_times_per_size[i]) / (log.nof_relation_generations_per_size[i]));
}
std::cout << "\n";
}
for (int i = 0; i < log.nof_sat_calls_per_size.size(); i++) {
std::cout << "#gates: " << i << " - avg. sat time: ";
if (log.nof_sat_calls_per_size[i] == 0) {
std::cout << "-";
} else {
printf("%.2f sec", static_cast<double>(log.cummulative_sat_runtimes_per_size[i]) / (1000 * log.nof_sat_calls_per_size[i]));
}
std::cout << " / avg. unsat time: ";
if (log.nof_unsat_calls_per_size[i] == 0) {
std::cout << "-";
} else {
printf("%.2f sec", static_cast<double>(log.cummulative_unsat_runtimes_per_size[i]) / (1000 * log.nof_unsat_calls_per_size[i]));
}
std::cout << "\n";
}
}
}
template <typename Approach, typename Inprocessor>
void eSLIMRun<Approach, Inprocessor>::runInprocessing() {
inprocessor.runInprocessing(es_man);
}
template <typename Approach, typename Inprocessor>
void setUpInprocessor();
DeepsynInprocessor::DeepsynInprocessor(eSLIMConfig& config)
: config(config) {
}
void DeepsynInprocessor::runInprocessing(eSLIMCirMan& es_man) {
Gia_Man_t* pGia = es_man.eSLIMCirManToGia();
Gia_Man_t* tmp = Gia_ManDeepSyn( pGia, 1, ABC_INFINITY, timeout, 0, config.seed , 0, 0, 0);
if ( Gia_ManAndNum(pGia) > Gia_ManAndNum(tmp) ) {
es_man = eSLIMCirMan(tmp);
}
Gia_ManStop( tmp );
Gia_ManStop( pGia );
}
void MfsInprocessor::runInprocessing(eSLIMCirMan& es_man) {
Abc_Ntk_t* pNtk = es_man.eSLIMCirManToNtk();
int nnodes = Abc_NtkNodeNum(pNtk);
Mfs_Par_t Pars, * pPars = &Pars;
Abc_NtkMfsParsDefault( pPars );
if ( Abc_NtkMfs( pNtk, pPars ) ) {
Abc_NtkToSop( pNtk, -1, ABC_INFINITY );
if (Abc_NtkNodeNum(pNtk) <= nnodes) {
es_man = eSLIMCirMan(pNtk, true);
}
}
Abc_NtkDelete(pNtk);
}
template <bool IncreaseSize>
DelayInprocessor<IncreaseSize>::DelayInprocessor(eSLIMConfig& config)
: config(config) {
}
template <bool IncreaseSize>
void DelayInprocessor<IncreaseSize>::runInprocessing(eSLIMCirMan& es_man) {
abctime clkStart = Abc_Clock();
abctime nTimeToStop = clkStart + timeout * CLOCKS_PER_SEC;
Gia_Man_t* pGia = es_man.eSLIMCirManToGia();
int nand = Gia_ManAndNum(pGia);
int nlevel = Gia_ManLevelNum(pGia);
char * resyn2 = "balance; rewrite; rewrite -z; balance; rewrite -z; balance";
char Command[2000];
sprintf( Command, "strash; if -g -K 6; %s; if -K 6", resyn2 );
bool reset_batch_mode = false ;
if ( !Abc_FrameIsBatchMode() ) {
reset_batch_mode = true;
Abc_FrameSetBatchMode( 1 );
}
Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pGia );
if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), "&put") ) {
return;
}
while (Abc_Clock() <= nTimeToStop) {
if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), Command) ) {
Abc_Print( 1, "Something did not work out with the command \"%s\".\n", Command );
return;
}
}
if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), "&get") ) {
return;
}
if (reset_batch_mode) {
Abc_FrameSetBatchMode( 0 );
}
Gia_Man_t* tmp = Abc_FrameReadGia(Abc_FrameGetGlobalFrame());
if constexpr (!IncreaseSize) {
if (Gia_ManAndNum(tmp) > nand) {
return;
}
}
if (Gia_ManLevelNum(tmp) <= nlevel) {
es_man = eSLIMCirMan(tmp);
}
}
Resyn2Inprocessor::Resyn2Inprocessor(eSLIMConfig& config)
// : config(config)
{
}
void Resyn2Inprocessor::runInprocessing(eSLIMCirMan& es_man) {
Gia_Man_t* pGia = es_man.eSLIMCirManToGia();
int nand = Gia_ManAndNum(pGia);
int nlevel = Gia_ManLevelNum(pGia);
char * resyn2 = "balance; rewrite; rewrite -z; balance; rewrite -z; balance";
bool reset_batch_mode = false ;
if ( !Abc_FrameIsBatchMode() ) {
reset_batch_mode = true;
Abc_FrameSetBatchMode( 1 );
}
Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pGia );
if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), "&put") ) {
return;
}
if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), resyn2) ) {
Abc_Print( 1, "Something did not work out with the command \"%s\".\n", resyn2 );
return;
}
if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), "&get") ) {
return;
}
if (reset_batch_mode) {
Abc_FrameSetBatchMode( 0 );
}
Gia_Man_t* tmp = Abc_FrameReadGia(Abc_FrameGetGlobalFrame());
if (Gia_ManAndNum(tmp) <= nand && Gia_ManLevelNum(tmp) <= nlevel) {
es_man = eSLIMCirMan(tmp);
}
}
template <typename Circuitrepresentation, typename Inprocessor, typename Minimizer, typename Approach>
Circuitrepresentation* runeSLIM(Circuitrepresentation * cir, const eSLIM_ParamStruct* params) {
return eSLIMRun<Approach, Inprocessor>::runeSLIM(cir, params);
}
template <typename Circuitrepresentation, typename Inprocessor, typename Minimizer, typename Validator, typename SearchDirection, typename BiasSelector, typename RootSelector>
Circuitrepresentation* toggleWindowing(Circuitrepresentation * cir, const eSLIM_ParamStruct* params) {
if (params->nWindows > 0) {
return runeSLIM<Circuitrepresentation, Inprocessor, Minimizer, WindowMan<Minimizer, RandomizedBFSSelection<Validator, RootSelector, SearchDirection, BiasSelector>>>(cir, params);
} else {
return runeSLIM<Circuitrepresentation, Inprocessor, Minimizer, eSLIM_Man<Minimizer, RandomizedBFSSelection<Validator, RootSelector, SearchDirection, BiasSelector>>>(cir, params);
}
}
template <typename Circuitrepresentation, typename Inprocessor, typename Minimizer, typename Validator, typename SearchDirection, typename BiasSelector>
Circuitrepresentation* setTabooApproach(Circuitrepresentation * cir, const eSLIM_ParamStruct* params) {
if (params->use_taboo_list) {
return toggleWindowing<Circuitrepresentation, Inprocessor, Minimizer, Validator, SearchDirection, BiasSelector, TabooRootSelector>(cir, params);
} else {
return toggleWindowing<Circuitrepresentation, Inprocessor, Minimizer, Validator, SearchDirection, BiasSelector, BaseRootSelector>(cir, params);
}
}
template <typename Circuitrepresentation, typename Inprocessor, typename Minimizer, typename Validator, typename SearchDirection>
Circuitrepresentation* setBiasApproach(Circuitrepresentation * cir, const eSLIM_ParamStruct* params) {
if (params->criticial_path_selection_bias) {
return toggleWindowing<Circuitrepresentation, Inprocessor, Minimizer, Validator, SearchDirection, CriticalPathBiasSelector, CriticalPathSelector>(cir, params);
} else {
return setTabooApproach<Circuitrepresentation, Inprocessor, Minimizer, Validator, SearchDirection, NoBiasSelector>(cir, params);
}
}
template <typename Circuitrepresentation, typename Inprocessor, typename Minimizer, typename Validator>
Circuitrepresentation* setSearchDirection(Circuitrepresentation * cir, const eSLIM_ParamStruct* params) {
if (params->forward_search) {
return setBiasApproach<Circuitrepresentation, Inprocessor, Minimizer, Validator, ForwardSearch>(cir, params);
} else {
return setBiasApproach<Circuitrepresentation, Inprocessor, Minimizer, Validator, BackwardSearch>(cir, params);
}
}
template <typename Circuitrepresentation>
Circuitrepresentation* setMinimizer(Circuitrepresentation * cir, const eSLIM_ParamStruct* params) {
switch (params->synthesis_approach) {
case 0:
if (params->apply_inprocessing) {
if constexpr ( std::is_same_v<Gia_Man_t, Circuitrepresentation> ) {
return setSearchDirection<Circuitrepresentation, DeepsynInprocessor, AreaMinimizer, SubcircuitValidator>(cir, params);
} else {
return setSearchDirection<Circuitrepresentation, MfsInprocessor, AreaMinimizer, SubcircuitValidator>(cir, params);
}
}
return setSearchDirection<Circuitrepresentation, EmptyInprocessor, AreaMinimizer, SubcircuitValidator>(cir, params);
case 1:
if constexpr ( std::is_same_v<Gia_Man_t, Circuitrepresentation> ) {
if (params->apply_inprocessing) {
return setSearchDirection<Circuitrepresentation, Resyn2Inprocessor, AreaDelayConstraintMinimizer, SubcircuitNoFBValidator>(cir, params);
}
}
return setSearchDirection<Circuitrepresentation, EmptyInprocessor, AreaDelayConstraintMinimizer, SubcircuitNoFBValidator>(cir, params);
case 2:
if constexpr ( std::is_same_v<Gia_Man_t, Circuitrepresentation> ) {
if (params->apply_inprocessing) {
return setSearchDirection<Circuitrepresentation, DelayInprocessor<false>, AreaDelayMinimizer, SubcircuitNoFBValidator>(cir, params);
}
}
return setSearchDirection<Circuitrepresentation, EmptyInprocessor, AreaDelayMinimizer, SubcircuitNoFBValidator>(cir, params);
case 3:
if constexpr ( std::is_same_v<Gia_Man_t, Circuitrepresentation> ) {
if (params->apply_inprocessing) {
return setSearchDirection<Circuitrepresentation, DelayInprocessor<false>, DelayMinimizer, SubcircuitNoFBValidator>(cir, params);
}
}
return setSearchDirection<Circuitrepresentation, EmptyInprocessor, DelayMinimizer, SubcircuitNoFBValidator>(cir, params);
default:
assert(false);
return NULL;
}
}
return pGia;
}
void printSetting(const eSLIM_ParamStruct* params) {
std::cout << "Apply eSLIM (timeout: " << params->timeout << ") ";
if (params->apply_inprocessing) {
std::cout << "+ deepsyn (timeout: " << params->timeout_inprocessing << ") ";
}
std::cout << params->nruns << " times.\n";
if (params->iterations > 0) {
std::cout << "Stop eSLIM runs after " << params->iterations << " iterations.\n";
}
std::cout << "Consider subcircuits with up to " << params->subcircuit_size_bound << " gates.\n";
printf("When expanding subcircuits, select gates with a probability of %.2f %%.\n", 100 * params->expansion_probability);
if (params->forbidden_pairs) {
std::cout << "Consider subcircuits containing gates, which are connected outside of the subcircuit.\n";
}
if (params->mode == 0) {
std::cout << "Use an incremental SAT encoding for exact synthesis and the SAT solver CaDiCaL.\n";
} else {
std::cout << "Use a one-shot SAT encoding for exact synthesis and the SAT solver Kissat.\n";
template <typename Circuitrepresentation>
Circuitrepresentation* runeSLIM(Circuitrepresentation * cir, const eSLIM_ParamStruct* params) {
// Windowing does currently not support Deleyconstraints/Delayoptimisation
if (params->nWindows && params->synthesis_approach != 0) {
return NULL;
}
return eSLIM::setMinimizer(cir, params);
}
Gia_Man_t* applyeSLIM(Gia_Man_t * pGia, const eSLIM_ParamStruct* params) {
eSLIM::eSLIMConfig config = getCfg(params);
config.verbosity_level = params->verbosity_level;
int eSLIM_reductions = 0;
int deepsyn_reductions = 0;
Gia_Man_t * pThis = Gia_ManDup(pGia);
eSLIM::eSLIMLog log(params->subcircuit_size_bound);
int initial_size = Gia_ManAndNum(pThis);
if (params->verbosity_level > 0) {
printSetting(params);
std::cout << "Initial size: " << initial_size << "\n";
}
for (unsigned int i = 0; i < params->nruns; i++) {
if (config.fix_seed) {
config.seed = params->seed + i;
}
int size_iteration_start = Gia_ManAndNum(pThis);
if (params->verbosity_level > 0) {
std::cout << "Start eslim run " << i + 1 << "\n";
}
pThis = selectApproach(pThis, config, log, params->mode, params->forbidden_pairs);
int size_eslim = Gia_ManAndNum(pThis);
eSLIM_reductions += size_iteration_start - size_eslim;
if (params->apply_inprocessing) {
if (params->verbosity_level > 0) {
std::cout << "Start inprocessing run " << i + 1 << "\n";
}
pThis = runInprocessing(pThis, params, i);
if (params->verbosity_level > 0) {
std::cout << "Inprocessing: Initial size: " << size_eslim << " final size: " << Gia_ManAndNum(pThis) << "\n";
}
deepsyn_reductions += size_eslim - Gia_ManAndNum(pThis);
}
}
if (params->verbosity_level > 0) {
int final_size = Gia_ManAndNum(pThis);
std::cout << "Final size: " << final_size << "\n";
int total_reductions = eSLIM_reductions + deepsyn_reductions;
double reduction_ratio = 100 * static_cast<double>(total_reductions) / initial_size;
printf("Total reduction: %d (%.2f %%)\n", total_reductions, reduction_ratio);
if (params->apply_inprocessing) {
std::cout << "#Gates reduced by eSLIM: " << eSLIM_reductions << " ";
std::cout << "#Gates reduced by deepsyn: " << deepsyn_reductions << "\n";
}
}
if (params->verbosity_level > 1) {
std::cout << "Total #iterations: " << log.iteration_count << "\n";
std::cout << "Total relation generation time (s): " << log.relation_generation_time << "\n";
std::cout << "Total synthesis time (s): " << log.synthesis_time << "\n";
std::cout << "#Iterations with forbidden pairs: " << log.subcircuits_with_forbidden_pairs << "\n";
}
if (params->verbosity_level > 2) {
for (int i = 2; i < log.nof_analyzed_circuits_per_size.size(); i++) {
int replaced = log.nof_replaced_circuits_per_size.size() > i ? log.nof_replaced_circuits_per_size[i] : 0;
int reduced = log.nof_reduced_circuits_per_size.size() > i ? log.nof_reduced_circuits_per_size[i] : 0;
std::cout << "#gates: " << i << " - #analysed: " << log.nof_analyzed_circuits_per_size[i] << " - #replaced: " << replaced << " - #reduced: " << reduced << "\n";
}
if (params->mode == 0) {
for (int i = 0; i < log.nof_sat_calls_per_size.size(); i++) {
if (log.nof_sat_calls_per_size[i] == 0) {
std::cout << "#gates: " << i << " - avg. sat time: -\n";
} else {
std::cout << "#gates: " << i << " - avg. sat time: " << static_cast<double>(log.cummulative_sat_runtimes_per_size[i]) / (1000 * log.nof_sat_calls_per_size[i]) << " sec\n";
}
}
for (int i = 0; i < log.nof_unsat_calls_per_size.size(); i++) {
if (log.nof_unsat_calls_per_size[i] == 0) {
std::cout << "#gates: " << i << " - avg. unsat time: -\n";
} else {
std::cout << "#gates: " << i << " - avg. unsat time: " << static_cast<double>(log.cummulative_unsat_runtimes_per_size[i]) / (1000* log.nof_unsat_calls_per_size[i]) << " sec\n";
}
}
}
}
return pThis;
return runeSLIM(pGia, params);
}
ABC_NAMESPACE_IMPL_END
Abc_Ntk_t* applyelSLIM(Abc_Ntk_t * ntk, const eSLIM_ParamStruct* params) {
return runeSLIM(ntk, params);
}
Abc_Ntk_t* applyetSLIM(Abc_Ntk_t * ntk, const eSLIM_ParamStruct* params) {
return runeSLIM(ntk, params);
}
ABC_NAMESPACE_IMPL_END

43
src/opt/eslim/eSLIM.h
View File

@ -12,9 +12,9 @@
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - March 2025.]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.h,v 1.00 2025/03/17 00:00:00 Exp $]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
@ -23,39 +23,52 @@
#include "misc/util/abc_namespaces.h"
#include "aig/gia/gia.h"
#include "base/abc/abc.h"
ABC_NAMESPACE_HEADER_START
typedef struct eSLIM_ParamStruct_ eSLIM_ParamStruct;
struct eSLIM_ParamStruct_ {
int forbidden_pairs; // Allow forbidden pairs in the selected subcircuits
int extended_normality_processing; // Additional checks for non normal subcircuits
int fill_subcircuits; // If a subcircuit has fewer than subcircuit_size_bound gates, try to fill it with rejected gates.
int fill_subcircuits; // If a subcircuit has fewer than subcircuit_max_size gates, try to fill it with rejected gates.
int apply_strash;
int fix_seed;
int trial_limit_active;
int apply_inprocessing;
int synthesis_approach;
int seed;
int verbosity_level;
int approximate_relation;
int relation_tfo_bound;
int generate_relation_with_tfi_limit;
int relation_tfi_bound;
int use_taboo_list;
int forward_search;
int nWindows;
int window_size;
int criticial_path_selection_bias;
unsigned int timeout; // available time in seconds (soft limit)
unsigned int timeout_inprocessing;
unsigned int iterations; // maximal number of iterations. No limit if 0
unsigned int subcircuit_size_bound; // upper bound for the subcircuit sizes
unsigned int strash_intervall;
unsigned int nselection_trials;
unsigned int nruns;
unsigned int subcircuit_max_size; // upper bound for the subcircuit sizes
unsigned int additional_gates; // number of gates that may be introduced to reduce delay
double expansion_probability; // the probability that a node is added to the subcircuit
unsigned int nruns;
int mode; // 0: Cadical Incremental, 1: Kissat Oneshot
int seed;
int verbosity_level;
unsigned int strash_intervall;
unsigned int nselection_trials;
int gate_size;
int aig;
};
void seteSLIMParams(eSLIM_ParamStruct* params);
Gia_Man_t* applyeSLIM(Gia_Man_t * pGia, const eSLIM_ParamStruct* params);
Gia_Man_t* applyeSLIMIncremental(Gia_Man_t * pGia, const eSLIM_ParamStruct* params, unsigned int restarts, unsigned int deepsynTimeout);
Abc_Ntk_t* applyelSLIM(Abc_Ntk_t * ntk, const eSLIM_ParamStruct* params); //LUT-eSLIM
ABC_NAMESPACE_HEADER_END

54
src/opt/eslim/eSLIMMan.hpp
View File

@ -26,67 +26,51 @@
#include <unordered_set>
#include "misc/util/abc_namespaces.h"
#include "misc/vec/vec.h"
#include "aig/gia/gia.h"
#include "misc/util/utilTruth.h" // ioResub.h depends on utilTruth.h
#include "base/io/ioResub.h"
#include "aig/miniaig/miniaig.h"
#include "eslimCirMan.hpp"
#include "relationGeneration.hpp"
#include "selectionStrategies.hpp"
#include "subcircuit.hpp"
#include "utils.hpp"
#include "selectionStrategy.hpp"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
template<class SynthesisEngine, class RelationEngine, class SelectionEngine>
class eSLIM_Man {
template <typename SynthesisEngine, typename SelectionStrategy>
class eSLIM_Man {
public:
static Gia_Man_t* applyeSLIM(Gia_Man_t * p, const eSLIMConfig& cfg, eSLIMLog& log);
static void applyeSLIM(eSLIMCirMan& cir, const eSLIMConfig& cfg, eSLIMLog& log);
private:
eSLIM_Man(Gia_Man_t * gia_man, const eSLIMConfig& cfg, eSLIMLog& log);
Gia_Man_t* getCircuit();
eSLIM_Man(eSLIMCirMan& es_man, const eSLIMConfig& cfg, eSLIMLog& log);
void optimize();
void minimize();
void findReplacement();
Mini_Aig_t* findMinimumAig(const Subcircuit& subcir);
eSLIMCirMan computeReplacement(Subcircuit& subcir);
eSLIMCirMan synthesiseRelation(Subcircuit& subcir, const Relation& rel);
Vec_Wrd_t* getSimsIn(Abc_RData_t* relation);
Vec_Wrd_t* getSimsOut(Abc_RData_t* relation);
word getAllFalseBehaviour(const Subcircuit& subcir);
bool getAllFalseBehaviourRec(Gia_Obj_t * pObj);
std::pair<int, Mini_Aig_t*> reduce( Vec_Wrd_t* vSimsDiv, Vec_Wrd_t* vSimsOut, const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs,
int nVars, int nDivs, int nOuts, int initial_size);
Mini_Aig_t* computeReplacement( SynthesisEngine& syn_man, int size);
double getDynamicTimeout(int size);
void insertReplacement(Mini_Aig_t* replacement, const Subcircuit& subcir);
std::vector<int> processReplacement(Gia_Man_t* gia_man, Gia_Man_t* pNew, const Subcircuit& subcir, Mini_Aig_t* replacement, std::vector<int>&& to_process, std::vector<int>& replacement_values);
Vec_Int_t * processEncompassing(Gia_Man_t* gia_man, Gia_Man_t* pNew, Vec_Int_t* to_process);
int getInsertionLiteral(Gia_Man_t* gia_man, const Subcircuit& subcir, Mini_Aig_t* replacement, const std::vector<int>& replacement_values, int fanin_lit);
Gia_Man_t* gia_man = nullptr;
eSLIMCirMan& es_man;
SelectionStrategy selection_strategy;
const eSLIMConfig& cfg;
eSLIMLog& log;
SelectionEngine subcircuit_selection;
double relation_generation_time ;
double synthesis_time ;
bool stopeSLIM=false;
bool stopeSLIM = false;
};
template <typename Y, typename R, typename S>
inline Gia_Man_t* eSLIM_Man<Y, R, S>::getCircuit() {
return gia_man;
}
}
ABC_NAMESPACE_CXX_HEADER_END
#include "eSLIMMan.tpp"

473
src/opt/eslim/eSLIMMan.tpp
View File

@ -14,79 +14,60 @@
Date [Ver. 1.0. Started - March 2025.]
Revision [$Id: eSLIMMan.tpp,v 1.00 2025/03/17 00:00:00 Exp $]
Revision [$Id: eSLIMMan.hpp,v 1.00 2025/03/17 00:00:00 Exp $]
***********************************************************************/
#include <cassert>
#include <queue>
#include <vector>
#include <tuple>
#include <unordered_set>
#include <iostream>
#include <climits>
#include "eSLIMMan.hpp"
#include "synthesisEngine.hpp"
#include "relationGeneration.hpp"
ABC_NAMESPACE_HEADER_START
Mini_Aig_t * Mini_AigDupCompl( Mini_Aig_t * p, int ComplIns, int ComplOuts );
int Exa6_ManFindPolar( word First, int nOuts );
Vec_Wrd_t * Exa6_ManTransformInputs( Vec_Wrd_t * vIns );
Vec_Wrd_t * Exa6_ManTransformOutputs( Vec_Wrd_t * vOuts, int nOuts );
ABC_NAMESPACE_HEADER_END
#include "synthesisEngines.hpp"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
template <typename Y, typename R, typename S>
Gia_Man_t* eSLIM_Man<Y, R, S>::applyeSLIM(Gia_Man_t * p, const eSLIMConfig& cfg, eSLIMLog& log) {
eSLIM_Man<Y, R, S> eslim(p, cfg, log);
eslim.minimize();
return eslim.getCircuit();
template <typename SynthesisEngine, typename SelectionStrategy>
void eSLIM_Man<SynthesisEngine, SelectionStrategy>::applyeSLIM(eSLIMCirMan& cir, const eSLIMConfig& cfg, eSLIMLog& log) {
eSLIM_Man eslim(cir, cfg, log);
eslim.optimize();
}
template <typename Y, typename R, typename S>
eSLIM_Man<Y, R, S>::eSLIM_Man(Gia_Man_t * pGia, const eSLIMConfig& cfg, eSLIMLog& log)
: gia_man(pGia), cfg(cfg), log(log),
subcircuit_selection(gia_man, cfg, log) {
template <typename SynthesisEngine, typename SelectionStrategy>
eSLIM_Man<SynthesisEngine, SelectionStrategy>::eSLIM_Man(eSLIMCirMan& es_man, const eSLIMConfig& cfg, eSLIMLog& log)
: es_man(es_man), selection_strategy(this->es_man, cfg, log), cfg(cfg), log(log) {
if (cfg.fix_seed) {
subcircuit_selection.setSeed(cfg.seed);
selection_strategy.setSeed(cfg.seed);
}
relation_generation_time = log.relation_generation_time;
synthesis_time = log.synthesis_time;
}
template <typename Y, typename R, typename S>
void eSLIM_Man<Y, R, S>::minimize() {
template <typename SynthesisEngine, typename SelectionStrategy>
void eSLIM_Man<SynthesisEngine, SelectionStrategy>::optimize() {
abctime clkStart = Abc_Clock();
abctime nTimeToStop = clkStart + cfg.timeout * CLOCKS_PER_SEC;
unsigned int iteration = 0;
unsigned int iterMax = cfg.iterations ? cfg.iterations - 1 : UINT_MAX;
int current_size = Gia_ManAndNum(gia_man);
int current_size = es_man.getNofGates();
const char* node_type = cfg.aig ? "#and" : "#nd";
while (Abc_Clock() <= nTimeToStop && iteration <= iterMax && !stopeSLIM) {
iteration++;
findReplacement();
if (Gia_ManHasDangling(gia_man)) {
Gia_Man_t* pTemp = gia_man;
gia_man = Gia_ManCleanup( pTemp );
Gia_ManStop( pTemp );
}
if (cfg.apply_strash && iteration % cfg.strash_intervall == 0) {
Gia_Man_t* pTemp = gia_man;
gia_man = Gia_ManRehash( pTemp, 0 );
Gia_Man_t* pTemp = es_man.eSLIMCirManToGia();
Gia_Man_t* gia_man = Gia_ManRehash( pTemp, 0 );
Gia_ManStop( pTemp );
es_man = eSLIMCirMan(gia_man);
Gia_ManStop( gia_man );
selection_strategy.reset();
}
if (cfg.verbosity_level > 0) {
int sz = Gia_ManAndNum(gia_man);
int sz = es_man.getNofGates();
if (sz < current_size) {
current_size = sz;
printf("\rIteration %8d : #and = %7d elapsed time = %7.2f sec\n", iteration, sz, (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC);
printf("\rIteration %8d : %s = %7d elapsed time = %7.2f sec\n", iteration, node_type, sz, (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC);
} else {
printf("\rIteration %8d", iteration);
fflush(stdout);
@ -95,8 +76,8 @@ namespace eSLIM {
}
log.iteration_count += iteration;
if (cfg.verbosity_level > 0) {
int sz = Gia_ManAndNum(gia_man);
printf("\r#Iterations %8d #and = %7d elapsed time = %7.2f sec\n", iteration, sz, (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC);
int sz = es_man.getNofGates();
printf("\r#Iterations %8d %s = %7d elapsed time = %7.2f sec\n", iteration, node_type, sz, (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC);
if (cfg.verbosity_level > 1) {
printf("Relation generation time: %.2f sec\n", log.relation_generation_time - relation_generation_time);
printf("Synthesis time: %.2f sec\n", log.synthesis_time - synthesis_time);
@ -104,379 +85,57 @@ namespace eSLIM {
}
}
template <typename Y, typename R, typename S>
Vec_Wrd_t* eSLIM_Man<Y, R, S>::getSimsIn(Abc_RData_t* relation) {
Vec_Wrd_t* vSimsDiv = Vec_WrdStart( relation->nPats );
for (int k = 0; k < relation->nIns; k++) {
for (int i = 0; i < relation->nPats; i++) {
if (Abc_RDataGetIn(relation, k, i)) {
// The first bit corresponds to the constant divisor thus we have +1
Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(vSimsDiv, i), 1+k);
}
}
template <typename SynthesisEngine, typename SelectionStrategy>
eSLIMCirMan eSLIM_Man<SynthesisEngine, SelectionStrategy>::computeReplacement(Subcircuit& subcir) {
abctime relation_generation_start = Abc_Clock();
Relation rel = RelationGenerator::computeRelation(es_man, subcir, cfg, log);
log.relation_generation_time += (double)1.0*(Abc_Clock() - relation_generation_start)/CLOCKS_PER_SEC;
log.cummulative_relation_generation_times_per_size[subcir.nodes.size()] += (double)1.0*(Abc_Clock() - relation_generation_start) / CLOCKS_PER_SEC;
log.nof_relation_generations_per_size[subcir.nodes.size()]++;
if (!rel.getStatus()) {
return eSLIMCirMan(0);
}
return vSimsDiv;
}
template <typename Y, typename R, typename S>
Vec_Wrd_t* eSLIM_Man<Y, R, S>::getSimsOut(Abc_RData_t* relation) {
Vec_Wrd_t* vSimsOut = Vec_WrdStart(relation->nPats);
for (int k = 0; k < (1 << relation->nOuts); k++) {
for (int i = 0; i < relation->nPats; i++) {
if (Abc_RDataGetOut(relation, k, i)) {
Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(vSimsOut, i), k);
}
}
}
return vSimsOut;
abctime synthesis_start = Abc_Clock();
eSLIMCirMan replacement = synthesiseRelation(subcir, rel);
log.synthesis_time += (double)1.0*(Abc_Clock() - synthesis_start)/CLOCKS_PER_SEC;
return replacement;
}
template <typename Y, typename R, typename S>
void eSLIM_Man<Y, R, S>::findReplacement() {
Subcircuit subcir = subcircuit_selection.getSubcircuit();
if (!subcircuit_selection.getStatus()) {
template <typename SynthesisEngine, typename SelectionStrategy>
eSLIMCirMan eSLIM_Man<SynthesisEngine, SelectionStrategy>::synthesiseRelation(Subcircuit& subcir, const Relation& rel) {
return SynthesisEngine::optimize(es_man, rel, subcir, cfg, log);
}
template <typename SynthesisEngine, typename SelectionStrategy>
void eSLIM_Man<SynthesisEngine, SelectionStrategy>::findReplacement() {
bool status = true;
if constexpr (SelectionStrategy::requiresRemainingTimes() || isDelayEngine<SynthesisEngine>::value) {
es_man.setupTimings();
}
Subcircuit subcir = selection_strategy.getSubcircuit(status);
if (!status) {
if (cfg.trial_limit_active) {
stopeSLIM = true;
}
return;
}
Mini_Aig_t* replacement = findMinimumAig(subcir);
if (replacement != nullptr) {
insertReplacement(replacement, subcir);
Mini_AigStop(replacement);
}
subcir.free();
}
eSLIMCirMan replacement = computeReplacement(subcir);
// Based on Exa_ManExactSynthesis6Int and Exa_ManExactSynthesis6
template <typename Y, typename R, typename S>
Mini_Aig_t* eSLIM_Man<Y, R, S>::findMinimumAig(const Subcircuit& subcir) {
if (subcir.forbidden_pairs.size() > 0) {
log.subcircuits_with_forbidden_pairs++;
if (log.nof_analyzed_circuits_per_size.size() < subcir.nodes.size() + 1) {
log.nof_analyzed_circuits_per_size.resize(subcir.nodes.size() + 1, 0);
log.nof_replaced_circuits_per_size.resize(subcir.nodes.size() + 1, 0);
log.nof_reduced_circuits_per_size.resize(subcir.nodes.size() + 1, 0);
}
abctime relation_generation_start = Abc_Clock();
Abc_RData_t* relation = RelationGenerator<R>::computeRelation(gia_man, subcir);
log.relation_generation_time += (double)1.0*(Abc_Clock() - relation_generation_start)/CLOCKS_PER_SEC;
int nDivs = 0;
int nOuts = relation->nOuts;
int nVars = relation->nIns;
if ( nVars == 0 ) {
return nullptr;
}
// assert (nVars <= 8);
Vec_Wrd_t* vSimsDiv = getSimsIn(relation);
Vec_Wrd_t* vSimsOut = getSimsOut(relation);
word original_all_false_behaviour = vSimsOut->pArray[0];
// If the original circuit computed a non-normal circuit, but the relations allows to set the outputs to false in the all inputs false case
// ABC does not "negate" the relation but forces the circuit to yield (0,...,0) for (0,...,0).
// As a consequence it is not necessarily possible to find a same sized circuit.
// In order to prevent this behaviour, we first modify the relation such that for the (0,...,0) input pattern only the original output patterns is allowed.
vSimsOut->pArray[0] = getAllFalseBehaviour(subcir);
int DivCompl = (int)Vec_WrdEntry(vSimsDiv, 0) >> 1;
int OutCompl = Exa6_ManFindPolar( Vec_WrdEntry(vSimsOut, 0), nOuts );
Vec_Wrd_t* vSimsDiv2 = Exa6_ManTransformInputs( vSimsDiv );
Vec_Wrd_t* vSimsOut2 = Exa6_ManTransformOutputs( vSimsOut, nOuts );
Mini_Aig_t* pMini = nullptr;
int original_size = Vec_IntSize(subcir.nodes);
int size = original_size;
if (log.nof_analyzed_circuits_per_size.size() < original_size + 1) {
log.nof_analyzed_circuits_per_size.resize(original_size + 1, 0);
log.nof_replaced_circuits_per_size.resize(original_size + 1, 0);
log.nof_reduced_circuits_per_size.resize(original_size + 1, 0);
}
log.nof_analyzed_circuits_per_size[original_size]++;
abctime synthesis_start = Abc_Clock();
std::tie(size, pMini) = reduce(vSimsDiv2, vSimsOut2, subcir.forbidden_pairs, nVars, nDivs, nOuts, size);
log.synthesis_time += (double)1.0*(Abc_Clock() - synthesis_start)/CLOCKS_PER_SEC;
if (size > original_size) {
// Could not find a replacement. This can be caused by a timeout.
Abc_RDataStop(relation);
Vec_WrdFreeP( &vSimsDiv );
Vec_WrdFreeP( &vSimsOut );
Vec_WrdFreeP( &vSimsDiv2 );
Vec_WrdFreeP( &vSimsOut2 );
return nullptr;
}
// It is possible that a better replacement is obtained with a non normal behaviour.
bool check_original_all_false_behaviour = cfg.extended_normality_processing && vSimsOut->pArray[0] != original_all_false_behaviour;
if (check_original_all_false_behaviour) {
vSimsOut->pArray[0] = original_all_false_behaviour;
int OutCompl_alt = Exa6_ManFindPolar( Vec_WrdEntry(vSimsOut, 0), nOuts );
Vec_Wrd_t* vSimsOut2_alt = Exa6_ManTransformOutputs( vSimsOut, nOuts );
abctime synthesis_start = Abc_Clock();
// auto [sz, mini] = reduce(vSimsDiv2, vSimsOut2_alt, subcir.forbidden_pairs, nVars, nDivs, nOuts, size - 1, true);
auto result = reduce(vSimsDiv2, vSimsOut2_alt, subcir.forbidden_pairs, nVars, nDivs, nOuts, size - 1);
int sz = result.first;
Mini_Aig_t* mini = result.second;
log.synthesis_time += (double)1.0*(Abc_Clock() - synthesis_start)/CLOCKS_PER_SEC;
if (mini != nullptr) {
size = sz;
if (pMini) {
Mini_AigStop(pMini);
}
pMini = mini;
OutCompl = OutCompl_alt;
}
}
Abc_RDataStop(relation);
if (pMini != nullptr) {
Mini_Aig_t* pTemp = pMini;
pMini = Mini_AigDupCompl(pTemp, DivCompl, OutCompl);
Mini_AigStop(pTemp);
log.nof_replaced_circuits_per_size[original_size]++;
if (size < original_size) {
log.nof_reduced_circuits_per_size[original_size]++;
}
}
Vec_WrdFreeP( &vSimsDiv );
Vec_WrdFreeP( &vSimsOut );
Vec_WrdFreeP( &vSimsDiv2 );
Vec_WrdFreeP( &vSimsOut2 );
return pMini;
}
template <typename Y, typename R, typename S>
word eSLIM_Man<Y, R, S>::getAllFalseBehaviour(const Subcircuit& subcir) {
Gia_ManIncrementTravId(gia_man);
Gia_Obj_t * pObj;
int i;
Gia_ManForEachObjVec( subcir.nodes, gia_man, pObj, i ) {
Gia_ObjSetTravIdCurrent(gia_man, pObj);
}
long assm_idx = 0;
Gia_ManForEachObjVecStart(subcir.io, gia_man, pObj, i, subcir.nof_inputs) {
int bit_idx = i - subcir.nof_inputs;
if (getAllFalseBehaviourRec(pObj)) {
assm_idx |= (1 << bit_idx);
}
}
return 1L << assm_idx;
}
template <typename Y, typename R, typename S>
bool eSLIM_Man<Y, R, S>::getAllFalseBehaviourRec(Gia_Obj_t * pObj) {
bool valuefanin0, valuefanin1;
if (Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin0(pObj))) {
valuefanin0 = getAllFalseBehaviourRec(Gia_ObjFanin0(pObj));
} else {
valuefanin0 = false;
}
valuefanin0 = valuefanin0 != pObj->fCompl0;
if (Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin1(pObj))) {
valuefanin1 = getAllFalseBehaviourRec(Gia_ObjFanin1(pObj));
} else {
valuefanin1 = false;
}
valuefanin1 = valuefanin1 != pObj->fCompl1;
return valuefanin0 && valuefanin1;
}
template <typename Y, typename R, typename S>
int eSLIM_Man<Y, R, S>::getInsertionLiteral(Gia_Man_t* gia_man, const Subcircuit& subcir, Mini_Aig_t* replacement, const std::vector<int>& replacement_values, int fanin_lit) {
int fanin_idx = Abc_Lit2Var(fanin_lit);
bool fanin_negated = Abc_LitIsCompl(fanin_lit);
int fanin_value;
if (fanin_idx == 0) { // constant fanin
fanin_value = 0;
} else if (fanin_idx <= subcir.nof_inputs) {
Gia_Obj_t* pObj = Gia_ManObj(gia_man, Vec_IntEntry(subcir.io, fanin_idx - 1));
if (Gia_ObjIsTravIdCurrent(gia_man, pObj)) { //the node has already been added
fanin_value = Gia_ManObj(gia_man, Vec_IntEntry(subcir.io, fanin_idx - 1))->Value;
} else {
return -1;
}
} else {
if (replacement_values[fanin_idx - subcir.nof_inputs - 1] == -1) {
return -1;
}
fanin_value = replacement_values[fanin_idx - subcir.nof_inputs - 1];
}
return Abc_LitNotCond( fanin_value, fanin_negated );
}
template <typename Y, typename R, typename S>
std::vector<int> eSLIM_Man<Y, R, S>::processReplacement(Gia_Man_t* gia_man, Gia_Man_t* pNew, const Subcircuit& subcir, Mini_Aig_t* replacement, std::vector<int>&& to_process, std::vector<int>& replacement_values) {
std::vector<int> to_process_next_it;
for (int id : to_process) {
int fanin0 = getInsertionLiteral(gia_man, subcir, replacement, replacement_values, Mini_AigNodeFanin0( replacement, id));
int fanin1 = getInsertionLiteral(gia_man, subcir, replacement, replacement_values, Mini_AigNodeFanin1( replacement, id));
if (fanin0 == -1 || fanin1 == -1) {
to_process_next_it.push_back(id);
} else {
int idx = id - subcir.nof_inputs - 1;
replacement_values[idx] = Gia_ManAppendAnd2(pNew, fanin0, fanin1);
}
}
int i, j = 0;
Mini_AigForEachPo(replacement, i) {
int old_id = Vec_IntEntry(subcir.io, j + subcir.nof_inputs);
j++;
Gia_Obj_t* obj = Gia_ManObj(gia_man, old_id);
int fanin0_lit = Mini_AigNodeFanin0( replacement, i);
int fanin0_idx = Abc_Lit2Var(fanin0_lit);
if (fanin0_idx == 0) { // constant fanin
obj->Value = Gia_ManConst0(gia_man)->Value;
} else if (fanin0_idx <= subcir.nof_inputs) {
Gia_Obj_t* fanin_obj = Gia_ManObj(gia_man, Vec_IntEntry(subcir.io, fanin0_idx - 1));
if (Gia_ObjIsTravIdCurrent(gia_man, fanin_obj)) {
obj->Value = fanin_obj->Value;
} else {
continue;
}
} else {
if (replacement_values[fanin0_idx - subcir.nof_inputs - 1] == -1 ) {
continue;
} else {
obj->Value = replacement_values[fanin0_idx - subcir.nof_inputs - 1];
}
}
Gia_ObjSetTravIdCurrent(gia_man, obj);
bool fanin0_negated = Abc_LitIsCompl(fanin0_lit);
if (fanin0_negated) {
obj->fMark0 = 1;
}
}
return to_process_next_it;
}
template <typename Y, typename R, typename S>
Vec_Int_t * eSLIM_Man<Y, R, S>::processEncompassing(Gia_Man_t* gia_man, Gia_Man_t* pNew, Vec_Int_t * to_process) {
int i;
Gia_Obj_t * pObj;
Vec_Int_t * to_process_remaining = Vec_IntAlloc( Vec_IntSize(to_process) );
Gia_ManForEachObjVec( to_process, gia_man, pObj, i ) {
if (Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin0(pObj)) && Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin1(pObj))) {
Gia_ObjSetTravIdCurrent(gia_man, pObj);
bool fanin0_negated = Gia_ObjFaninC0(pObj) ^ Gia_ObjFanin0(pObj)->fMark0;
bool fanin1_negated = Gia_ObjFaninC1(pObj) ^ Gia_ObjFanin1(pObj)->fMark0;
int fanin0 = Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, fanin0_negated);
int fanin1 = Abc_LitNotCond(Gia_ObjFanin1(pObj)->Value, fanin1_negated);
pObj->Value = Gia_ManAppendAnd2( pNew, fanin0, fanin1);
} else {
Vec_IntPush(to_process_remaining, Gia_ObjId(gia_man, pObj));
}
}
Vec_IntFree(to_process);
return to_process_remaining;
}
template <typename Y, typename R, typename S>
void eSLIM_Man<Y, R, S>::insertReplacement(Mini_Aig_t* replacement, const Subcircuit& subcir) {
// A miniaig contains a constant node, nodes for each PI/PO and for each and.
int repalcement_size = Mini_AigNodeNum(replacement) - Vec_IntSize(subcir.io) - 1;
int size_diff = Vec_IntSize(subcir.nodes) - repalcement_size;
Gia_Man_t * pNew = Gia_ManStart( Gia_ManObjNum(gia_man) - size_diff );
pNew->pName = Abc_UtilStrsav( gia_man->pName );
pNew->pSpec = Abc_UtilStrsav( gia_man->pSpec );
Gia_Obj_t * pObj;
int i;
Gia_ManConst0(gia_man)->Value = 0;
Gia_ManForEachPi( gia_man, pObj, i ) {
pObj->Value = Gia_ManAppendCi(pNew);
}
Gia_ManIncrementTravId(gia_man);
Gia_ManForEachObjVec( subcir.nodes, gia_man, pObj, i ) {
Gia_ObjSetTravIdCurrent(gia_man, pObj);
}
Gia_ManIncrementTravId(gia_man);
Gia_ManForEachPi( gia_man, pObj, i ) {
Gia_ObjSetTravIdCurrent(gia_man, pObj);
}
Vec_Int_t * to_process_encompassing = Vec_IntAlloc( gia_man->nObjs );
Gia_ManForEachAnd( gia_man, pObj, i ) {
// nodes from the subcircuit shall not be added
if (Gia_ObjIsTravIdPrevious(gia_man, pObj)) {
continue;
} else if (Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin0(pObj)) && Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin1(pObj))) {
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ObjSetTravIdCurrent(gia_man, pObj);
} else {
Vec_IntPush(to_process_encompassing, Gia_ObjId(gia_man, pObj));
}
}
std::vector<int> to_process_replacement;
Mini_AigForEachAnd(replacement, i) {
to_process_replacement.push_back(i);
}
std::vector<int> replacement_values(to_process_replacement.size(), -1);
while (Vec_IntSize(to_process_encompassing) > 0 || to_process_replacement.size() > 0) {
to_process_replacement = processReplacement(gia_man, pNew, subcir, replacement, std::move(to_process_replacement), replacement_values);
to_process_encompassing = processEncompassing(gia_man, pNew, to_process_encompassing);
}
Vec_IntFree(to_process_encompassing);
int po_idx = 0;
Mini_AigForEachPo(replacement, i) {
Gia_Obj_t* pObj = Gia_ManObj(gia_man, Vec_IntEntry(subcir.io, subcir.nof_inputs + po_idx));
if (!Gia_ObjIsTravIdCurrent(gia_man, pObj)) {
int fanin_lit = Mini_AigNodeFanin0( replacement, i);
int fanin_idx = Abc_Lit2Var(fanin_lit);
assert (fanin_idx <= subcir.nof_inputs);
Gia_Obj_t* fanin_obj = Gia_ManObj(gia_man, Vec_IntEntry(subcir.io, fanin_idx - 1));
pObj->Value = fanin_obj->Value;
if (Abc_LitIsCompl(fanin_lit)) {
pObj->fMark0 = 1;
}
Gia_ObjSetTravIdCurrent(gia_man, pObj);
}
po_idx++;
}
Gia_ManForEachPo( gia_man, pObj, i ) {
assert(Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin0(pObj)));
bool fanin_negated = Gia_ObjFaninC0(pObj) ^ Gia_ObjFanin0(pObj)->fMark0;
int fanin0 = Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, fanin_negated);
pObj->Value = Gia_ManAppendCo( pNew, fanin0 );
}
Gia_ManStop(gia_man);
gia_man = pNew;
}
template <typename Y, typename R, typename S>
std::pair<int, Mini_Aig_t*> eSLIM_Man<Y, R, S>::reduce(Vec_Wrd_t* vSimsDiv, Vec_Wrd_t* vSimsOut, const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs,
int nVars, int nDivs, int nOuts, int size) {
Y synth_man(vSimsDiv,vSimsOut,nVars,1+nVars+nDivs,nOuts,size, forbidden_pairs, log, cfg);
Mini_Aig_t* result = nullptr;
while (size >= 0) {
Mini_Aig_t* pTemp = computeReplacement(synth_man, size);
if (pTemp) {
if (result) {
Mini_AigStop(result);
}
result = pTemp;
size--;
} else {
break;
}
}
return std::make_pair(size + 1, result);
}
template <typename Y, typename R, typename S>
double eSLIM_Man<Y, R, S>::getDynamicTimeout(int size) {
if (this->log.nof_sat_calls_per_size[size] > cfg.minimum_dynamic_timeout_sample_size) {
return std::max(static_cast<double>(cfg.minimum_sat_timeout), static_cast<double>(log.cummulative_sat_runtimes_per_size[size]) / (1000*log.nof_sat_calls_per_size[size])); //logged timings are given in ms
} else {
return cfg.base_sat_timeout;
}
}
template <typename Y, typename R, typename S>
Mini_Aig_t* eSLIM_Man<Y, R, S>::computeReplacement(Y& syn_man, int size) {
return syn_man.getCircuit(size, getDynamicTimeout(size));
log.nof_analyzed_circuits_per_size[subcir.nodes.size()]++;
log.subcircuits_with_forbidden_pairs += !subcir.forbidden_pairs.empty();
if (replacement.getNofObjs() > 1) { //replacement found
log.nof_replaced_circuits_per_size[subcir.nodes.size()]++;
log.nof_reduced_circuits_per_size[subcir.nodes.size()] += (replacement.getNofGates() < subcir.nodes.size());
es_man.replace(replacement, subcir);
}
}
}
ABC_NAMESPACE_CXX_HEADER_END

1121
src/opt/eslim/eslimCirMan.cpp Normal file
View File

File diff suppressed because it is too large Load Diff

234
src/opt/eslim/eslimCirMan.hpp Normal file
View File

@ -0,0 +1,234 @@
/**CFile****************************************************************
FileName [eslimCirMan.hpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Internal circuit representation.]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__OPT__ESLIM__ESLIMCIRMAN_hpp
#define ABC__OPT__ESLIM__ESLIMCIRMAN_hpp
#include <vector>
#include <memory>
#include <unordered_map>
#include <set>
#include "aig/gia/gia.h"
#include "base/abc/abc.h"
#include "misc/util/abc_namespaces.h"
#include "misc/util/abc_global.h"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
class Subcircuit;
class eSLIMCirMan;
class TabooList;
template <typename SynthesisEngine, typename SelectionStrategy> class WindowMan;
// Nodes must not have more than 6 fanins
class eSLIMCirObj {
private:
// This comparator is used in sets of pointers to nodes.
// As the order does not really matter, the comparator could be replaced by comparing addresses.
// This would slightly simplify the code as we would not need to change the fanouts of replacement circuits
// (unlike to the ids the addresses of the nodes in the replacement do not change during the replacement).
// Nevertheless, we use this iterator to make iteration orders more predictable.
struct eSLIMObjComp {
bool operator()(eSLIMCirObj* a, eSLIMCirObj* b) const {
return a->getId() < b->getId();
}
};
public:
eSLIMCirObj(int id, std::vector<eSLIMCirObj*>&& fanins);
int getNFanins() const;
int getTTLength() const;
unsigned int getId() const;
int node_id;
std::vector<eSLIMCirObj*> fanins;
std::set<eSLIMCirObj*, eSLIMObjComp> fanouts;
ABC_UINT64_T tt; //truth table representing the function
int depth = 0; // the step from a input/gate node to an output node is also counted -> depth differs from depths in abc
int remaining_time = 0;
int value1 = 0;
private:
unsigned int id = 0;
// set traversal_id
unsigned int trav_id = 0;
unsigned int inSubcircuit = 0;
unsigned int inTFI = 0;
unsigned int inTFO = 0;
unsigned int isTaboo = 0;
friend eSLIMCirMan;
friend TabooList;
};
class eSLIMCirMan {
public:
eSLIMCirMan(int nObjEstimate);
eSLIMCirMan(Gia_Man_t * pGia);
eSLIMCirMan(Abc_Ntk_t * pNtk, bool simplify);
eSLIMCirMan(eSLIMCirMan& es_man, const Subcircuit& scir);
// normalises the aig
// static eSLIMCirMan eSLIMCirManFromGia(Gia_Man_t * pGia);
static ABC_UINT64_T negateTT(ABC_UINT64_T tt, unsigned int nfanin);
static ABC_UINT64_T ttNegateFanin(ABC_UINT64_T tt, unsigned int fan);
static bool ttisnormal(ABC_UINT64_T tt);
void registerTabooList(TabooList* taboo);
void unregisterTabooList();
void replace(eSLIMCirMan& replacement, const Subcircuit& subcir);
Gia_Man_t* eSLIMCirManToGia();
Abc_Ntk_t* eSLIMCirManToNtk();
Abc_Ntk_t* eSLIMCirManToMappedNtk();
void setupTimings();
bool isConst(int id) const;
bool isPi(int id) const; // or constant node
bool isPo(int id) const;
bool isGate(int id) const;
bool isConst(const eSLIMCirObj&) const;
bool isPi(const eSLIMCirObj&) const;
bool isOnCricticalPath(const eSLIMCirObj&) const;
int getNofObjs() const;
int getNofPis() const;
int getNofPos() const;
int getNofGates() const;
int getDepth() const;
const eSLIMCirObj& getObj(int id) const;
void incrementTraversalId() {traversal_id++;}
void setTraversalId(eSLIMCirObj& obj);
void setTraversalId(int n);
bool isCurrentTraversalId(const eSLIMCirObj& obj) const;
bool isCurrentTraversalId(int n) const;
void setInSubcircuit(eSLIMCirObj& obj);
void setInTFI(eSLIMCirObj& obj);
void setInTFO(eSLIMCirObj& obj);
bool inSubcircuit(const eSLIMCirObj& obj) const;
bool inTFI(const eSLIMCirObj& obj) const;
bool inTFO(const eSLIMCirObj& obj) const;
void markSubcircuit(const std::vector<int>& nodes);
void markCones(const std::vector<int>& nodes);
int addPi();
int addPo(int fanin, bool negated);
int addNode(const std::vector<int>& fanins, ABC_UINT64_T tt);
void print() const;
void print(const Subcircuit& scir) const;
eSLIMCirMan duplicate() const;
private:
bool isTaboo(const eSLIMCirObj& obj, int taboo_time) const;
void setTaboo(eSLIMCirObj& obj);
eSLIMCirObj* getpObj(int id);
const eSLIMCirObj* getpObj(int id) const;
eSLIMCirObj* getPo(int id);
static ABC_UINT64_T ttFromGiaObj(Gia_Man_t * pGia, Gia_Obj_t * pObj);
static ABC_UINT64_T ttFromNtkObj(Abc_Ntk_t * pNtk, Abc_Obj_t * pObj);
std::vector<std::unique_ptr<eSLIMCirObj>> replaceInternal(eSLIMCirMan& replacement, const Subcircuit& subcir);
void setupMarksForReplacement(eSLIMCirMan& replacement);
void clearFanouts(const Subcircuit& subcir);
void insertSorted(eSLIMCirObj* obj, std::vector<std::unique_ptr<eSLIMCirObj>>& sorted,
eSLIMCirMan& replacement, const std::unordered_map<int,int>& out_map, const std::vector<eSLIMCirObj*>& in_vec);
void insertSortedRec( eSLIMCirObj* obj, std::vector<std::unique_ptr<eSLIMCirObj>>& sorted,
eSLIMCirMan& replacement, const std::unordered_map<int,int>& out_map, const std::vector<eSLIMCirObj*>& in_vec);
void insertSortedRecRep(eSLIMCirObj* obj, std::vector<std::unique_ptr<eSLIMCirObj>>& sorted,
eSLIMCirMan& replacement, const std::unordered_map<int,int>& out_map, const std::vector<eSLIMCirObj*>& in_vec);
void processRepFanin( eSLIMCirObj* obj, eSLIMCirObj* fan, int fid, std::vector<std::unique_ptr<eSLIMCirObj>>& sorted,
eSLIMCirMan& replacement, const std::unordered_map<int,int>& out_map, const std::vector<eSLIMCirObj*>& in_vec);
void processRepPo( eSLIMCirObj* obj, eSLIMCirObj* fan, int fid, std::vector<std::unique_ptr<eSLIMCirObj>>& sorted,
eSLIMCirMan& replacement, const std::unordered_map<int,int>& out_map, const std::vector<eSLIMCirObj*>& in_vec);
void processNonGateRepFanin(eSLIMCirObj* obj, eSLIMCirObj* fan, int fid, std::vector<std::unique_ptr<eSLIMCirObj>>& sorted,
eSLIMCirMan& replacement, const std::unordered_map<int,int>& out_map, const std::vector<eSLIMCirObj*>& in_vec);
void addFans(eSLIMCirObj* out, eSLIMCirObj* in, int fin_id);
int addGiaGate(Gia_Man_t * pGia, int node_id, std::vector<int>& node_ids, std::vector<bool>& is_node_negated);
static ABC_UINT64_T sop2tt(char * pSop);
static char* tt2sop(ABC_UINT64_T tt, int nVars, Mem_Flex_t * pMan);
int insertNtkNodes(Abc_Ntk_t * pNtk, int node_id, std::unordered_map<int,int>& ids, bool simplify);
int processRedundant(const Subcircuit& subcir);
void moveNode(std::vector<std::unique_ptr<eSLIMCirObj>>& vec, std::unique_ptr<eSLIMCirObj>& pobj);
void setMarks(eSLIMCirObj& pObj, int id);
// The nodes vector contains nodes in topological order.
// This does not necessarily ensure that if a < b we have lv(a) < lv(b) (lv: the level/depth of the node)
// If nodes are sorted according to their levels i.e. a <= b iff lv(a) <= lv(b) then the nodes are also topologically sorted.
void applyLevelBasedOrdering();
void applyDFSOrdering(const std::vector<int>& po_nodes); // po_nodes must contain the node_id of each primary output
void applyDFSOrderingRec(eSLIMCirObj* obj, std::vector<std::unique_ptr<eSLIMCirObj>>& sorted);
// remove repeated fanins
// The Gia representation does not allow repeated fanins.
void simplifyDuplicateFanins();
ABC_UINT64_T removeInputFromTT(ABC_UINT64_T tt, unsigned int first_occurrence, unsigned int second_occurrence);
ABC_UINT64_T compressTT(ABC_UINT64_T tt, unsigned int input);
unsigned int nof_pis = 0;
unsigned int nof_pos = 0;
std::vector<std::unique_ptr<eSLIMCirObj>> nodes;
unsigned int last_node_id = 0;
static constexpr int const_false_id = 0;
unsigned int traversal_id = 0;
int depth = 0;
TabooList* taboo = nullptr;
friend TabooList;
template <typename SynthesisEngine, typename SelectionStrategy> friend class WindowMan;
};
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

9
src/opt/eslim/module.make
View File

@ -1,2 +1,7 @@
SRC += src/opt/eslim/relationGeneration.cpp \
src/opt/eslim/eSLIM.cpp
SRC += src/opt/eslim/eSLIM.cpp \
src/opt/eslim/eslimCirMan.cpp \
src/opt/eslim/relationGeneration.cpp \
src/opt/eslim/subcircuit.cpp \
src/opt/eslim/relationSynthesiser.cpp \
src/opt/eslim/areaEngine.cpp \
src/opt/eslim/delayEngine.cpp \

512
src/opt/eslim/relationGeneration.cpp
View File

@ -6,167 +6,419 @@
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Procedures for computing Boolean relations.]
Synopsis [SAT-based computation of Boolean relations.]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - March 2025.]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: relationGeneration.cpp,v 1.00 2025/03/17 00:00:00 Exp $]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#include <cassert>
#include <algorithm>
#include "misc/vec/vec.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
#include "misc/util/abc_global.h"
#include "relationGeneration.hpp"
ABC_NAMESPACE_HEADER_START
void * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fMapping, int fVerbose );
void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
Vec_Int_t * Gia_ManCollectNodeTfos( Gia_Man_t * p, int * pNodes, int nNodes );
Vec_Int_t * Gia_ManCollectNodeTfis( Gia_Man_t * p, Vec_Int_t * vNodes );
ABC_NAMESPACE_HEADER_END
ABC_NAMESPACE_IMPL_START
namespace eSLIM {
RelationGeneratorABC::RelationGeneratorABC(Gia_Man_t* pGia, const Subcircuit& subcir)
: RelationGenerator(pGia, subcir) {
// for (const auto& [out, inputs] : subcir.forbidden_pairs) {
for (const auto& it: subcir.forbidden_pairs) {
const auto& inputs = it.second;
inputs_in_forbidden_pairs.insert(inputs.begin(), inputs.end());
Relation::Relation(int nfanins) : output_patterns(1 << nfanins) {
}
}
Vec_Int_t* RelationGeneratorABC::getRelationImpl() {
abctime clkStart = Abc_Clock();
int nTimeOut = 600, nConfLimit = 1000000;
int i, iNode, iSatVar, Iter, Mask, nSolutions = 0, RetValue = 0;
// --------------- Modification ---------------
Gia_Man_t* pMiter = generateMiter();
// --------------- Modification ---------------
Cnf_Dat_t * pCnf = (Cnf_Dat_t*)Mf_ManGenerateCnf( pMiter, 8, 0, 0, 0, 0 );
sat_solver * pSat = (sat_solver*)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
int iLit = Abc_Var2Lit( 1, 0 ); // enumerating the care set (the miter output is 1)
int status = sat_solver_addclause( pSat, &iLit, &iLit + 1 ); assert( status );
Vec_Int_t * vSatVars = Vec_IntAlloc( Vec_IntSize(subcir.io) );
Vec_IntForEachEntry( subcir.io, iNode, i )
Vec_IntPush( vSatVars, i < subcir.nof_inputs ? 2+i : pCnf->nVars-Vec_IntSize(subcir.io)+i );
Vec_Int_t * vLits = Vec_IntAlloc( 100 );
Vec_Int_t * vRes = Vec_IntAlloc( 1000 );
for ( Iter = 0; Iter < 1000000; Iter++ )
{
int status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 );
if ( status == l_False ) { RetValue = 1; break; }
if ( status == l_Undef ) { RetValue = 0; break; }
nSolutions++;
// extract SAT assignment
Mask = 0;
Vec_IntClear( vLits );
Vec_IntForEachEntry( vSatVars, iSatVar, i ) {
Vec_IntPush( vLits, Abc_Var2Lit(iSatVar, sat_solver_var_value(pSat, iSatVar)) );
if ( sat_solver_var_value(pSat, iSatVar) )
Mask |= 1 << (Vec_IntSize(subcir.io)-1-i);
void Relation::addOutputPattern(int inputidx, std::vector<bool>&& pattern) {
lines_with_pattern += output_patterns[inputidx].empty();
output_patterns[inputidx].push_back(pattern);
}
RelationGenerator::RelationGenerator( const eSLIMCirMan& cir, const Subcircuit& subcir,
const eSLIMConfig& cfg, eSLIMLog& log)
: cir(cir), subcir(subcir), cfg(cfg), log(log),
gate2varref(cir.getNofObjs() - cir.getNofPos()),
gate2varcone(cir.getNofObjs() - cir.getNofPos()) {
setupEncoding();
}
Relation RelationGenerator::computeRelation(const eSLIMCirMan& cir, const Subcircuit& subcir,
const eSLIMConfig& cfg, eSLIMLog& log) {
RelationGenerator rgen(cir, subcir, cfg, log);
return rgen.getRelation();
}
int RelationGenerator::getNewVar() {
return max_var++;
}
void RelationGenerator::setupEncoding() {
if (cfg.approximate_relation) {
if (cfg.generate_relation_with_tfi_limit) {
encodeCircuitApproximativeBoundedTFI();
} else {
encodeCircuitApproximative();
}
} else {
// encodeCircuitFull();
encodeCircuitAffected();
}
}
void RelationGenerator::encodeGate(const eSLIMCirObj& obj, int var, const std::vector<int>& gate2var) {
int bc = popcount(obj.tt);
int tt_length = obj.getTTLength();
if (bc == 0) {
solver.addClause({-var});
} else if (bc == tt_length) {
solver.addClause({var});
} else if (bc == 1) {
return getGateEncodingUnique(obj, var, gate2var, true);
} else if (bc == tt_length - 1) {
return getGateEncodingUnique(obj, var, gate2var, false);
} else {
return getGateEncodingNaive(obj, var, gate2var);
}
}
void RelationGenerator::getGateEncodingUnique(const eSLIMCirObj& obj, int var, const std::vector<int>& gate2var, bool unique_bit) {
ABC_UINT64_T tt = obj.tt;
if (!unique_bit) {
tt = eSLIMCirMan::negateTT(tt, obj.getNFanins());
}
int bit_index = lsb(tt);
std::vector<int> clause;
int lit = unique_bit ? -var : var;
for (int i = 0; i < obj.getNFanins(); i++) {
if ((bit_index >> i) & 1 ) {
clause.push_back(-gate2var[obj.fanins[i]->node_id]);
solver.addClause({gate2var[obj.fanins[i]->node_id], lit});
} else {
clause.push_back(gate2var[obj.fanins[i]->node_id]);
solver.addClause({-gate2var[obj.fanins[i]->node_id], lit});
}
}
clause.push_back(-lit);
solver.addClause(clause);
}
void RelationGenerator::getGateEncodingNaive(const eSLIMCirObj& obj, int var, const std::vector<int>& gate2var) {
int tt_length = obj.getTTLength();
int nfans = obj.getNFanins();
std::vector<int> clause;
clause.reserve(nfans+1);
for (int i = 0; i < tt_length; i++) {
clause.clear();
for (int j = 0; j < nfans; j++) {
if ((i >> j) & 1 ) {
clause.push_back(-gate2var[obj.fanins[j]->node_id]);
} else {
clause.push_back(gate2var[obj.fanins[j]->node_id]);
}
Vec_IntPush( vRes, Mask );
if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ) )
{ RetValue = 1; break; }
if ( nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= nTimeOut ) { RetValue = 0; break; }
}
bool polarity = (obj.tt >> i) & 1;
if (polarity) {
clause.push_back(var);
} else {
clause.push_back(-var);
}
solver.addClause(clause);
}
// complement the set of input/output minterms
Vec_Int_t * vBits = Vec_IntStart( 1 << Vec_IntSize(subcir.io) );
Vec_IntForEachEntry( vRes, Mask, i )
Vec_IntWriteEntry( vBits, Mask, 1 );
Vec_IntClear( vRes );
Vec_IntForEachEntry( vBits, Mask, i )
if ( !Mask )
Vec_IntPush( vRes, i );
Vec_IntFree( vBits );
// cleanup
Vec_IntFree( vLits );
Vec_IntFree( vSatVars );
sat_solver_delete( pSat );
Gia_ManStop( pMiter );
Cnf_DataFree( pCnf );
if ( RetValue == 0 )
Vec_IntFreeP( &vRes );
return vRes;
}
Gia_Man_t * RelationGeneratorABC::generateMiter() {
Vec_Int_t * vInsOuts = subcir.io;
int nIns = subcir.nof_inputs;
Vec_Int_t * vTfo = Gia_ManCollectNodeTfos( pGia, Vec_IntEntryP(vInsOuts, nIns), Vec_IntSize(vInsOuts)-nIns );
Vec_Int_t * vTfi = Gia_ManCollectNodeTfis( pGia, vTfo );
Vec_Int_t * vInLits = Vec_IntAlloc( nIns );
Vec_Int_t * vOutLits = Vec_IntAlloc( Vec_IntSize(vInsOuts) - nIns );
Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; int i, iLit = 0;
Gia_ManFillValue( pGia );
pNew = Gia_ManStart( 1000 );
pNew->pName = Abc_UtilStrsav( pGia->pName );
Gia_ManHashAlloc( pNew );
Gia_ManForEachObjVec( vTfi, pGia, pObj, i )
if ( Gia_ObjIsCi(pObj) )
pObj->Value = Gia_ManAppendCi(pNew);
for ( i = 0; i < Vec_IntSize(vInsOuts)-nIns; i++ )
Vec_IntPush( vInLits, Gia_ManAppendCi(pNew) );
Gia_ManForEachObjVec( vTfi, pGia, pObj, i )
if ( Gia_ObjIsAnd(pObj) )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachObjVec( vTfo, pGia, pObj, i )
if ( Gia_ObjIsCo(pObj) )
pObj->Value = Gia_ObjFanin0Copy(pObj);
Gia_ManForEachObjVec( vInsOuts, pGia, pObj, i )
if ( i < nIns )
Vec_IntPush( vOutLits, pObj->Value );
else
pObj->Value = Vec_IntEntry( vInLits, i-nIns );
void RelationGenerator::encodeCircuitAffected() {
setupConstantGate();
std::vector<int> compare_nodes;
for (int i = cir.getNofObjs() - cir.getNofPos(); i < cir.getNofObjs(); i++) {
const auto obj = cir.getObj(i);
int fid = obj.fanins[0]->node_id;
// multiple POs can use the same fanin
// if gate2varref[fid] is not 0 we have already seen it
if (cir.inTFO(obj) && !gate2varref[fid]) {
gate2varref[fid] = getNewVar();
gate2varcone[fid] = getNewVar();
compare_nodes.push_back(fid);
}
}
setupEqualityConstraints(compare_nodes);
for (int i = cir.getNofObjs() - cir.getNofPos() - 1; i > cir.getNofPis(); i--) {
if (gate2varref[i]) { // the gate is connected to a PO that is in the TFO of the subcircuit
const auto obj = cir.getObj(i);
for (const auto& f : obj.fanins) {
int fid = f->node_id;
if (gate2varref[fid] == 0) {
gate2varref[fid] = getNewVar();
}
}
encodeGate(obj, gate2varref[i], gate2varref);
if (cir.inTFO(obj) && !cir.inSubcircuit(obj)) {
// For an input in a forbidden pair no successors needs to be processed before
gate2varcone[i] = gate2varcone[i] ? gate2varcone[i] : getNewVar();
for (const auto& f : obj.fanins) {
int fid = f->node_id;
if (cir.inSubcircuit(*f) || cir.inTFO(*f)) {
if (gate2varcone[fid] == 0) {
gate2varcone[fid] = getNewVar();
}
} else {
gate2varcone[fid] = gate2varref[fid];
}
}
encodeGate(obj, gate2varcone[i], gate2varcone);
} else if (gate2varcone[i] == 0) {
gate2varcone[i] = gate2varref[i];
}
}
}
Gia_ManIncrementTravId(pGia);
Gia_ManForEachObjVec( subcir.nodes, pGia, pObj, i ) {
Gia_ObjSetTravIdCurrent(pGia, pObj);
for (int i = 1; i <= cir.getNofPis(); i++) {
if (gate2varref[i] != 0) {
cone_input_variables.push_back(gate2varref[i]);
// Simplifies handling of variables
if (gate2varcone[i] == 0) {
gate2varcone[i] = gate2varref[i];
}
}
}
}
Gia_ManForEachObjVec( vTfo, pGia, pObj, i )
// in case there are forbidden pairs we have to ensure that nodes from the sucircuit are not added
if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsTravIdCurrent(pGia, pObj) )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachObjVec( vTfo, pGia, pObj, i )
if ( Gia_ObjIsCo(pObj) )
iLit = Gia_ManHashOr( pNew, iLit, Gia_ManHashXor(pNew, Gia_ObjFanin0Copy(pObj), pObj->Value) );
// --------------- Modification ---------------
// In case there are forbidden pairs, the outputs of the subcircuit influence the inputs of the subcircuit.
// Therefore, we need the values of the inputs in the version of the circuit that is affected by the new outputs.
for (int inp : inputs_in_forbidden_pairs) {
int node_id = Vec_IntEntry(vInsOuts, inp);
pObj = Gia_ManObj(pGia, node_id);
Vec_IntWriteEntry(vOutLits, inp, pObj->Value);
void RelationGenerator::encodeCircuitApproximative() {
setupConstantGate();
std::vector<int> compare_nodes = markRestrictedCone();
int max_node = *std::max_element(compare_nodes.begin(), compare_nodes.end());
for (int i = max_node; i > cir.getNofPis(); i--) {
const auto obj = cir.getObj(i);
if (gate2varref[i] != 0) {
for (auto& f : obj.fanins ) {
if (gate2varref[f->node_id] == 0) {
gate2varref[f->node_id] = getNewVar();
gate2varcone[f->node_id] = gate2varref[f->node_id];
}
}
encodeGate(obj, gate2varref[i], gate2varref);
if (!cir.inSubcircuit(obj) && gate2varcone[i] != gate2varref[i]) {
encodeGate(obj, gate2varcone[i], gate2varcone);
}
}
}
// --------------- Modification ---------------
Gia_ManAppendCo( pNew, iLit );
Vec_IntForEachEntry( vOutLits, iLit, i )
Gia_ManAppendCo( pNew, iLit );
Vec_IntFree( vTfo );
Vec_IntFree( vTfi );
Vec_IntFree( vInLits );
Vec_IntFree( vOutLits );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia) );
return pNew;
for (int i = 1; i <= cir.getNofPis(); i++) {
if (gate2varref[i] != 0) {
cone_input_variables.push_back(gate2varref[i]);
}
}
setupEqualityConstraints(compare_nodes);
}
}
void RelationGenerator::encodeCircuitApproximativeBoundedTFI() {
setupConstantGate();
std::vector<int> compare_nodes = markRestrictedCone();
std::vector<unsigned char> counts(cir.getNofObjs() - cir.getNofPos());
int max_node = *std::max_element(compare_nodes.begin(), compare_nodes.end());
for (int i = max_node; i > cir.getNofPis(); i--) {
const auto obj = cir.getObj(i);
if (gate2varref[i] != 0) {
if (cir.inTFO(obj) || cir.inSubcircuit(obj)) {
counts[i] = cfg.relation_tfi_bound + 1;
} else if (counts[i] == 0) {
cone_input_variables.push_back(gate2varref[i]);
continue;
}
for (auto& f : obj.fanins ) {
if (gate2varref[f->node_id] == 0) {
gate2varref[f->node_id] = getNewVar();
gate2varcone[f->node_id] = gate2varref[f->node_id];
counts[f->node_id] = std::max(counts[f->node_id], static_cast<unsigned char>(counts[i] - 1));
}
}
encodeGate(obj, gate2varref[i], gate2varref);
if (!cir.inSubcircuit(obj) && gate2varcone[i] != gate2varref[i]) {
encodeGate(obj, gate2varcone[i], gate2varcone);
}
}
}
for (int i = 1; i <= cir.getNofPis(); i++) {
if (gate2varref[i] != 0) {
cone_input_variables.push_back(gate2varref[i]);
}
}
setupEqualityConstraints(compare_nodes);
}
std::vector<int> RelationGenerator::markRestrictedCone() {
std::vector<unsigned char> counts(cir.getNofObjs() - cir.getNofPos());
for (int i : subcir.outputs) {
gate2varref[i] = getNewVar();
gate2varcone[i] = getNewVar();
counts[i] = cfg.relation_tfo_bound;
}
if (cfg.relation_tfo_bound == 0) {
std::vector<int> nodes(subcir.outputs.begin(), subcir.outputs.end());
return nodes;
}
std::vector<int> nodes;
for (int i = subcir.outputs[0] + 1; i < cir.getNofObjs() - cir.getNofPos(); i++) { //outputs are ordered
const auto obj = cir.getObj(i);
if (!cir.inTFO(obj) || cir.inSubcircuit(obj)) {
continue;
}
unsigned char x = 0;
for (auto& f : obj.fanins) {
x = std::max(x, counts[f->node_id]);
}
if (x > 0) {
gate2varcone[i] = getNewVar();
gate2varref[i] = getNewVar();
counts[i] = x - 1;
if (x == 1) {
nodes.push_back(i);
}
}
}
std::set<int> used;
for (int i = cir.getNofObjs() - cir.getNofPos(); i < cir.getNofObjs(); i++) {
const auto obj = cir.getObj(i);
if (cir.inTFO(obj) && counts[obj.fanins[0]->node_id] > 0 && used.find(obj.fanins[0]->node_id) == used.end()) {
nodes.push_back(obj.fanins[0]->node_id);
used.insert(obj.fanins[0]->node_id);
}
}
return nodes;
}
void RelationGenerator::setupConstantGate() {
int const_var = getNewVar();
gate2varref[0] = const_var;
gate2varcone[0] = const_var;
solver.addClause({-const_var});
}
void RelationGenerator::setupEqualityConstraints(const std::vector<int>& nodes) {
mode_selection_variable = getNewVar();
std::vector<int> one_different {-mode_selection_variable};
for (int cnd : nodes) {
int eq_var = getNewVar();
equality_variables.push_back(eq_var);
getEqualityClauses(gate2varref[cnd], gate2varcone[cnd], eq_var);
one_different.push_back(-eq_var);
}
solver.addClause(one_different);
}
void RelationGenerator::getEqualityClauses(int x, int y, int aux) {
solver.addClause({x, -y, -aux});
solver.addClause({-x, y, -aux});
solver.addClause({x, y, aux});
solver.addClause({-x, -y, aux});
}
int RelationGenerator::findConflict(double& timeout, int mode_selection) {
abctime time_start = Abc_Clock();
int solver_status = solver.solve(timeout, {mode_selection});
double solver_time = (double)1.0*(Abc_Clock() - time_start)/CLOCKS_PER_SEC;
log.cummulative_sat_runtime_relation_generation += solver_time;
log.max_sat_runtime_relation_generation = std::max(log.max_sat_runtime_relation_generation, solver_time);
// log.cummulative_sat_runtime_relation_generation += solver.getRunTime();
log.nof_sat_calls_relation_generation++;
return solver_status;
}
int RelationGenerator::reduceConflict(double& timeout, const std::vector<int>& cone_input,
const std::vector<int>& subcircuit_output, const std::vector<int>& equality) {
solver.assume(cone_input);
solver.assume(subcircuit_output);
solver.assume(equality);
abctime time_start = Abc_Clock();
int status = solver.solve(timeout);
double solver_time = (double)1.0*(Abc_Clock() - time_start)/CLOCKS_PER_SEC;
log.cummulative_sat_runtime_relation_generation += solver_time;
log.max_sat_runtime_relation_generation = std::max(log.max_sat_runtime_relation_generation, solver_time);
// log.cummulative_sat_runtime_relation_generation += solver.getRunTime();
log.nof_sat_calls_relation_generation++;
return status;
}
Relation RelationGenerator::getRelation() {
std::vector<int> subcircuit_input_variables;
subcircuit_input_variables.reserve(subcir.inputs.size());
for (int sin : subcir.inputs) {
int var = gate2varcone[sin];
subcircuit_input_variables.push_back(var);
}
std::vector<int> subcircuit_output_variables;
subcircuit_output_variables.reserve(subcir.outputs.size());
// outputs in forbidden pairs must not removed
std::vector<bool> outputs_to_keep(subcir.outputs.size(), false);
for (int i = 0; i < subcir.outputs.size(); i++) {
int sout = subcir.outputs[i];
int var = gate2varcone[sout];
subcircuit_output_variables.push_back(var);
if (subcir.forbidden_pairs.find(sout) != subcir.forbidden_pairs.end()) {
outputs_to_keep[i] = true;
}
}
Relation rel(subcir.inputs.size());
int solver_status;
double timeout = cfg.relation_generation_timeout;
abctime time_start = Abc_Clock();
while( (solver_status=findConflict(timeout, mode_selection_variable)) == 10) {
timeout -= (double)1.0*(Abc_Clock() - time_start)/CLOCKS_PER_SEC;
time_start = Abc_Clock();
if (timeout <= 0) {
rel.status = false;
return rel;
}
std::vector<int> cone_in_assm = solver.getValues(cone_input_variables);
std::vector<int> sin_assm = solver.getValues(subcircuit_input_variables);
std::vector<int> sout_assm = solver.getValues(subcircuit_output_variables);
int status = reduceConflict(timeout, cone_in_assm, sout_assm, equality_variables);
if (status != 20) {
assert (status != 10);
rel.status = false;
return rel;
}
assert (status == 20);
std::vector<int> blocking_clause {-mode_selection_variable};
for (int i = 0; i < subcir.inputs.size(); i++) {
blocking_clause.push_back(-sin_assm[i]);
}
std::vector<bool> pattern (2*subcir.outputs.size(), false);
for (int i = 0; i < subcir.outputs.size(); i++) {
if (solver.isFailed(sout_assm[i]) || outputs_to_keep[i]) {
pattern[2*i] = true;
pattern[2*i + 1] = sout_assm[i] < 0; // at least one output must be assigned differently in order to preserve the function
blocking_clause.push_back(-sout_assm[i]);
}
}
solver.addClause(blocking_clause);
rel.addOutputPattern(assignment2bvindex(sin_assm), std::move(pattern));
}
if (solver_status != 20) {
rel.status = false;
}
return rel;
}
int RelationGenerator::assignment2bvindex(const std::vector<int>& assm) {
int idx = 0;
for (int i = 0; i < assm.size(); i++) {
if (assm[i] > 0) {
idx |= 1 << i;
}
}
return idx;
}
}
ABC_NAMESPACE_IMPL_END

222
src/opt/eslim/relationGeneration.hpp
View File

@ -6,190 +6,114 @@
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Procedures for computing Boolean relations.]
Synopsis [SAT-based computation of Boolean relations.]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - March 2025.]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: relationGeneration.hpp,v 1.00 2025/03/17 00:00:00 Exp $]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__OPT__ESLIM__RELATIONGENERATION_h
#define ABC__OPT__ESLIM__RELATIONGENERATION_h
#ifndef ABC__OPT__ESLIM__RELATIONGENERATION_hpp
#define ABC__OPT__ESLIM__RELATIONGENERATION_hpp
#include <vector>
#include <unordered_map>
#include <unordered_set>
#include "misc/util/abc_namespaces.h"
#include <misc/util/abc_global.h>
#include "aig/gia/gia.h"
#include "misc/util/utilTruth.h" // ioResub.h depends on utilTruth.h
#include "base/io/ioResub.h"
#include "eslimCirMan.hpp"
#include "cadicalSolver.hpp"
#include "subcircuit.hpp"
#include "utils.hpp"
// #include "satInterfaces.hpp"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
template<class Derived>
class RelationGenerator {
class RelationGenerator;
class Relation{
public:
static Abc_RData_t* computeRelation(Gia_Man_t* gia_man, const Subcircuit& subcir);
Relation(int nfanins);
const std::vector<std::vector<bool>>& getPattern(int id) const {return output_patterns[id];}
int getNPatterns() const {return output_patterns.size();}
int getPatternSize(int id) const {return output_patterns[id].size();}
unsigned int getNLinesWithPattern() const {return lines_with_pattern;}
bool getStatus() const {return status;}
private:
Gia_Man_t* pGia;
const Subcircuit& subcir;
RelationGenerator(Gia_Man_t* pGia, const Subcircuit& subcir);
void setup();
Vec_Int_t* getRelation();
static Abc_RData_t* constructABCRelationRepresentation(Vec_Int_t * patterns, int nof_inputs, int nof_outputs);
// Reimplementation with disabled prints
// We do not want to modify code in other parts of ABC
static Abc_RData_t * Abc_RData2Rel( Abc_RData_t * p );
// Each entry of the first vector level corresponds to an input assignment.
// The second level lists all conflicting output assignments.
// The third lists the individual conflicting output assignments.
// One output is represented by two bits, the first bit determines if this output is present the conflicting output assignments
// and the second indicate if it is true or false
void addOutputPattern(int inputidx, std::vector<bool>&& pattern);
std::vector<std::vector<std::vector<bool>>> output_patterns;
friend Derived;
};
unsigned int lines_with_pattern = 0;
bool status = true;
// The class almost entirely duplicates the functionality provided by Gia_ManGenIoCombs in giaQBF.c
// But the implementation in this class allows to take forbidden pairs into account.
class RelationGeneratorABC : public RelationGenerator<RelationGeneratorABC> {
private:
RelationGeneratorABC(Gia_Man_t* pGia, const Subcircuit& subcir);
void setupImpl() {};
Vec_Int_t* getRelationImpl();
Gia_Man_t * generateMiter();
std::unordered_set<int> inputs_in_forbidden_pairs;
friend RelationGenerator;
};
class RelationGenerator {
// Add other engine for the generation of relations
// class MyRelationGenerator : public RelationGenerator<MyRelationGenerator> {
// private:
// void setupImpl()
// Vec_Int_t* getRelationImpl();
// friend RelationGenerator;
// };
public:
static Relation computeRelation(const eSLIMCirMan& cir, const Subcircuit& subcir, const eSLIMConfig& cfg, eSLIMLog& log);
private:
const eSLIMCirMan& cir;
const Subcircuit& subcir;
const eSLIMConfig& cfg;
eSLIMLog& log;
int max_var = 1;
std::vector<int> gate2varref;
std::vector<int> gate2varcone;
std::vector<int> equality_variables;
std::vector<int> cone_input_variables;
int mode_selection_variable;
CadicalSolver solver;
RelationGenerator(const eSLIMCirMan& cir, const Subcircuit& subcir, const eSLIMConfig& cfg, eSLIMLog& log);
void setupEncoding();
void encodeCircuitAffected();
void encodeCircuitApproximative();
void encodeCircuitApproximativeBoundedTFI();
std::vector<int> markRestrictedCone();
void setupConstantGate();
void setupEqualityConstraints(const std::vector<int>& nodes);
Relation getRelation();
void encodeGate(const eSLIMCirObj& obj, int var, const std::vector<int>& gate2var);
void getGateEncodingUnique(const eSLIMCirObj& obj, int var, const std::vector<int>& gate2var, bool unique_bit);
void getGateEncodingNaive(const eSLIMCirObj& obj, int var, const std::vector<int>& gate2var);
void getEqualityClauses(int x, int y, int aux);
int assignment2bvindex(const std::vector<int>& assm);
int findConflict(double& timeout, int mode_selection);
int reduceConflict(double& timeout, const std::vector<int>& cone_input, const std::vector<int>& subcircuit_output, const std::vector<int>& equality);
template <typename T>
inline RelationGenerator<T>::RelationGenerator(Gia_Man_t* pGia, const Subcircuit& subcir)
: pGia(pGia), subcir(subcir) {
}
int getNewVar();
template <typename T>
inline Abc_RData_t* RelationGenerator<T>::computeRelation(Gia_Man_t* gia_man, const Subcircuit& subcir) {
T generator(gia_man, subcir);
generator.setup();
Vec_Int_t* relation_patterns_masks = generator.getRelation();
if ( relation_patterns_masks == NULL ) {
return nullptr;
}
int nof_inputs = subcir.nof_inputs;
int nof_outputs = Vec_IntSize(subcir.io) - subcir.nof_inputs;
Abc_RData_t* r = constructABCRelationRepresentation(relation_patterns_masks, nof_inputs, nof_outputs);
Vec_IntFree(relation_patterns_masks);
return r;
}
};
template <typename T>
inline Abc_RData_t* RelationGenerator<T>::constructABCRelationRepresentation(Vec_Int_t * patterns, int nof_inputs, int nof_outputs) {
int i, mask;
int nof_vars = nof_inputs + nof_outputs;
Abc_RData_t* p = Abc_RDataStart( nof_inputs, nof_outputs, Vec_IntSize(patterns) );
Vec_IntForEachEntry( patterns, mask, i ) {
for ( int k = 0; k < nof_vars; k++ ) {
if ( (mask >> (nof_vars-1-k)) & 1 ) {
if ( k < nof_inputs ) {
Abc_RDataSetIn( p, k, i );
} else {
Abc_RDataSetOut( p, 2*(k-nof_inputs)+1, i );
}
} else {
if ( k >= nof_inputs ) {
Abc_RDataSetOut( p, 2*(k-nof_inputs), i );
}
}
}
}
Abc_RData_t* p2 = Abc_RData2Rel(p);
Abc_RDataStop(p);
return p2;
}
template <typename T>
inline Abc_RData_t * RelationGenerator<T>::Abc_RData2Rel( Abc_RData_t * p ) {
assert( p->nIns < 64 );
assert( p->nOuts < 32 );
int w;
Vec_Wrd_t * vSimsIn2 = Vec_WrdStart( 64*p->nSimWords );
Vec_Wrd_t * vSimsOut2 = Vec_WrdStart( 64*p->nSimWords );
for ( w = 0; w < p->nIns; w++ )
Abc_TtCopy( Vec_WrdEntryP(vSimsIn2, w*p->nSimWords), Vec_WrdEntryP(p->vSimsIn, w*p->nSimWords), p->nSimWords, 0 );
for ( w = 0; w < p->nOuts; w++ )
Abc_TtCopy( Vec_WrdEntryP(vSimsOut2, w*p->nSimWords), Vec_WrdEntryP(p->vSimsOut, (2*w+1)*p->nSimWords), p->nSimWords, 0 );
Vec_Wrd_t * vTransIn = Vec_WrdStart( 64*p->nSimWords );
Vec_Wrd_t * vTransOut = Vec_WrdStart( 64*p->nSimWords );
Extra_BitMatrixTransposeP( vSimsIn2, p->nSimWords, vTransIn, 1 );
Extra_BitMatrixTransposeP( vSimsOut2, p->nSimWords, vTransOut, 1 );
Vec_WrdShrink( vTransIn, p->nPats );
Vec_WrdShrink( vTransOut, p->nPats );
Vec_Wrd_t * vTransInCopy = Vec_WrdDup(vTransIn);
Vec_WrdUniqify( vTransInCopy );
// if ( Vec_WrdSize(vTransInCopy) == p->nPats )
// printf( "This resub problem is not a relation.\n" );
// create the relation
Abc_RData_t * pNew = Abc_RDataStart( p->nIns, 1 << (p->nOuts-1), Vec_WrdSize(vTransInCopy) );
pNew->nOuts = p->nOuts;
int i, k, n, iLine = 0; word Entry, Entry2;
Vec_WrdForEachEntry( vTransInCopy, Entry, i ) {
for ( n = 0; n < p->nIns; n++ )
if ( (Entry >> n) & 1 )
Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(pNew->vSimsIn, n*pNew->nSimWords), iLine );
Vec_WrdForEachEntry( vTransIn, Entry2, k ) {
if ( Entry != Entry2 )
continue;
Entry2 = Vec_WrdEntry( vTransOut, k );
assert( Entry2 < (1 << p->nOuts) );
Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(pNew->vSimsOut, Entry2*pNew->nSimWords), iLine );
}
iLine++;
}
assert( iLine == pNew->nPats );
Vec_WrdFree( vTransOut );
Vec_WrdFree( vTransInCopy );
Vec_WrdFree( vTransIn );
Vec_WrdFree( vSimsIn2 );
Vec_WrdFree( vSimsOut2 );
return pNew;
}
template <typename T>
inline void RelationGenerator<T>::setup() {
static_cast<T*>(this)->setupImpl();
}
template <typename T>
inline Vec_Int_t* RelationGenerator<T>::getRelation() {
return static_cast<T*>(this)->getRelationImpl();
}
}
ABC_NAMESPACE_CXX_HEADER_END
#endif
#endif

612
src/opt/eslim/relationSynthesiser.cpp Normal file
View File

@ -0,0 +1,612 @@
/**CFile****************************************************************
FileName [relationSynthesiser.cpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Base class for SAT-based synthesis]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#include <cassert>
#include "relationSynthesiser.hpp"
ABC_NAMESPACE_IMPL_START
namespace eSLIM {
RelationSynthesiser::RelationSynthesiser(const Relation& relation, const Subcircuit& subcir, unsigned int max_size, const eSLIMConfig& cfg, eSLIMLog& log)
: relation(relation), subcir(subcir),
max_size(max_size), config(cfg), log(log) {
setupEncoding();
}
double RelationSynthesiser::getDynamicTimeout(int size) {
if (log.nof_sat_calls_per_size[size] > config.minimum_dynamic_timeout_sample_size) {
return std::max(static_cast<double>(config.minimum_sat_timeout), static_cast<double>(log.cummulative_sat_runtimes_per_size[size]) / (1000*log.nof_sat_calls_per_size[size])); //logged timings are given in ms
} else {
return config.base_sat_timeout;
}
}
unsigned int RelationSynthesiser::getSizeFromActivationVars(const std::vector<bool>& model) {
unsigned int sz = 0;
for (int i = 0; i < max_size; i++) {
if (model[gate_activation_variables[i]]) {
sz++;
} else {
break;
}
}
return sz;
}
unsigned int RelationSynthesiser::getSizeFromActivationVars() {
unsigned int sz = 0;
for (int i = 0; i < max_size; i++) {
if (solver.getValue(gate_activation_variables[i])) {
sz++;
} else {
break;
}
}
return sz;
}
void RelationSynthesiser::logRun(int status, unsigned int size) {
log.cummulative_sat_runtime_synthesis += solver.getRunTime();
log.max_sat_runtime_synthesis = std::max(log.max_sat_runtime_synthesis, solver.getRunTime());
log.nof_sat_calls_synthesis++;
if (status == 10) {
log.cummulative_sat_runtimes_per_size[size] += solver.getRunTime();
log.nof_sat_calls_per_size[size] ++;
} else if (status == 20) { //if the solver does not report sat the formula is unsat or there was a timeout
log.cummulative_unsat_runtimes_per_size[size] += solver.getRunTime();
log.nof_unsat_calls_per_size[size] ++;
}
}
std::vector<int> RelationSynthesiser::getSizeAssumption(int size) {
std::vector<int> assumptions;
assumptions.reserve(max_size - size);
for (int i = size; i < max_size; i++) {
assumptions.push_back(-gate_activation_variables[i]);
}
return assumptions;
}
eSLIMCirMan RelationSynthesiser::getReplacement(const std::vector<bool>& model, int size) {
assert (model.size() > 0);
eSLIMCirMan circ(subcir.inputs.size() + subcir.outputs.size() + size);
for (int i = 0; i < subcir.inputs.size(); i++) {
circ.addPi();
}
for (int i = 0; i < size; i++) {
std::vector<int> fanins;
for (int j = 0; j < selection_variables[i].size(); j++) {
if (model[selection_variables[i][j]]) {
fanins.push_back(j+1);
}
}
ABC_UINT64_T tt = 0;
for (int j = 0; j < gate_definition_variables[i].size(); j++) {
int idx = j + 1;
if (model[gate_definition_variables[i][j]]) {
tt |= static_cast<ABC_UINT64_T>(1) << idx;
}
}
circ.addNode(fanins, tt);
}
// outputs
for (int i = 0; i < subcir.outputs.size(); i++) {
for (int j = 0; j < max_size; j++) {
if (model[gate_output_variables[j][i]]) {
circ.addPo(subcir.inputs.size() + j + 1, false);
goto end;
}
}
for (int j = 0; j < subcir.inputs.size(); j++) {
if (model[gate_output_variables[max_size + j][i]]) {
circ.addPo(j + 1, false);
goto end;
}
}
if (model[gate_output_variables.back()[i]]) {
circ.addPo(0, false);
}
end:;
}
return circ;
}
void RelationSynthesiser::setupEncoding() {
setupVariables();
setupStructuralConstraints();
setupSymmetryBreaking();
setupEquivalenceConstraints();
}
void RelationSynthesiser::setupVariables() {
gate_activation_variables.reserve(max_size);
selection_variables.reserve(max_size);
gate_definition_variables.reserve(max_size);
gate_variables.reserve(max_size);
is_ith_fanin_variable.reserve(max_size);
for (int i = 0; i < max_size; i++) {
gate_activation_variables.push_back(getNewVariable());
selection_variables.push_back(getNewVariableVector(subcir.inputs.size() + i));
gate_definition_variables.push_back(getNewVariableVector(pow2(config.gate_size) - 1));
// The replacement circuit shall be normal so we ignore the all-false-behaviour
int normality_offset = relation.getPatternSize(0) > 0;
gate_variables.push_back(getNewVariableVector(relation.getNLinesWithPattern() - normality_offset));
std::vector<std::vector<int>> fanin_vars;
for (int j = 0; j < config.gate_size; j++) {
std::vector<int> fvs(subcir.inputs.size() + i, 0);
for (int k = j; k < subcir.inputs.size() + i - config.gate_size + j + 1; k++) {
fvs[k] = getNewVariable();
}
fanin_vars.push_back(fvs);
}
is_ith_fanin_variable.push_back(fanin_vars);
}
gate_output_variables.reserve(max_size + subcir.inputs.size() + 1);
for (int i = 0; i < max_size + subcir.inputs.size() + 1; i++) {
gate_output_variables.push_back(getNewVariableVector(subcir.outputs.size()));
}
}
void RelationSynthesiser::setupStructuralConstraints() {
constrainSelectionVariables();
constraintGateOutputVariables();
setupActivationCompatibilityConstraints();
if (config.aig) {
setupAigerConstraints();
}
}
void RelationSynthesiser::setupSymmetryBreaking() {
addNonTrivialConstraint();
addUseAllStepsConstraint();
// addNoReapplicationConstraint();
// addOrderedStepsConstraint();
}
void RelationSynthesiser::setupIsFaninVariables(int gtidx, const std::vector<std::vector<int>>& counter_vars) {
// If we have 3 inputs and gates with two fanins then the first fanin of the first gate can be input 1 or 2 but not input 3.
int noptions = subcir.inputs.size() + gtidx - config.gate_size + 1;
for (int i = 0; i < config.gate_size; i++) {
solver.addClause({-counter_vars[i][i], is_ith_fanin_variable[gtidx][i][i]});
solver.addClause({counter_vars[i][i], -is_ith_fanin_variable[gtidx][i][i]});
int offset = (i == config.gate_size - 1); // we do not use block variables for the last selection variables
for (int j = i + 1; j < i + noptions - offset; j++) {
solver.addClause({counter_vars[j - 1][i], counter_vars[j][i], -is_ith_fanin_variable[gtidx][i][j]});
solver.addClause({counter_vars[j - 1][i], -counter_vars[j][i], is_ith_fanin_variable[gtidx][i][j]});
}
}
solver.addClause({selection_variables[gtidx].back(), -is_ith_fanin_variable[gtidx].back().back()});
solver.addClause({-selection_variables[gtidx].back(), is_ith_fanin_variable[gtidx].back().back()});
}
void RelationSynthesiser::constrainSelectionVariables() {
int start = 0;
// if the subcircuit has k inputs and gates have k fanins each input is a fanin of the first gate
if (selection_variables[0].size() == config.gate_size) {
start = 1;
for (int j = 0; j < config.gate_size; j++) {
solver.addClause({selection_variables[0][j]});
solver.addClause({is_ith_fanin_variable[0][j][j]});
}
}
for (int i = start; i < max_size; i++) {
std::vector<std::vector<int>> counter_vars = addSequentialCounter(selection_variables[i], config.gate_size);
setupIsFaninVariables(i, counter_vars);
}
}
void RelationSynthesiser::constraintGateOutputVariables() {
// If the activation variable is false then the gate must not be an output
for (int i = 0; i < max_size; i++) {
for (int v : gate_output_variables[i]) {
solver.addClause({gate_activation_variables[i], -v});
}
}
for (int i = 0; i < subcir.outputs.size(); i++) {
std::vector<int> clause;
clause.reserve(max_size + subcir.inputs.size() + 1);
for (int j = 0; j < max_size + subcir.inputs.size() + 1; j++) {
clause.push_back(gate_output_variables[j][i]);
}
addCardinalityConstraint(clause, 1);
}
}
void RelationSynthesiser::addGateValueConstraint(int gtidx, int gt_val, const std::vector<int>& fanin_variables) {
// If all fanins are 0, then the gate yields 0
std::vector<int> clause {-gate_activation_variables[gtidx]};
clause.reserve(config.gate_size + 3);
for (int j = 0; j < config.gate_size; j++) {
clause.push_back(fanin_variables[j]);
}
clause.push_back(-gt_val);
solver.addClause(clause);
clause.push_back(0);
for (int i = 1; i < pow2(config.gate_size); i++) { // we consider normal gates -> the all-0-behaviour does not need to be considered
for (int j = 0; j < config.gate_size; j++) {
clause[j + 1] = abs(clause[j + 1]) * (1-2*getTTValue(i, j));
}
int gdv = gate_definition_variables[gtidx][i - 1]; // we do not use a gdv for the all-0-behaviour
clause[config.gate_size + 1] = -gdv;
clause[config.gate_size + 2] = gt_val;
solver.addClause(clause);
clause[config.gate_size + 1] = gdv;
clause[config.gate_size + 2] = -gt_val;
solver.addClause(clause);
}
}
std::vector<int> RelationSynthesiser::setupFaninVariables(int gtidx, int tt_line, int pidx) {
int noptions = subcir.inputs.size() + gtidx - config.gate_size + 1;
std::vector<int> fanin_variables = getNewVariableVector(config.gate_size);
for (int i = 0; i < config.gate_size; i++) {
int bound = i + noptions < subcir.inputs.size() ? i + noptions : subcir.inputs.size();
for (int j = i; j < bound; j++) {
if (getTTValue(tt_line, j)) {
solver.addClause({-is_ith_fanin_variable[gtidx][i][j], fanin_variables[i]});
} else {
solver.addClause({-is_ith_fanin_variable[gtidx][i][j], -fanin_variables[i]});
}
}
for (int j = subcir.inputs.size(); j < i + noptions; j++) {
solver.addClause({-is_ith_fanin_variable[gtidx][i][j], gate_variables[j - subcir.inputs.size()][pidx], -fanin_variables[i]});
solver.addClause({-is_ith_fanin_variable[gtidx][i][j], -gate_variables[j - subcir.inputs.size()][pidx], fanin_variables[i]});
}
}
return fanin_variables;
}
void RelationSynthesiser::setupGateValues() {
int pidx = 0;
for (int i = 1; i < relation.getNPatterns(); i++) {
if (relation.getPatternSize(i) > 0) {
for (int j = 0; j < max_size; j++) {
std::vector<int> fanin_variables = setupFaninVariables(j, i, pidx);
addGateValueConstraint(j, gate_variables[j][pidx], fanin_variables);
}
pidx++;
}
}
}
void RelationSynthesiser::setupEquivalenceConstraints() {
setupGateValues();
// normal circuit: all-0-behaviour is ignored
int pidx = 0;
for (int i = 1; i < relation.getNPatterns(); i++) {
std::vector<int> output_vars (subcir.outputs.size(), 0);
const auto& patterns = relation.getPattern(i);
for (const auto& p : patterns) {
assert(2 * subcir.outputs.size() == p.size());
std::vector<int> cl;
for (int j = 0; j < subcir.outputs.size(); j++) {
if (p[2*j]) {
if (output_vars[j] == 0) {
output_vars[j] = setupOutputVariable(j, i, pidx);
}
if (p[2*j + 1]) {
cl.push_back(output_vars[j]);
} else {
cl.push_back(-output_vars[j]);
}
}
}
solver.addClause(cl);
}
pidx += !patterns.empty();
}
}
void RelationSynthesiser::setupActivationCompatibilityConstraints() {
for (int i = 1; i < max_size; i++) {
solver.addClause({-gate_activation_variables[i], gate_activation_variables[i-1]});
}
}
int RelationSynthesiser::setupOutputVariable(int output_index, int tt_index, int pattern_idx) {
int var = getNewVariable();
std::vector<int> clause;
for (int i = 0; i < max_size; i++) {
clause.assign({-gate_activation_variables[i], -gate_output_variables[i][output_index], -gate_variables[i][pattern_idx], var});
solver.addClause(clause);
clause[2] = -clause[2];
clause[3] = -clause[3];
solver.addClause(clause);
}
for (int i = 0; i < subcir.inputs.size(); i++) {
if (getTTValue(tt_index, i)) {
clause.assign({-gate_output_variables[i + max_size][output_index], var});
} else {
clause.assign({-gate_output_variables[i + max_size][output_index], -var});
}
solver.addClause(clause);
}
clause.assign({-gate_output_variables.back()[output_index], -var});
solver.addClause(clause);
return var;
}
void RelationSynthesiser::setupAigerConstraints() {
assert (config.gate_size == 2);
for (int i = 0; i < max_size; i++) {
solver.addClause({-gate_definition_variables[i][0], -gate_definition_variables[i][1], gate_definition_variables[i][2]});
}
}
void RelationSynthesiser::addCardinalityConstraint(const std::vector<int>& vars, unsigned int cardinality, int activator) {
assert (cardinality > 0);
assert (vars.size() >= cardinality);
if (vars.size() == cardinality) {
std::vector<int> clause;
if (activator != 0) {
clause.push_back(activator);
}
for (int var : vars) {
clause.push_back(var);
solver.addClause(clause);
clause.pop_back();
}
} else {
// CHECK: is the naive encoding better?
if (activator == 0) {
if (cardinality == 1) {
addNaiveIs1CardinalityConstraint(vars);
} else if (cardinality == 2) {
addNaiveIs2CardinalityConstraint(vars);
} else {
addSequentialCounter(vars, cardinality, activator);
}
} else {
addSequentialCounter(vars, cardinality, activator);
}
}
}
// see Carsten Sinz: Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
// As we want that exactly cardinality many variables are set to true we need additional constraints.
// Because of this reason we cannot use the single polarity encoding presented in the paper
std::vector<std::vector<int>> RelationSynthesiser::addSequentialCounter(const std::vector<int>& vars, unsigned int cardinality, int activator) {
std::vector<std::vector<int>> component_outputs;
component_outputs.push_back({vars.front()});
assert (vars.size() > cardinality);
for (int i = 1; i < vars.size() - 1; i++) {
std::vector<int> current_component_outputs;
int v = vars[i];
int in_var = v;
for (int j = 0; j < component_outputs.back().size(); j++) {
int orv = getNewVariable();
defineDisjunction(orv, {in_var, component_outputs.back()[j]}, activator);
current_component_outputs.push_back(orv);
if (j < cardinality - 1) {
in_var = getNewVariable();
defineConjunction(in_var, {v, component_outputs.back()[j]}, activator);
} else {
solver.addClause({-component_outputs.back().back(), -v});
}
}
if (component_outputs.back().size() < cardinality) {
current_component_outputs.push_back(in_var);
}
component_outputs.push_back(current_component_outputs);
}
solver.addClause({-component_outputs.back().back(), -vars.back()});
// Either subcircuit_outputs.back() is true or subcircuit_outputs[-2] and vars.back() is true
std::vector<int> clause {component_outputs.back().back(), vars.back()};
solver.addClause(clause);
if (cardinality > 1) {
clause.pop_back();
clause.push_back(component_outputs.back()[component_outputs.back().size() - 2]);
solver.addClause(clause);
}
return component_outputs;
}
void RelationSynthesiser::addNaiveIs1CardinalityConstraint(const std::vector<int>& vars) {
solver.addClause(vars);
for (int i = 0; i < vars.size(); i++) {
for (int j = i + 1; j < vars.size(); j++) {
solver.addClause({-vars[i], -vars[j]});
}
}
}
void RelationSynthesiser::addNaiveIs2CardinalityConstraint(const std::vector<int>& vars) {
std::vector<int> cl;
cl.reserve(vars.size() - 1);
for (int i = 0; i < vars.size(); i++) {
for (int j = 0; j < i; j++) {
cl.push_back(vars[j]);
}
for (int j = i + 1; j < vars.size(); j++) {
cl.push_back(vars[j]);
}
solver.addClause(cl);
cl.clear();
for (int j = i + 1; j < vars.size(); j++) {
for (int k = j + 1; k < vars.size(); k++) {
solver.addClause({-vars[i], -vars[j], -vars[k]});
}
}
}
}
void RelationSynthesiser::defineConjunction(int var, std::vector<int>&& literals, int activator) {
std::vector<int> big_clause, small_clause;
if (activator != 0) {
big_clause.reserve(literals.size() + 2);
small_clause.reserve(3);
big_clause.push_back(activator);
small_clause.push_back(activator);
} else {
big_clause.reserve(literals.size() + 1);
small_clause.reserve(2);
}
big_clause.push_back(var);
small_clause.push_back(-var);
for (int lit : literals) {
big_clause.push_back(-lit);
small_clause.push_back(lit);
solver.addClause(small_clause);
small_clause.pop_back();
}
solver.addClause(big_clause);
}
void RelationSynthesiser::defineDisjunction(int var, std::vector<int>&& literals, int activator) {
std::vector<int> clause;
literals.push_back(-var);
if (activator != 0) {
literals.push_back(activator);
solver.addClause(literals);
literals.pop_back();
clause.reserve(3);
clause.push_back(activator);
} else {
clause.reserve(2);
solver.addClause(literals);
}
literals.pop_back();
clause.push_back(var);
for (int lit : literals) {
clause.push_back(-lit);
solver.addClause(clause);
clause.pop_back();
}
}
void RelationSynthesiser::addNonTrivialConstraint() {
for (int i = 0; i < max_size; i++) {
// We do not allow constant gates
solver.addClause(gate_definition_variables[i]);
// We exclude gates representing the projection to one of its inputs
for (int j = 0; j < config.gate_size; j++) {
int start = pow2(config.gate_size - j);
int block_length = pow2(config.gate_size - j - 1);
std::vector<int> clause;
clause.reserve(pow2(config.gate_size) - 1);
for (int k = 0; k < pow2(j); k++) {
for (int l = k * start - (k == 0 ? 0 : 1); l < k * start + block_length -1; l++) {
clause.push_back(gate_definition_variables[i][l]);
}
for (int l = k * start + block_length - 1; l < (k + 1) * start - 1; l++) {
clause.push_back(-gate_definition_variables[i][l]);
}
}
solver.addClause(clause);
}
}
}
// Every gate is either an output or an input of another gate
void RelationSynthesiser::addUseAllStepsConstraint() {
for (int i = 0; i < max_size; i++) {
std::vector<int> clause (gate_output_variables[i].begin(), gate_output_variables[i].end());
clause.reserve(max_size - i + 1);
for (int j = i + 1; j < max_size; j++) {
clause.push_back(selection_variables[j][subcir.inputs.size() + i]);
}
clause.push_back(-gate_activation_variables[i]);
solver.addClause(clause);
}
}
// Suppose gate i has inputs i1,...,in and gate j uses i as an input.
// Then the other n-1 inputs of j shall not be contained in the inputs of i.
// Otherwise j could be directly represented by a gate with inputs i1,...,in
void RelationSynthesiser::addNoReapplicationConstraint() {
std::vector<bool> filter(config.gate_size, 1);
// A 1 at index i indicates that the ith node is used as an input.
// By using prev_permutation we get all possible permutations of the filter
filter.resize(subcir.inputs.size() + max_size - 1);
std::vector<int> indices(config.gate_size,0);
// int tt_size = RelationSynthesiser::pow2(subcir.inputs.size()) - 1;
do {
indices.clear();
for (int i = 0; i < subcir.inputs.size() + max_size - 1; i++) {
if (filter[i]) {
indices.push_back(i);
}
}
int first_gate = getPotentialSuccessors(indices);
for (int i = first_gate; i < max_size; i++) {
std::vector<int> clause;
clause.reserve(subcir.inputs.size() + max_size);
for (int idx : indices) {
clause.push_back(-selection_variables[i][idx]);
}
int start_with = clause.size();
for (int j = i + 1; j < max_size; j++) {
// gate j has inputs.size() + j potential inputs
clause.resize(subcir.inputs.size() + j + 1, 0);
clause[start_with] = -selection_variables[j][subcir.inputs.size() + i];
clause[start_with + 1] = -gate_activation_variables[j];
int k = 0, l = 0, m = 0;
// while (k < inputs.size() + j && l < indices.size()) {
while (k < subcir.inputs.size() + j) {
if (l >= indices.size() || k < indices[l]) {
if (k != subcir.inputs.size() + i) {
clause[start_with + m + 2] = selection_variables[j][k];
m++;
}
k++;
} else if (k > indices[l]) {
l++;
} else {
k++;
l++;
}
}
solver.addClause(clause);
}
}
} while (std::prev_permutation(filter.begin(), filter.end()));
}
// Order steps according to their inputs.
// If step i has input j then step i+1 must have an input >=j
void RelationSynthesiser::addOrderedStepsConstraint() {
for (int i = 0; i < max_size - 1; i++) {
for (int j = 0; j < subcir.inputs.size() + i; j++) {
std::vector<int> clause {-gate_activation_variables[i+1], -selection_variables[i][j]};
clause.reserve(subcir.inputs.size() + i - j + 3);
for (int k = j; k < subcir.inputs.size() + i + 1; k++) {
clause.push_back(selection_variables[i+1][k]);
}
solver.addClause(clause);
}
}
}
}
ABC_NAMESPACE_IMPL_END

145
src/opt/eslim/relationSynthesiser.hpp Normal file
View File

@ -0,0 +1,145 @@
/**CFile****************************************************************
FileName [relationSynthesiser.hpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Base class for SAT-based synthesis]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__OPT__ESLIM__RELATIONSYNTHESISER_hpp
#define ABC__OPT__ESLIM__RELATIONSYNTHESISER_hpp
#include <vector>
#include <unordered_map>
#include "misc/util/abc_global.h"
#include "relationGeneration.hpp"
#include "subcircuit.hpp"
#include "cadicalSolver.hpp"
#include "utils.hpp"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
class RelationSynthesiser {
protected:
CadicalSolver solver;
const Subcircuit& subcir;
unsigned int max_size; // The maximal circuit size that can be checked
std::vector<int> gate_activation_variables;
std::vector<std::vector<int>> selection_variables;
std::vector<std::vector<int>> gate_output_variables;
RelationSynthesiser(const Relation& relation, const Subcircuit& subcir, unsigned int max_size, const eSLIMConfig& cfg, eSLIMLog& log);
int getNewVariable();
std::vector<int> getNewVariableVector(unsigned int size);
std::vector<int> getSizeAssumption(int size);
double getDynamicTimeout(int size);
unsigned int getSizeFromActivationVars(const std::vector<bool>& model);
unsigned int getSizeFromActivationVars();
void logRun(int status, unsigned int size);
eSLIMCirMan getReplacement(const std::vector<bool>& model, int size);
private:
const Relation& relation;
const eSLIMConfig& config;
eSLIMLog& log;
int max_var = 0; // The maximal variable occurring in inputs/outputs
std::vector<std::vector<std::vector<int>>> is_ith_fanin_variable;
std::vector<std::vector<int>> gate_definition_variables;
std::vector<std::vector<int>> gate_variables;
void setupEncoding();
void setupVariables();
void setupStructuralConstraints();
void setupSymmetryBreaking();
void setupGateValues();
std::vector<int> setupFaninVariables(int gtidx, int tt_line, int pidx);
void setupEquivalenceConstraints();
void setupActivationCompatibilityConstraints();
void setupIsFaninVariables(int gtidx, const std::vector<std::vector<int>>& counter_vars);
void constrainSelectionVariables();
void constraintGateOutputVariables();
void addGateValueConstraint(int gtidx, int gt_val, const std::vector<int>& fanin_variables);
void setupCycleConstraints();
void setupAigerConstraints();
int setupOutputVariable(int output_index, int tt_index, int pattern_idx);
void addNonTrivialConstraint();
void addUseAllStepsConstraint();
void addNoReapplicationConstraint();
void addOrderedStepsConstraint();
// activator = 0: do not use an activation variable
void addCardinalityConstraint(const std::vector<int>& vars, unsigned int cardinality, int activator = 0);
std::vector<std::vector<int>> addSequentialCounter(const std::vector<int>& vars, unsigned int cardinality, int activator = 0);
void addNaiveIs1CardinalityConstraint(const std::vector<int>& vars);
void addNaiveIs2CardinalityConstraint(const std::vector<int>& vars);
void defineConjunction(int var, std::vector<int>&& literals, int activator);
void defineDisjunction(int var, std::vector<int>&& literals, int activator);
// computes the index of the first gate that can used the indexed nodes as inputs
// indices must be ordered
int getPotentialSuccessors(const std::vector<int>& indices) const;
static bool getTTValue(int tt_line, int var);
static unsigned int pow2(int x);
};
inline int RelationSynthesiser::getNewVariable() {
return ++max_var;
}
inline std::vector<int> RelationSynthesiser::getNewVariableVector(unsigned int size) {
std::vector<int> vars;
vars.reserve(size);
for (int i = 0; i < size; i++) {
vars.push_back(getNewVariable());
}
return vars;
}
inline int RelationSynthesiser::getPotentialSuccessors(const std::vector<int>& indices) const {
if (indices.back() < subcir.inputs.size()) {
return 0;
}
return indices.back() - subcir.inputs.size() + 1;
}
inline bool RelationSynthesiser::getTTValue(int tt_line, int var) {
return (tt_line >> var) & 1;
}
inline unsigned int RelationSynthesiser::pow2(int x) {
return 1u << x;
}
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

196
src/opt/eslim/satInterfaces.hpp
View File

@ -1,196 +0,0 @@
/**CFile****************************************************************
FileName [satInterfaces.hpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Interface to SAT solvers.]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - March 2025.]
Revision [$Id: satInterfaces.hpp,v 1.00 2025/03/17 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__OPT__ESLIM__SATINTERFACE_h
#define ABC__OPT__ESLIM__SATINTERFACE_h
#include <vector>
#include <chrono>
#include <iostream>
#include "misc/util/abc_namespaces.h"
#include "misc/vec/vec.h"
#include "sat/kissat/kissat.h"
#include "sat/cadical/cadical.hpp"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
class CadicalSolver {
public:
void addClause(int * pLits, int nLits );
void assume(const std::vector<int>& assumptions);
int solve(double timeout);
int solve();
Vec_Int_t* getModelVec();
double getRunTime() const;
private:
int val(int variable);
double last_runtime;
CaDiCaL::Solver solver;
public:
class TimeoutTerminator : public CaDiCaL::Terminator {
public:
TimeoutTerminator(double max_runtime);
bool terminate();
private:
double max_runtime; //in seconds
std::chrono::time_point<std::chrono::steady_clock> start = std::chrono::steady_clock::now();
};
};
class KissatSolver {
public:
KissatSolver();
~KissatSolver();
void init(int max_var);
void addClause(int * pLits, int nLits );
int solve();
// int solve(int timeout);
Vec_Int_t* getModelVec();
private:
int max_var = 0;
int val(int variable);
kissat * solver = nullptr;
};
inline CadicalSolver::TimeoutTerminator::TimeoutTerminator(double max_runtime) : max_runtime(max_runtime) {}
inline bool CadicalSolver::TimeoutTerminator::terminate() {
auto current_time = std::chrono::steady_clock::now();
std::chrono::duration<double> elapsed_seconds = current_time - start;
return elapsed_seconds.count() > max_runtime;
}
inline double CadicalSolver::getRunTime() const {
return last_runtime;
}
inline void CadicalSolver::addClause(int * pLits, int nLits ) {
for ( int i = 0; i < nLits; i++ ) {
if (pLits[i] == 0) {
continue;;
}
solver.add(Abc_LitIsCompl(pLits[i]) ? -Abc_Lit2Var(pLits[i]) : Abc_Lit2Var(pLits[i]));
}
solver.add(0);
}
inline void CadicalSolver::assume(const std::vector<int>& assumptions) {
for (auto& l: assumptions) {
solver.assume(l);
}
}
inline int CadicalSolver::solve() {
std::chrono::time_point<std::chrono::steady_clock> start = std::chrono::steady_clock::now();
int status = solver.solve();
last_runtime = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::steady_clock::now() - start).count();
return status;
}
inline int CadicalSolver::solve(double timeout) {
std::chrono::time_point<std::chrono::steady_clock> start = std::chrono::steady_clock::now();
TimeoutTerminator terminator(timeout);
solver.connect_terminator(&terminator);
int status = solver.solve();
last_runtime = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::steady_clock::now() - start).count();
if (solver.state() == CaDiCaL::INVALID) {
std::cerr<<"Solver is in invalid state"<<std::endl;
return -1;
}
solver.disconnect_terminator();
return status;
}
inline Vec_Int_t* CadicalSolver::getModelVec() {
Vec_Int_t* assignment = Vec_IntAlloc( solver.vars() );
for (int v = 1; v <= solver.vars(); v++) {
Vec_IntSetEntryFull( assignment, Abc_AbsInt(val(v)), val(v) > 0 );
}
return assignment;
}
inline int CadicalSolver::val(int variable) {
auto l = solver.val(variable);
auto v = abs(l);
if (v == variable) {
return l;
} else {
return variable;
}
}
inline KissatSolver::KissatSolver() {
solver = kissat_init();
}
inline KissatSolver::~KissatSolver() {
kissat_release(solver);
}
inline void KissatSolver::init(int max_var) {
this->max_var = max_var;
kissat_reserve(solver, max_var);
}
inline void KissatSolver::addClause(int * pLits, int nLits ) {
for ( int i = 0; i < nLits; i++ ) {
if (pLits[i] == 0) {
continue;
}
kissat_add (solver, Abc_LitIsCompl(pLits[i]) ? -Abc_Lit2Var(pLits[i]) : Abc_Lit2Var(pLits[i]));
}
kissat_add (solver, 0);
}
inline int KissatSolver::solve() {
int status = kissat_solve(solver);
return status;
}
inline int KissatSolver::val(int variable) {
int l = kissat_value (solver, variable);
auto v = abs(l);
if (v == variable) {
return l;
} else {
return variable;
}
}
inline Vec_Int_t* KissatSolver::getModelVec() {
Vec_Int_t* assignment = Vec_IntAlloc( max_var );
for (int v = 1; v <= max_var; v++) {
Vec_IntSetEntryFull( assignment, Abc_AbsInt(val(v)), val(v) > 0 );
}
return assignment;
}
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

181
src/opt/eslim/selectionStrategies.hpp Normal file
View File

@ -0,0 +1,181 @@
/**CFile****************************************************************
FileName [selectionStrategies.hpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Subcircuit selection]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__OPT__ESLIM__SELECTIONSTRATEGIES_hpp
#define ABC__OPT__ESLIM__SELECTIONSTRATEGIES_hpp
#include <random>
#include <queue>
#include <set>
#include "misc/util/abc_namespaces.h"
#include "eslimCirMan.hpp"
#include "subcircuit.hpp"
#include "utils.hpp"
#include "tabooList.hpp"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
struct SubcircuitValidator {
public:
SubcircuitValidator(const eSLIMConfig& cf);
bool check(const Subcircuit& candidate) const;
private:
const eSLIMConfig& cfg;
static constexpr unsigned int min_size = 2;
static constexpr unsigned int max_ninputs = 10;
};
struct SubcircuitNoFBValidator : public SubcircuitValidator {
public:
using SubcircuitValidator::SubcircuitValidator;
bool check(const Subcircuit& candidate) const;
};
class ForwardSearch {
public:
ForwardSearch(eSLIMCirMan& es_man);
auto getNextBegin(const eSLIMCirObj& obj);
auto getNextEnd(const eSLIMCirObj& obj);
bool check(const eSLIMCirObj& obj) const;
private:
eSLIMCirMan& es_man;
};
class BackwardSearch {
public:
BackwardSearch(eSLIMCirMan& es_man);
auto getNextBegin(const eSLIMCirObj& obj);
auto getNextEnd(const eSLIMCirObj& obj);
bool check(const eSLIMCirObj& obj) const;
private:
eSLIMCirMan& es_man;
};
class BaseRootSelector {
public:
BaseRootSelector(eSLIMCirMan& es_man, const eSLIMConfig& cfg);
int getRoot(std::mt19937& rng);
void reset() {}
private:
unsigned int getUniformRandomNumber(std::mt19937& rng, unsigned int lower, unsigned int upper); // requires lower < upper
eSLIMCirMan& es_man;
// const eSLIMConfig& cfg;
std::uniform_int_distribution<std::mt19937::result_type> udistr;
};
class TabooRootSelector {
public:
TabooRootSelector(eSLIMCirMan& es_man, const eSLIMConfig& cfg);
~TabooRootSelector();
int getRoot(std::mt19937& rng);
void reset();
private:
eSLIMCirMan& es_man;
protected:
const eSLIMConfig& cfg;
TabooList taboo;
};
class CriticalPathSelector : public TabooRootSelector {
public:
using TabooRootSelector::TabooRootSelector;
int getRoot(std::mt19937& rng);
};
struct BaseCandidateNodeConstraint {
static bool check(int to_check, const eSLIMCirMan& cir, const std::set<int>& subcircuit);
};
struct SingleOutputCandidateNodeConstraint {
static bool check(int to_check, const eSLIMCirMan& cir, const std::set<int>& subcircuit);
};
struct NoBiasSelector {
static bool useBias(const eSLIMCirMan& es_man, const eSLIMCirObj& obj) {return false;}
};
struct CriticalPathBiasSelector {
static bool useBias(const eSLIMCirMan& es_man, const eSLIMCirObj& obj) {return es_man.isOnCricticalPath(obj);}
};
template <typename Validator, typename RootSelector, typename SearchDirection, typename BiasSelector = NoBiasSelector, typename CandidateNodeConstraint = BaseCandidateNodeConstraint>
class RandomizedBFSSelection {
public:
RandomizedBFSSelection(eSLIMCirMan& es_man, const eSLIMConfig& cfg, eSLIMLog& log);
Subcircuit getSubcircuit(bool& status); // status indicates if the search was successful
void setSeed(int seed);
void reset();
static constexpr bool requiresRemainingTimes() {return std::is_same_v<CriticalPathBiasSelector, BiasSelector>;}
private:
std::set<int> computeSubcircuitCandidate();
int selectRoot();
void processCandidateNode(int candidate, std::set<int>& subcircuit, std::queue<int>& candidates);
bool getRandomBool();
bool getBiasedRandomBool();
eSLIMCirMan& es_man;
const eSLIMConfig& cfg;
static constexpr unsigned int min_size = 2;
static constexpr unsigned int max_ninputs = 10;
eSLIMLog& log;
Validator validator;
RootSelector root_selector;
SearchDirection search_direction;
std::mt19937 rng;
std::bernoulli_distribution bdist;
std::bernoulli_distribution biased_bdist;
};
using RamdomizedBFS=RandomizedBFSSelection<SubcircuitValidator,BaseRootSelector, BackwardSearch>;
using RamdomizedBFSForward=RandomizedBFSSelection<SubcircuitValidator,BaseRootSelector, ForwardSearch>;
using RandomizedBFSNoFB=RandomizedBFSSelection<SubcircuitNoFBValidator,BaseRootSelector, BackwardSearch>;
using RamdomizedBFSTaboo=RandomizedBFSSelection<SubcircuitValidator,TabooRootSelector, BackwardSearch>;
using RamdomizedBFSTabooForward=RandomizedBFSSelection<SubcircuitValidator,TabooRootSelector, ForwardSearch>;
using RamdomizedBFSTabooNoFB=RandomizedBFSSelection<SubcircuitNoFBValidator,TabooRootSelector, BackwardSearch>;
using SingleOutputBFS = RandomizedBFSSelection<SubcircuitValidator,TabooRootSelector, BackwardSearch, NoBiasSelector, SingleOutputCandidateNodeConstraint>;
}
ABC_NAMESPACE_CXX_HEADER_END
#include "selectionStrategies.tpp"
#endif

226
src/opt/eslim/selectionStrategies.tpp Normal file
View File

@ -0,0 +1,226 @@
/**CFile****************************************************************
FileName [selectionStrategies.tpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Subcircuit selection]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#include "selectionStrategies.hpp"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
inline SubcircuitValidator::SubcircuitValidator(const eSLIMConfig& cfg) : cfg(cfg) {
}
inline bool SubcircuitValidator::check(const Subcircuit& candidate) const {
return candidate.inputs.size() <= max_ninputs && candidate.inputs.size() >= cfg.gate_size;
}
inline bool SubcircuitNoFBValidator::check(const Subcircuit& candidate) const {
return SubcircuitValidator::check(candidate) && candidate.forbidden_pairs.empty();
}
inline ForwardSearch::ForwardSearch(eSLIMCirMan& es_man) : es_man(es_man) {
}
inline auto ForwardSearch::getNextBegin(const eSLIMCirObj& obj) {
return obj.fanouts.begin();
}
inline auto ForwardSearch::getNextEnd(const eSLIMCirObj& obj) {
return obj.fanouts.end();
}
inline bool ForwardSearch::check(const eSLIMCirObj& obj) const {
return !es_man.isPo(obj.node_id);
}
inline BackwardSearch::BackwardSearch(eSLIMCirMan& es_man) : es_man(es_man) {
}
inline auto BackwardSearch::getNextBegin(const eSLIMCirObj& obj) {
return obj.fanins.begin();
}
inline auto BackwardSearch::getNextEnd(const eSLIMCirObj& obj) {
return obj.fanins.end();
}
inline bool BackwardSearch::check(const eSLIMCirObj& obj) const {
return !es_man.isPi(obj.node_id);
}
// inline BaseRootSelector::BaseRootSelector(eSLIMCirMan& es_man, const eSLIMConfig& cfg) : es_man(es_man), cfg(cfg) {
inline BaseRootSelector::BaseRootSelector(eSLIMCirMan& es_man, const eSLIMConfig& cfg) : es_man(es_man) {
}
inline TabooRootSelector::TabooRootSelector(eSLIMCirMan& es_man, const eSLIMConfig& cfg) : es_man(es_man), cfg(cfg), taboo(es_man) {
es_man.registerTabooList(&taboo);
}
inline TabooRootSelector::~TabooRootSelector() {
es_man.unregisterTabooList();
}
inline unsigned int BaseRootSelector::getUniformRandomNumber(std::mt19937& rng, unsigned int lower, unsigned int upper) {
udistr.param(std::uniform_int_distribution<std::mt19937::result_type>::param_type(lower, upper));
return udistr(rng);
}
inline int BaseRootSelector::getRoot(std::mt19937& rng) {
int min_id = es_man.getNofPis() + 1;
int max_id = es_man.getNofObjs() - es_man.getNofPos() - 1;
return getUniformRandomNumber(rng, min_id, max_id);
}
inline int TabooRootSelector::getRoot(std::mt19937& rng) {
return taboo.getRandomNonTaboo(rng, cfg.taboo_ratio, cfg.taboo_time);
}
inline void TabooRootSelector::reset() {
taboo.reset();
es_man.registerTabooList(&taboo);
}
inline int CriticalPathSelector::getRoot(std::mt19937& rng) {
return taboo.getBiasedRandomNonTaboo<CriticalPathBiasSelector>(rng, cfg.bias, cfg.taboo_ratio, cfg.taboo_time);
}
inline bool BaseCandidateNodeConstraint::check(int to_check, const eSLIMCirMan& cir, const std::set<int>& subcircuit) {
return subcircuit.find(to_check) == subcircuit.end();
}
inline bool SingleOutputCandidateNodeConstraint::check(int to_check, const eSLIMCirMan& cir, const std::set<int>& subcircuit) {
if (subcircuit.find(to_check) != subcircuit.end()) {
return false;
}
const auto& obj = cir.getObj(to_check);
for (const auto& fo : obj.fanouts) {
// The node has a fanout that is not yet in the subcircuit
if (subcircuit.find(fo->node_id) == subcircuit.end()) {
return false;
}
}
return true;
}
template <typename Validator, typename RootSelector, typename SearchDirection, typename BiasSelector, typename CandidateNodeConstraint>
RandomizedBFSSelection<Validator, RootSelector, SearchDirection, BiasSelector, CandidateNodeConstraint>::RandomizedBFSSelection(eSLIMCirMan& es_man, const eSLIMConfig& cfg, eSLIMLog& log)
: es_man(es_man), cfg(cfg), log(log), validator(cfg), root_selector(es_man, cfg), search_direction(es_man),
bdist(cfg.expansion_probability), biased_bdist(std::min(1., cfg.expansion_probability*1.5)) {
}
template <typename Validator, typename RootSelector, typename SearchDirection, typename BiasSelector, typename CandidateNodeConstraint>
void RandomizedBFSSelection<Validator, RootSelector, SearchDirection, BiasSelector, CandidateNodeConstraint>::setSeed(int seed) {
rng.seed(seed);
}
template <typename Validator, typename RootSelector, typename SearchDirection, typename BiasSelector, typename CandidateNodeConstraint>
bool RandomizedBFSSelection<Validator, RootSelector, SearchDirection, BiasSelector, CandidateNodeConstraint>::getRandomBool() {
return bdist(rng);
}
template <typename Validator, typename RootSelector, typename SearchDirection, typename BiasSelector, typename CandidateNodeConstraint>
bool RandomizedBFSSelection<Validator, RootSelector, SearchDirection, BiasSelector, CandidateNodeConstraint>::getBiasedRandomBool() {
return biased_bdist(rng);
}
template <typename Validator, typename RootSelector, typename SearchDirection, typename BiasSelector, typename CandidateNodeConstraint>
int RandomizedBFSSelection<Validator, RootSelector, SearchDirection, BiasSelector, CandidateNodeConstraint>::selectRoot() {
return root_selector.getRoot(rng);
}
template <typename Validator, typename RootSelector, typename SearchDirection, typename BiasSelector, typename CandidateNodeConstraint>
void RandomizedBFSSelection<Validator, RootSelector, SearchDirection, BiasSelector, CandidateNodeConstraint>::reset() {
root_selector.reset();
}
template <typename Validator, typename RootSelector, typename SearchDirection, typename BiasSelector, typename CandidateNodeConstraint>
std::set<int> RandomizedBFSSelection<Validator, RootSelector, SearchDirection, BiasSelector, CandidateNodeConstraint>::computeSubcircuitCandidate() {
std::set<int> scir;
int root_id = selectRoot();
std::queue<int> candidates;
processCandidateNode(root_id, scir, candidates);
std::queue<int> rejected_nodes;
while (!candidates.empty() && scir.size() < cfg.subcircuit_max_size) {
int c = candidates.front();
candidates.pop();
if (CandidateNodeConstraint::check(c, es_man, scir)) {
bool add_node;
if (BiasSelector::useBias(es_man, es_man.getObj(c))) {
add_node = getBiasedRandomBool();
} else {
add_node = getRandomBool();
}
if (add_node) {
processCandidateNode(c, scir, candidates);
} else {
rejected_nodes.push(c);
}
}
}
if (this->cfg.fill_subcircuits) {
while (!rejected_nodes.empty() && scir.size() < cfg.subcircuit_max_size) {
int c = rejected_nodes.front();
rejected_nodes.pop();
if (CandidateNodeConstraint::check(c, es_man, scir)) {
processCandidateNode(c, scir, rejected_nodes);
}
}
}
return scir;
}
template <typename Validator, typename RootSelector, typename SearchDirection, typename BiasSelector, typename CandidateNodeConstraint>
void RandomizedBFSSelection<Validator, RootSelector, SearchDirection, BiasSelector, CandidateNodeConstraint>::processCandidateNode(int node, std::set<int>& subcircuit, std::queue<int>& candidates) {
subcircuit.insert(node);
auto& obj = es_man.getObj(node);
for (auto it = search_direction.getNextBegin(obj); it != search_direction.getNextEnd(obj); it++) {
const auto& f = *it;
if (search_direction.check(*f)) {
candidates.push(f->node_id);
}
}
}
template <typename Validator, typename RootSelector, typename SearchDirection, typename BiasSelector, typename CandidateNodeConstraint>
Subcircuit RandomizedBFSSelection<Validator, RootSelector, SearchDirection, BiasSelector, CandidateNodeConstraint>::getSubcircuit(bool& status) {
std::set<int> scir;
status = false;
for (int i = 1; i < cfg.nselection_trials; i++) {
scir = computeSubcircuitCandidate();
if (scir.size() < min_size) {
scir.clear();
continue;
}
es_man.incrementTraversalId();
Subcircuit candidate = Subcircuit::getSubcircuit(es_man, scir);
if (validator.check(candidate)) {
status = true;
return candidate;
}
}
return Subcircuit::getEmptySubcircuit();
}
}
ABC_NAMESPACE_CXX_HEADER_END

154
src/opt/eslim/selectionStrategy.hpp
View File

@ -1,154 +0,0 @@
/**CFile****************************************************************
FileName [selectionStrategy.hpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Procedures for selecting subcircuits.]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - March 2025.]
Revision [$Id: selectionStrategy.hpp,v 1.00 2025/03/17 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__OPT__ESLIM__SELECTIONSTRATEGY_h
#define ABC__OPT__ESLIM__SELECTIONSTRATEGY_h
#include <random>
#include <queue>
#include "misc/util/abc_namespaces.h"
#include "misc/vec/vec.h"
#include "aig/gia/gia.h"
#include "utils.hpp"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
template<typename T>
class SelectionStrategy {
public:
Subcircuit getSubcircuit();
bool getStatus() {return status;};
void setSeed(int seed);
protected:
SelectionStrategy(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log);
unsigned int getUniformRandomNumber(unsigned int lower, unsigned int upper); // requires lower < upper
bool getRandomBool();
int getSubcircuitIO(Vec_Int_t* subcircuit, Vec_Int_t* io);
// The resulting map assigns inputs of the subcircuit to outputs of the subcircuit s.t. each associated input is reachable from the output
std::unordered_map<int, std::unordered_set<int>> computeForbiddenPairs(const Subcircuit& subcir);
Gia_Man_t*& gia_man;
const eSLIMConfig& cfg;
eSLIMLog& log;
private:
bool filterSubcircuit(const Subcircuit& subcir);
void forbiddenPairsRec(Gia_Obj_t * pObj, int input, int min_level, std::unordered_map<int, std::unordered_set<int>>& pairs, const std::unordered_map<int,int>& out_ids );
bool status = true; //set to false if selection fails too often
static constexpr unsigned int min_size = 2;
std::mt19937 rng;
std::bernoulli_distribution bdist;
std::uniform_int_distribution<std::mt19937::result_type> udistr;
};
template<typename T>
class randomizedBFS : public SelectionStrategy<T> {
private:
randomizedBFS(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log);
Subcircuit findSubcircuit();
int selectRoot();
void checkCandidate(Subcircuit& subcircuit, std::queue<int>& candidate, std::queue<int>& rejected, bool add);
const int nPis;
const int nPos;
friend SelectionStrategy<T>;
friend T;
};
class randomizedBFSFP : public randomizedBFS<randomizedBFSFP> {
public :
randomizedBFSFP(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log);
private:
Subcircuit getSubcircuitImpl();
bool filterSubcircuitImpl(const Subcircuit& subcir);
friend SelectionStrategy<randomizedBFSFP>;
};
class randomizedBFSnoFP : public randomizedBFS<randomizedBFSnoFP> {
public:
randomizedBFSnoFP(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log);
private:
Subcircuit getSubcircuitImpl() {return findSubcircuit();};
bool filterSubcircuitImpl(const Subcircuit& subcir);
bool filterSubcircuitRec(Gia_Obj_t * pObj, unsigned int min_level);
friend SelectionStrategy<randomizedBFSnoFP>;
};
template<typename T>
SelectionStrategy<T>::SelectionStrategy(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log)
: gia_man(gia_man), cfg(cfg), log(log), rng(std::random_device()()), bdist(cfg.expansion_probability) {
}
template<typename T>
void SelectionStrategy<T>::setSeed(int seed) {
rng.seed(seed);
}
template<typename T>
unsigned int SelectionStrategy<T>::getUniformRandomNumber(unsigned int lower, unsigned int upper) {
udistr.param(std::uniform_int_distribution<std::mt19937::result_type>::param_type(lower, upper));
return udistr(rng);
}
template<typename T>
bool SelectionStrategy<T>::getRandomBool() {
return bdist(rng);
}
template<typename T>
randomizedBFS<T>::randomizedBFS(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log)
: SelectionStrategy<T>(gia_man, cfg, log), nPis(Gia_ManPiNum(gia_man)), nPos(Gia_ManPoNum(gia_man)) {
}
inline randomizedBFSFP::randomizedBFSFP(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log)
: randomizedBFS<randomizedBFSFP>(gia_man, cfg, log){
}
inline Subcircuit randomizedBFSFP::getSubcircuitImpl() {
Subcircuit subcir = findSubcircuit();
subcir.forbidden_pairs = computeForbiddenPairs(subcir);
return subcir;
}
inline randomizedBFSnoFP::randomizedBFSnoFP(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log)
: randomizedBFS<randomizedBFSnoFP>(gia_man, cfg, log) {
}
inline bool randomizedBFSFP::filterSubcircuitImpl(const Subcircuit& subcir) {
return true;
}
}
ABC_NAMESPACE_CXX_HEADER_END
#include "selectionStrategy.tpp"
#endif

233
src/opt/eslim/selectionStrategy.tpp
View File

@ -1,233 +0,0 @@
/**CFile****************************************************************
FileName [selectionStrategy.tpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Procedures for selecting subcircuits.]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - March 2025.]
Revision [$Id: selectionStrategy.tpp,v 1.00 2025/03/17 00:00:00 Exp $]
***********************************************************************/
#include <queue>
#include "misc/util/abc_namespaces.h"
#include "selectionStrategy.hpp"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
template<typename T>
Subcircuit SelectionStrategy<T>::getSubcircuit() {
for (int i = 0; i < cfg.nselection_trials; i++) {
Subcircuit subcir = static_cast<T*>(this)->getSubcircuitImpl();
if (filterSubcircuit(subcir)) {
return subcir;
} else {
subcir.free();
}
}
status = false;
Subcircuit empty_subcir;
return empty_subcir;
}
template<typename T>
bool SelectionStrategy<T>::filterSubcircuit(const Subcircuit& subcir) {
// if (subcir.nof_inputs > 8) {
if (subcir.nof_inputs > 10) {
return false;
}
// ABC internally requires that the subcircuit has not more than 6 outputs (e.g. generateMinterm)
if (Vec_IntSize(subcir.io)-subcir.nof_inputs > 6) {
return false;
}
if (Vec_IntSize(subcir.nodes) < min_size) {
return false;
}
return static_cast<T*>(this)->filterSubcircuitImpl(subcir);
}
template <typename T>
int SelectionStrategy<T>::getSubcircuitIO(Vec_Int_t* subcircuit, Vec_Int_t* io) {
assert(Vec_IntSize(io) == 0);
Gia_ManIncrementTravId(gia_man);
Gia_Obj_t * pObj;
int i;
Gia_ManForEachObjVec( subcircuit, gia_man, pObj, i ) {
Gia_ObjSetTravIdCurrent(gia_man, pObj);
}
Gia_ManIncrementTravId(gia_man);
// inputs
Gia_ManForEachObjVec( subcircuit, gia_man, pObj, i ) {
// fanin0 is not in the subcircuit and was not considered yet
if (!Gia_ObjIsTravIdPrevious(gia_man, Gia_ObjFanin0(pObj)) && !Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin0(pObj))) {
Gia_ObjSetTravIdCurrent(gia_man, Gia_ObjFanin0(pObj));
Vec_IntPush(io, Gia_ObjId(gia_man, Gia_ObjFanin0(pObj)));
}
// fanin1 is not in the subcircuit and was not considered yet
if (!Gia_ObjIsTravIdPrevious(gia_man, Gia_ObjFanin1(pObj)) && !Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin1(pObj))) {
Gia_ObjSetTravIdCurrent(gia_man, Gia_ObjFanin1(pObj));
Vec_IntPush(io, Gia_ObjId(gia_man, Gia_ObjFanin1(pObj)));
}
}
int nof_inputs = Vec_IntSize(io);
// outputs
Gia_ManForEachAnd( gia_man, pObj, i ) {
// If there is an object that is not contained in the subcircuit that has a fanin in the subcircuit then this fanin is an output
if (!Gia_ObjIsTravIdPrevious(gia_man, pObj)) {
if (Gia_ObjIsTravIdPrevious(gia_man, Gia_ObjFanin0(pObj))) {
Gia_ObjSetTravIdCurrent(gia_man, Gia_ObjFanin0(pObj));
Vec_IntPush(io, Gia_ObjId(gia_man, Gia_ObjFanin0(pObj)));
}
if (Gia_ObjIsTravIdPrevious(gia_man, Gia_ObjFanin1(pObj))) {
Gia_ObjSetTravIdCurrent(gia_man, Gia_ObjFanin1(pObj));
Vec_IntPush(io, Gia_ObjId(gia_man, Gia_ObjFanin1(pObj)));
}
}
}
Gia_ManForEachPo( gia_man, pObj, i ) {
if (Gia_ObjIsTravIdPrevious(gia_man, Gia_ObjFanin0(pObj))) {
Gia_ObjSetTravIdCurrent(gia_man, Gia_ObjFanin0(pObj));
Vec_IntPush(io, Gia_ObjId(gia_man, Gia_ObjFanin0(pObj)));
}
}
return nof_inputs;
}
template <typename T>
std::unordered_map<int, std::unordered_set<int>> SelectionStrategy<T>::computeForbiddenPairs(const Subcircuit& subcir) {
Gia_Obj_t * pObj;
int i;
unsigned int min_output_level = Gia_ManLevelNum(gia_man);
Gia_ManIncrementTravId(gia_man);
std::unordered_map<int,int> out_id;
Gia_ManForEachObjVecStart(subcir.io, gia_man, pObj, i, subcir.nof_inputs) {
min_output_level = Gia_ObjLevel(gia_man, pObj) < min_output_level ? Gia_ObjLevel(gia_man, pObj) : min_output_level;
Gia_ObjSetTravIdCurrent(gia_man, pObj);
auto id = Gia_ObjId(gia_man, pObj);
out_id[id] = i - subcir.nof_inputs;
}
std::unordered_map<int, std::unordered_set<int>> forbidden_pairs;
Gia_ManForEachObjVecStop(subcir.io, gia_man, pObj, i, subcir.nof_inputs) {
forbiddenPairsRec(pObj, i, min_output_level, forbidden_pairs, out_id);
}
return forbidden_pairs;
}
template <typename T>
void SelectionStrategy<T>::forbiddenPairsRec(Gia_Obj_t * pObj, int input, int min_level, std::unordered_map<int, std::unordered_set<int>>& pairs, const std::unordered_map<int,int>& out_id) {
if (Gia_ObjIsTravIdCurrent(gia_man, pObj)) {
auto id = Gia_ObjId(gia_man, pObj);
pairs[out_id.at(id)].insert(input);
return;
}
if (Gia_ObjLevel(gia_man, pObj) < min_level) {
return;
}
forbiddenPairsRec(Gia_ObjFanin0(pObj), input, min_level, pairs, out_id);
forbiddenPairsRec(Gia_ObjFanin1(pObj), input, min_level, pairs, out_id);
}
template<typename T>
int randomizedBFS<T>::selectRoot() {
int nof_objs = Gia_ManObjNum(this->gia_man);
int root_id = this->getUniformRandomNumber(this->nPis + 1, nof_objs - this->nPos - 1);
return root_id;
}
template<typename T>
void randomizedBFS<T>::checkCandidate(Subcircuit& subcircuit, std::queue<int>& candidates, std::queue<int>& rejected, bool add) {
int obj_id = candidates.front();
candidates.pop();
Gia_Obj_t * gia_obj = Gia_ManObj(this->gia_man, obj_id);
if (Gia_ObjIsAnd(gia_obj) && !Gia_ObjIsTravIdCurrent(this->gia_man, gia_obj)) {
if (add) {
Gia_ObjSetTravIdCurrent(this->gia_man, gia_obj);
Vec_IntPush(subcircuit.nodes, obj_id);
candidates.push(Gia_ObjFaninId0(gia_obj, obj_id));
candidates.push(Gia_ObjFaninId1(gia_obj, obj_id));
} else {
rejected.push(obj_id);
}
}
}
template<typename T>
Subcircuit randomizedBFS<T>::findSubcircuit() {
Subcircuit result;
assert (Gia_ManIsNormalized(this->gia_man));
int root_id = selectRoot();
Gia_Obj_t * gia_obj = Gia_ManObj(this->gia_man, root_id);
assert (Gia_ObjIsAnd(gia_obj));
result.nodes = Vec_IntAlloc(this->cfg.subcircuit_size_bound);
result.io = Vec_IntAlloc(this->cfg.subcircuit_size_bound);
Vec_IntPush(result.nodes, root_id);
std::queue<int> candidates;
candidates.push(Gia_ObjFaninId0(gia_obj, root_id));
candidates.push(Gia_ObjFaninId1(gia_obj, root_id));
std::queue<int> rejected_nodes;
Gia_ManIncrementTravId(this->gia_man);
while (!candidates.empty() && Vec_IntSize(result.nodes) < this->cfg.subcircuit_size_bound) {
checkCandidate(result, candidates, rejected_nodes, this->getRandomBool());
}
if (this->cfg.fill_subcircuits) {
while (!rejected_nodes.empty() && Vec_IntSize(result.nodes) < this->cfg.subcircuit_size_bound) {
checkCandidate(result, rejected_nodes, rejected_nodes, true);
}
}
result.nof_inputs = this->getSubcircuitIO(result.nodes, result.io);
return result;
}
inline bool randomizedBFSnoFP::filterSubcircuitImpl(const Subcircuit& subcir) {
Gia_Obj_t * pObj;
int i;
unsigned int min_output_level = Gia_ManLevelNum(gia_man);
Gia_ManIncrementTravId(gia_man);
Gia_ManForEachObjVecStart(subcir.io, gia_man, pObj, i, subcir.nof_inputs) {
min_output_level = Gia_ObjLevel(gia_man, pObj) < min_output_level ? Gia_ObjLevel(gia_man, pObj) : min_output_level;
Gia_ObjSetTravIdCurrent(gia_man, pObj);
}
Gia_ManIncrementTravId(gia_man);
Gia_ManForEachObjVecStop(subcir.io, gia_man, pObj, i, subcir.nof_inputs) {
if (!filterSubcircuitRec(pObj, min_output_level)) {
return false;
}
}
return true;
}
inline bool randomizedBFSnoFP::filterSubcircuitRec(Gia_Obj_t * pObj, unsigned int min_level) {
if (Gia_ObjIsTravIdPrevious(gia_man, pObj)) {
return false;
} else if (Gia_ObjIsTravIdCurrent(gia_man, pObj)) {
return true;
} else if (Gia_ObjLevel(gia_man, pObj) < min_level) {
return true;
}
Gia_ObjSetTravIdCurrent(gia_man, pObj);
return filterSubcircuitRec(Gia_ObjFanin0(pObj), min_level) && filterSubcircuitRec(Gia_ObjFanin1(pObj), min_level);
}
}
ABC_NAMESPACE_CXX_HEADER_END

132
src/opt/eslim/subcircuit.cpp Normal file
View File

@ -0,0 +1,132 @@
/**CFile****************************************************************
FileName [subcircuit.cpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Subcircuit representation]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#include <algorithm>
#include <set>
#include <iostream>
#include "subcircuit.hpp"
ABC_NAMESPACE_IMPL_START
namespace eSLIM {
Subcircuit Subcircuit::getSubcircuit(eSLIMCirMan& es_man, const std::set<int>& nodes) {
Subcircuit scir = getSubcircuitBare(es_man, nodes.begin(), nodes.end());
es_man.markCones(scir.nodes);
scir.setForbiddenPairs(es_man);
return scir;
}
Subcircuit Subcircuit::getEmptySubcircuit() {
Subcircuit scir;
return scir;
}
void Subcircuit::setIO(eSLIMCirMan& es_man) {
std::set<int> input_set;
std::set<int> output_set;
for (int n : nodes) {
const auto& obj = es_man.getObj(n);
for (const auto& f : obj.fanins) {
if (!es_man.inSubcircuit(*f) && !es_man.isConst(*f)) {
input_set.insert(f->node_id);
}
}
for (const auto& f : obj.fanouts) {
if (!es_man.inSubcircuit(*f)) {
output_set.insert(obj.node_id);
}
}
}
inputs.insert(inputs.end(), input_set.begin(), input_set.end());
outputs.insert(outputs.end(), output_set.begin(), output_set.end());
}
void Subcircuit::setForbiddenPairs(const eSLIMCirMan& es_man) {
std::unordered_set<int> seen;
for (int inp : inputs) {
getForbiddenPairsRec(inp, seen, es_man.getObj(inp), es_man);
seen.clear();
}
}
void Subcircuit::getForbiddenPairsRec(int inp, std::unordered_set<int>& seen, const eSLIMCirObj& obj, const eSLIMCirMan& es_man) {
if (seen.find(obj.node_id) != seen.end()) {
return;
}
seen.insert(obj.node_id);
for (const auto& f : obj.fanins) {
if (es_man.inSubcircuit(*f)) {
forbidden_pairs[f->node_id].emplace(inp);
} else if (es_man.inTFI(*f) && es_man.inTFO(*f)) {
getForbiddenPairsRec(inp, seen, *f, es_man);
}
}
}
int Subcircuit::setupTimings(eSLIMCirMan& es_man) {
// es_man.setupTimings();
for (int in : inputs) {
arrival_times.push_back(es_man.getObj(in).depth);
}
int max_crossing_path = 0;
for (int out : outputs) {
remaining_times.push_back(es_man.getObj(out).remaining_time);
max_crossing_path = std::max(max_crossing_path, es_man.getObj(out).remaining_time + es_man.getObj(out).depth);
}
return max_crossing_path;
}
void Subcircuit::print() const {
std::cout << "Inputs:";
for (int i : inputs) {
std::cout << " " << i;
}
std::cout << "\nOutputs:";
for (int o : outputs) {
std::cout << " " << o;
}
std::cout << "\nArrival times:";
for (int ar : arrival_times) {
std::cout << " " << ar;
}
std::cout << "\nRemaining times:";
for (int re : remaining_times) {
std::cout << " " << re;
}
std::cout << "\nNodes:";
for (int n : nodes) {
std::cout << " " << n;
}
std::cout << "\nForbidden pairs:";
for (const auto & [out,inps] : forbidden_pairs) {
std::cout << "\n" << out << " :";
for (int inp : inps) {
std::cout << " " << inp;
}
}
std::cout << "\n";
}
}
ABC_NAMESPACE_IMPL_END

80
src/opt/eslim/subcircuit.hpp Normal file
View File

@ -0,0 +1,80 @@
/**CFile****************************************************************
FileName [subcircuit.hpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Subcircuit representation]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__OPT__ESLIM__SUBCIRCUIT_hpp
#define ABC__OPT__ESLIM__SUBCIRCUIT_hpp
#include <vector>
#include <unordered_map>
#include <unordered_set>
#include <set>
#include "misc/util/abc_namespaces.h"
#include "eslimCirMan.hpp"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
class Subcircuit {
public:
template <typename It>
static Subcircuit getSubcircuitBare(eSLIMCirMan& es_man, It begin, It end);
static Subcircuit getSubcircuit(eSLIMCirMan& es_man, const std::set<int>& nodes);
static Subcircuit getEmptySubcircuit();
int setupTimings(eSLIMCirMan& es_man);
std::vector<int> nodes;
std::vector<int> inputs;
std::vector<int> outputs;
// Assigns the inputs of the subcircuit that can be reached from an output x to x.
std::unordered_map<int, std::set<int>> forbidden_pairs;
std::vector<unsigned int> arrival_times;
std::vector<unsigned int> remaining_times;
void print() const;
private:
template <typename It>
Subcircuit(eSLIMCirMan& es_man, It begin, It end);
Subcircuit() = default;
void setIO(eSLIMCirMan& es_man);
void setForbiddenPairs(const eSLIMCirMan& es_man);
void getForbiddenPairsRec(int inp, std::unordered_set<int>& seen, const eSLIMCirObj& obj, const eSLIMCirMan& es_man);
};
template <typename It>
Subcircuit::Subcircuit(eSLIMCirMan& es_man, It begin, It end) : nodes(begin, end) {
es_man.markSubcircuit(this->nodes);
setIO(es_man);
}
template <typename It>
Subcircuit Subcircuit::getSubcircuitBare(eSLIMCirMan& es_man, It begin, It end) {
Subcircuit scir(es_man, begin, end);
return scir;
}
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

240
src/opt/eslim/synthesisEngine.hpp
View File

@ -1,240 +0,0 @@
/**CFile****************************************************************
FileName [synthesisEngine.hpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Procedures for synthesising Boolean relations.]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - March 2025.]
Revision [$Id: synthesisEngine.hpp,v 1.00 2025/03/17 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__OPT__ESLIM__SYNTHESISENGINE_h
#define ABC__OPT__ESLIM__SYNTHESISENGINE_h
#include <vector>
#include <unordered_set>
#include <unordered_map>
#include <memory>
#include "misc/util/abc_namespaces.h"
#include "aig/miniaig/miniaig.h"
#include "misc/vec/vec.h"
#include "satInterfaces.hpp"
ABC_NAMESPACE_CXX_HEADER_START
#define MAJ_NOBJS 64 // Const0 + Const1 + nVars + nNodes
namespace eSLIM {
// Based on Exa6_ManGenStart
template<class Derived>
class exactSynthesisEngine {
private:
Vec_Wrd_t * vSimsIn; // input signatures (nWords = 1, nIns <= 64)
Vec_Wrd_t * vSimsOut; // output signatures (nWords = 1, nOuts <= 6)
int nIns;
int nDivs; // divisors (const + inputs + tfi + sidedivs)
int nNodes;
int nOuts;
int nObjs;
int VarMarks[MAJ_NOBJS][2][MAJ_NOBJS] = {}; // default init the array
int nCnfVars;
int nCnfVars2;
int nCnfClauses;
// Assign outputs to their connectivity variables
std::unordered_map<int, std::vector<int>> connection_variables;
const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs;
eSLIMLog& log;
const eSLIMConfig& cfg;
exactSynthesisEngine( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes,
const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg);
int addClause(int lit1, int lit2, int lit3, int lit4);
static bool isNormalized( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut );
int markup();
int findFanin( Vec_Int_t * vValues, int i, int k, int nof_objs);
Mini_Aig_t * getAig(Vec_Int_t * assignment, int size);
Mini_Aig_t * getAig(Vec_Int_t * assignment);
void generateCNF(int fOrderNodes, int fUniqFans);
int startEncoding(int fOrderNodes, int fUniqFans );
void generateMinterm( int iMint);
int getGateEnablingLiteral(int index, bool negated);
int getAuxilaryVariableCount();
void introduceConnectionVariables();
void setupConnectionVariables();
void addConnectivityConstraints();
void addCombinedCycleConstraints();
std::unordered_map<int, std::unordered_set<int>> computeNotInPair(const std::unordered_map<int, std::unordered_set<int>>& pairs);
int prepareLits(int * pLits, int& nLits);
friend Derived;
};
// applies Cadical incrementally
class CadicalEngine : public exactSynthesisEngine<CadicalEngine> {
public:
CadicalEngine(Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes,
const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg);
Mini_Aig_t* getCircuit(int size, double timeout);
private:
using exactSynthesisEngine::addClause;
std::vector<int> gate_enabling_assumptions;
CadicalSolver solver;
int addClause( int * pLits, int nLits );
Vec_Int_t * solve(int size, double timeout);
int getAuxilaryVariableCountDerived();
int getGateEnablingLiteralImpl(int index, bool negated);
void addAssumptions(int size);
void addGateDeactivatedConstraint(int out);
std::vector<int> getAssumptions(int size);
friend exactSynthesisEngine<CadicalEngine>;
};
class OneshotEngine {
protected:
int getAuxilaryVariableCountDerived() {return 0;};
int getGateEnablingLiteralImpl(int index, bool negated) {return 0;};
// void addAssumptions(int size) {};
void addGateDeactivatedConstraint(int idx) {};
};
template <typename T>
class OneshotManager {
public:
OneshotManager(Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int maxnNodes,
const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg);
Mini_Aig_t* getCircuit(int size, double timeout);
private:
T getOneshotEngine(int size);
Vec_Wrd_t * vSimsIn; // input signatures (nWords = 1, nIns <= 64)
Vec_Wrd_t * vSimsOut; // output signatures (nWords = 1, nOuts <= 6)
int nIns;
int nDivs; // divisors (const + inputs + tfi + sidedivs)
int maxnNodes;
int nOuts;
const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs;
eSLIMLog& log;
const eSLIMConfig& cfg;
};
class CadicalEngineOneShot : public exactSynthesisEngine<CadicalEngineOneShot>, public OneshotEngine {
public:
CadicalEngineOneShot( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes,
const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg);
Mini_Aig_t* getCircuit(int size, double timeout);
private:
using exactSynthesisEngine::addClause;
int addClause( int * pLits, int nLits );
Vec_Int_t * solve(int size, double timeout);
CadicalSolver solver;
friend exactSynthesisEngine<CadicalEngineOneShot>;
};
class KissatEngineOneShot : public exactSynthesisEngine<KissatEngineOneShot>, public OneshotEngine {
public:
KissatEngineOneShot( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes,
const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg);
Mini_Aig_t* getCircuit(int size, double timeout);
private:
using exactSynthesisEngine::addClause;
int addClause( int * pLits, int nLits );
Vec_Int_t * solve(int size, double timeout);
KissatSolver solver;
friend exactSynthesisEngine<KissatEngineOneShot>;
};
class KissatCmdEngine : public exactSynthesisEngine<KissatCmdEngine>, public OneshotEngine {
public:
KissatCmdEngine( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes,
const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg);
Mini_Aig_t* getCircuit(int size, double timeout);
private:
using exactSynthesisEngine::addClause;
int addClause( int * pLits, int nLits );
Vec_Int_t * solve(int size, double timeout);
FILE * encoding_file;
// Ensure that there is no file with the same name in the diretory
constexpr static char * pFileNameIn = "_temp_.cnf";
constexpr static char * pFileNameOut = "_temp_out.cnf";
#ifdef WIN32
constexpr static char * pKissat = "kissat.exe";
#else
constexpr static char * pKissat = "kissat";
#endif
friend exactSynthesisEngine<KissatCmdEngine>;
};
template <typename T>
inline int exactSynthesisEngine<T>::addClause(int lit1, int lit2, int lit3, int lit4) {
int clause[4] = {lit1, lit2, lit3, lit4};
return static_cast<T*>(this)->addClause(clause, 4);
}
template <typename T>
inline int exactSynthesisEngine<T>::getGateEnablingLiteral(int index, bool negated) {
return static_cast<T*>(this)->getGateEnablingLiteralImpl(index, negated);
}
template <typename T>
inline int exactSynthesisEngine<T>::getAuxilaryVariableCount() {
int ncvars = connection_variables.empty() ? 0 : connection_variables.begin()->second.size() * connection_variables.size();
return ncvars + static_cast<T*>(this)->getAuxilaryVariableCountDerived();
}
typedef OneshotManager<CadicalEngineOneShot> CadicalOneShot;
typedef OneshotManager<KissatEngineOneShot> KissatOneShot;
typedef OneshotManager<KissatCmdEngine> KissatCmdOneShot;
}
ABC_NAMESPACE_CXX_HEADER_END
#include "synthesisEngine.tpp"
#endif

632
src/opt/eslim/synthesisEngine.tpp
View File

@ -1,632 +0,0 @@
/**CFile****************************************************************
FileName [synthesisEngine.tpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Procedures for synthesising Boolean relations.]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - March 2025.]
Revision [$Id: synthesisEngine.tpp,v 1.00 2025/03/17 00:00:00 Exp $]
***********************************************************************/
#include <numeric>
#ifdef WIN32
#include <process.h>
#define unlink _unlink
#else
#include <unistd.h>
#endif
#include "misc/util/utilTruth.h"
#include "synthesisEngine.hpp"
#include "utils.hpp"
ABC_NAMESPACE_HEADER_START
Vec_Int_t * Exa4_ManParse( char * pFileName );
ABC_NAMESPACE_HEADER_END
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
template <typename T>
exactSynthesisEngine<T>::exactSynthesisEngine( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes,
const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg)
: vSimsIn(vSimsIn), vSimsOut(vSimsOut), nIns(nIns), nDivs(nDivs), nNodes(nNodes),
nOuts(nOuts), forbidden_pairs(forbidden_pairs), log(log), cfg(cfg) {
assert( Vec_WrdSize(vSimsIn) == Vec_WrdSize(vSimsOut) );
nObjs = nDivs + nNodes + nOuts;
nCnfVars = markup();
introduceConnectionVariables();
nCnfVars2 = 0;
nCnfClauses = 0;
assert( nObjs < 64 );
}
template <typename T>
bool exactSynthesisEngine<T>::isNormalized( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut ) {
int i, Count = 0; word Temp;
Vec_WrdForEachEntry( vSimsIn, Temp, i ) {
if ( Temp & 1 ) {
Count++;
}
}
if ( Count ) {
return false;
}
if ( !(Vec_WrdEntry(vSimsOut, 0) & 1) ) {
return false;
}
return true;
}
template <typename T>
int exactSynthesisEngine<T>::markup() {
int i, k, j, nVars[3] = {1 + 3*nNodes, 0, 3*nNodes*Vec_WrdSize(vSimsIn)};
assert( nObjs <= MAJ_NOBJS );
for ( i = nDivs; i < nDivs + nNodes; i++ ) {
for ( k = 0; k < 2; k++ ) {
for ( j = 1+!k; j < i-k; j++ ) {
VarMarks[i][k][j] = nVars[0] + nVars[1]++;
}
}
}
for ( i = nDivs + nNodes; i < nObjs; i++ ) {
for ( j = 0; j < nDivs + nNodes; j++ ) {
VarMarks[i][0][j] = nVars[0] + nVars[1]++;
}
}
return nVars[0] + nVars[1] + nVars[2];
}
template <typename T>
int exactSynthesisEngine<T>::findFanin( Vec_Int_t * vValues, int i, int k, int nof_objs ) {
int j, Count = 0, iVar = -1;
for ( j = 0; j < nof_objs; j++ ) {
if ( VarMarks[i][k][j] && Vec_IntEntry(vValues, VarMarks[i][k][j]) ){
iVar = j;
Count++;
}
}
assert( Count == 1 );
return iVar;
}
template <typename T>
Mini_Aig_t * exactSynthesisEngine<T>::getAig(Vec_Int_t * vValues) {
return getAig(vValues, nNodes);
}
template <typename T>
Mini_Aig_t * exactSynthesisEngine<T>::getAig(Vec_Int_t * vValues, int size) {
assert (size >= 0 && size <= nNodes && "Invalid size for AIG construction given.");
int i, k, Compl[MAJ_NOBJS] = {0};
int nof_Objs = nDivs + size + nOuts;
Mini_Aig_t * pMini = Mini_AigStartSupport( nDivs-1, nof_Objs );
for ( i = nDivs; i < nDivs + size; i++ ) {
int iNodes[2] = {0};
int iVarStart = 1 + 3*(i - nDivs);//
int Val1 = Vec_IntEntry(vValues, iVarStart);
int Val2 = Vec_IntEntry(vValues, iVarStart+1);
int Val3 = Vec_IntEntry(vValues, iVarStart+2);
Compl[i] = Val1 && Val2 && Val3;
for ( k = 0; k < 2; k++ ) {
int iNode = findFanin(vValues, i, !k, nof_Objs);
int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
iNodes[k] = Abc_Var2Lit(iNode, fComp ^ Compl[iNode]);
}
if ( Val1 && Val2 ) {
if ( Val3 ) {
Mini_AigOr( pMini, iNodes[0], iNodes[1] );
} else {
Mini_AigXorSpecial( pMini, iNodes[0], iNodes[1] );
}
} else {
Mini_AigAnd( pMini, iNodes[0], iNodes[1] );
}
}
for ( i = nDivs + nNodes; i < nObjs; i++ ) {
int iVar = findFanin( vValues, i, 0, nof_Objs);
Mini_AigCreatePo( pMini, Abc_Var2Lit(iVar, Compl[iVar]) );
}
assert( nof_Objs == Mini_AigNodeNum(pMini) );
return pMini;
}
template <typename T>
void exactSynthesisEngine<T>::generateCNF( int fOrderNodes, int fUniqFans ) {
int m;
startEncoding( fOrderNodes, fUniqFans );
// Ignore pattern for all false input pattern (as we start with m=1)
for ( m = 1; m < Vec_WrdSize(vSimsIn); m++ ) {
generateMinterm( m );
}
if (forbidden_pairs.size() > 0) {
addConnectivityConstraints();
}
}
template <typename T>
void exactSynthesisEngine<T>::introduceConnectionVariables() {
std::unordered_set<int> inputs_in_pairs;
// for (const auto& [out, inputs] : forbidden_pairs) {
for (const auto& it: forbidden_pairs) {
const auto& inputs = it.second;
inputs_in_pairs.insert(inputs.begin(), inputs.end());
}
int nCVars = nObjs - 1; // The constant node does not depend on any node
for (int in : inputs_in_pairs) {
connection_variables.emplace(in, std::vector<int> (nCVars, 0));
std::iota(connection_variables[in].begin(), connection_variables[in].end(), nCnfVars);
nCnfVars += nCVars;
}
}
template <typename T>
void exactSynthesisEngine<T>::setupConnectionVariables() {
// for (const auto& [in, cvars] : connection_variables) {
for (const auto& it: connection_variables) {
const auto& in = it.first;
const auto& cvars = it.second;
addClause(Abc_Var2Lit(cvars[in],0),0,0,0);
for (int i = nDivs; i < nDivs + nNodes; i++ ) {
int gate_idx = i - nDivs;
for (int j = 1; j < i - 1; j++) {
addClause(Abc_Var2Lit(VarMarks[i][0][j + 1], 1), Abc_Var2Lit(cvars[j], 1), Abc_Var2Lit(cvars[i - 1], 0), getGateEnablingLiteral(gate_idx, 1));
addClause(Abc_Var2Lit(VarMarks[i][1][j], 1), Abc_Var2Lit(cvars[j - 1], 1), Abc_Var2Lit(cvars[i - 1], 0), getGateEnablingLiteral(gate_idx, 1));
}
}
for (int i = nDivs + nNodes; i < nObjs; i++) {
for (int j = 1; j < nDivs + nNodes; j++) {
addClause(Abc_Var2Lit(VarMarks[i][0][j], 1), Abc_Var2Lit(cvars[j - 1], 1), Abc_Var2Lit(cvars[i - 1], 0),0);
}
}
}
}
template <typename T>
void exactSynthesisEngine<T>::addConnectivityConstraints() {
assert (forbidden_pairs.size() > 0 && "Connectivity constraints are only needed if there are forbidden pairs.");
setupConnectionVariables();
// If there are forbidden pairs for more than one input it is possible that a loop is obtained via two pairs
if (forbidden_pairs.size() > 1) {
addCombinedCycleConstraints();
}
// for (const auto& [out, inputs] : forbidden_pairs) {
for (const auto& it: forbidden_pairs) {
const auto& out = it.first;
const auto& inputs = it.second;
for (int in : inputs) {
const auto& cvars = connection_variables.at(in);
int out_obj_idx = nDivs + nNodes + out;
addClause(Abc_Var2Lit(cvars[out_obj_idx - 1], 1), 0, 0, 0);
}
}
}
template <typename T>
void exactSynthesisEngine<T>::addCombinedCycleConstraints() {
assert (forbidden_pairs.size() > 1 && "Combined connectivity constraints are only needed if there are forbidden pairs for multiple inputs.");
std::unordered_map<int, std::unordered_set<int>> not_in_pair = computeNotInPair(forbidden_pairs);
// for (const auto& [out, inputs] : not_in_pair) {
for (const auto& it: not_in_pair) {
const auto& out = it.first;
const auto& inputs = it.second;
for (int in : inputs) {
const auto& cvars = connection_variables.at(in);
int out_obj_idx = nDivs + nNodes + out;
for (int in2 : forbidden_pairs.at(out)) {
addClause(Abc_Var2Lit(cvars[out_obj_idx - 1], 1), Abc_Var2Lit(cvars[in2], 0),0,0);
}
}
}
}
template <typename T>
std::unordered_map<int, std::unordered_set<int>> exactSynthesisEngine<T>::computeNotInPair(const std::unordered_map<int, std::unordered_set<int>>& pairs) {
std::unordered_set<int> all_inputs_in_pairs;
// for (const auto& [out, in] : pairs) {
for (const auto& it: pairs) {
const auto& in = it.second;
all_inputs_in_pairs.insert(in.begin(), in.end());
}
std::unordered_map<int, std::unordered_set<int>> not_in_pair;
// for (const auto& [out, in] : pairs) {
for (const auto& it: pairs) {
const auto& out = it.first;
const auto& in = it.second;
if (in.size() == all_inputs_in_pairs.size()) {
continue;
}
for (int i : all_inputs_in_pairs) {
if (in.find(i) == in.end()) {
not_in_pair[out].insert(i);
}
}
}
return not_in_pair;
}
template <typename T>
int exactSynthesisEngine<T>::startEncoding(int fOrderNodes, int fUniqFans )
{
int pLits[2*MAJ_NOBJS], i, j, k, n, m, nLits;
for ( i = nDivs; i < nDivs + nNodes; i++ )
{
int gate_idx = i - nDivs;
int iVarStart = 1 + 3*(i - nDivs);//
for ( k = 0; k < 2; k++ )
{
nLits = 0;
for ( j = 0; j < nObjs; j++ )
if ( VarMarks[i][k][j] )
pLits[nLits++] = Abc_Var2Lit( VarMarks[i][k][j], 0 );
assert( nLits > 0 );
static_cast<T*>(this)->addClause( pLits, nLits );
for ( n = 0; n < nLits; n++ )
for ( m = n+1; m < nLits; m++ )
addClause( Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), getGateEnablingLiteral(gate_idx, 1), 0 );
if ( k == 1 )
break;
for ( j = 0; j < nObjs; j++ ) if ( VarMarks[i][0][j] )
for ( n = j; n < nObjs; n++ ) if ( VarMarks[i][1][n] )
addClause( Abc_Var2Lit(VarMarks[i][0][j], 1), Abc_Var2Lit(VarMarks[i][1][n], 1), getGateEnablingLiteral(gate_idx, 1), 0 );
}
if ( fOrderNodes )
for ( j = nDivs; j < i; j++ )
for ( n = 0; n < nObjs; n++ ) if ( VarMarks[i][0][n] )
for ( m = n+1; m < nObjs; m++ ) if ( VarMarks[j][0][m] )
addClause( Abc_Var2Lit(VarMarks[i][0][n], 1), Abc_Var2Lit(VarMarks[j][0][m], 1), getGateEnablingLiteral(gate_idx, 1), 0 );
for ( j = nDivs; j < i; j++ )
for ( k = 0; k < 2; k++ ) if ( VarMarks[i][k][j] )
for ( n = 0; n < nObjs; n++ ) if ( VarMarks[i][!k][n] )
for ( m = 0; m < 2; m++ ) if ( VarMarks[j][m][n] )
addClause( Abc_Var2Lit(VarMarks[i][k][j], 1), Abc_Var2Lit(VarMarks[i][!k][n], 1), Abc_Var2Lit(VarMarks[j][m][n], 1), getGateEnablingLiteral(gate_idx, 1) );
for ( k = 0; k < 3; k++ )
addClause( Abc_Var2Lit(iVarStart, k==1), Abc_Var2Lit(iVarStart+1, k==2), Abc_Var2Lit(iVarStart+2, k!=0), getGateEnablingLiteral(gate_idx, 1));
if ( !cfg.allow_xors )
addClause( Abc_Var2Lit(iVarStart, 1), Abc_Var2Lit(iVarStart+1, 1), Abc_Var2Lit(iVarStart+2, 0), getGateEnablingLiteral(gate_idx, 1));
}
for ( i = nDivs; i < nDivs + nNodes; i++ )
{
int gate_idx = i - nDivs;
nLits = 0;
for ( k = 0; k < 2; k++ )
for ( j = i+1; j < nObjs; j++ )
if ( VarMarks[j][k][i] )
pLits[nLits++] = Abc_Var2Lit( VarMarks[j][k][i], 0 );
if ( fUniqFans )
for ( n = 0; n < nLits; n++ )
for ( m = n+1; m < nLits; m++ )
addClause( Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), getGateEnablingLiteral(gate_idx, 1), 0 );
}
for ( i = nDivs + nNodes; i < nObjs; i++ )
{
static_cast<T*>(this)->addGateDeactivatedConstraint(i);
nLits = 0;
for ( j = 0; j < nDivs + nNodes; j++ ) if ( VarMarks[i][0][j] ) {
pLits[nLits++] = Abc_Var2Lit( VarMarks[i][0][j], 0 );
}
static_cast<T*>(this)->addClause( pLits, nLits );
for ( n = 0; n < nLits; n++ )
for ( m = n+1; m < nLits; m++ )
addClause( Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
}
return 1;
}
template <typename T>
void exactSynthesisEngine<T>::generateMinterm( int iMint) {
int internalCnfVars = nCnfVars - getAuxilaryVariableCount(); // for each gate we add an assumption
int iNodeVar = internalCnfVars + 3*nNodes*(iMint - Vec_WrdSize(vSimsIn));
int iOutMint = Abc_Tt6FirstBit( Vec_WrdEntry(vSimsOut, iMint) );
int fOnlyOne = Abc_TtSuppOnlyOne( (int)Vec_WrdEntry(vSimsOut, iMint) );
int i, k, n, j, VarVals[MAJ_NOBJS];
int fAllOnes = Abc_TtCountOnes( Vec_WrdEntry(vSimsOut, iMint) ) == (1 << nOuts);
if ( fAllOnes )
return;
assert( nObjs <= MAJ_NOBJS );
assert( iMint < Vec_WrdSize(vSimsIn) );
assert( nOuts <= 6 );
for ( i = 0; i < nDivs; i++ ) {
VarVals[i] = (Vec_WrdEntry(vSimsIn, iMint) >> i) & 1;
}
for ( i = 0; i < nNodes; i++ ) {
VarVals[nDivs + i] = Abc_Var2Lit(iNodeVar + 3*i + 2, 0);
}
if ( fOnlyOne ) {
for ( i = 0; i < nOuts; i++ )
VarVals[nDivs + nNodes + i] = (iOutMint >> i) & 1;
} else {
word t = Abc_Tt6Stretch( Vec_WrdEntry(vSimsOut, iMint), nOuts );
int i, c, nCubes = 0, pCover[100], pLits[10];
int iOutVar = nCnfVars + nCnfVars2; nCnfVars2 += nOuts;
for ( i = 0; i < nOuts; i++ ) {
VarVals[nDivs + nNodes + i] = Abc_Var2Lit(iOutVar + i, 0);
}
assert( t );
if ( ~t ) {
Abc_Tt6IsopCover( ~t, ~t, nOuts, pCover, &nCubes );
for ( c = 0; c < nCubes; c++ ) {
int nLits = 0;
for ( i = 0; i < nOuts; i++ ) {
int iLit = (pCover[c] >> (2*i)) & 3;
if ( iLit == 1 || iLit == 2 )
pLits[nLits++] = Abc_Var2Lit(iOutVar + i, iLit != 1);
}
static_cast<T*>(this)->addClause( pLits, nLits );
}
}
}
for ( i = nDivs; i < nDivs + nNodes; i++ ) {
int iVarStart = 1 + 3*(i - nDivs);//
int iBaseVarI = iNodeVar + 3*(i - nDivs);
for ( k = 0; k < 2; k++ ) {
for ( j = 0; j < i; j++ ) {
if ( VarMarks[i][k][j] ) {
for ( n = 0; n < 2; n++ ) {
addClause( Abc_Var2Lit(VarMarks[i][k][j], 1), Abc_Var2Lit(iBaseVarI + k, n), Abc_LitNotCond(VarVals[j], !n), 0);
}
}
}
}
for ( k = 0; k < 4; k++ ) {
for ( n = 0; n < 2; n++ ) {
addClause( Abc_Var2Lit(iBaseVarI + 0, k&1), Abc_Var2Lit(iBaseVarI + 1, k>>1), Abc_Var2Lit(iBaseVarI + 2, !n), Abc_Var2Lit(k ? iVarStart + k-1 : 0, n));
}
}
}
for ( i = nDivs + nNodes; i < nObjs; i++ ) {
for ( j = 0; j < nDivs + nNodes; j++ ) {
if ( VarMarks[i][0][j] ) {
for ( n = 0; n < 2; n++ ) {
addClause( Abc_Var2Lit(VarMarks[i][0][j], 1), Abc_LitNotCond(VarVals[j], n), Abc_LitNotCond(VarVals[i], !n), 0);
}
}
}
}
}
template <typename T>
int exactSynthesisEngine<T>::prepareLits(int * pLits, int& nLits) {
int k = 0;
for ( int i = 0; i < nLits; i++ ) {
if ( pLits[i] == 1 )
return 0;
else if ( pLits[i] == 0 )
continue;
else if ( pLits[i] <= 2*(nCnfVars + nCnfVars2) )
pLits[k++] = pLits[i];
else assert( 0 );
}
nLits = k;
return 1;
}
inline CadicalEngine::CadicalEngine(Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes,
const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg)
: exactSynthesisEngine(vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, forbidden_pairs, log, cfg) {
gate_enabling_assumptions.reserve(nNodes);
for (int i = 0; i < nNodes; i++) {
gate_enabling_assumptions.push_back(nCnfVars + i);
}
nCnfVars += nNodes;
generateCNF(0, 0);
}
inline int CadicalEngine::addClause( int * pLits, int nLits ) {
if (prepareLits(pLits, nLits) == 0) {
return 0;
}
assert( nLits > 0 );
solver.addClause(pLits, nLits);
return 1;
}
inline Vec_Int_t * CadicalEngine::solve( int size, double timeout) {
std::vector<int> assumptions = getAssumptions(size);
solver.assume(assumptions);
int status = timeout > 0 ? solver.solve(timeout) : solver.solve();
Vec_Int_t * vRes = status == 10 ? solver.getModelVec() : nullptr;
if (status == 10) {
log.cummulative_sat_runtimes_per_size[size] += solver.getRunTime();
log.nof_sat_calls_per_size[size] ++;
} else if (status == 20) {
log.cummulative_unsat_runtimes_per_size[size] += solver.getRunTime();
log.nof_unsat_calls_per_size[size] ++;
}
return vRes;
}
Mini_Aig_t* CadicalEngine::getCircuit(int size, double timeout) {
addAssumptions(size);
Vec_Int_t * vValues = solve(size, timeout);
Mini_Aig_t * pMini = vValues ? getAig(vValues, size) : nullptr;
Vec_IntFreeP( &vValues );
return pMini;
}
inline std::vector<int> CadicalEngine::getAssumptions(int size) {
std::vector<int> assumptions(nNodes);
for (int i = 0; i < size; i++) {
assumptions[i] = gate_enabling_assumptions[i];
}
for (int i = size; i < nNodes; i++) {
assumptions[i] = -gate_enabling_assumptions[i];
}
return assumptions;
}
inline void CadicalEngine::addGateDeactivatedConstraint(int out_idx) {
for (int j = nDivs; j < nDivs + nNodes; j++ ) {
int gate_idx = j - nDivs;
// if a gate is disabled then it shall not be an output
addClause( Abc_Var2Lit(VarMarks[out_idx][0][j],1), Abc_Var2Lit( gate_enabling_assumptions[gate_idx], 0 ), 0, 0 );
}
}
inline int CadicalEngine::getGateEnablingLiteralImpl(int index, bool negated) {
return Abc_Var2Lit( gate_enabling_assumptions[index], negated );
}
inline int CadicalEngine::getAuxilaryVariableCountDerived() {
return nNodes; // We add an assumption for each gate
}
inline void CadicalEngine::addAssumptions(int size) {
solver.assume(getAssumptions(size));
}
template <typename T>
OneshotManager<T>::OneshotManager(Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int maxnNodes,
const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg)
: vSimsIn(vSimsIn), vSimsOut(vSimsOut), nIns(nIns), nDivs(nDivs), maxnNodes(maxnNodes), nOuts(nOuts), forbidden_pairs(forbidden_pairs), log(log), cfg(cfg) {
}
template <typename T>
T OneshotManager<T>::getOneshotEngine(int size) {
assert(size <= maxnNodes);
T oneshotEngine(vSimsIn, vSimsOut, nIns, nDivs, nOuts, size, forbidden_pairs, log, cfg);
return oneshotEngine;
}
template <typename T>
Mini_Aig_t* OneshotManager<T>::getCircuit(int size, double timeout) {
T synth = getOneshotEngine(size);
return synth.getCircuit(size, timeout);
}
inline CadicalEngineOneShot::CadicalEngineOneShot( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes,
const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg)
: exactSynthesisEngine<CadicalEngineOneShot>(vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, forbidden_pairs, log, cfg) {
}
inline Vec_Int_t* CadicalEngineOneShot::solve( int size, double timeout) {
int status = timeout > 0 ? solver.solve(timeout) : solver.solve();
Vec_Int_t * vRes = status != 10 ? nullptr : solver.getModelVec();
return vRes;
}
Mini_Aig_t* CadicalEngineOneShot::getCircuit(int size, double timeout) {
generateCNF(0, 0);
Vec_Int_t * vValues = solve(size, timeout);
Mini_Aig_t * pMini = vValues ? getAig(vValues, size) : nullptr;
Vec_IntFreeP( &vValues );
return pMini;
}
inline int CadicalEngineOneShot::addClause( int * pLits, int nLits ) {
if (prepareLits(pLits, nLits) == 0) {
return 0;
}
assert( nLits > 0 );
solver.addClause(pLits, nLits);
return 1;
}
inline KissatEngineOneShot::KissatEngineOneShot(Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes,
const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg)
: exactSynthesisEngine<KissatEngineOneShot>(vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, forbidden_pairs, log, cfg) {
}
Mini_Aig_t* KissatEngineOneShot::getCircuit(int size, double timeout) {
solver.init(nCnfVars);
generateCNF(0, 0);
Vec_Int_t * vValues = solve(size, timeout);
Mini_Aig_t * pMini = vValues ? getAig(vValues, size) : nullptr;
Vec_IntFreeP( &vValues );
return pMini;
}
inline Vec_Int_t *KissatEngineOneShot::solve( int size, double timeout) {
// TODO: The used interface does not yet allow timeouts
int status = solver.solve();
Vec_Int_t * vRes = status != 10 ? nullptr : solver.getModelVec();
return vRes;
}
inline int KissatEngineOneShot::addClause( int * pLits, int nLits ) {
if (prepareLits(pLits, nLits) == 0) {
return 0;
}
assert( nLits > 0 );
solver.addClause(pLits, nLits);
return 1;
}
inline KissatCmdEngine::KissatCmdEngine(Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes,
const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg)
: exactSynthesisEngine<KissatCmdEngine>(vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, forbidden_pairs, log, cfg) {
}
Mini_Aig_t* KissatCmdEngine::getCircuit(int size, double timeout) {
encoding_file = fopen( pFileNameIn, "wb" );
fputs( "p cnf \n", encoding_file );
generateCNF(0, 0);
Vec_Int_t * vValues = solve(size, timeout);
Mini_Aig_t * pMini = vValues ? getAig(vValues, size) : nullptr;
Vec_IntFreeP( &vValues );
return pMini;
}
inline int KissatCmdEngine::addClause( int * pLits, int nLits ) {
if (prepareLits(pLits, nLits) == 0) {
return 0;
}
assert( nLits > 0 );
if ( encoding_file ) {
nCnfClauses++;
for ( int i = 0; i < nLits; i++ ) {
fprintf( encoding_file, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
}
fprintf( encoding_file, "0\n" );
}
return 1;
}
inline Vec_Int_t * KissatCmdEngine::solve(int size, double timeout) {
rewind( encoding_file );
fprintf( encoding_file, "p cnf %d %d", nCnfVars + nCnfVars2, nCnfClauses );
fclose( encoding_file );
encoding_file = nullptr;
char Command[1000], * pCommand = (char *)&Command;
// TODO:
// if ( TimeOut )
// sprintf( pCommand, "%s --time=%d -q %s > %s", pKissat, TimeOut, pFileNameIn, pFileNameOut );
// else
// sprintf( pCommand, "%s -q %s > %s", pKissat, pFileNameIn, pFileNameOut );
sprintf( pCommand, "%s -q %s > %s", pKissat, pFileNameIn, pFileNameOut );
#ifdef __wasm
if ( 1 ) {
#else
if ( system( pCommand ) == -1 ) {
#endif
std::cerr << "Command " << pCommand << " failed\n";
return nullptr;
}
Vec_Int_t * vRes = Exa4_ManParse( pFileNameOut );
unlink( pFileNameIn );
return vRes;
}
}
ABC_NAMESPACE_CXX_HEADER_END

115
src/opt/eslim/synthesisEngines.hpp Normal file
View File

@ -0,0 +1,115 @@
/**CFile****************************************************************
FileName [synthesisEngines.hpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Synthesis engines]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__OPT__ESLIM__SYNTHESISENGINES_hpp
#define ABC__OPT__ESLIM__SYNTHESISENGINES_hpp
#include "misc/util/abc_global.h"
#include "eslimCirMan.hpp"
#include "areaEngine.hpp"
#include "delayEngine.hpp"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
class Relation;
class Subcircuit;
class eSLIMConfig;
class eSLIMLog;
class AreaMinimizer {
public:
static eSLIMCirMan optimize(const eSLIMCirMan& encompassing, const Relation& relation, const Subcircuit& subcir,
const eSLIMConfig& cfg, eSLIMLog& log) {
return AreaEngine::synthesiseMinimumSizeCircuit(relation, subcir, cfg, log);
}
private:
AreaMinimizer() = default;
};
class AreaDelayConstraintMinimizer {
public:
static eSLIMCirMan optimize(eSLIMCirMan& encompassing, const Relation& relation, Subcircuit& subcir,
const eSLIMConfig& cfg, eSLIMLog& log) {
subcir.setupTimings(encompassing);
return DelayEngine::synthesizeMinimumAreaDelayConstraintCircuit(relation, subcir, encompassing.getDepth(), cfg, log);
}
private:
AreaDelayConstraintMinimizer() = default;
};
class AreaDelayMinimizer {
public:
static eSLIMCirMan optimize(eSLIMCirMan& encompassing, const Relation& relation, Subcircuit& subcir,
const eSLIMConfig& cfg, eSLIMLog& log) {
subcir.setupTimings(encompassing);
return DelayEngine::synthesizeMinimumAreaDelayCircuit(relation, subcir, cfg, log);
}
private:
AreaDelayMinimizer() = default;
};
class DelayMinimizer {
public:
static eSLIMCirMan optimize(eSLIMCirMan& encompassing, const Relation& relation, Subcircuit& subcir,
const eSLIMConfig& cfg, eSLIMLog& log) {
int max_crossing_path = subcir.setupTimings(encompassing);
unsigned int max_size = std::min(cfg.subcircuit_max_size, static_cast<unsigned int>(subcir.nodes.size() + cfg.additional_gates));
return DelayEngine::synthesizeMinimumDelayCircuit(relation, subcir, max_crossing_path, max_size, cfg, log);
}
private:
DelayMinimizer() = default;
};
class DelayAreaMinimizer {
public:
static eSLIMCirMan optimize(eSLIMCirMan& encompassing, const Relation& relation, Subcircuit& subcir,
const eSLIMConfig& cfg, eSLIMLog& log) {
int max_crossing_path = subcir.setupTimings(encompassing);
unsigned int max_size = std::min(cfg.subcircuit_max_size, static_cast<unsigned int>(subcir.nodes.size() + cfg.additional_gates));
return DelayEngine::synthesizeMinimumDelayAreaCircuit(relation, subcir, max_crossing_path, max_size, cfg, log);
}
private:
DelayAreaMinimizer() = default;
};
template<class T>
struct isDelayEngine : std::integral_constant< bool,
std::is_same<eSLIM::AreaDelayMinimizer, typename std::remove_cv<T>::type>::value
|| std::is_same<eSLIM::AreaDelayConstraintMinimizer, typename std::remove_cv<T>::type>::value
|| std::is_same<eSLIM::DelayMinimizer, typename std::remove_cv<T>::type>::value
|| std::is_same<eSLIM::DelayAreaMinimizer, typename std::remove_cv<T>::type>::value
> {};
static_assert(!isDelayEngine<AreaMinimizer>::value);
static_assert(isDelayEngine<AreaDelayMinimizer>::value);
static_assert(isDelayEngine<AreaDelayConstraintMinimizer>::value);
static_assert(isDelayEngine<DelayMinimizer>::value);
static_assert(isDelayEngine<DelayAreaMinimizer>::value);
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

178
src/opt/eslim/tabooList.hpp Normal file
View File

@ -0,0 +1,178 @@
/**CFile****************************************************************
FileName [tabooList.hpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Taboo list for subcircuit selection.]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__OPT__ESLIM__TABOOLIST_hpp
#define ABC__OPT__ESLIM__TABOOLIST_hpp
#include <set>
#include <random>
#include <algorithm>
#include "misc/util/abc_namespaces.h"
#include "eslimCirMan.hpp"
#include "subcircuit.hpp"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
class TabooList {
public:
TabooList(const eSLIMCirMan& es_man);
int getRandomNonTaboo(std::mt19937& rng, double taboo_ratio, unsigned int taboo_time);
template<typename BiasCondition>
int getBiasedRandomNonTaboo(std::mt19937& rng, unsigned int bias, double taboo_ratio, unsigned int taboo_time);
void reset();
private:
struct eSLIMCirObjCompBase {
bool operator()(eSLIMCirObj* a, eSLIMCirObj* b) const {
return a->getId() < b->getId();
}
};
struct eSLIMCirObjComp {
bool operator()(eSLIMCirObj* a, eSLIMCirObj* b) const {
return a->isTaboo < b->isTaboo || (a->isTaboo == b->isTaboo && eSLIMCirObjCompBase()(a,b));
}
};
void updateTaboo(double taboo_ratio, unsigned int taboo_time);
void registerReplacement(eSLIMCirMan& replacement, const Subcircuit& subcir);
void discardSubcircuit(const Subcircuit& subcir);
void removeRedundantNode(eSLIMCirObj* nptr);
void fill();
void addNode(eSLIMCirObj* pobj);
void discardNode(eSLIMCirObj* pobj);
void addNonTaboo(eSLIMCirObj* pobj);
void removeNonTaboo(eSLIMCirObj* pobj);
const eSLIMCirMan& es_man;
std::set<eSLIMCirObj*, eSLIMCirObjComp> taboo_nodes;
std::set<eSLIMCirObj*, eSLIMCirObjCompBase> non_taboo_nodes;
friend eSLIMCirMan;
};
inline TabooList::TabooList(const eSLIMCirMan& es_man)
: es_man(es_man) {
fill();
}
inline void TabooList::fill() {
for (int i = es_man.getNofPis() + 1; i < es_man.getNofObjs()-es_man.getNofPos(); i++) {
auto pObj = es_man.nodes[i].get();
addNonTaboo(pObj);
}
}
inline void TabooList::reset() {
taboo_nodes.clear();
non_taboo_nodes.clear();
fill();
}
inline void TabooList::updateTaboo(double taboo_ratio, unsigned int taboo_time) {
assert (taboo_ratio > 0 && taboo_ratio < 1);
auto it = taboo_nodes.begin();
while (it != taboo_nodes.end()) {
if (!es_man.isTaboo(*(*it), taboo_time)) {
addNonTaboo(*it);
it = taboo_nodes.erase(it);
} else if (taboo_nodes.size() > static_cast<double>(es_man.getNofGates()) * taboo_ratio) {
addNonTaboo(*it);
it = taboo_nodes.erase(it);
} else {
return;
}
}
}
inline void TabooList::registerReplacement(eSLIMCirMan& replacement, const Subcircuit& subcir) {
discardSubcircuit(subcir);
for (int i = replacement.getNofPis() + 1; i < replacement.getNofObjs() - replacement.getNofPos(); i++) {
auto pObj = replacement.nodes[i].get();
taboo_nodes.insert(pObj);
}
}
inline void TabooList::discardSubcircuit(const Subcircuit& subcir) {
for (int nd : subcir.nodes) {
discardNode(es_man.nodes[nd].get());
}
}
inline void TabooList::removeRedundantNode(eSLIMCirObj* nptr) {
discardNode(nptr);
}
inline int TabooList::getRandomNonTaboo(std::mt19937& rng, double taboo_ratio, unsigned int taboo_time) {
updateTaboo(taboo_ratio, taboo_time);
assert(non_taboo_nodes.size() > 0);
std::uniform_int_distribution<std::mt19937::result_type> udistr(0, non_taboo_nodes.size() - 1);
int rv = udistr(rng);
auto it = non_taboo_nodes.begin();
std::advance(it, rv);
return (*it)->node_id;
}
template<typename BiasCondition>
int TabooList::getBiasedRandomNonTaboo(std::mt19937& rng, unsigned int bias, double taboo_ratio, unsigned int taboo_time) {
updateTaboo(taboo_ratio, taboo_time);
std::vector<int> weights;
weights.reserve(non_taboo_nodes.size());
for (const auto& pObj : non_taboo_nodes) {
if (BiasCondition::useBias(es_man, *pObj)) {
weights.push_back(bias);
} else {
weights.push_back(1);
}
}
std::discrete_distribution<std::mt19937::result_type> ddistr(weights.begin(), weights.end());
int rv = ddistr(rng);
auto it = non_taboo_nodes.begin();
std::advance(it, rv);
return (*it)->node_id;
}
inline void TabooList::addNode(eSLIMCirObj* pobj) {
taboo_nodes.insert(pobj);
}
inline void TabooList::discardNode(eSLIMCirObj* pobj) {
removeNonTaboo(pobj);
taboo_nodes.erase(pobj);
}
inline void TabooList::addNonTaboo(eSLIMCirObj* pobj) {
non_taboo_nodes.insert(pobj);
}
inline void TabooList::removeNonTaboo(eSLIMCirObj* pobj) {
non_taboo_nodes.erase(pobj);
}
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

184
src/opt/eslim/utils.hpp
View File

@ -6,48 +6,118 @@
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Utilities for the eSLIM package.]
Synopsis [Utilities]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - March 2025.]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: utils.hpp,v 1.00 2025/03/17 00:00:00 Exp $]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__OPT__ESLIM__UTILS_h
#define ABC__OPT__ESLIM__UTILS_h
#ifndef ABC__OPT__ESLIM__UTILS_hpp
#define ABC__OPT__ESLIM__UTILS_hpp
#include <vector>
#include <unordered_map>
#include <unordered_set>
#include "misc/util/abc_namespaces.h"
#include "misc/vec/vec.h"
#include "aig/gia/gia.h"
#include "misc/util/abc_global.h"
#if __cplusplus >= 202002L
// C++20 (and later) code
#include <bit>
#endif
#if __cplusplus >= 202002L
// // C++20 (and later) code
// #include <bit>
#define popcount(x) std::popcount(x)
#elif defined(__GNUC__)
#define popcount(x) __builtin_popcountll(x)
// #elif defined(_MSC_VER)
#elif defined(_WIN64)
#define popcount(x) __popcnt64(x)
#else
inline int popcount64Impl(ABC_UINT64_T x) {
// Constants are 64-bit masks
const ABC_UINT64_T m1 = 0x5555555555555555;
const ABC_UINT64_T m2 = 0x3333333333333333;
const ABC_UINT64_T m3 = 0x0F0F0F0F0F0F0F0F;
const ABC_UINT64_T m4 = 0x0101010101010101;
x = x - ((x >> 1) & m1);
x = (x & m2) + ((x >> 2) & m2);
x = (x + (x >> 4)) & m3;
return (x * m4) >> 56;
}
#define popcount(x) popcount64Impl(x)
#endif
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
struct eSLIMConfig {
bool extended_normality_processing = false;
inline int lsb(ABC_UINT64_T tt) {
#if __cplusplus >= 202002L
if (tt == 0) {
return -1;
}
return std::countr_zero(tt);
#elif defined(__GNUC__)
return __builtin_ffsl(tt) - 1;
// #elif defined(_MSC_VER)
#elif defined(_WIN64)
if (tt == 0) {
return -1;
}
int x = 0;
bool status = _BitScanForward64(x, tt);
return x;
#else
if (tt == 0) {
return -1;
}
ABC_UINT64_T lsb = tt & -tt;
const ABC_UINT64_T debruijn = 0x03f79d71b4cb0a89ULL;
ABC_UINT64_T scrambled = (lsb * debruijn) >> 58;
const int index64[64] = {
0, 1, 48, 2, 57, 49, 28, 3, 61, 58, 50, 42, 29, 17, 4, 62,
55, 59, 36, 53, 51, 43, 22, 30, 18, 12, 5, 63, 35, 56, 60, 54,
37, 52, 44, 27, 23, 31, 19, 8, 13, 6, 64, 32, 47, 38, 45, 21,
26, 24, 39, 16, 7, 64, 33, 46, 20, 25, 41, 15, 64, 34, 40, 64
};
return index64[scrambled];
#endif
}
struct eSLIMConfig {
bool aig = true;
int gate_size = 2;
bool apply_strash = true;
bool fix_seed = false;
bool fill_subcircuits = false;
bool trial_limit_active = true;
bool allow_xors = false;
bool allow_xors = false;
unsigned int timeout = 3600;
unsigned int iterations = 0;
unsigned int subcircuit_size_bound = 6;
unsigned int subcircuit_max_size = 6;
unsigned int additional_gates = 0;
unsigned int strash_intervall = 100;
int seed = 0;
unsigned int nselection_trials = 100;
double expansion_probability = 0.6;
unsigned int nselection_trials = 120;
double expansion_probability = 0.5;
unsigned int bias = 2;
unsigned int nwindows = 1;
unsigned int window_size = 500;
unsigned int taboo_time = 100;
double taboo_ratio = 0.5;
// times given in sec
int minimum_sat_timeout = 1;
@ -55,49 +125,73 @@ namespace eSLIM {
int minimum_dynamic_timeout_sample_size = 50;
double dynamic_timeout_buffer_factor = 1.4;
int relation_generation_timeout = 180;
bool approximate_relation = false; // Compute an overapproximation of the relation that may not use all don't cares by limiting the tfo of the subcircuit
bool generate_relation_with_tfi_limit = false; // If approximate_relation is true, also limit the tfi of the subcircuit
unsigned int relation_tfi_bound = 0;
unsigned int relation_tfo_bound = 0;
int verbosity_level = 0;
};
struct eSLIMLog {
unsigned int iteration_count = 0;
double relation_generation_time = 0;
double synthesis_time = 0;
unsigned int subcircuits_with_forbidden_pairs = 0;
class eSLIMLog {
std::vector<int> nof_analyzed_circuits_per_size;
std::vector<int> nof_replaced_circuits_per_size;
std::vector<int> nof_reduced_circuits_per_size;
public:
unsigned int iteration_count = 0;
double relation_generation_time = 0;
double synthesis_time = 0;
unsigned int subcircuits_with_forbidden_pairs = 0;
std::vector<ABC_UINT64_T> cummulative_sat_runtimes_per_size;
std::vector<int> nof_sat_calls_per_size;
std::vector<ABC_UINT64_T> cummulative_unsat_runtimes_per_size;
std::vector<int> nof_unsat_calls_per_size;
std::vector<int> nof_analyzed_circuits_per_size;
std::vector<int> nof_replaced_circuits_per_size;
std::vector<int> nof_reduced_circuits_per_size;
eSLIMLog(int size);
std::vector<ABC_UINT64_T> cummulative_sat_runtimes_per_size;
std::vector<int> nof_sat_calls_per_size;
std::vector<ABC_UINT64_T> cummulative_unsat_runtimes_per_size;
std::vector<int> nof_unsat_calls_per_size;
std::vector<double> cummulative_relation_generation_times_per_size;
std::vector<int> nof_relation_generations_per_size;
double cummulative_sat_runtime_synthesis = 0; // msec
double max_sat_runtime_synthesis = 0; // msec
ABC_UINT64_T nof_sat_calls_synthesis = 0;
double cummulative_sat_runtime_relation_generation = 0; // sec
double max_sat_runtime_relation_generation = 0; // sec
ABC_UINT64_T nof_sat_calls_relation_generation = 0;
eSLIMLog(int size);
int getSize() const;
void resize(int size);
};
struct Subcircuit {
Vec_Int_t* nodes;
Vec_Int_t* io;
unsigned int nof_inputs;
std::unordered_map<int, std::unordered_set<int>> forbidden_pairs;
void free();
};
inline void Subcircuit::free() {
Vec_IntFree(nodes);
Vec_IntFree(io);
}
inline eSLIMLog::eSLIMLog(int size)
: nof_analyzed_circuits_per_size(size + 1, 0), nof_replaced_circuits_per_size(size + 1, 0),
nof_reduced_circuits_per_size(size + 1, 0), cummulative_sat_runtimes_per_size(size + 1, 0),
nof_sat_calls_per_size(size + 1, 0), cummulative_unsat_runtimes_per_size(size + 1, 0),
nof_unsat_calls_per_size(size + 1, 0) {
nof_reduced_circuits_per_size(size + 1, 0),
cummulative_sat_runtimes_per_size(size + 1, 0), nof_sat_calls_per_size(size + 1, 0),
cummulative_unsat_runtimes_per_size(size + 1, 0), nof_unsat_calls_per_size(size + 1, 0),
cummulative_relation_generation_times_per_size(size + 1, 0), nof_relation_generations_per_size(size + 1, 0) {
}
inline int eSLIMLog::getSize() const {
return nof_analyzed_circuits_per_size.size() - 1;
}
inline void eSLIMLog::resize(int size) {
int sz = size + 1;
nof_analyzed_circuits_per_size.resize(sz);
nof_replaced_circuits_per_size.resize(sz);
nof_reduced_circuits_per_size.resize(size);
cummulative_sat_runtimes_per_size.resize(sz);
nof_sat_calls_per_size.resize(sz);
cummulative_unsat_runtimes_per_size.resize(sz);
nof_unsat_calls_per_size.resize(sz);
cummulative_relation_generation_times_per_size.resize(sz);
nof_relation_generations_per_size.resize(sz);
}
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

79
src/opt/eslim/windowMan.hpp Normal file
View File

@ -0,0 +1,79 @@
/**CFile****************************************************************
FileName [windowMan.hpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Basic implementation of a window manager.]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__OPT__ESLIM__WINDOWMAN_hpp
#define ABC__OPT__ESLIM__WINDOWMAN_hpp
#include <vector>
#include "misc/util/abc_global.h"
#include "eslimCirMan.hpp"
#include "utils.hpp"
ABC_NAMESPACE_CXX_HEADER_START
namespace eSLIM {
// The parallelisation strategy implemented in this class is rather easy and mainly intended to demonstrate
// how the eslim package could make use of parallel computing
template <typename SynthesisEngine, typename SelectionStrategy>
class WindowMan {
public:
void static applyeSLIM(eSLIMCirMan& es_man, eSLIMConfig& cfg, eSLIMLog& log);
private:
WindowMan(eSLIMCirMan& es_man, const eSLIMConfig& cfg, eSLIMLog& log);
eSLIMCirMan getCircuit();
void setupWindows();
void computeWindow(const std::vector<int>& gate_ids, int node_begin, int node_end);
void reorderCircuit();
void runParallel();
eSLIMCirMan recombineWindows();
void addEncompassing(eSLIMCirMan& es_man, int node_begin, int node_end);
void addWindow(eSLIMCirMan& es_man, int wid);
void combineLogs();
int nwindows = 0;
eSLIMCirMan& es_man;
const eSLIMConfig& cfg;
eSLIMLog& log;
std::vector<eSLIMLog> wlogs;
std::mt19937 rng;
std::vector<eSLIMCirMan> windows;
std::vector<Subcircuit> scirs;
std::vector<int> node_ranges_begin;
std::vector<int> node_ranges_end;
};
}
ABC_NAMESPACE_CXX_HEADER_END
#include "windowMan.tpp"
#endif

221
src/opt/eslim/windowMan.tpp Normal file
View File

@ -0,0 +1,221 @@
/**CFile****************************************************************
FileName [windowMan.tpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]
Synopsis [Basic implementation of a window manager.]
Author [Franz-Xaver Reichl]
Affiliation [University of Freiburg]
Date [Ver. 1.0. Started - April 2026.]
Revision [$Id: eSLIM.cpp,v 1.00 2025/04/14 00:00:00 Exp $]
***********************************************************************/
#include <random>
#include <algorithm>
#include <set>
#include <cmath>
#include <numeric>
#include <unordered_map>
#include <iostream>
#ifdef ABC_USE_PTHREADS
#include <thread>
#endif
#include "windowMan.hpp"
#include "subcircuit.hpp"
ABC_NAMESPACE_IMPL_START
namespace eSLIM {
template <typename SynthesisEngine, typename SelectionStrategy>
void WindowMan<SynthesisEngine, SelectionStrategy>::applyeSLIM(eSLIMCirMan& es_man, eSLIMConfig& cfg, eSLIMLog& log) {
int v = cfg.verbosity_level;
cfg.verbosity_level = 0;
WindowMan win_man(es_man, cfg, log);
win_man.setupWindows();
win_man.runParallel();
cfg.verbosity_level = v;
// eSLIMCirMan combined = win_man.recombineWindows();
// std::swap(es_man, combined);
es_man = win_man.recombineWindows();
}
template <typename SynthesisEngine, typename SelectionStrategy>
WindowMan<SynthesisEngine, SelectionStrategy>::WindowMan(eSLIMCirMan& es_man, const eSLIMConfig& cfg, eSLIMLog& log)
: es_man(es_man), cfg(cfg), log(log) {
if (cfg.fix_seed) {
rng.seed(cfg.seed);
}
}
template <typename SynthesisEngine, typename SelectionStrategy>
void WindowMan<SynthesisEngine, SelectionStrategy>::setupWindows() {
reorderCircuit();
unsigned int nmax_windows = std::ceil(static_cast<double>(es_man.getNofGates()) / cfg.window_size);
nwindows = std::min(nmax_windows, cfg.nwindows);
std::vector<int> gate_ids(es_man.getNofGates());
std::iota(gate_ids.begin(), gate_ids.end(), es_man.getNofPis() + 1);
std::vector<int> window_ids (nmax_windows);
std::iota(window_ids.begin(), window_ids.end(), 0);
std::vector<int> selected_window_ids;
selected_window_ids.reserve(nwindows);
std::sample(window_ids.begin(), window_ids.end(), std::back_inserter(selected_window_ids), nwindows, rng);
for (int i = 0; i < nwindows; i++) {
int begin_idx = selected_window_ids[i]*cfg.window_size;
// int end_idx = selected_window_ids[i] == nmax_windows ? gate_ids.size() : selected_window_ids[i+1]*cfg.window_size;
// int end_idx = selected_window_ids[i] == nmax_windows - 1 ? gate_ids.size() : begin_idx + cfg.window_size;
int end_idx = begin_idx + cfg.window_size;
computeWindow(gate_ids, begin_idx, end_idx);
wlogs.emplace_back(log.getSize());
}
}
template <typename SynthesisEngine, typename SelectionStrategy>
void WindowMan<SynthesisEngine, SelectionStrategy>::reorderCircuit() {
std::vector<int> pos;
pos.reserve(es_man.getNofPos());
for (int i = es_man.getNofObjs() - es_man.getNofPos(); i < es_man.getNofObjs(); i++) {
pos.push_back(i);
}
std::shuffle(pos.begin(), pos.end(), rng);
es_man.applyDFSOrdering(pos);
}
template <typename SynthesisEngine, typename SelectionStrategy>
void WindowMan<SynthesisEngine, SelectionStrategy>::computeWindow(const std::vector<int>& gate_ids, int node_begin, int node_end) {
es_man.incrementTraversalId(); // needed for the insubcircuit marks
int end_node;
if (node_end >= gate_ids.size()) {
node_end = gate_ids.size();
end_node = gate_ids.back() + 1;
} else {
end_node = gate_ids[node_end];
}
Subcircuit scir = Subcircuit::getSubcircuitBare(es_man, gate_ids.begin() + node_begin, gate_ids.begin() + node_end);
scirs.push_back(scir);
windows.emplace_back(es_man, scir);
node_ranges_begin.push_back(gate_ids[node_begin]);
node_ranges_end.push_back(end_node);
}
template <typename SynthesisEngine, typename SelectionStrategy>
void WindowMan<SynthesisEngine, SelectionStrategy>::runParallel() {
#ifdef ABC_USE_PTHREADS
std::vector<std::thread> eslim_threads;
eslim_threads.reserve(nwindows);
for (int i = 0; i < nwindows; i++) {
std::thread esman_thread(eSLIM_Man<SynthesisEngine, SelectionStrategy>::applyeSLIM, std::ref(windows[i]), std::ref(cfg), std::ref(wlogs[i]));
eslim_threads.push_back(std::move(esman_thread));
}
for(auto& t: eslim_threads) {
t.join();
}
#else
std::cout << "PThreads not available, minimize random window.\n";
std::uniform_int_distribution<> udist(0, windows.size() - 1);
int wid = udist(rng);
eSLIM_Man<SynthesisEngine, SelectionStrategy>::applyeSLIM(windows[wid], cfg, wlogs[wid])
#endif
}
template <typename SynthesisEngine, typename SelectionStrategy>
eSLIMCirMan WindowMan<SynthesisEngine, SelectionStrategy>::recombineWindows() {
combineLogs();
eSLIMCirMan combined(es_man.getNofObjs());
for (int i = 1; i <= es_man.getNofPis(); i++) {
es_man.nodes[i]->value1 = combined.addPi(); //node 0 is the constant node
}
int block_begin = es_man.getNofPis() + 1;
for (int i = 0; i < nwindows; i++) {
// windows[i].print();
int block_end = node_ranges_begin[i];
addEncompassing(combined, block_begin, block_end);
addWindow(combined, i);
block_begin = node_ranges_end[i];
}
if (node_ranges_end.back() < es_man.getNofObjs() - es_man.getNofPos()) {
addEncompassing(combined, node_ranges_end.back(), es_man.getNofObjs() - es_man.getNofPos());
}
for (int i = 0; i < es_man.getNofPos(); i++) {
int nd_id = es_man.getNofObjs() - es_man.getNofPos() + i;
auto& nd = es_man.nodes[nd_id];
bool is_negated = nd->tt == 1;
combined.addPo(nd->fanins[0]->value1, is_negated);
}
return combined;
}
template <typename SynthesisEngine, typename SelectionStrategy>
void WindowMan<SynthesisEngine, SelectionStrategy>::addEncompassing(eSLIMCirMan& combined, int node_begin, int node_end) {
for (int i = node_begin; i < node_end; i++) {
auto& nd = es_man.nodes[i];
std::vector<int> fanins;
fanins.reserve(nd->fanins.size());
for (int i = 0; i < nd->fanins.size(); i++) {
fanins.push_back(nd->fanins[i]->value1);
}
nd->value1 = combined.addNode(fanins, nd->tt);
}
}
template <typename SynthesisEngine, typename SelectionStrategy>
void WindowMan<SynthesisEngine, SelectionStrategy>::addWindow(eSLIMCirMan& combined, int wid) {
for (int i = 1; i <= windows[wid].getNofPis(); i++) {
windows[wid].nodes[i]->value1 = es_man.nodes[scirs[wid].inputs[i-1]]->value1;
}
for (int i = windows[wid].getNofPis() + 1; i < windows[wid].getNofObjs() - windows[wid].getNofPos(); i++) {
auto& nd = windows[wid].nodes[i];
std::vector<int> fanins;
fanins.reserve(nd->fanins.size());
for (int i = 0; i < nd->fanins.size(); i++) {
fanins.push_back(nd->fanins[i]->value1);
}
nd->value1 = combined.addNode(fanins, nd->tt);
}
for (int i = 0; i < windows[wid].getNofPos(); i++) {
auto& out_nd = windows[wid].nodes[windows[wid].getNofObjs() - windows[wid].getNofPos() + i];
es_man.nodes[scirs[wid].outputs[i]]->value1 = out_nd->fanins[0]->value1;
}
}
template <typename SynthesisEngine, typename SelectionStrategy>
void WindowMan<SynthesisEngine, SelectionStrategy>::combineLogs() {
for (const auto& wl : wlogs) {
int wl_size = wl.getSize();
if (log.getSize() < wl_size) {
log.resize(wl_size);
}
log.iteration_count += wl.iteration_count;
log.relation_generation_time += wl.relation_generation_time;
log.synthesis_time += wl.synthesis_time;
log.subcircuits_with_forbidden_pairs += wl.subcircuits_with_forbidden_pairs;
for (int i = 0; i <= wl_size; i++) {
log.nof_analyzed_circuits_per_size[i] += wl.nof_analyzed_circuits_per_size[i];
log.nof_replaced_circuits_per_size[i] += wl.nof_replaced_circuits_per_size[i];
log.nof_reduced_circuits_per_size[i] += wl.nof_reduced_circuits_per_size[i];
log.cummulative_sat_runtimes_per_size[i] += wl.cummulative_sat_runtimes_per_size[i];
log.nof_sat_calls_per_size[i] += wl.nof_sat_calls_per_size[i];
log.cummulative_unsat_runtimes_per_size[i] += wl.cummulative_unsat_runtimes_per_size[i];
log.nof_unsat_calls_per_size[i] += wl.nof_unsat_calls_per_size[i];
log.cummulative_relation_generation_times_per_size[i] += wl.cummulative_relation_generation_times_per_size[i];
log.nof_relation_generations_per_size[i] += wl.nof_relation_generations_per_size[i];
}
}
}
}
ABC_NAMESPACE_IMPL_END