abcSaucy.c File Reference

#include "base/abc/abc.h"
#include "opt/sim/sim.h"

Include dependency graph for abcSaucy.c:

Go to the source code of this file.

Classes
struct	saucy_stats
struct	saucy_graph
struct	coloring
struct	sim_result
struct	saucy

Macros
#define	REFINE_BY_SIM_1   0
#define	REFINE_BY_SIM_2   0
#define	BACKTRACK_BY_SAT   1
#define	SELECT_DYNAMICALLY   0
#define	CLAUSE_DECAY   0.9
#define	MAX_LEARNTS   50

Functions
void	prepare_permutation_ntk (struct saucy *s)
void	unprepare_permutation_ntk (struct saucy *s)
void	saucy_search (Abc_Ntk_t *pNtk, struct saucy *s, int directed, const int *colors, struct saucy_stats *stats)
void	saucy_free (struct saucy *s)
struct saucy *	saucy_alloc (Abc_Ntk_t *pNtk)
void	saucyGateWay (Abc_Ntk_t *pNtkOrig, Abc_Obj_t *pNodePo, FILE *gFile, int fBooleanMatching, int fLookForSwaps, int fFixOutputs, int fFixInputs, int fQuiet, int fPrintTree)

Variables
int	NUM_SIM1_ITERATION
int	NUM_SIM2_ITERATION

Macro Definition Documentation

BACKTRACK_BY_SAT

#define BACKTRACK_BY_SAT   1

Definition at line 35 of file abcSaucy.c.

CLAUSE_DECAY

#define CLAUSE_DECAY   0.9

Definition at line 43 of file abcSaucy.c.

MAX_LEARNTS

#define MAX_LEARNTS   50

Definition at line 44 of file abcSaucy.c.

REFINE_BY_SIM_1

#define REFINE_BY_SIM_1   0

CFile****************************************************************

FileName [abcSaucy.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Symmetry Detection Package.]

Synopsis [Finds symmetries under permutation (but not negation) of I/Os.]

Author [Hadi Katebi]

Affiliation [University of Michigan]

Date [Ver. 1.0. Started - April, 2012.]

Revision [No revisions so far]

Comments []

Debugging [There are some part of the code that are commented out. Those parts mostly print the contents of the data structures to the standard output. Un-comment them if you find them useful for debugging.]

Definition at line 33 of file abcSaucy.c.

REFINE_BY_SIM_2

#define REFINE_BY_SIM_2   0

Definition at line 34 of file abcSaucy.c.

SELECT_DYNAMICALLY

#define SELECT_DYNAMICALLY   0

Definition at line 36 of file abcSaucy.c.

Function Documentation

prepare_permutation_ntk()

void prepare_permutation_ntk

(

struct saucy *

s

)

Definition at line 2155 of file abcSaucy.c.

{       
    int i;
    Abc_Obj_t * pObj, * pObjPerm;
    int numouts = Abc_NtkPoNum(s->pNtk);
 
    Nm_ManFree( s->pNtk_permuted->pManName );
    s->pNtk_permuted->pManName = Nm_ManCreate( Abc_NtkCiNum(s->pNtk) + Abc_NtkCoNum(s->pNtk) + Abc_NtkBoxNum(s->pNtk) );    
 
    for (i = 0; i < s->n; ++i) {        
        if (i < numouts) {
            pObj     = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk->vPos, i);
            pObjPerm = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk_permuted->vPos, s->gamma[i]);           
        }
        else {          
            pObj     = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk->vPis, i - numouts);
            pObjPerm = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk_permuted->vPis, s->gamma[i] - numouts);
            
        }
        Abc_ObjAssignName( pObjPerm, Abc_ObjName(pObj), NULL );         
    }
 
    Abc_NtkOrderObjsByName( s->pNtk_permuted, 1 );
 
    /* print the permutation */
    /*for (i = 0; i < s->ndiffs; ++i)
        printf(" %d->%d", s->unsupp[i], s->diffs[i]);
    printf("\n");
    Abc_NtkForEachCo( s->pNtk, pObj, i )
        printf (" %d", Abc_ObjId(pObj)-1-Abc_NtkPiNum(s->pNtk));
    Abc_NtkForEachCi( s->pNtk, pObj, i )
        printf (" %d", Abc_ObjId(pObj)-1+Abc_NtkPoNum(s->pNtk));
    printf("\n");
    Abc_NtkForEachCo( s->pNtk_permuted, pObj, i )
        printf (" %d", Abc_ObjId(pObj)-1-Abc_NtkPiNum(s->pNtk_permuted));
    Abc_NtkForEachCi( s->pNtk_permuted, pObj, i )
        printf (" %d", Abc_ObjId(pObj)-1+Abc_NtkPoNum(s->pNtk_permuted));   
    printf("\n");*/
}

