From 60bb6dbf69efb5b1cb7253eff9e2a836bc21d5d0 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Jul 2013 18:06:09 -0700 Subject: Adding commands 'bm2' and 'saucy3' developed by Hadi Katebi, Igor Markov, and Karem Sakallah at U Michigan. --- src/base/abci/abc.c | 267 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 267 insertions(+) (limited to 'src/base/abci/abc.c') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7012e7ba..b17acfea 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -299,6 +299,8 @@ static int Abc_CommandConstr ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandUnfold ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFold ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBm ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBm2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSaucy ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTestCex ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPdr ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandReconcile ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -850,6 +852,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "unfold", Abc_CommandUnfold, 1 ); Cmd_CommandAdd( pAbc, "Verification", "fold", Abc_CommandFold, 1 ); Cmd_CommandAdd( pAbc, "Verification", "bm", Abc_CommandBm, 1 ); + Cmd_CommandAdd( pAbc, "Verification", "bm2", Abc_CommandBm2, 1 ); + Cmd_CommandAdd( pAbc, "Verification", "saucy3", Abc_CommandSaucy, 1 ); Cmd_CommandAdd( pAbc, "Verification", "testcex", Abc_CommandTestCex, 0 ); Cmd_CommandAdd( pAbc, "Verification", "pdr", Abc_CommandPdr, 0 ); Cmd_CommandAdd( pAbc, "Verification", "reconcile", Abc_CommandReconcile, 1 ); @@ -23091,6 +23095,269 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandBm2( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t *pNtk, *pNtk1, *pNtk2; + int fDelete1, fDelete2; + Abc_Obj_t * pObj; + char ** pArgvNew; + int c, nArgcNew, i; + + extern void saucyGateWay( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodePo, FILE * gFile, int fBooleanMatching, + int fLookForSwaps, int fFixOutputs, int fFixInputs, int fQuiet, int fPrintTree); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + Abc_Print( -2, "Unknown switch.\n"); + goto usage; + } + } + + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; + if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew , &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) + return 1; + + if( (unsigned)Abc_NtkPiNum(pNtk1) != (unsigned)Abc_NtkPiNum(pNtk2) || + (unsigned)Abc_NtkPoNum(pNtk1) != (unsigned)Abc_NtkPoNum(pNtk2) ) + { + Abc_Print( -2, "Mismatch in the number of inputs or outputs\n"); + Abc_Print( -2, "*** Networks are NOT equivalent ***\n"); + if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); + if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); + return 1; + } + + Abc_NtkPermute(pNtk2, 1, 1, 0 ); + Abc_NtkShortNames(pNtk2); + + Abc_NtkForEachCi( pNtk1, pObj, i ) { + char * newName = Abc_ObjNamePrefix( pObj, "N1:" ); + Nm_ManDeleteIdName( pNtk1->pManName, pObj->Id); + Abc_ObjAssignName( pObj, newName, NULL ); + } + Abc_NtkForEachCo( pNtk1, pObj, i ) { + char * newName = Abc_ObjNamePrefix( pObj, "N1:" ); + Nm_ManDeleteIdName( pNtk1->pManName, pObj->Id); + Abc_ObjAssignName( pObj, newName, NULL ); + } + + Abc_NtkForEachCi( pNtk2, pObj, i ) { + char * newName = Abc_ObjNamePrefix( pObj, "N2:" ); + Nm_ManDeleteIdName( pNtk2->pManName, pObj->Id); + Abc_ObjAssignName( pObj, newName, NULL ); + } + Abc_NtkForEachCo( pNtk2, pObj, i ) { + char * newName = Abc_ObjNamePrefix( pObj, "N2:" ); + Nm_ManDeleteIdName( pNtk2->pManName, pObj->Id); + Abc_ObjAssignName( pObj, newName, NULL ); + } + + Abc_NtkAppend( pNtk1, pNtk2, 1 ); + saucyGateWay( pNtk1, NULL, NULL, 1, 0, 0, 0, 0, 0); + + if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); + if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); + return 0; + +usage: + Abc_Print( -2, "usage: bm2 \n" ); + Abc_Print( -2, "\t performs Boolean matching (PP-equivalence)\n" ); + Abc_Print( -2, "\t for equivalent circuits, permutation that maps one circuit\n" ); + Abc_Print( -2, "\t to another is printed to standard output (PIs and POs of the\n" ); + Abc_Print( -2, "\t first network have prefix \"N1:\", while PIs and POs of the\n" ); + Abc_Print( -2, "\t second network have prefix \"N2:\")\n" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\tfile1 : the file with the first network\n"); + Abc_Print( -2, "\tfile2 : the file with the second network\n"); + + Abc_Print( -2, "\t \n" ); + Abc_Print( -2, "\t This command was contributed by Hadi Katebi from U Michigan.\n" ); + Abc_Print( -2, "\t The paper describing the method: H. Katebi, K. Sakallah and\n"); + Abc_Print( -2, "\t I. L. Markov.\n" ); + Abc_Print( -2, "\t \"Generalized Boolean Symmetries Through Nested Partition\n"); + Abc_Print( -2, "\t Refinement\". Proc. ICCAD 2013. \n" ); + //Abc_Print( -2, "\t http://www.eecs.umich.edu/~imarkov/pubs/conf/date10-match.pdf\n" ); + Abc_Print( -2, "\t \n" ); + + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandSaucy( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t *pNtk; + char * outputName = NULL; + FILE * gFile = NULL; + int fOutputsOneAtTime = 0; + int fFixOutputs = 0; + int fFixInputs = 0; + int fLookForSwaps = 0; + int fQuiet = 0; + int fPrintTree = 0; + int c; + + extern void saucyGateWay( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodePo, FILE * gFile, int fBooleanMatching, + int fLookForSwaps, int fFixOutputs, int fFixInputs, int fQuiet, int fPrintTree); + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "OFiosqvh" ) ) != EOF ) + { + switch ( c ) + { + case 'O': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-O\" should be followed by an output name or the keyword all.\n" ); + goto usage; + } + outputName = argv[globalUtilOptind]; + if ( !strcmp(argv[globalUtilOptind], "all") ) + fOutputsOneAtTime ^= 1; + globalUtilOptind++; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by a file name.\n" ); + goto usage; + } + if ( (gFile = fopen( argv[globalUtilOptind], "w" )) == NULL ) + { + Abc_Print( -1, "Cannot create output file \"%s\". ", argv[globalUtilOptind] ); + return 1; + } + globalUtilOptind++; + break; + case 'i': + fFixOutputs ^= 1; + break; + case 'o': + fFixInputs ^= 1; + break; + case 's': + fLookForSwaps ^= 1; + break; + case 'q': + fQuiet ^= 1; + break; + case 'v': + fPrintTree ^= 1; + break; + case 'h': + goto usage; + default: + Abc_Print( -2, "Unknown switch.\n"); + goto usage; + } + } + + pNtk = Abc_FrameReadNtk(pAbc); + + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + Abc_Print( -1, "This command works only for AIGs (run \"strash\").\n" ); + return 1; + } + + pNtk = Abc_NtkDup( pNtk ); + Abc_NtkOrderObjsByName( pNtk, 1 ); + + if (fOutputsOneAtTime) { + int i; + Abc_Obj_t * pNodePo; + FILE * hadi = fopen("hadi.txt", "w"); + Abc_NtkForEachPo( pNtk, pNodePo, i ) { + printf("Ouput %s\n\n", Abc_ObjName(pNodePo)); + saucyGateWay( pNtk, pNodePo, gFile, 0, fLookForSwaps, fFixOutputs, fFixInputs, fQuiet, fPrintTree ); + printf("----------------------------------------\n"); + } + fclose(hadi); + } else if (outputName != NULL) { + int i; + Abc_Obj_t * pNodePo; + Abc_NtkForEachPo( pNtk, pNodePo, i ) { + if (!strcmp(Abc_ObjName(pNodePo), outputName)) { + saucyGateWay( pNtk, pNodePo, gFile, 0, fLookForSwaps, fFixOutputs, fFixInputs, fQuiet, fPrintTree ); + Abc_NtkDelete( pNtk ); + return 0; + } + } + Abc_Print( -1, "Output not found\n" ); + return 1; + } else + saucyGateWay( pNtk, NULL, gFile, 0, fLookForSwaps, fFixOutputs, fFixInputs, fQuiet, fPrintTree ); + + if (gFile != NULL) fclose(gFile); + Abc_NtkDelete( pNtk ); + return 0; + +usage: + Abc_Print( -2, "usage: saucy3 [-O ] [-F ] [-iosqvh]\n\n" ); + Abc_Print( -2, "\t computes functional symmetries of the netowrk\n" ); + Abc_Print( -2, "\t prints symmetry generators to the standard output\n" ); + Abc_Print( -2, "\t-O : (optional) compute symmetries only for output given by name\n"); + Abc_Print( -2, "\t only inputs in the output cone are permuted\n"); + Abc_Print( -2, "\t (special case) name=all, compute symmetries for each\n" ); + Abc_Print( -2, "\t output, but only one output at a time\n" ); + Abc_Print( -2, "\t [default = compute symmetries by permuting all I/Os]\n" ); + Abc_Print( -2, "\t-F : print symmetry generators to file [default = stdout]\n"); + Abc_Print( -2, "\t-i : permute just the inputs (fix the outputs) [default = no]\n"); + Abc_Print( -2, "\t-o : permute just the outputs (fix the inputs) [default = no]\n"); + Abc_Print( -2, "\t-s : only look for swaps of inputs [default = no]\n"); + Abc_Print( -2, "\t-q : quiet (do not print symmetry generators) [default = no]\n"); + Abc_Print( -2, "\t-v : verbose (print the search tree) [default = no]\n"); + Abc_Print( -2, "\t-h : print the command usage\n"); + + Abc_Print( -2, "\t \n" ); + Abc_Print( -2, "\t This command was contributed by Hadi Katebi from U Michigan." ); + Abc_Print( -2, "\t The paper describing the method: H. Katebi, K. Sakallah and\n"); + Abc_Print( -2, "\t I. L. Markov.\n" ); + Abc_Print( -2, "\t \"Generalized Boolean Symmetries Through Nested Partition\n"); + Abc_Print( -2, "\t Refinement\". Proc. ICCAD 2013. \n" ); + //Abc_Print( -2, "\t http://www.eecs.umich.edu/~imarkov/pubs/conf/date10-match.pdf\n" ); + Abc_Print( -2, "\t Saucy webpage: http://vlsicad.eecs.umich.edu/BK/SAUCY/\n" ); + + return 1; +} + /**Function************************************************************* Synopsis [] -- cgit v1.2.3