Here is the call graph for this function:

saucy_alloc()

struct saucy * saucy_alloc

(

Abc_Ntk_t *

pNtk

)

Definition at line 2576 of file abcSaucy.c.

{
    int i;
    int numouts = Abc_NtkPoNum(pNtk);
    int numins =  Abc_NtkPiNum(pNtk);
    int n = numins + numouts;
    struct saucy *s = ABC_ALLOC(struct saucy, 1);
    if (s == NULL) return NULL;
 
    s->ninduce = ints(n);
    s->sinduce = ints(n);
    s->indmark = bits(n);
    s->left.cfront = zeros(n);
    s->left.clen = ints(n);
    s->right.cfront = zeros(n);
    s->right.clen = ints(n);
    s->stuff = bits(n+1);
    s->bucket = ints(n+2);
    s->count = ints(n+1);
    s->ccount = zeros(n);
    s->clist = ints(n);
    s->nextnon = ints(n+1) + 1;
    s->prevnon = ints(n+1);
    s->anctar = ints(n);
    s->start = ints(n);
    s->gamma = ints(n);
    s->junk = ints(n);
    s->theta = ints(n);
    s->thsize = ints(n);
    s->left.lab = ints(n);
    s->left.unlab = ints(n);
    s->right.lab = ints(n);
    s->right.unlab = ints(n);
    s->splitvar = ints(n);
    s->splitwho = ints(n);
    s->splitfrom = ints(n);
    s->splitlev = ints(n+1);
    s->unsupp = ints(n);
    s->conncnts = zeros(n);
    s->diffmark = bits(n);
    s->diffs = ints(n);
    s->difflev = ints(n);
    s->undifflev = ints(n);
    s->specmin = ints(n);
    s->thnext = ints(n);
    s->thprev = ints(n);
    s->threp = ints(n);
    s->thfront = ints(n);
    s->pairs = ints(n);
    s->unpairs = ints(n);
    s->diffnons = ints(n);
    s->undiffnons = ints(n);
    s->marks = bits(n);
 
    s->iDep = ABC_ALLOC( Vec_Int_t*,  numins );
    s->oDep = ABC_ALLOC( Vec_Int_t*,  numouts );
    s->obs  = ABC_ALLOC( Vec_Int_t*,  numins );
    s->ctrl = ABC_ALLOC( Vec_Int_t*,  numouts );
 
    for(i = 0; i < numins; i++) {       
        s->iDep[i] = Vec_IntAlloc( 1 );
        s->obs[i] = Vec_IntAlloc( 1 );
    }
    for(i = 0; i < numouts; i++) {      
        s->oDep[i] = Vec_IntAlloc( 1 );
        s->ctrl[i] = Vec_IntAlloc( 1 );
    }   
 
    s->randomVectorArray_sim1 = Vec_PtrAlloc( n );  
    s->randomVectorSplit_sim1 = zeros( n );
    s->randomVectorArray_sim2 = Vec_PtrAlloc( n );  
    s->randomVectorSplit_sim2= zeros( n );
 
    s->satCounterExamples = Vec_PtrAlloc( 1 );
    s->pModel = ints( numins );
 
    if (s->ninduce && s->sinduce && s->left.cfront && s->left.clen
        && s->right.cfront && s->right.clen
        && s->stuff && s->bucket && s->count && s->ccount
        //&& s->clist && s->nextnon-1 && s->prevnon
        && s->clist && s->nextnon[-1] && s->prevnon
        && s->start && s->gamma && s->theta && s->left.unlab
        && s->right.lab && s->right.unlab
        && s->left.lab &&  s->splitvar && s->splitwho && s->junk
        && s->splitfrom && s->splitlev && s->thsize
        && s->unsupp && s->conncnts && s->anctar
        && s->diffmark && s->diffs && s->indmark
        && s->thnext && s->thprev && s->threp && s->thfront
        && s->pairs && s->unpairs && s->diffnons && s->undiffnons
        && s->difflev && s->undifflev && s->specmin)
    {
        return s;
    }
    else {
        saucy_free(s);
        return NULL;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

saucy_free()

void saucy_free

(

struct saucy *

s

)

Definition at line 2491 of file abcSaucy.c.

{
    int i;
 
    ABC_FREE(s->undiffnons);
    ABC_FREE(s->diffnons);
    ABC_FREE(s->unpairs);
    ABC_FREE(s->pairs);
    ABC_FREE(s->thfront);
    ABC_FREE(s->threp);
    ABC_FREE(s->thnext);
    ABC_FREE(s->thprev);
    ABC_FREE(s->specmin);
    ABC_FREE(s->anctar);
    ABC_FREE(s->thsize);
    ABC_FREE(s->undifflev);
    ABC_FREE(s->difflev);
    ABC_FREE(s->diffs);
    ABC_FREE(s->diffmark);
    ABC_FREE(s->conncnts);
    ABC_FREE(s->unsupp);
    ABC_FREE(s->splitlev);
    ABC_FREE(s->splitfrom);
    ABC_FREE(s->splitwho);
    ABC_FREE(s->splitvar);
    ABC_FREE(s->right.unlab);
    ABC_FREE(s->right.lab);
    ABC_FREE(s->left.unlab);
    ABC_FREE(s->left.lab);
    ABC_FREE(s->theta);
    ABC_FREE(s->junk);
    ABC_FREE(s->gamma);
    ABC_FREE(s->start);
    ABC_FREE(s->prevnon);
    free(s->nextnon-1);
    ABC_FREE(s->clist);
    ABC_FREE(s->ccount);
    ABC_FREE(s->count);
    ABC_FREE(s->bucket);
    ABC_FREE(s->stuff);
    ABC_FREE(s->right.clen);
    ABC_FREE(s->right.cfront);
    ABC_FREE(s->left.clen);
    ABC_FREE(s->left.cfront);
    ABC_FREE(s->indmark);
    ABC_FREE(s->sinduce);
    ABC_FREE(s->ninduce);
    ABC_FREE(s->depAdj);
    ABC_FREE(s->depEdg);
    ABC_FREE(s->marks);
    for (i = 0; i < Abc_NtkPiNum(s->pNtk); i++) {
        Vec_IntFree( s->iDep[i] );
        Vec_IntFree( s->obs[i] );
        Vec_PtrFree( s->topOrder[i] );
    }
    for (i = 0; i < Abc_NtkPoNum(s->pNtk); i++) {
        Vec_IntFree( s->oDep[i] );
        Vec_IntFree( s->ctrl[i] );
    }
    for (i = 0; i < Vec_PtrSize(s->randomVectorArray_sim1); i++)
        Vec_IntFree((Vec_Int_t *)Vec_PtrEntry(s->randomVectorArray_sim1, i));
    for (i = 0; i < Vec_PtrSize(s->randomVectorArray_sim2); i++)
        Vec_IntFree((Vec_Int_t *)Vec_PtrEntry(s->randomVectorArray_sim2, i));
    Vec_PtrFree( s->randomVectorArray_sim1 );
    Vec_PtrFree( s->randomVectorArray_sim2 );
    ABC_FREE(s->randomVectorSplit_sim1);
    ABC_FREE(s->randomVectorSplit_sim2);
    Abc_NtkDelete( s->pNtk_permuted );
    for (i = 0; i < Vec_PtrSize(s->satCounterExamples); i++) {
        struct sim_result * cex = (struct sim_result *)Vec_PtrEntry(s->satCounterExamples, i);
        ABC_FREE( cex->inVec );
        ABC_FREE( cex->outVec );
        ABC_FREE( cex );
    }
    Vec_PtrFree(s->satCounterExamples);
    ABC_FREE( s->pModel );
    ABC_FREE( s->iDep );
    ABC_FREE( s->oDep );
    ABC_FREE( s->obs );
    ABC_FREE( s->ctrl );
    ABC_FREE( s->topOrder );
    ABC_FREE(s);
}

Here is the call graph for this function:

Here is the caller graph for this function:

saucy_search()

void saucy_search	(	Abc_Ntk_t *	pNtk,
		struct saucy *	s,
		int	directed,
		const int *	colors,
		struct saucy_stats *	stats )

Definition at line 2311 of file abcSaucy.c.

{
    int i, j, max = 0;  
    struct saucy_graph *g;
 
    extern Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk );
 
    /* Save network information */
    s->pNtk = pNtk;
    s->pNtk_permuted = Abc_NtkDup( pNtk );  
 
    /* Builde dependency graph */
    g = buildDepGraph(pNtk, s->iDep, s->oDep);  
 
    /* Save graph information */
    s->n = g->n;
    s->depAdj = g->adj;
    s->depEdg = g->edg;
    /*s->dadj = g->adj + g->n + 1;
    s->dedg = g->edg + g->e;*/
 
    /* Save client information */
    s->stats = stats;       
 
    /* Polymorphism */
    if (directed) {
        s->is_automorphism = is_directed_automorphism;
        s->ref_singleton = ref_singleton_directed;
        s->ref_nonsingle = ref_nonsingle_directed;
    }
    else {
        s->is_automorphism = is_undirected_automorphism;
        s->ref_singleton = ref_singleton_undirected;
        s->ref_nonsingle = ref_nonsingle_undirected;
    }
 
    /* Initialize scalars */
    s->indmin = 0;  
    s->lev = s->anc = 1;
    s->ndiffs = s->nundiffs = s->ndiffnons = 0;
    s->activityInc = 1;
 
    /* The initial orbit partition is discrete */
    for (i = 0; i < s->n; ++i) {
        s->theta[i] = i;
    }
 
    /* The initial permutation is the identity */
    for (i = 0; i < s->n; ++i) {
        s->gamma[i] = i;
    }
 
    /* Initially every cell of theta has one element */
    for (i = 0; i < s->n; ++i) {
        s->thsize[i] = 1;
    }
 
    /* Every theta rep list is singleton */
    for (i = 0; i < s->n; ++i) {
        s->thprev[i] = s->thnext[i] = i;
    }
 
    /* We have no pairs yet */
    s->npairs = 0;
    for (i = 0; i < s->n; ++i) {
        s->unpairs[i] = -1;
    }
 
    /* Ensure no stray pointers in undiffnons, which is checked by removed_diffnon() */
    for (i = 0; i < s->n; ++i) {
        s->undiffnons[i] = -1;
    }
 
    /* Initialize stats */
    s->stats->grpsize_base = 1.0;
    s->stats->grpsize_exp = 0;
    s->stats->nodes = 1;
    s->stats->bads = s->stats->gens = s->stats->support = 0;
 
    /* Prepare for refinement */
    s->nninduce = s->nsinduce = 0;
    s->csize = 0;
 
    /* Count cell sizes */
    for (i = 0; i < s->n; ++i) {
        s->ccount[colors[i]]++;
        if (max < colors[i]) max = colors[i];
    }
    s->nsplits = max + 1;
 
    /* Build cell lengths */
    s->left.clen[0] = s->ccount[0] - 1;
    for (i = 0; i < max; ++i) {
        s->left.clen[s->ccount[i]] = s->ccount[i+1] - 1;
        s->ccount[i+1] += s->ccount[i];
    }
 
    /* Build the label array */
    for (i = 0; i < s->n; ++i) {
        set_label(&s->left, --s->ccount[colors[i]], i);
    }
 
    /* Clear out ccount */
    for (i = 0; i <= max; ++i) {
        s->ccount[i] = 0;
    }
 
    /* Update refinement stuff based on initial partition */
    for (i = 0; i < s->n; i += s->left.clen[i]+1) {
        add_induce(s, &s->left, i);
        fix_fronts(&s->left, i, i);
    }
 
    /* Prepare lists based on cell lengths */
    for (i = 0, j = -1; i < s->n; i += s->left.clen[i] + 1) {
        if (!s->left.clen[i]) continue;
        s->prevnon[i] = j;
        s->nextnon[j] = i;
        j = i;
    }
 
    /* Fix the end */
    s->prevnon[s->n] = j;
    s->nextnon[j] = s->n;
 
    /* Preprocessing after initial coloring */
    s->split = split_init;  
    s->refineBySim1 = refineBySim1_init;
    s->refineBySim2 = refineBySim2_init;    
 
    //print_partition(&s->left, NULL, s->n, s->pNtk, 1);
    printf("Initial Refine by Dependency graph ... ");
    refineByDepGraph(s, &s->left);
    //print_partition(&s->left, NULL, s->n, s->pNtk, 1);
    printf("done!\n");
    
    printf("Initial Refine by Simulation ... ");
    if (REFINE_BY_SIM_1) s->refineBySim1(s, &s->left);
    //print_partition(&s->left, NULL, s->n, s->pNtk, 1);
    if (REFINE_BY_SIM_2) s->refineBySim2(s, &s->left);
    //print_partition(&s->left, NULL, s->n, s->pNtk, 1);
    printf("done!\n\t--------------------\n");
 
    /* Descend along the leftmost branch and compute zeta */
    s->refineBySim1 = refineBySim1_left;
    s->refineBySim2 = refineBySim2_left;
    descend_leftmost(s);    
    s->split = split_other; 
    s->refineBySim1 = refineBySim1_other;
    s->refineBySim2 = refineBySim2_other;   
 
    /* Our common ancestor with zeta is the current level */
    s->stats->levels = s->anc = s->lev;
 
    /* Copy over this data to our non-leftmost coloring */
    memcpy(s->right.lab, s->left.lab, s->n * sizeof(int));
    memcpy(s->right.unlab, s->left.unlab, s->n * sizeof(int));
    memcpy(s->right.clen, s->left.clen, s->n * sizeof(int));
    memcpy(s->right.cfront, s->left.cfront, s->n * sizeof(int));
 
    /* The reps are just the labels at this point */
    memcpy(s->threp, s->left.lab, s->n * sizeof(int));
    memcpy(s->thfront, s->left.unlab, s->n * sizeof(int));
 
    /* choose cell selection method */
    if (SELECT_DYNAMICALLY) s->select_decomposition = select_dynamically;
    else                    s->select_decomposition = select_statically;
 
    /* Keep running till we're out of automorphisms */
    while (do_search(s));
 
    ABC_FREE(g);
}

Here is the call graph for this function:

Here is the caller graph for this function:

saucyGateWay()

void saucyGateWay	(	Abc_Ntk_t *	pNtkOrig,
		Abc_Obj_t *	pNodePo,
		FILE *	gFile,
		int	fBooleanMatching,
		int	fLookForSwaps,
		int	fFixOutputs,
		int	fFixInputs,
		int	fQuiet,
		int	fPrintTree )

Definition at line 3249 of file abcSaucy.c.

{
    Abc_Ntk_t * pNtk;
    struct saucy *s;
    struct saucy_stats stats;
    int *colors;
    int i, clk = clock();   
    
    if (pNodePo == NULL)
        pNtk = Abc_NtkDup( pNtkOrig );
    else
        pNtk = Abc_NtkCreateCone( pNtkOrig, Abc_ObjFanin0(pNodePo), Abc_ObjName(pNodePo), 0 );
    
    if (Abc_NtkPiNum(pNtk) == 0) {
        Abc_Print( 0, "This output is not dependent on any input\n" );
        Abc_NtkDelete( pNtk );
        return;
    }
 
    s = saucy_alloc( pNtk );    
 
    /******* Getting Dependencies *******/  
    printf("Build functional dependency graph (dependency stats are below) ... ");      
    getDependencies( pNtk, s->iDep, s->oDep );
    printf("\t--------------------\n");
    /************************************/
 
    /* Finding toplogical orde */
    s->topOrder = findTopologicalOrder( pNtk );                 
 
    /* Setting graph colors: outputs = 0 and inputs = 1 */
    colors = ints(Abc_NtkPoNum(pNtk) + Abc_NtkPiNum(pNtk));
    if (fFixOutputs) {
        for (i = 0; i < Abc_NtkPoNum(pNtk); i++)
            colors[i] = i;
    } else {
        for (i = 0; i < Abc_NtkPoNum(pNtk); i++)
            colors[i] = 0;
    }
    if (fFixInputs) {
        int c = (fFixOutputs) ? Abc_NtkPoNum(pNtk) : 1;
        for (i = 0; i < Abc_NtkPiNum(pNtk); i++)
            colors[i+Abc_NtkPoNum(pNtk)] = c+i;     
    } else {
        int c = (fFixOutputs) ? Abc_NtkPoNum(pNtk) : 1;
        for (i = 0; i < Abc_NtkPiNum(pNtk); i++)
            colors[i+Abc_NtkPoNum(pNtk)] = c;   
    }   
 
    /* Are we looking for Boolean matching? */
    s->fBooleanMatching = fBooleanMatching;
    if (fBooleanMatching) {
        NUM_SIM1_ITERATION = 50;
        NUM_SIM2_ITERATION = 50;
    } else {
        NUM_SIM1_ITERATION = 200;
        NUM_SIM2_ITERATION = 200;
    }
 
    /* Set the print automorphism routine */
    if (!fQuiet)
        s->print_automorphism = print_automorphism_ntk;
    else
        s->print_automorphism = print_automorphism_quiet;
 
    /* Set the output file for generators */
    if (gFile == NULL)
        s->gFile = stdout;
    else
        s->gFile = gFile;
 
    /* Set print tree option */
    s->fPrintTree = fPrintTree;
 
    /* Set input permutations option */
    s->fLookForSwaps = fLookForSwaps;
 
    saucy_search(pNtk, s, 0, colors, &stats);   
    print_stats(stdout, stats);
    if (fBooleanMatching) {
        if (stats.grpsize_base > 1 || stats.grpsize_exp > 0)
            printf("*** Networks are equivalent ***\n");
        else
            printf("*** Networks are NOT equivalent ***\n");
    }
    saucy_free(s);
    Abc_NtkDelete(pNtk);
 
    if (1) {
        FILE * hadi = fopen("hadi.txt", "a");
        fprintf(hadi, "group size = %fe%d\n",
        stats.grpsize_base, stats.grpsize_exp); 
        fclose(hadi);
    }
 
    ABC_PRT( "Runtime", clock() - clk );
 
}ABC_NAMESPACE_IMPL_END

Here is the call graph for this function:

unprepare_permutation_ntk()

void unprepare_permutation_ntk

(

struct saucy *

s

)

Definition at line 2209 of file abcSaucy.c.

{       
    int i;
    Abc_Obj_t * pObj, * pObjPerm;
    int numouts = Abc_NtkPoNum(s->pNtk);
 
    Nm_ManFree( s->pNtk_permuted->pManName );
    s->pNtk_permuted->pManName = Nm_ManCreate( Abc_NtkCiNum(s->pNtk) + Abc_NtkCoNum(s->pNtk) + Abc_NtkBoxNum(s->pNtk) );    
 
    for (i = 0; i < s->n; ++i) {        
        if (i < numouts) {
            pObj     = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk->vPos, s->gamma[i]);
            pObjPerm = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk_permuted->vPos, i);         
        }
        else {          
            pObj     = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk->vPis, s->gamma[i] - numouts);
            pObjPerm = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk_permuted->vPis, i - numouts);
            
        }
        Abc_ObjAssignName( pObjPerm, Abc_ObjName(pObj), NULL );         
    }
 
    Abc_NtkOrderObjsByName( s->pNtk_permuted, 1 );
}

Here is the call graph for this function:

Variable Documentation

NUM_SIM1_ITERATION

int NUM_SIM1_ITERATION

Definition at line 39 of file abcSaucy.c.

NUM_SIM2_ITERATION

int NUM_SIM2_ITERATION

Definition at line 40 of file abcSaucy.c.