src/aig/fra/fra.h File Reference
#include <stdio.h>#include <stdlib.h>#include <string.h>#include <assert.h>#include <time.h>#include "vec.h"#include "aig.h"#include "dar.h"#include "satSolver.h"#include "bar.h"
Include dependency graph for fra.h:
This graph shows which files directly or indirectly include this file:
Go to the source code of this file.
Typedef Documentation
| typedef struct Fra_Bmc_t_ Fra_Bmc_t |
| typedef struct Fra_Cla_t_ Fra_Cla_t |
| typedef struct Fra_Man_t_ Fra_Man_t |
| typedef struct Fra_Par_t_ Fra_Par_t |
CFile****************************************************************
FileName [fra.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [[New FRAIG package.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [
- Id
- fra.h,v 1.00 2007/06/30 00:00:00 alanmi Exp
] INCLUDES /// PARAMETERS /// BASIC TYPES ///
| typedef struct Fra_Sml_t_ Fra_Sml_t |
Function Documentation
| int Fra_BmcNodeIsConst | ( | Aig_Obj_t * | pObj | ) |
ITERATORS /// FUNCTION DECLARATIONS ///
Function*************************************************************
Synopsis [Returns 1 if the node is costant.]
Description []
SideEffects []
SeeAlso []
Definition at line 100 of file fraBmc.c.
00101 { 00102 Fra_Man_t * p = pObj->pData; 00103 return Fra_BmcNodesAreEqual( pObj, Aig_ManConst1(p->pManAig) ); 00104 }
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Returns 1 if the nodes are equivalent.]
Description []
SideEffects []
SeeAlso []
Definition at line 69 of file fraBmc.c.
00070 { 00071 Fra_Man_t * p = pObj0->pData; 00072 Aig_Obj_t * pObjFrames0, * pObjFrames1; 00073 Aig_Obj_t * pObjFraig0, * pObjFraig1; 00074 int i; 00075 for ( i = p->pBmc->nPref; i < p->pBmc->nFramesAll; i++ ) 00076 { 00077 pObjFrames0 = Aig_Regular( Bmc_ObjFrames(pObj0, i) ); 00078 pObjFrames1 = Aig_Regular( Bmc_ObjFrames(pObj1, i) ); 00079 if ( pObjFrames0 == pObjFrames1 ) 00080 continue; 00081 pObjFraig0 = Aig_Regular( Bmc_ObjFraig(pObjFrames0) ); 00082 pObjFraig1 = Aig_Regular( Bmc_ObjFraig(pObjFrames1) ); 00083 if ( pObjFraig0 != pObjFraig1 ) 00084 return 0; 00085 } 00086 return 1; 00087 }
| void Fra_BmcPerform | ( | Fra_Man_t * | p, | |
| int | nPref, | |||
| int | nDepth | |||
| ) |
Function*************************************************************
Synopsis [Performs BMC for the given AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 297 of file fraBmc.c.
00298 { 00299 Aig_Obj_t * pObj; 00300 int i, nImpsOld, clk = clock(); 00301 assert( p->pBmc == NULL ); 00302 // derive and fraig the frames 00303 p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth ); 00304 p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc ); 00305 // if implications are present, configure the AIG manager to check them 00306 if ( p->pCla->vImps ) 00307 { 00308 p->pBmc->pAigFrames->pImpFunc = Fra_BmcFilterImplications; 00309 p->pBmc->pAigFrames->pImpData = p->pBmc; 00310 p->pBmc->vImps = p->pCla->vImps; 00311 nImpsOld = Vec_IntSize(p->pCla->vImps); 00312 } 00313 p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000 ); 00314 p->pBmc->pObjToFraig = p->pBmc->pAigFrames->pObjCopies; 00315 p->pBmc->pAigFrames->pObjCopies = NULL; 00316 // annotate frames nodes with pointers to the manager 00317 Aig_ManForEachObj( p->pBmc->pAigFrames, pObj, i ) 00318 pObj->pData = p; 00319 // report the results 00320 if ( p->pPars->fVerbose ) 00321 { 00322 printf( "Original AIG = %d. Init %d frames = %d. Fraig = %d. ", 00323 Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll, 00324 Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) ); 00325 PRT( "Time", clock() - clk ); 00326 printf( "Before BMC: " ); 00327 // Fra_ClassesPrint( p->pCla, 0 ); 00328 printf( "Const = %5d. Class = %5d. Lit = %5d. ", 00329 Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) ); 00330 if ( p->pCla->vImps ) 00331 printf( "Imp = %5d. ", nImpsOld ); 00332 printf( "\n" ); 00333 } 00334 // refine the classes 00335 p->pCla->pFuncNodeIsConst = Fra_BmcNodeIsConst; 00336 p->pCla->pFuncNodesAreEqual = Fra_BmcNodesAreEqual; 00337 Fra_ClassesRefine( p->pCla ); 00338 Fra_ClassesRefine1( p->pCla, 1, NULL ); 00339 p->pCla->pFuncNodeIsConst = Fra_SmlNodeIsConst; 00340 p->pCla->pFuncNodesAreEqual = Fra_SmlNodesAreEqual; 00341 // report the results 00342 if ( p->pPars->fVerbose ) 00343 { 00344 printf( "After BMC: " ); 00345 // Fra_ClassesPrint( p->pCla, 0 ); 00346 printf( "Const = %5d. Class = %5d. Lit = %5d. ", 00347 Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) ); 00348 if ( p->pCla->vImps ) 00349 printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) ); 00350 printf( "\n" ); 00351 } 00352 // free the BMC manager 00353 Fra_BmcStop( p->pBmc ); 00354 p->pBmc = NULL; 00355 }
| void Fra_BmcStop | ( | Fra_Bmc_t * | p | ) |
Function*************************************************************
Synopsis [Stops the BMC manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 213 of file fraBmc.c.
00214 { 00215 Aig_ManStop( p->pAigFrames ); 00216 Aig_ManStop( p->pAigFraig ); 00217 free( p->pObjToFrames ); 00218 free( p->pObjToFraig ); 00219 free( p ); 00220 }
Function*************************************************************
Synopsis [Starts representation of equivalence classes.]
Description []
SideEffects []
SeeAlso []
Definition at line 111 of file fraClass.c.
00112 { 00113 Aig_Obj_t * pObj; 00114 int i; 00115 Aig_ManReprStart( p->pAig, Aig_ManObjNumMax(p->pAig) ); 00116 memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) ); 00117 if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 ) 00118 { 00119 Aig_ManForEachObj( p->pAig, pObj, i ) 00120 { 00121 if ( p->pAig->pReprs[i] != NULL ) 00122 printf( "Classes are not cleared!\n" ); 00123 assert( p->pAig->pReprs[i] == NULL ); 00124 } 00125 } 00126 if ( vFailed ) 00127 Vec_PtrForEachEntry( vFailed, pObj, i ) 00128 p->pAig->pReprs[pObj->Id] = NULL; 00129 }
| int Fra_ClassesCountLits | ( | Fra_Cla_t * | p | ) |
Function*************************************************************
Synopsis [Count the number of literals.]
Description []
SideEffects []
SeeAlso []
Definition at line 161 of file fraClass.c.
00162 { 00163 Aig_Obj_t ** pClass; 00164 int i, nNodes, nLits = 0; 00165 nLits = Vec_PtrSize( p->vClasses1 ); 00166 Vec_PtrForEachEntry( p->vClasses, pClass, i ) 00167 { 00168 nNodes = Fra_ClassCount( pClass ); 00169 assert( nNodes > 1 ); 00170 nLits += nNodes - 1; 00171 } 00172 return nLits; 00173 }
| int Fra_ClassesCountPairs | ( | Fra_Cla_t * | p | ) |
Function*************************************************************
Synopsis [Count the number of pairs.]
Description []
SideEffects []
SeeAlso []
Definition at line 186 of file fraClass.c.
00187 { 00188 Aig_Obj_t ** pClass; 00189 int i, nNodes, nPairs = 0; 00190 Vec_PtrForEachEntry( p->vClasses, pClass, i ) 00191 { 00192 nNodes = Fra_ClassCount( pClass ); 00193 assert( nNodes > 1 ); 00194 nPairs += nNodes * (nNodes - 1) / 2; 00195 } 00196 return nPairs; 00197 }
Function*************************************************************
Synopsis [Derives AIG for the partitioned problem.]
Description []
SideEffects []
SeeAlso []
Definition at line 791 of file fraClass.c.
00792 { 00793 Aig_Man_t * pManFraig; 00794 Aig_Obj_t * pObj, * pObjNew; 00795 Aig_Obj_t ** pLatches, ** ppEquivs; 00796 int i, k, f, nFramesAll = nFramesK + 1; 00797 assert( Aig_ManRegNum(p->pAig) > 0 ); 00798 assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); 00799 assert( nFramesK > 0 ); 00800 // start the fraig package 00801 pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll ); 00802 pManFraig->pName = Aig_UtilStrsav( p->pAig->pName ); 00803 // allocate place for the node mapping 00804 ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); 00805 Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) ); 00806 // create latches for the first frame 00807 Aig_ManForEachLoSeq( p->pAig, pObj, i ) 00808 Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) ); 00809 // add timeframes 00810 pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) ); 00811 for ( f = 0; f < nFramesAll; f++ ) 00812 { 00813 // create PIs for this frame 00814 Aig_ManForEachPiSeq( p->pAig, pObj, i ) 00815 Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) ); 00816 // set the constraints on the latch outputs 00817 Aig_ManForEachLoSeq( p->pAig, pObj, i ) 00818 Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs ); 00819 // add internal nodes of this frame 00820 Aig_ManForEachNode( p->pAig, pObj, i ) 00821 { 00822 pObjNew = Aig_And( pManFraig, Fra_ObjChild0Equ(ppEquivs, pObj), Fra_ObjChild1Equ(ppEquivs, pObj) ); 00823 Fra_ObjSetEqu( ppEquivs, pObj, pObjNew ); 00824 Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs ); 00825 } 00826 if ( f == nFramesAll - 1 ) 00827 break; 00828 if ( f == nFramesAll - 2 ) 00829 pManFraig->nAsserts = Aig_ManPoNum(pManFraig); 00830 // save the latch input values 00831 k = 0; 00832 Aig_ManForEachLiSeq( p->pAig, pObj, i ) 00833 pLatches[k++] = Fra_ObjChild0Equ( ppEquivs, pObj ); 00834 // insert them to the latch output values 00835 k = 0; 00836 Aig_ManForEachLoSeq( p->pAig, pObj, i ) 00837 Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] ); 00838 } 00839 free( pLatches ); 00840 free( ppEquivs ); 00841 // mark the asserts 00842 assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 ); 00843 printf( "Assert miters = %6d. Output miters = %6d.\n", 00844 pManFraig->nAsserts, Aig_ManPoNum(pManFraig) - pManFraig->nAsserts ); 00845 // remove dangling nodes 00846 Aig_ManCleanup( pManFraig ); 00847 return pManFraig; 00848 }
| void Fra_ClassesLatchCorr | ( | Fra_Man_t * | p | ) |
Function*************************************************************
Synopsis [Creates latch correspondence classes.]
Description []
SideEffects []
SeeAlso []
Definition at line 611 of file fraClass.c.
00612 { 00613 Aig_Obj_t * pObj; 00614 int i, nEntries = 0; 00615 Vec_PtrClear( p->pCla->vClasses1 ); 00616 Aig_ManForEachLoSeq( p->pManAig, pObj, i ) 00617 { 00618 Vec_PtrPush( p->pCla->vClasses1, pObj ); 00619 Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pManAig) ); 00620 } 00621 // allocate room for classes 00622 p->pCla->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) ); 00623 p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries; 00624 }
| void Fra_ClassesPostprocess | ( | Fra_Cla_t * | p | ) |
Function*************************************************************
Synopsis [Postprocesses the classes by removing half of the less useful.]
Description []
SideEffects []
SeeAlso []
Definition at line 637 of file fraClass.c.
00638 { 00639 int Ratio = 2; 00640 Fra_Sml_t * pComb; 00641 Aig_Obj_t * pObj, * pRepr, ** ppClass; 00642 int * pWeights, WeightMax = 0, i, k, c; 00643 // perform combinational simulation 00644 pComb = Fra_SmlSimulateComb( p->pAig, 32 ); 00645 // compute the weight of each node in the classes 00646 pWeights = ALLOC( int, Aig_ManObjNumMax(p->pAig) ); 00647 memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) ); 00648 Aig_ManForEachObj( p->pAig, pObj, i ) 00649 { 00650 pRepr = Fra_ClassObjRepr( pObj ); 00651 if ( pRepr == NULL ) 00652 continue; 00653 pWeights[i] = Fra_SmlNodeNotEquWeight( pComb, pRepr->Id, pObj->Id ); 00654 WeightMax = AIG_MAX( WeightMax, pWeights[i] ); 00655 } 00656 Fra_SmlStop( pComb ); 00657 printf( "Before: Const = %6d. Class = %6d. ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) ); 00658 // remove nodes from classes whose weight is less than WeightMax/Ratio 00659 k = 0; 00660 Vec_PtrForEachEntry( p->vClasses1, pObj, i ) 00661 { 00662 if ( pWeights[pObj->Id] >= WeightMax/Ratio ) 00663 Vec_PtrWriteEntry( p->vClasses1, k++, pObj ); 00664 else 00665 Fra_ClassObjSetRepr( pObj, NULL ); 00666 } 00667 Vec_PtrShrink( p->vClasses1, k ); 00668 // in each class, compact the nodes 00669 Vec_PtrForEachEntry( p->vClasses, ppClass, i ) 00670 { 00671 k = 1; 00672 for ( c = 1; ppClass[c]; c++ ) 00673 { 00674 if ( pWeights[ppClass[c]->Id] >= WeightMax/Ratio ) 00675 ppClass[k++] = ppClass[c]; 00676 else 00677 Fra_ClassObjSetRepr( ppClass[c], NULL ); 00678 } 00679 ppClass[k] = NULL; 00680 } 00681 // remove classes with only repr 00682 k = 0; 00683 Vec_PtrForEachEntry( p->vClasses, ppClass, i ) 00684 if ( ppClass[1] != NULL ) 00685 Vec_PtrWriteEntry( p->vClasses, k++, ppClass ); 00686 Vec_PtrShrink( p->vClasses, k ); 00687 printf( "After: Const = %6d. Class = %6d. \n", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) ); 00688 free( pWeights ); 00689 }
| void Fra_ClassesPrepare | ( | Fra_Cla_t * | p, | |
| int | fLatchCorr | |||
| ) |
Function*************************************************************
Synopsis [Creates initial simulation classes.]
Description [Assumes that simulation info is assigned.]
SideEffects []
SeeAlso []
Definition at line 273 of file fraClass.c.
00274 { 00275 Aig_Obj_t ** ppTable, ** ppNexts; 00276 Aig_Obj_t * pObj, * pTemp; 00277 int i, k, nTableSize, nEntries, nNodes, iEntry; 00278 00279 // allocate the hash table hashing simulation info into nodes 00280 nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig) ); 00281 ppTable = ALLOC( Aig_Obj_t *, nTableSize ); 00282 ppNexts = ALLOC( Aig_Obj_t *, nTableSize ); 00283 memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize ); 00284 00285 // add all the nodes to the hash table 00286 Vec_PtrClear( p->vClasses1 ); 00287 Aig_ManForEachObj( p->pAig, pObj, i ) 00288 { 00289 if ( fLatchCorr ) 00290 { 00291 if ( !Aig_ObjIsPi(pObj) ) 00292 continue; 00293 } 00294 else 00295 { 00296 if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) 00297 continue; 00298 // skip the node with more that the given number of levels 00299 // if ( pObj->Level > 3 ) 00300 // continue; 00301 } 00302 // hash the node by its simulation info 00303 iEntry = p->pFuncNodeHash( pObj, nTableSize ); 00304 // check if the node belongs to the class of constant 1 00305 if ( p->pFuncNodeIsConst( pObj ) ) 00306 { 00307 Vec_PtrPush( p->vClasses1, pObj ); 00308 Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pAig) ); 00309 continue; 00310 } 00311 // add the node to the class 00312 if ( ppTable[iEntry] == NULL ) 00313 { 00314 ppTable[iEntry] = pObj; 00315 Fra_ObjSetNext( ppNexts, pObj, pObj ); 00316 } 00317 else 00318 { 00319 Fra_ObjSetNext( ppNexts, pObj, Fra_ObjNext(ppNexts,ppTable[iEntry]) ); 00320 Fra_ObjSetNext( ppNexts, ppTable[iEntry], pObj ); 00321 } 00322 } 00323 00324 // count the total number of nodes in the non-trivial classes 00325 // mark the representative nodes of each equivalence class 00326 nEntries = 0; 00327 for ( i = 0; i < nTableSize; i++ ) 00328 if ( ppTable[i] && ppTable[i] != Fra_ObjNext(ppNexts, ppTable[i]) ) 00329 { 00330 for ( pTemp = Fra_ObjNext(ppNexts, ppTable[i]), k = 1; 00331 pTemp != ppTable[i]; 00332 pTemp = Fra_ObjNext(ppNexts, pTemp), k++ ); 00333 assert( k > 1 ); 00334 nEntries += k; 00335 // mark the node 00336 assert( ppTable[i]->fMarkA == 0 ); 00337 ppTable[i]->fMarkA = 1; 00338 } 00339 00340 // allocate room for classes 00341 p->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) ); 00342 p->pMemClassesFree = p->pMemClasses + 2*nEntries; 00343 00344 // copy the entries into storage in the topological order 00345 Vec_PtrClear( p->vClasses ); 00346 nEntries = 0; 00347 Aig_ManForEachObj( p->pAig, pObj, i ) 00348 { 00349 if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) 00350 continue; 00351 // skip the nodes that are not representatives of non-trivial classes 00352 if ( pObj->fMarkA == 0 ) 00353 continue; 00354 pObj->fMarkA = 0; 00355 // add the class of nodes 00356 Vec_PtrPush( p->vClasses, p->pMemClasses + 2*nEntries ); 00357 // count the number of entries in this class 00358 for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; 00359 pTemp != pObj; 00360 pTemp = Fra_ObjNext(ppNexts, pTemp), k++ ); 00361 nNodes = k; 00362 assert( nNodes > 1 ); 00363 // add the nodes to the class in the topological order 00364 p->pMemClasses[2*nEntries] = pObj; 00365 for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; 00366 pTemp != pObj; 00367 pTemp = Fra_ObjNext(ppNexts, pTemp), k++ ) 00368 { 00369 p->pMemClasses[2*nEntries+nNodes-k] = pTemp; 00370 Fra_ClassObjSetRepr( pTemp, pObj ); 00371 } 00372 // add as many empty entries 00373 p->pMemClasses[2*nEntries + nNodes] = NULL; 00374 // increment the number of entries 00375 nEntries += k; 00376 } 00377 free( ppTable ); 00378 free( ppNexts ); 00379 // now it is time to refine the classes 00380 Fra_ClassesRefine( p ); 00381 }
| void Fra_ClassesPrint | ( | Fra_Cla_t * | p, | |
| int | fVeryVerbose | |||
| ) |
Function*************************************************************
Synopsis [Prints simulation classes.]
Description []
SideEffects []
SeeAlso []
Definition at line 233 of file fraClass.c.
00234 { 00235 Aig_Obj_t ** pClass; 00236 Aig_Obj_t * pObj; 00237 int i; 00238 00239 printf( "Const = %5d. Class = %5d. Lit = %5d. ", 00240 Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) ); 00241 if ( p->vImps && Vec_IntSize(p->vImps) > 0 ) 00242 printf( "Imp = %5d. ", Vec_IntSize(p->vImps) ); 00243 printf( "\n" ); 00244 00245 if ( fVeryVerbose ) 00246 { 00247 Vec_PtrForEachEntry( p->vClasses1, pObj, i ) 00248 assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) ); 00249 printf( "Constants { " ); 00250 Vec_PtrForEachEntry( p->vClasses1, pObj, i ) 00251 printf( "%d ", pObj->Id ); 00252 printf( "}\n" ); 00253 Vec_PtrForEachEntry( p->vClasses, pClass, i ) 00254 { 00255 printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) ); 00256 Fra_PrintClass( pClass ); 00257 } 00258 printf( "\n" ); 00259 } 00260 }
| int Fra_ClassesRefine | ( | Fra_Cla_t * | p | ) |
Function*************************************************************
Synopsis [Refines the classes after simulation.]
Description [Assumes that simulation info is assigned. Returns the number of classes refined.]
SideEffects []
SeeAlso []
Definition at line 489 of file fraClass.c.
00490 { 00491 Vec_Ptr_t * vTemp; 00492 Aig_Obj_t ** pClass; 00493 int i, nRefis; 00494 // refine the classes 00495 nRefis = 0; 00496 Vec_PtrClear( p->vClassesTemp ); 00497 Vec_PtrForEachEntry( p->vClasses, pClass, i ) 00498 { 00499 // add the class to the new array 00500 assert( pClass[0] != NULL ); 00501 Vec_PtrPush( p->vClassesTemp, pClass ); 00502 // refine the class iteratively 00503 nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp ); 00504 } 00505 // exchange the class representation 00506 vTemp = p->vClassesTemp; 00507 p->vClassesTemp = p->vClasses; 00508 p->vClasses = vTemp; 00509 return nRefis; 00510 }
| int Fra_ClassesRefine1 | ( | Fra_Cla_t * | p, | |
| int | fRefineNewClass, | |||
| int * | pSkipped | |||
| ) |
Function*************************************************************
Synopsis [Refines constant 1 equivalence class.]
Description []
SideEffects []
SeeAlso []
Definition at line 523 of file fraClass.c.
00524 { 00525 Aig_Obj_t * pObj, ** ppClass; 00526 int i, k, nRefis = 1; 00527 // check if there is anything to refine 00528 if ( Vec_PtrSize(p->vClasses1) == 0 ) 00529 return 0; 00530 // make sure constant 1 class contains only non-constant nodes 00531 assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pAig) ); 00532 // collect all the nodes to be refined 00533 k = 0; 00534 Vec_PtrClear( p->vClassNew ); 00535 Vec_PtrForEachEntry( p->vClasses1, pObj, i ) 00536 { 00537 if ( p->pFuncNodeIsConst( pObj ) ) 00538 Vec_PtrWriteEntry( p->vClasses1, k++, pObj ); 00539 else 00540 Vec_PtrPush( p->vClassNew, pObj ); 00541 } 00542 Vec_PtrShrink( p->vClasses1, k ); 00543 if ( Vec_PtrSize(p->vClassNew) == 0 ) 00544 return 0; 00545 /* 00546 printf( "Refined const-1 class: {" ); 00547 Vec_PtrForEachEntry( p->vClassNew, pObj, i ) 00548 printf( " %d", pObj->Id ); 00549 printf( " }\n" ); 00550 */ 00551 if ( Vec_PtrSize(p->vClassNew) == 1 ) 00552 { 00553 Fra_ClassObjSetRepr( Vec_PtrEntry(p->vClassNew,0), NULL ); 00554 return 1; 00555 } 00556 // create a new class composed of these nodes 00557 ppClass = p->pMemClassesFree; 00558 p->pMemClassesFree += 2 * Vec_PtrSize(p->vClassNew); 00559 Vec_PtrForEachEntry( p->vClassNew, pObj, i ) 00560 { 00561 ppClass[i] = pObj; 00562 ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL; 00563 Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL ); 00564 } 00565 assert( ppClass[0] != NULL ); 00566 Vec_PtrPush( p->vClasses, ppClass ); 00567 // iteratively refine this class 00568 if ( fRefineNewClass ) 00569 nRefis += Fra_RefineClassLastIter( p, p->vClasses ); 00570 else if ( pSkipped ) 00571 (*pSkipped)++; 00572 return nRefis; 00573 }
| void Fra_ClassesSelectRepr | ( | Fra_Cla_t * | p | ) |
Function*************************************************************
Synopsis [Postprocesses the classes by selecting representative lowest in top order.]
Description []
SideEffects []
SeeAlso []
Definition at line 702 of file fraClass.c.
00703 { 00704 Aig_Obj_t ** pClass, * pNodeMin; 00705 int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur; 00706 // reassign representatives in each class 00707 Vec_PtrForEachEntry( p->vClasses, pClass, i ) 00708 { 00709 // collect support sizes and find the min-support node 00710 pNodeMin = NULL; 00711 nSuppSizeMin = AIG_INFINITY; 00712 for ( c = 0; pClass[c]; c++ ) 00713 { 00714 nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] ); 00715 // nSuppSizeCur = 1; 00716 if ( nSuppSizeMin > nSuppSizeCur || 00717 (nSuppSizeMin == nSuppSizeCur && pNodeMin->Level > pClass[c]->Level) ) 00718 { 00719 nSuppSizeMin = nSuppSizeCur; 00720 pNodeMin = pClass[c]; 00721 cMinSupp = c; 00722 } 00723 } 00724 // skip the case when the repr did not change 00725 if ( cMinSupp == 0 ) 00726 continue; 00727 // make the new node the representative of the class 00728 pClass[cMinSupp] = pClass[0]; 00729 pClass[0] = pNodeMin; 00730 // set the representative 00731 for ( c = 0; pClass[c]; c++ ) 00732 Fra_ClassObjSetRepr( pClass[c], c? pClass[0] : NULL ); 00733 } 00734 }
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Starts representation of equivalence classes.]
Description []
SideEffects []
SeeAlso []
Definition at line 57 of file fraClass.c.
00058 { 00059 Fra_Cla_t * p; 00060 p = ALLOC( Fra_Cla_t, 1 ); 00061 memset( p, 0, sizeof(Fra_Cla_t) ); 00062 p->pAig = pAig; 00063 p->pMemRepr = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) ); 00064 memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) ); 00065 p->vClasses = Vec_PtrAlloc( 100 ); 00066 p->vClasses1 = Vec_PtrAlloc( 100 ); 00067 p->vClassesTemp = Vec_PtrAlloc( 100 ); 00068 p->vClassOld = Vec_PtrAlloc( 100 ); 00069 p->vClassNew = Vec_PtrAlloc( 100 ); 00070 p->pFuncNodeHash = Fra_SmlNodeHash; 00071 p->pFuncNodeIsConst = Fra_SmlNodeIsConst; 00072 p->pFuncNodesAreEqual = Fra_SmlNodesAreEqual; 00073 return p; 00074 }
| void Fra_ClassesStop | ( | Fra_Cla_t * | p | ) |
Function*************************************************************
Synopsis [Stop representation of equivalence classes.]
Description []
SideEffects []
SeeAlso []
Definition at line 87 of file fraClass.c.
00088 { 00089 FREE( p->pMemClasses ); 00090 FREE( p->pMemRepr ); 00091 if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp ); 00092 if ( p->vClassNew ) Vec_PtrFree( p->vClassNew ); 00093 if ( p->vClassOld ) Vec_PtrFree( p->vClassOld ); 00094 if ( p->vClasses1 ) Vec_PtrFree( p->vClasses1 ); 00095 if ( p->vClasses ) Vec_PtrFree( p->vClasses ); 00096 if ( p->vImps ) Vec_IntFree( p->vImps ); 00097 free( p ); 00098 }
| void Fra_ClassesTest | ( | Fra_Cla_t * | p, | |
| int | Id1, | |||
| int | Id2 | |||
| ) |
Function*************************************************************
Synopsis [Starts representation of equivalence classes with one class.]
Description []
SideEffects []
SeeAlso []
Definition at line 586 of file fraClass.c.
00587 { 00588 Aig_Obj_t ** pClass; 00589 p->pMemClasses = ALLOC( Aig_Obj_t *, 4 ); 00590 pClass = p->pMemClasses; 00591 assert( Id1 < Id2 ); 00592 pClass[0] = Aig_ManObj( p->pAig, Id1 ); 00593 pClass[1] = Aig_ManObj( p->pAig, Id2 ); 00594 pClass[2] = NULL; 00595 pClass[3] = NULL; 00596 Fra_ClassObjSetRepr( pClass[1], pClass[0] ); 00597 Vec_PtrPush( p->vClasses, pClass ); 00598 }
Function*************************************************************
Synopsis [Updates the solver clause database.]
Description []
SideEffects []
SeeAlso []
Definition at line 237 of file fraCnf.c.
00238 { 00239 Vec_Ptr_t * vFrontier, * vFanins; 00240 Aig_Obj_t * pNode, * pFanin; 00241 int i, k, fUseMuxes = 1; 00242 assert( pOld || pNew ); 00243 // quit if CNF is ready 00244 if ( (!pOld || Fra_ObjFaninVec(pOld)) && (!pNew || Fra_ObjFaninVec(pNew)) ) 00245 return; 00246 // start the frontier 00247 vFrontier = Vec_PtrAlloc( 100 ); 00248 if ( pOld ) Fra_ObjAddToFrontier( p, pOld, vFrontier ); 00249 if ( pNew ) Fra_ObjAddToFrontier( p, pNew, vFrontier ); 00250 // explore nodes in the frontier 00251 Vec_PtrForEachEntry( vFrontier, pNode, i ) 00252 { 00253 // create the supergate 00254 assert( Fra_ObjSatNum(pNode) ); 00255 assert( Fra_ObjFaninVec(pNode) == NULL ); 00256 if ( fUseMuxes && Aig_ObjIsMuxType(pNode) ) 00257 { 00258 vFanins = Vec_PtrAlloc( 4 ); 00259 Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) ); 00260 Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) ); 00261 Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) ); 00262 Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) ); 00263 Vec_PtrForEachEntry( vFanins, pFanin, k ) 00264 Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); 00265 Fra_AddClausesMux( p, pNode ); 00266 } 00267 else 00268 { 00269 vFanins = Fra_CollectSuper( pNode, fUseMuxes ); 00270 Vec_PtrForEachEntry( vFanins, pFanin, k ) 00271 Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); 00272 Fra_AddClausesSuper( p, pNode, vFanins ); 00273 } 00274 assert( Vec_PtrSize(vFanins) > 1 ); 00275 Fra_ObjSetFaninVec( pNode, vFanins ); 00276 } 00277 Vec_PtrFree( vFrontier ); 00278 }
Function*************************************************************
Synopsis [Performs choicing of the AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 385 of file fraCore.c.
00386 { 00387 Fra_Par_t Pars, * pPars = &Pars; 00388 Fra_ParamsDefault( pPars ); 00389 pPars->nBTLimitNode = nConfMax; 00390 pPars->fChoicing = 1; 00391 pPars->fDoSparse = 1; 00392 pPars->fSpeculate = 0; 00393 pPars->fProve = 0; 00394 pPars->fVerbose = 0; 00395 return Fra_FraigPerform( pManAig, pPars ); 00396 }
Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 409 of file fraCore.c.
00410 { 00411 Aig_Man_t * pFraig; 00412 Fra_Par_t Pars, * pPars = &Pars; 00413 Fra_ParamsDefault( pPars ); 00414 pPars->nBTLimitNode = nConfMax; 00415 pPars->fChoicing = 0; 00416 pPars->fDoSparse = 1; 00417 pPars->fSpeculate = 0; 00418 pPars->fProve = 0; 00419 pPars->fVerbose = 0; 00420 pFraig = Fra_FraigPerform( pManAig, pPars ); 00421 return pFraig; 00422 }
| Aig_Man_t* Fra_FraigInduction | ( | Aig_Man_t * | pManAig, | |
| int | nFramesP, | |||
| int | nFramesK, | |||
| int | nMaxImps, | |||
| int | fRewrite, | |||
| int | fUseImps, | |||
| int | fLatchCorr, | |||
| int | fWriteImps, | |||
| int | fVerbose, | |||
| int * | pnIter | |||
| ) |
Function*************************************************************
Synopsis [Performs choicing of the AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 247 of file fraInd.c.
00248 { 00249 int fUseSimpleCnf = 0; 00250 int fUseOldSimulation = 0; 00251 // other paramaters affecting performance 00252 // - presence of FRAIGing in Abc_NtkDarSeqSweep() 00253 // - using distance-1 patterns in Fra_SmlAssignDist1() 00254 // - the number of simulation patterns 00255 // - the number of BMC frames 00256 00257 Fra_Man_t * p; 00258 Fra_Par_t Pars, * pPars = &Pars; 00259 Aig_Obj_t * pObj; 00260 Cnf_Dat_t * pCnf; 00261 Aig_Man_t * pManAigNew; 00262 int nNodesBeg, nRegsBeg; 00263 int nIter, i, clk = clock(), clk2; 00264 00265 if ( Aig_ManNodeNum(pManAig) == 0 ) 00266 { 00267 if ( pnIter ) *pnIter = 0; 00268 return Aig_ManDup(pManAig, 1); 00269 } 00270 assert( Aig_ManLatchNum(pManAig) == 0 ); 00271 assert( Aig_ManRegNum(pManAig) > 0 ); 00272 assert( nFramesK > 0 ); 00273 //Aig_ManShow( pManAig, 0, NULL ); 00274 00275 nNodesBeg = Aig_ManNodeNum(pManAig); 00276 nRegsBeg = Aig_ManRegNum(pManAig); 00277 00278 // enhance the AIG by adding timeframes 00279 // Fra_FramesAddMore( pManAig, 3 ); 00280 00281 // get parameters 00282 Fra_ParamsDefaultSeq( pPars ); 00283 pPars->nFramesP = nFramesP; 00284 pPars->nFramesK = nFramesK; 00285 pPars->nMaxImps = nMaxImps; 00286 pPars->fVerbose = fVerbose; 00287 pPars->fRewrite = fRewrite; 00288 pPars->fLatchCorr = fLatchCorr; 00289 pPars->fUseImps = fUseImps; 00290 pPars->fWriteImps = fWriteImps; 00291 00292 // start the fraig manager for this run 00293 p = Fra_ManStart( pManAig, pPars ); 00294 // derive and refine e-classes using K initialized frames 00295 if ( fUseOldSimulation ) 00296 { 00297 if ( pPars->nFramesP > 0 ) 00298 { 00299 pPars->nFramesP = 0; 00300 printf( "Fra_FraigInduction(): Prefix cannot be used.\n" ); 00301 } 00302 p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords ); 00303 Fra_SmlSimulate( p, 1 ); 00304 } 00305 else 00306 { 00307 // bug: r iscas/blif/s5378.blif ; st; ssw -v 00308 // bug: r iscas/blif/s1238.blif ; st; ssw -v 00309 // refine the classes with more simulation rounds 00310 if ( fVerbose ) 00311 printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 ); 00312 p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1 ); //pPars->nFramesK + 1, 1 ); 00313 if ( fVerbose ) 00314 { 00315 PRT( "Time", clock() - clk ); 00316 } 00317 Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr ); 00318 // Fra_ClassesPostprocess( p->pCla ); 00319 // allocate new simulation manager for simulating counter-examples 00320 Fra_SmlStop( p->pSml ); 00321 p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords ); 00322 } 00323 00324 // select the most expressive implications 00325 if ( pPars->fUseImps ) 00326 p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr ); 00327 00328 // perform BMC (for the min number of frames) 00329 Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement 00330 //Fra_ClassesPrint( p->pCla, 1 ); 00331 // if ( p->vCex == NULL ) 00332 // p->vCex = Vec_IntAlloc( 1000 ); 00333 00334 p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); 00335 p->nNodesBeg = nNodesBeg; // Aig_ManNodeNum(pManAig); 00336 p->nRegsBeg = nRegsBeg; // Aig_ManRegNum(pManAig); 00337 00338 // dump AIG of the timeframes 00339 // pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK ); 00340 // Aig_ManDumpBlif( pManAigNew, "frame_aig.blif" ); 00341 // Fra_ManPartitionTest2( pManAigNew ); 00342 // Aig_ManStop( pManAigNew ); 00343 00344 // iterate the inductive case 00345 p->pCla->fRefinement = 1; 00346 for ( nIter = 0; p->pCla->fRefinement; nIter++ ) 00347 { 00348 int nLitsOld = Fra_ClassesCountLits(p->pCla); 00349 int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0; 00350 // mark the classes as non-refined 00351 p->pCla->fRefinement = 0; 00352 // derive non-init K-timeframes while implementing e-classes 00353 clk2 = clock(); 00354 p->pManFraig = Fra_FramesWithClasses( p ); 00355 p->timeTrav += clock() - clk2; 00356 //Aig_ManDumpBlif( p->pManFraig, "testaig.blif" ); 00357 00358 // perform AIG rewriting 00359 if ( p->pPars->fRewrite ) 00360 Fra_FraigInductionRewrite( p ); 00361 00362 // convert the manager to SAT solver (the last nLatches outputs are inputs) 00363 if ( fUseSimpleCnf || pPars->fUseImps ) 00364 pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); 00365 else 00366 pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); 00367 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); 00368 00369 p->pSat = Cnf_DataWriteIntoSolver( pCnf ); 00370 p->nSatVars = pCnf->nVars; 00371 assert( p->pSat != NULL ); 00372 if ( p->pSat == NULL ) 00373 printf( "Fra_FraigInduction(): Computed CNF is not valid.\n" ); 00374 if ( pPars->fUseImps ) 00375 { 00376 Fra_ImpAddToSolver( p, p->pCla->vImps, pCnf->pVarNums ); 00377 if ( p->pSat == NULL ) 00378 printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" ); 00379 } 00380 00381 // set the pointers to the manager 00382 Aig_ManForEachObj( p->pManFraig, pObj, i ) 00383 pObj->pData = p; 00384 00385 // prepare solver for fraiging the last timeframe 00386 Fra_ManClean( p, Aig_ManObjNumMax(p->pManFraig) + Aig_ManNodeNum(p->pManAig) ); 00387 00388 // transfer PI/LO variable numbers 00389 Aig_ManForEachObj( p->pManFraig, pObj, i ) 00390 { 00391 if ( pCnf->pVarNums[pObj->Id] == -1 ) 00392 continue; 00393 Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); 00394 Fra_ObjSetFaninVec( pObj, (void *)1 ); 00395 } 00396 Cnf_DataFree( pCnf ); 00397 00398 // report the intermediate results 00399 if ( fVerbose ) 00400 { 00401 printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. ", 00402 nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 00403 Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts ); 00404 if ( p->pCla->vImps ) 00405 printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) ); 00406 printf( "NR = %6d.\n", Aig_ManNodeNum(p->pManFraig) ); 00407 } 00408 00409 // perform sweeping 00410 p->nSatCallsRecent = 0; 00411 p->nSatCallsSkipped = 0; 00412 Fra_FraigSweep( p ); 00413 00414 // Sat_SolverPrintStats( stdout, p->pSat ); 00415 00416 // remove FRAIG and SAT solver 00417 Aig_ManStop( p->pManFraig ); p->pManFraig = NULL; 00418 sat_solver_delete( p->pSat ); p->pSat = NULL; 00419 memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); 00420 // printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped ); 00421 assert( p->vTimeouts == NULL ); 00422 if ( p->vTimeouts ) 00423 printf( "Fra_FraigInduction(): SAT solver timed out!\n" ); 00424 // check if refinement has happened 00425 // p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla)); 00426 if ( p->pCla->fRefinement && 00427 nLitsOld == Fra_ClassesCountLits(p->pCla) && 00428 nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) ) 00429 { 00430 printf( "Fra_FraigInduction(): Internal error. The result may not verify.\n" ); 00431 break; 00432 } 00433 } 00434 /* 00435 // verify implications using simulation 00436 if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) ) 00437 { 00438 int Temp, clk = clock(); 00439 if ( Temp = Fra_ImpVerifyUsingSimulation( p ) ) 00440 printf( "Implications failing the simulation test = %d (out of %d). ", Temp, Vec_IntSize(p->pCla->vImps) ); 00441 else 00442 printf( "All %d implications have passed the simulation test. ", Vec_IntSize(p->pCla->vImps) ); 00443 PRT( "Time", clock() - clk ); 00444 } 00445 */ 00446 00447 // move the classes into representatives and reduce AIG 00448 clk2 = clock(); 00449 // Fra_ClassesPrint( p->pCla, 1 ); 00450 Fra_ClassesSelectRepr( p->pCla ); 00451 Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); 00452 pManAigNew = Aig_ManDupRepr( pManAig, 0 ); 00453 // add implications to the manager 00454 if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) ) 00455 Fra_ImpRecordInManager( p, pManAigNew ); 00456 // cleanup the new manager 00457 Aig_ManSeqCleanup( pManAigNew ); 00458 // Aig_ManCountMergeRegs( pManAigNew ); 00459 p->timeTrav += clock() - clk2; 00460 p->timeTotal = clock() - clk; 00461 // get the final stats 00462 p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); 00463 p->nNodesEnd = Aig_ManNodeNum(pManAigNew); 00464 p->nRegsEnd = Aig_ManRegNum(pManAigNew); 00465 // free the manager 00466 Fra_ManStop( p ); 00467 // check the output 00468 // if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 ) 00469 // if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) ) 00470 // printf( "Proved output constant 0.\n" ); 00471 if ( pnIter ) *pnIter = nIter; 00472 return pManAigNew; 00473 }
| Aig_Man_t* Fra_FraigLatchCorrespondence | ( | Aig_Man_t * | pAig, | |
| int | nFramesP, | |||
| int | nConfMax, | |||
| int | fProve, | |||
| int | fVerbose, | |||
| int * | pnIter | |||
| ) |
Function*************************************************************
Synopsis [Performs choicing of the AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 503 of file fraLcr.c.
00504 { 00505 int nPartSize = 200; 00506 int fReprSelect = 0; 00507 00508 Fra_Lcr_t * p; 00509 Fra_Sml_t * pSml; 00510 Fra_Man_t * pTemp; 00511 Aig_Man_t * pAigPart, * pAigNew = NULL; 00512 Vec_Int_t * vPart; 00513 // Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078); 00514 int i, nIter, timeSim, clk = clock(), clk2, clk3; 00515 if ( Aig_ManNodeNum(pAig) == 0 ) 00516 { 00517 if ( pnIter ) *pnIter = 0; 00518 return Aig_ManDup(pAig, 1); 00519 } 00520 assert( Aig_ManLatchNum(pAig) == 0 ); 00521 assert( Aig_ManRegNum(pAig) > 0 ); 00522 00523 // simulate the AIG 00524 clk2 = clock(); 00525 if ( fVerbose ) 00526 printf( "Simulating AIG with %d nodes for %d cycles ... ", Aig_ManNodeNum(pAig), nFramesP + 32 ); 00527 pSml = Fra_SmlSimulateSeq( pAig, nFramesP, 32, 1 ); 00528 if ( fVerbose ) 00529 { 00530 PRT( "Time", clock() - clk2 ); 00531 timeSim = clock() - clk2; 00532 } 00533 // check if simulation discovered non-constant-0 POs 00534 if ( fProve && pSml->fNonConstOut ) 00535 { 00536 Fra_SmlStop( pSml ); 00537 return NULL; 00538 } 00539 00540 // start the manager 00541 p = Lcr_ManAlloc( pAig ); 00542 p->nFramesP = nFramesP; 00543 p->fVerbose = fVerbose; 00544 p->timeSim += timeSim; 00545 00546 pTemp = Fra_LcrAigPrepare( pAig ); 00547 pTemp->pBmc = (Fra_Bmc_t *)p; 00548 pTemp->pSml = pSml; 00549 00550 // get preliminary info about equivalence classes 00551 pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig ); 00552 Fra_ClassesPrepare( p->pCla, 1 ); 00553 p->pCla->pFuncNodeIsConst = Fra_LcrNodeIsConst; 00554 p->pCla->pFuncNodesAreEqual = Fra_LcrNodesAreEqual; 00555 Fra_SmlStop( pTemp->pSml ); 00556 00557 // partition the AIG for latch correspondence computation 00558 clk2 = clock(); 00559 if ( fVerbose ) 00560 printf( "Partitioning AIG ... " ); 00561 pAigPart = Fra_LcrDeriveAigForPartitioning( p ); 00562 p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL ); 00563 Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum ); 00564 Aig_ManStop( pAigPart ); 00565 if ( fVerbose ) 00566 { 00567 PRT( "Time", clock() - clk2 ); 00568 p->timePart += clock() - clk2; 00569 } 00570 00571 // get the initial stats 00572 p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); 00573 p->nNodesBeg = Aig_ManNodeNum(p->pAig); 00574 p->nRegsBeg = Aig_ManRegNum(p->pAig); 00575 00576 // perforn interative reduction of the partitions 00577 p->fRefining = 1; 00578 for ( nIter = 0; p->fRefining; nIter++ ) 00579 { 00580 p->fRefining = 0; 00581 clk3 = clock(); 00582 // derive AIGs for each partition 00583 Fra_ClassNodesMark( p ); 00584 Vec_PtrClear( p->vFraigs ); 00585 Vec_PtrForEachEntry( p->vParts, vPart, i ) 00586 { 00587 clk2 = clock(); 00588 pAigPart = Fra_LcrCreatePart( p, vPart ); 00589 p->timeTrav += clock() - clk2; 00590 clk2 = clock(); 00591 pAigNew = Fra_FraigEquivence( pAigPart, nConfMax ); 00592 p->timeFraig += clock() - clk2; 00593 Vec_PtrPush( p->vFraigs, pAigNew ); 00594 Aig_ManStop( pAigPart ); 00595 } 00596 Fra_ClassNodesUnmark( p ); 00597 // report the intermediate results 00598 if ( fVerbose ) 00599 { 00600 printf( "%3d : Const = %6d. Class = %6d. L = %6d. Part = %3d. ", 00601 nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 00602 Fra_ClassesCountLits(p->pCla), Vec_PtrSize(p->vParts) ); 00603 PRT( "T", clock() - clk3 ); 00604 } 00605 // refine the classes 00606 Fra_LcrAigPrepareTwo( p->pAig, pTemp ); 00607 if ( Fra_ClassesRefine( p->pCla ) ) 00608 p->fRefining = 1; 00609 if ( Fra_ClassesRefine1( p->pCla, 0, NULL ) ) 00610 p->fRefining = 1; 00611 // clean the fraigs 00612 Vec_PtrForEachEntry( p->vFraigs, pAigPart, i ) 00613 Aig_ManStop( pAigPart ); 00614 00615 // repartition if needed 00616 if ( 1 ) 00617 { 00618 clk2 = clock(); 00619 Vec_VecFree( (Vec_Vec_t *)p->vParts ); 00620 pAigPart = Fra_LcrDeriveAigForPartitioning( p ); 00621 p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL ); 00622 Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum ); 00623 Aig_ManStop( pAigPart ); 00624 p->timePart += clock() - clk2; 00625 } 00626 } 00627 free( pTemp ); 00628 p->nIters = nIter; 00629 00630 // move the classes into representatives and reduce AIG 00631 clk2 = clock(); 00632 // Fra_ClassesPrint( p->pCla, 1 ); 00633 if ( fReprSelect ) 00634 Fra_ClassesSelectRepr( p->pCla ); 00635 Fra_ClassesCopyReprs( p->pCla, NULL ); 00636 pAigNew = Aig_ManDupRepr( p->pAig, 0 ); 00637 Aig_ManSeqCleanup( pAigNew ); 00638 // Aig_ManCountMergeRegs( pAigNew ); 00639 p->timeUpdate += clock() - clk2; 00640 p->timeTotal = clock() - clk; 00641 // get the final stats 00642 p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); 00643 p->nNodesEnd = Aig_ManNodeNum(pAigNew); 00644 p->nRegsEnd = Aig_ManRegNum(pAigNew); 00645 Lcr_ManFree( p ); 00646 if ( pnIter ) *pnIter = nIter; 00647 return pAigNew; 00648 }
| int Fra_FraigMiterStatus | ( | Aig_Man_t * | p | ) |
CFile****************************************************************
FileName [fraCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [
- Id
- fraCore.c,v 1.00 2007/06/30 00:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Reports the status of the miter.]
Description []
SideEffects []
SeeAlso []
Definition at line 59 of file fraCore.c.
00060 { 00061 Aig_Obj_t * pObj, * pObjNew; 00062 int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0; 00063 if ( p->pData ) 00064 return 0; 00065 Aig_ManForEachPoSeq( p, pObj, i ) 00066 { 00067 pObjNew = Aig_ObjChild0(pObj); 00068 // check if the output is constant 0 00069 if ( pObjNew == Aig_ManConst0(p) ) 00070 { 00071 CountConst0++; 00072 continue; 00073 } 00074 // check if the output is constant 1 00075 if ( pObjNew == Aig_ManConst1(p) ) 00076 { 00077 CountNonConst0++; 00078 continue; 00079 } 00080 // check if the output can be constant 0 00081 if ( Aig_Regular(pObjNew)->fPhase != (unsigned)Aig_IsComplement(pObjNew) ) 00082 { 00083 CountNonConst0++; 00084 continue; 00085 } 00086 CountUndecided++; 00087 } 00088 /* 00089 if ( p->pParams->fVerbose ) 00090 { 00091 printf( "Miter has %d outputs. ", Aig_ManPoNum(p->pManAig) ); 00092 printf( "Const0 = %d. ", CountConst0 ); 00093 printf( "NonConst0 = %d. ", CountNonConst0 ); 00094 printf( "Undecided = %d. ", CountUndecided ); 00095 printf( "\n" ); 00096 } 00097 */ 00098 if ( CountNonConst0 ) 00099 return 0; 00100 if ( CountUndecided ) 00101 return -1; 00102 return 1; 00103 }
Function*************************************************************
Synopsis [Performs fraiging of the AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 321 of file fraCore.c.
00322 { 00323 Fra_Man_t * p; 00324 Aig_Man_t * pManAigNew; 00325 int clk; 00326 if ( Aig_ManNodeNum(pManAig) == 0 ) 00327 return Aig_ManDup(pManAig, 1); 00328 clk = clock(); 00329 assert( Aig_ManLatchNum(pManAig) == 0 ); 00330 p = Fra_ManStart( pManAig, pPars ); 00331 p->pManFraig = Fra_ManPrepareComb( p ); 00332 p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords ); 00333 Fra_SmlSimulate( p, 0 ); 00334 // if ( p->pPars->fChoicing ) 00335 // Aig_ManReprStart( p->pManFraig, Aig_ManObjNumMax(p->pManAig) ); 00336 // collect initial states 00337 p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); 00338 p->nNodesBeg = Aig_ManNodeNum(pManAig); 00339 p->nRegsBeg = Aig_ManRegNum(pManAig); 00340 // perform fraig sweep 00341 Fra_FraigSweep( p ); 00342 // call back the procedure to check implications 00343 if ( pManAig->pImpFunc ) 00344 pManAig->pImpFunc( p, pManAig->pImpData ); 00345 // finalize the fraiged manager 00346 Fra_ManFinalizeComb( p ); 00347 if ( p->pPars->fChoicing ) 00348 { 00349 int clk2 = clock(); 00350 Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); 00351 pManAigNew = Aig_ManDupRepr( p->pManAig, 1 ); 00352 Aig_ManReprStart( pManAigNew, Aig_ManObjNumMax(pManAigNew) ); 00353 Aig_ManTransferRepr( pManAigNew, p->pManAig ); 00354 Aig_ManMarkValidChoices( pManAigNew ); 00355 Aig_ManStop( p->pManFraig ); 00356 p->pManFraig = NULL; 00357 p->timeTrav += clock() - clk2; 00358 } 00359 else 00360 { 00361 Aig_ManCleanup( p->pManFraig ); 00362 pManAigNew = p->pManFraig; 00363 p->pManFraig = NULL; 00364 } 00365 p->timeTotal = clock() - clk; 00366 // collect final stats 00367 p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); 00368 p->nNodesEnd = Aig_ManNodeNum(pManAigNew); 00369 p->nRegsEnd = Aig_ManRegNum(pManAigNew); 00370 Fra_ManStop( p ); 00371 return pManAigNew; 00372 }
| int Fra_FraigSec | ( | Aig_Man_t * | p, | |
| int | nFramesMax, | |||
| int | fRetimeFirst, | |||
| int | fVerbose, | |||
| int | fVeryVerbose | |||
| ) |
Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 104 of file fraSec.c.
00105 { 00106 Fra_Sml_t * pSml; 00107 Aig_Man_t * pNew, * pTemp; 00108 int nFrames, RetValue, nIter, clk, clkTotal = clock(); 00109 int fLatchCorr = 0; 00110 00111 pNew = Aig_ManDup( p, 1 ); 00112 if ( fVerbose ) 00113 { 00114 printf( "Original miter: Latches = %5d. Nodes = %6d.\n", 00115 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); 00116 } 00117 //Aig_ManDumpBlif( pNew, "after.blif" ); 00118 00119 // perform sequential cleanup 00120 clk = clock(); 00121 if ( pNew->nRegs ) 00122 pNew = Aig_ManReduceLaches( pNew, 0 ); 00123 if ( pNew->nRegs ) 00124 pNew = Aig_ManConstReduce( pNew, 0 ); 00125 if ( fVerbose ) 00126 { 00127 printf( "Sequential cleanup: Latches = %5d. Nodes = %6d. ", 00128 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); 00129 PRT( "Time", clock() - clk ); 00130 } 00131 00132 // perform forward retiming 00133 if ( fRetimeFirst && pNew->nRegs ) 00134 { 00135 clk = clock(); 00136 pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); 00137 Aig_ManStop( pTemp ); 00138 if ( fVerbose ) 00139 { 00140 printf( "Forward retiming: Latches = %5d. Nodes = %6d. ", 00141 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); 00142 PRT( "Time", clock() - clk ); 00143 } 00144 } 00145 00146 // run latch correspondence 00147 clk = clock(); 00148 if ( pNew->nRegs ) 00149 { 00150 pNew = Aig_ManDup( pTemp = pNew, 1 ); 00151 Aig_ManStop( pTemp ); 00152 pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter ); 00153 Aig_ManStop( pTemp ); 00154 if ( pNew == NULL ) 00155 { 00156 RetValue = 0; 00157 printf( "Networks are NOT EQUIVALENT after simulation. " ); 00158 PRT( "Time", clock() - clkTotal ); 00159 return RetValue; 00160 } 00161 00162 if ( fVerbose ) 00163 { 00164 printf( "Latch-corr (I=%3d): Latches = %5d. Nodes = %6d. ", 00165 nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); 00166 PRT( "Time", clock() - clk ); 00167 } 00168 } 00169 00170 // perform fraiging 00171 clk = clock(); 00172 pNew = Fra_FraigEquivence( pTemp = pNew, 100 ); 00173 Aig_ManStop( pTemp ); 00174 if ( fVerbose ) 00175 { 00176 printf( "Fraiging: Latches = %5d. Nodes = %6d. ", 00177 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); 00178 PRT( "Time", clock() - clk ); 00179 } 00180 00181 // perform seq sweeping while increasing the number of frames 00182 RetValue = Fra_FraigMiterStatus( pNew ); 00183 if ( RetValue == -1 ) 00184 for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 ) 00185 { 00186 clk = clock(); 00187 pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter ); 00188 Aig_ManStop( pTemp ); 00189 RetValue = Fra_FraigMiterStatus( pNew ); 00190 if ( fVerbose ) 00191 { 00192 printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ", 00193 nFrames, nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); 00194 PRT( "Time", clock() - clk ); 00195 } 00196 if ( RetValue != -1 ) 00197 break; 00198 00199 // perform rewriting 00200 clk = clock(); 00201 pNew = Aig_ManDup( pTemp = pNew, 1 ); 00202 Aig_ManStop( pTemp ); 00203 pNew = Dar_ManRewriteDefault( pNew ); 00204 if ( fVerbose ) 00205 { 00206 printf( "Rewriting: Latches = %5d. Nodes = %6d. ", 00207 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); 00208 PRT( "Time", clock() - clk ); 00209 } 00210 00211 // perform retiming 00212 if ( pNew->nRegs ) 00213 { 00214 clk = clock(); 00215 pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); 00216 Aig_ManStop( pTemp ); 00217 pNew = Aig_ManDup( pTemp = pNew, 1 ); 00218 Aig_ManStop( pTemp ); 00219 if ( fVerbose ) 00220 { 00221 printf( "Forward retiming: Latches = %5d. Nodes = %6d. ", 00222 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); 00223 PRT( "Time", clock() - clk ); 00224 } 00225 } 00226 00227 if ( pNew->nRegs ) 00228 pNew = Aig_ManConstReduce( pNew, 0 ); 00229 00230 // perform sequential simulation 00231 clk = clock(); 00232 pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000) ); 00233 if ( fVerbose ) 00234 { 00235 printf( "Seq simulation : Latches = %5d. Nodes = %6d. ", 00236 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); 00237 PRT( "Time", clock() - clk ); 00238 } 00239 if ( pSml->fNonConstOut ) 00240 { 00241 Fra_SmlStop( pSml ); 00242 Aig_ManStop( pNew ); 00243 RetValue = 0; 00244 printf( "Networks are NOT EQUIVALENT after simulation. " ); 00245 PRT( "Time", clock() - clkTotal ); 00246 return RetValue; 00247 } 00248 Fra_SmlStop( pSml ); 00249 } 00250 00251 // get the miter status 00252 RetValue = Fra_FraigMiterStatus( pNew ); 00253 00254 // report the miter 00255 if ( RetValue == 1 ) 00256 { 00257 printf( "Networks are equivalent. " ); 00258 PRT( "Time", clock() - clkTotal ); 00259 } 00260 else if ( RetValue == 0 ) 00261 { 00262 printf( "Networks are NOT EQUIVALENT. " ); 00263 PRT( "Time", clock() - clkTotal ); 00264 } 00265 else 00266 { 00267 static int Counter = 1; 00268 char pFileName[1000]; 00269 printf( "Networks are UNDECIDED. " ); 00270 PRT( "Time", clock() - clkTotal ); 00271 sprintf( pFileName, "sm%03d.aig", Counter++ ); 00272 Ioa_WriteAiger( pNew, pFileName, 0 ); 00273 printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName ); 00274 } 00275 Aig_ManStop( pNew ); 00276 return RetValue; 00277 }
| void Fra_FraigSweep | ( | Fra_Man_t * | p | ) |
Function*************************************************************
Synopsis [Performs fraiging for the internal nodes.]
Description []
SideEffects []
SeeAlso []
Definition at line 268 of file fraCore.c.
00269 { 00270 Bar_Progress_t * pProgress; 00271 Aig_Obj_t * pObj, * pObjNew; 00272 int i, k = 0, Pos = 0; 00273 // fraig latch outputs 00274 Aig_ManForEachLoSeq( p->pManAig, pObj, i ) 00275 { 00276 Fra_FraigNode( p, pObj ); 00277 if ( p->pPars->fUseImps ) 00278 Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos ); 00279 } 00280 if ( p->pPars->fLatchCorr ) 00281 return; 00282 // fraig internal nodes 00283 pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pManAig) ); 00284 Aig_ManForEachNode( p->pManAig, pObj, i ) 00285 { 00286 Bar_ProgressUpdate( pProgress, i, NULL ); 00287 // derive and remember the new fraig node 00288 pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,p->pPars->nFramesK), Fra_ObjChild1Fra(pObj,p->pPars->nFramesK) ); 00289 Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjNew ); 00290 Aig_Regular(pObjNew)->pData = p; 00291 // quit if simulation detected a counter-example for a PO 00292 if ( p->pManFraig->pData ) 00293 continue; 00294 // perform fraiging 00295 Fra_FraigNode( p, pObj ); 00296 if ( p->pPars->fUseImps ) 00297 Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos ); 00298 } 00299 Bar_ProgressStop( pProgress ); 00300 // try to prove the outputs of the miter 00301 p->nNodesMiter = Aig_ManNodeNum(p->pManFraig); 00302 // Fra_MiterStatus( p->pManFraig ); 00303 // if ( p->pPars->fProve && p->pManFraig->pData == NULL ) 00304 // Fra_MiterProve( p ); 00305 // compress implications after processing all of them 00306 if ( p->pPars->fUseImps ) 00307 Fra_ImpCompactArray( p->pCla->vImps ); 00308 }
Function*************************************************************
Synopsis [Add implication clauses to the SAT solver.]
Description [Note that implications should be checked in the first frame!]
SideEffects []
SeeAlso []
Definition at line 419 of file fraImp.c.
00420 { 00421 sat_solver * pSat = p->pSat; 00422 Aig_Obj_t * pLeft, * pRight; 00423 Aig_Obj_t * pLeftF, * pRightF; 00424 int pLits[2], Imp, Left, Right, i, f, status; 00425 int fComplL, fComplR; 00426 Vec_IntForEachEntry( vImps, Imp, i ) 00427 { 00428 // get the corresponding nodes 00429 pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) ); 00430 pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) ); 00431 // check if all the nodes are present 00432 for ( f = 0; f < p->pPars->nFramesK; f++ ) 00433 { 00434 // map these info fraig 00435 pLeftF = Fra_ObjFraig( pLeft, f ); 00436 pRightF = Fra_ObjFraig( pRight, f ); 00437 if ( Aig_ObjIsNone(Aig_Regular(pLeftF)) || Aig_ObjIsNone(Aig_Regular(pRightF)) ) 00438 { 00439 Vec_IntWriteEntry( vImps, i, 0 ); 00440 break; 00441 } 00442 } 00443 if ( f < p->pPars->nFramesK ) 00444 continue; 00445 // add constraints in each timeframe 00446 for ( f = 0; f < p->pPars->nFramesK; f++ ) 00447 { 00448 // map these info fraig 00449 pLeftF = Fra_ObjFraig( pLeft, f ); 00450 pRightF = Fra_ObjFraig( pRight, f ); 00451 // get the corresponding SAT numbers 00452 Left = pSatVarNums[ Aig_Regular(pLeftF)->Id ]; 00453 Right = pSatVarNums[ Aig_Regular(pRightF)->Id ]; 00454 assert( Left > 0 && Left < p->nSatVars ); 00455 assert( Right > 0 && Right < p->nSatVars ); 00456 // get the complemented attributes 00457 fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF); 00458 fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF); 00459 // get the constraint 00460 // L => R L' v R (complement = L & R') 00461 pLits[0] = 2 * Left + !fComplL; 00462 pLits[1] = 2 * Right + fComplR; 00463 // add contraint to solver 00464 if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) ) 00465 { 00466 sat_solver_delete( pSat ); 00467 p->pSat = NULL; 00468 return; 00469 } 00470 } 00471 } 00472 status = sat_solver_simplify(pSat); 00473 if ( status == 0 ) 00474 { 00475 sat_solver_delete( pSat ); 00476 p->pSat = NULL; 00477 } 00478 // printf( "Total imps = %d. ", Vec_IntSize(vImps) ); 00479 Fra_ImpCompactArray( vImps ); 00480 // printf( "Valid imps = %d. \n", Vec_IntSize(vImps) ); 00481 }
Function*************************************************************
Synopsis [Check implications for the node (if they are present).]
Description [Returns the new position in the array.]
SideEffects []
SeeAlso []
Definition at line 494 of file fraImp.c.
00495 { 00496 Aig_Obj_t * pLeft, * pRight; 00497 Aig_Obj_t * pLeftF, * pRightF; 00498 int i, Imp, Left, Right, Max, RetValue; 00499 int fComplL, fComplR; 00500 Vec_IntForEachEntryStart( vImps, Imp, i, Pos ) 00501 { 00502 if ( Imp == 0 ) 00503 continue; 00504 Left = Fra_ImpLeft(Imp); 00505 Right = Fra_ImpRight(Imp); 00506 Max = AIG_MAX( Left, Right ); 00507 assert( Max >= pNode->Id ); 00508 if ( Max > pNode->Id ) 00509 return i; 00510 // get the corresponding nodes 00511 pLeft = Aig_ManObj( p->pManAig, Left ); 00512 pRight = Aig_ManObj( p->pManAig, Right ); 00513 // get the corresponding FRAIG nodes 00514 pLeftF = Fra_ObjFraig( pLeft, p->pPars->nFramesK ); 00515 pRightF = Fra_ObjFraig( pRight, p->pPars->nFramesK ); 00516 // get the complemented attributes 00517 fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF); 00518 fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF); 00519 // check equality 00520 if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) ) 00521 { 00522 if ( fComplL == fComplR ) // x => x - always true 00523 continue; 00524 assert( fComplL != fComplR ); 00525 // consider 4 possibilities: 00526 // NOT(1) => 1 or 0 => 1 - always true 00527 // 1 => NOT(1) or 1 => 0 - never true 00528 // NOT(x) => x or x - not always true 00529 // x => NOT(x) or NOT(x) - not always true 00530 if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication 00531 continue; 00532 // disproved implication 00533 p->pCla->fRefinement = 1; 00534 Vec_IntWriteEntry( vImps, i, 0 ); 00535 continue; 00536 } 00537 // check the implication 00538 // - if true, a clause is added 00539 // - if false, a cex is simulated 00540 // make sure the implication is refined 00541 RetValue = Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ); 00542 if ( RetValue != 1 ) 00543 { 00544 p->pCla->fRefinement = 1; 00545 if ( RetValue == 0 ) 00546 Fra_SmlResimulate( p ); 00547 if ( Vec_IntEntry(vImps, i) != 0 ) 00548 printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" ); 00549 assert( Vec_IntEntry(vImps, i) == 0 ); 00550 } 00551 } 00552 return i; 00553 }
| void Fra_ImpCompactArray | ( | Vec_Int_t * | vImps | ) |
Function*************************************************************
Synopsis [Removes empty implications.]
Description []
SideEffects []
SeeAlso []
Definition at line 598 of file fraImp.c.
00599 { 00600 int i, k, Imp; 00601 k = 0; 00602 Vec_IntForEachEntry( vImps, Imp, i ) 00603 if ( Imp ) 00604 Vec_IntWriteEntry( vImps, k++, Imp ); 00605 Vec_IntShrink( vImps, k ); 00606 }
| double Fra_ImpComputeStateSpaceRatio | ( | Fra_Man_t * | p | ) |
Function*************************************************************
Synopsis [Determines the ratio of the state space by computed implications.]
Description []
SideEffects []
SeeAlso []
Definition at line 619 of file fraImp.c.
00620 { 00621 int nSimWords = 64; 00622 Fra_Sml_t * pComb; 00623 unsigned * pResult; 00624 double Ratio = 0.0; 00625 int Left, Right, Imp, i; 00626 if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 ) 00627 return Ratio; 00628 // simulate the AIG manager with combinational patterns 00629 pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords ); 00630 // go through the implications and collect where they do not hold 00631 pResult = Fra_ObjSim( pComb, 0 ); 00632 assert( pResult[0] == 0 ); 00633 Vec_IntForEachEntry( p->pCla->vImps, Imp, i ) 00634 { 00635 Left = Fra_ImpLeft(Imp); 00636 Right = Fra_ImpRight(Imp); 00637 Sml_NodeSaveNotImpPatterns( pComb, Left, Right, pResult ); 00638 } 00639 // count the number of ones in this area 00640 Ratio = 100.0 * Fra_SmlCountOnesOne( pComb, 0 ) / (32*(pComb->nWordsTotal-pComb->nWordsPref)); 00641 Fra_SmlStop( pComb ); 00642 return Ratio; 00643 }
| static int Fra_ImpCreate | ( | int | Left, | |
| int | Right | |||
| ) | [inline, static] |
Function*************************************************************
Synopsis [Derives implication candidates.]
Description [Implication candidates have the property that (1) they hold using sequential simulation information (2) they do not hold using combinational simulation information (3) they have as high expressive power as possible (heuristically) that is, they are easy to disprove combinationally meaning they cover relatively larger sequential subspace.]
SideEffects []
SeeAlso []
Definition at line 318 of file fraImp.c.
00319 { 00320 int nSimWords = 64; 00321 Fra_Sml_t * pSeq, * pComb; 00322 Vec_Int_t * vImps, * vTemp; 00323 Vec_Ptr_t * vNodes; 00324 int * pImpCosts, * pNodesI, * pNodesK; 00325 int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0; 00326 int CostMin = AIG_INFINITY, CostMax = 0; 00327 int i, k, Imp, CostRange, clk = clock(); 00328 assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) ); 00329 assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit ); 00330 // normalize both managers 00331 pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords ); 00332 pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1 ); 00333 // get the nodes sorted by the number of 1s 00334 vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr ); 00335 // count the total number of implications 00336 for ( k = nSimWords * 32; k > 0; k-- ) 00337 for ( i = k - 1; i > 0; i-- ) 00338 for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ ) 00339 for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ ) 00340 nImpsTotal++; 00341 00342 // compute implications and their costs 00343 pImpCosts = ALLOC( int, nImpMaxLimit ); 00344 vImps = Vec_IntAlloc( nImpMaxLimit ); 00345 for ( k = pSeq->nWordsTotal * 32; k > 0; k-- ) 00346 for ( i = k - 1; i > 0; i-- ) 00347 { 00348 for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ ) 00349 for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ ) 00350 { 00351 nImpsTried++; 00352 if ( !Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) ) 00353 { 00354 nImpsNonSeq++; 00355 continue; 00356 } 00357 if ( Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) ) 00358 { 00359 nImpsComb++; 00360 continue; 00361 } 00362 nImpsCollected++; 00363 Imp = Fra_ImpCreate( *pNodesI, *pNodesK ); 00364 pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK); 00365 CostMin = AIG_MIN( CostMin, pImpCosts[ Vec_IntSize(vImps) ] ); 00366 CostMax = AIG_MAX( CostMax, pImpCosts[ Vec_IntSize(vImps) ] ); 00367 Vec_IntPush( vImps, Imp ); 00368 if ( Vec_IntSize(vImps) == nImpMaxLimit ) 00369 goto finish; 00370 } 00371 } 00372 finish: 00373 Fra_SmlStop( pComb ); 00374 Fra_SmlStop( pSeq ); 00375 00376 // select implications with the highest cost 00377 CostRange = CostMin; 00378 if ( Vec_IntSize(vImps) > nImpUseLimit ) 00379 { 00380 vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit, &CostRange ); 00381 Vec_IntFree( vTemp ); 00382 } 00383 00384 // dealloc 00385 free( pImpCosts ); 00386 free( Vec_PtrEntry(vNodes, 0) ); 00387 Vec_PtrFree( vNodes ); 00388 // reorder implications topologically 00389 qsort( (void *)Vec_IntArray(vImps), Vec_IntSize(vImps), sizeof(int), 00390 (int (*)(const void *, const void *)) Sml_CompareMaxId ); 00391 if ( p->pPars->fVerbose ) 00392 { 00393 printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n", 00394 nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected ); 00395 printf( "Implication weight: Min = %d. Pivot = %d. Max = %d. ", 00396 CostMin, CostRange, CostMax ); 00397 PRT( "Time", clock() - clk ); 00398 } 00399 return vImps; 00400 }
| static int Fra_ImpLeft | ( | int | Imp | ) | [inline, static] |
Function*************************************************************
Synopsis [Record proven implications in the AIG manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 696 of file fraImp.c.
00697 { 00698 Aig_Obj_t * pLeft, * pRight, * pMiter; 00699 int nPosOld, Imp, i; 00700 if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 ) 00701 return; 00702 // go through the implication 00703 nPosOld = Aig_ManPoNum(pNew); 00704 Vec_IntForEachEntry( p->pCla->vImps, Imp, i ) 00705 { 00706 pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) ); 00707 pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) ); 00708 // record the implication: L' + R 00709 pMiter = Aig_Or( pNew, 00710 Aig_NotCond(pLeft->pData, !pLeft->fPhase), 00711 Aig_NotCond(pRight->pData, pRight->fPhase) ); 00712 Aig_ObjCreatePo( pNew, pMiter ); 00713 } 00714 pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld; 00715 }
Function*************************************************************
Synopsis [Removes those implications that no longer hold.]
Description [Returns 1 if refinement has happened.]
SideEffects []
SeeAlso []
Definition at line 566 of file fraImp.c.
00567 { 00568 Aig_Obj_t * pLeft, * pRight; 00569 int Imp, i, RetValue = 0; 00570 Vec_IntForEachEntry( vImps, Imp, i ) 00571 { 00572 if ( Imp == 0 ) 00573 continue; 00574 // get the corresponding nodes 00575 pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) ); 00576 pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) ); 00577 // check if implication holds using this simulation info 00578 if ( !Sml_NodeCheckImp(p->pSml, pLeft->Id, pRight->Id) ) 00579 { 00580 Vec_IntWriteEntry( vImps, i, 0 ); 00581 RetValue = 1; 00582 } 00583 } 00584 return RetValue; 00585 }
| static int Fra_ImpRight | ( | int | Imp | ) | [inline, static] |
| int Fra_ImpVerifyUsingSimulation | ( | Fra_Man_t * | p | ) |
Function*************************************************************
Synopsis [Returns the number of failed implications.]
Description []
SideEffects []
SeeAlso []
Definition at line 656 of file fraImp.c.
00657 { 00658 int nFrames = 2000; 00659 int nSimWords = 8; 00660 Fra_Sml_t * pSeq; 00661 char * pfFails; 00662 int Left, Right, Imp, i, Counter; 00663 if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 ) 00664 return 0; 00665 // simulate the AIG manager with combinational patterns 00666 pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords ); 00667 // go through the implications and check how many of them do not hold 00668 pfFails = ALLOC( char, Vec_IntSize(p->pCla->vImps) ); 00669 memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) ); 00670 Vec_IntForEachEntry( p->pCla->vImps, Imp, i ) 00671 { 00672 Left = Fra_ImpLeft(Imp); 00673 Right = Fra_ImpRight(Imp); 00674 pfFails[i] = !Sml_NodeCheckImp( pSeq, Left, Right ); 00675 } 00676 // count how many has failed 00677 Counter = 0; 00678 for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ ) 00679 Counter += pfFails[i]; 00680 free( pfFails ); 00681 Fra_SmlStop( pSeq ); 00682 return Counter; 00683 }
| void Fra_ManClean | ( | Fra_Man_t * | p, | |
| int | nNodesMax | |||
| ) |
Function*************************************************************
Synopsis [Starts the fraiging manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 141 of file fraMan.c.
00142 { 00143 int i; 00144 // remove old arrays 00145 for ( i = 0; i < p->nMemAlloc; i++ ) 00146 if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 ) 00147 Vec_PtrFree( p->pMemFanins[i] ); 00148 // realloc for the new size 00149 if ( p->nMemAlloc < nNodesMax ) 00150 { 00151 int nMemAllocNew = nNodesMax + 5000; 00152 p->pMemFanins = REALLOC( Vec_Ptr_t *, p->pMemFanins, nMemAllocNew ); 00153 p->pMemSatNums = REALLOC( int, p->pMemSatNums, nMemAllocNew ); 00154 p->nMemAlloc = nMemAllocNew; 00155 } 00156 // prepare for the new run 00157 memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc ); 00158 memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc ); 00159 }
| void Fra_ManFinalizeComb | ( | Fra_Man_t * | p | ) |
Function*************************************************************
Synopsis [Finalizes the combinational miter after fraiging.]
Description []
SideEffects []
SeeAlso []
Definition at line 212 of file fraMan.c.
00213 { 00214 Aig_Obj_t * pObj; 00215 int i; 00216 // add the POs 00217 Aig_ManForEachPo( p->pManAig, pObj, i ) 00218 Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj,0) ); 00219 // postprocess 00220 Aig_ManCleanMarkB( p->pManFraig ); 00221 }
Function*************************************************************
Synopsis [Prepares the new manager to begin fraiging.]
Description []
SideEffects []
SeeAlso []
Definition at line 172 of file fraMan.c.
00173 { 00174 Aig_Man_t * pManFraig; 00175 Aig_Obj_t * pObj; 00176 int i; 00177 assert( p->pManFraig == NULL ); 00178 // start the fraig package 00179 pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) ); 00180 pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName ); 00181 pManFraig->nRegs = p->pManAig->nRegs; 00182 pManFraig->nAsserts = p->pManAig->nAsserts; 00183 // set the pointers to the available fraig nodes 00184 Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), 0, Aig_ManConst1(pManFraig) ); 00185 Aig_ManForEachPi( p->pManAig, pObj, i ) 00186 Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) ); 00187 // set the pointers to the manager 00188 Aig_ManForEachObj( pManFraig, pObj, i ) 00189 pObj->pData = p; 00190 // allocate memory for mapping FRAIG nodes into SAT numbers and fanins 00191 p->nMemAlloc = p->nSizeAlloc; 00192 p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nMemAlloc ); 00193 memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc ); 00194 p->pMemSatNums = ALLOC( int, p->nMemAlloc ); 00195 memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc ); 00196 // make sure the satisfying assignment is node assigned 00197 assert( pManFraig->pData == NULL ); 00198 return pManFraig; 00199 }
| void Fra_ManPrint | ( | Fra_Man_t * | p | ) |
Function*************************************************************
Synopsis [Prints stats for the fraiging manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 272 of file fraMan.c.
00273 { 00274 double nMemory = 1.0*Aig_ManObjNumMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20); 00275 printf( "SimWord = %d. Round = %d. Mem = %0.2f Mb. LitBeg = %d. LitEnd = %d. (%6.2f %%).\n", 00276 p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/(p->nLitsBeg?p->nLitsBeg:1) ); 00277 printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. C-lim = %d. ImpRatio = %6.2f %%\n", 00278 p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->pPars->nBTLimitNode, Fra_ImpComputeStateSpaceRatio(p) ); 00279 printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 00280 p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), 00281 p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) ); 00282 if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat ); 00283 PRT( "AIG simulation ", p->pSml->timeSim ); 00284 PRT( "AIG traversal ", p->timeTrav ); 00285 if ( p->timeRwr ) 00286 { 00287 PRT( "AIG rewriting ", p->timeRwr ); 00288 } 00289 PRT( "SAT solving ", p->timeSat ); 00290 PRT( " Unsat ", p->timeSatUnsat ); 00291 PRT( " Sat ", p->timeSatSat ); 00292 PRT( " Fail ", p->timeSatFail ); 00293 PRT( "Class refining ", p->timeRef ); 00294 PRT( "TOTAL RUNTIME ", p->timeTotal ); 00295 if ( p->time1 ) { PRT( "time1 ", p->time1 ); } 00296 if ( p->nSpeculs ) 00297 printf( "Speculations = %d.\n", p->nSpeculs ); 00298 }
Function*************************************************************
Synopsis [Starts the fraiging manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 101 of file fraMan.c.
00102 { 00103 Fra_Man_t * p; 00104 Aig_Obj_t * pObj; 00105 int i; 00106 // allocate the fraiging manager 00107 p = ALLOC( Fra_Man_t, 1 ); 00108 memset( p, 0, sizeof(Fra_Man_t) ); 00109 p->pPars = pPars; 00110 p->pManAig = pManAig; 00111 p->nSizeAlloc = Aig_ManObjNumMax( pManAig ); 00112 p->nFramesAll = pPars->nFramesK + 1; 00113 // allocate storage for sim pattern 00114 p->nPatWords = Aig_BitWordNum( (Aig_ManPiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) ); 00115 p->pPatWords = ALLOC( unsigned, p->nPatWords ); 00116 p->vPiVars = Vec_PtrAlloc( 100 ); 00117 // equivalence classes 00118 p->pCla = Fra_ClassesStart( pManAig ); 00119 // allocate other members 00120 p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll ); 00121 memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); 00122 // set random number generator 00123 srand( 0xABCABC ); 00124 // set the pointer to the manager 00125 Aig_ManForEachObj( p->pManAig, pObj, i ) 00126 pObj->pData = p; 00127 return p; 00128 }
| void Fra_ManStop | ( | Fra_Man_t * | p | ) |
Function*************************************************************
Synopsis [Stops the fraiging manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 235 of file fraMan.c.
00236 { 00237 if ( p->pPars->fVerbose ) 00238 Fra_ManPrint( p ); 00239 // save mapping from original nodes into FRAIG nodes 00240 if ( p->pManAig ) 00241 { 00242 if ( p->pManAig->pObjCopies ) 00243 free( p->pManAig->pObjCopies ); 00244 p->pManAig->pObjCopies = p->pMemFraig; 00245 p->pMemFraig = NULL; 00246 } 00247 Fra_ManClean( p, 0 ); 00248 if ( p->vTimeouts ) Vec_PtrFree( p->vTimeouts ); 00249 if ( p->vPiVars ) Vec_PtrFree( p->vPiVars ); 00250 if ( p->pSat ) sat_solver_delete( p->pSat ); 00251 if ( p->pCla ) Fra_ClassesStop( p->pCla ); 00252 if ( p->pSml ) Fra_SmlStop( p->pSml ); 00253 if ( p->vCex ) Vec_IntFree( p->vCex ); 00254 FREE( p->pMemFraig ); 00255 FREE( p->pMemFanins ); 00256 FREE( p->pMemSatNums ); 00257 FREE( p->pPatWords ); 00258 free( p ); 00259 }
Function*************************************************************
Synopsis [Runs equivalence test for one node.]
Description [Returns the fraiged node.]
SideEffects []
SeeAlso []
Definition at line 312 of file fraSat.c.
00313 { 00314 int pLits[2], RetValue1, RetValue, clk; 00315 00316 // make sure the nodes are not complemented 00317 assert( !Aig_IsComplement(pNew) ); 00318 assert( pNew != p->pManFraig->pConst1 ); 00319 p->nSatCalls++; 00320 00321 // make sure the solver is allocated and has enough variables 00322 if ( p->pSat == NULL ) 00323 { 00324 p->pSat = sat_solver_new(); 00325 p->nSatVars = 1; 00326 sat_solver_setnvars( p->pSat, 1000 ); 00327 // var 0 is reserved for const1 node - add the clause 00328 pLits[0] = toLit( 0 ); 00329 sat_solver_addclause( p->pSat, pLits, pLits + 1 ); 00330 } 00331 00332 // if the nodes do not have SAT variables, allocate them 00333 Fra_CnfNodeAddToSolver( p, NULL, pNew ); 00334 00335 // prepare variable activity 00336 if ( p->pPars->fConeBias ) 00337 Fra_SetActivityFactors( p, NULL, pNew ); 00338 00339 // solve under assumptions 00340 clk = clock(); 00341 pLits[0] = toLitCond( Fra_ObjSatNum(pNew), pNew->fPhase ); 00342 RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1, 00343 (sint64)p->pPars->nBTLimitMiter, (sint64)0, 00344 p->nBTLimitGlobal, p->nInsLimitGlobal ); 00345 p->timeSat += clock() - clk; 00346 if ( RetValue1 == l_False ) 00347 { 00348 p->timeSatUnsat += clock() - clk; 00349 pLits[0] = lit_neg( pLits[0] ); 00350 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 ); 00351 assert( RetValue ); 00352 // continue solving the other implication 00353 p->nSatCallsUnsat++; 00354 } 00355 else if ( RetValue1 == l_True ) 00356 { 00357 p->timeSatSat += clock() - clk; 00358 if ( p->pPatWords ) 00359 Fra_SmlSavePattern( p ); 00360 p->nSatCallsSat++; 00361 return 0; 00362 } 00363 else // if ( RetValue1 == l_Undef ) 00364 { 00365 p->timeSatFail += clock() - clk; 00366 // mark the node as the failed node 00367 pNew->fMarkB = 1; 00368 p->nSatFailsReal++; 00369 return -1; 00370 } 00371 00372 // return SAT proof 00373 p->nSatProof++; 00374 return 1; 00375 }
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Runs equivalence test for the two nodes.]
Description []
SideEffects []
SeeAlso []
Definition at line 45 of file fraSat.c.
00046 { 00047 int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock(); 00048 int status; 00049 00050 // make sure the nodes are not complemented 00051 assert( !Aig_IsComplement(pNew) ); 00052 assert( !Aig_IsComplement(pOld) ); 00053 assert( pNew != pOld ); 00054 00055 // if at least one of the nodes is a failed node, perform adjustments: 00056 // if the backtrack limit is small, simply skip this node 00057 // if the backtrack limit is > 10, take the quare root of the limit 00058 nBTLimit = p->pPars->nBTLimitNode; 00059 if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) ) 00060 { 00061 p->nSatFails++; 00062 // fail immediately 00063 // return -1; 00064 if ( nBTLimit <= 10 ) 00065 return -1; 00066 nBTLimit = (int)pow(nBTLimit, 0.7); 00067 } 00068 00069 p->nSatCalls++; 00070 p->nSatCallsRecent++; 00071 00072 // make sure the solver is allocated and has enough variables 00073 if ( p->pSat == NULL ) 00074 { 00075 p->pSat = sat_solver_new(); 00076 p->nSatVars = 1; 00077 sat_solver_setnvars( p->pSat, 1000 ); 00078 // var 0 is reserved for const1 node - add the clause 00079 pLits[0] = toLit( 0 ); 00080 sat_solver_addclause( p->pSat, pLits, pLits + 1 ); 00081 } 00082 00083 // if the nodes do not have SAT variables, allocate them 00084 Fra_CnfNodeAddToSolver( p, pOld, pNew ); 00085 00086 if ( p->pSat->qtail != p->pSat->qhead ) 00087 { 00088 status = sat_solver_simplify(p->pSat); 00089 assert( status != 0 ); 00090 assert( p->pSat->qtail == p->pSat->qhead ); 00091 } 00092 00093 // prepare variable activity 00094 if ( p->pPars->fConeBias ) 00095 Fra_SetActivityFactors( p, pOld, pNew ); 00096 00097 // solve under assumptions 00098 // A = 1; B = 0 OR A = 1; B = 1 00099 clk = clock(); 00100 pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 ); 00101 pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase ); 00102 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); 00103 RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 00104 (sint64)nBTLimit, (sint64)0, 00105 p->nBTLimitGlobal, p->nInsLimitGlobal ); 00106 p->timeSat += clock() - clk; 00107 if ( RetValue1 == l_False ) 00108 { 00109 p->timeSatUnsat += clock() - clk; 00110 pLits[0] = lit_neg( pLits[0] ); 00111 pLits[1] = lit_neg( pLits[1] ); 00112 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); 00113 assert( RetValue ); 00114 // continue solving the other implication 00115 p->nSatCallsUnsat++; 00116 } 00117 else if ( RetValue1 == l_True ) 00118 { 00119 p->timeSatSat += clock() - clk; 00120 Fra_SmlSavePattern( p ); 00121 p->nSatCallsSat++; 00122 return 0; 00123 } 00124 else // if ( RetValue1 == l_Undef ) 00125 { 00126 p->timeSatFail += clock() - clk; 00127 // mark the node as the failed node 00128 if ( pOld != p->pManFraig->pConst1 ) 00129 pOld->fMarkB = 1; 00130 pNew->fMarkB = 1; 00131 p->nSatFailsReal++; 00132 return -1; 00133 } 00134 00135 // if the old node was constant 0, we already know the answer 00136 if ( pOld == p->pManFraig->pConst1 ) 00137 { 00138 p->nSatProof++; 00139 return 1; 00140 } 00141 00142 // solve under assumptions 00143 // A = 0; B = 1 OR A = 0; B = 0 00144 clk = clock(); 00145 pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 1 ); 00146 pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase ); 00147 RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 00148 (sint64)nBTLimit, (sint64)0, 00149 p->nBTLimitGlobal, p->nInsLimitGlobal ); 00150 p->timeSat += clock() - clk; 00151 if ( RetValue1 == l_False ) 00152 { 00153 p->timeSatUnsat += clock() - clk; 00154 pLits[0] = lit_neg( pLits[0] ); 00155 pLits[1] = lit_neg( pLits[1] ); 00156 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); 00157 assert( RetValue ); 00158 p->nSatCallsUnsat++; 00159 } 00160 else if ( RetValue1 == l_True ) 00161 { 00162 p->timeSatSat += clock() - clk; 00163 Fra_SmlSavePattern( p ); 00164 p->nSatCallsSat++; 00165 return 0; 00166 } 00167 else // if ( RetValue1 == l_Undef ) 00168 { 00169 p->timeSatFail += clock() - clk; 00170 // mark the node as the failed node 00171 pOld->fMarkB = 1; 00172 pNew->fMarkB = 1; 00173 p->nSatFailsReal++; 00174 return -1; 00175 } 00176 /* 00177 // check BDD proof 00178 { 00179 int RetVal; 00180 PRT( "Sat", clock() - clk2 ); 00181 clk2 = clock(); 00182 RetVal = Fra_NodesAreEquivBdd( pOld, pNew ); 00183 // printf( "%d ", RetVal ); 00184 assert( RetVal ); 00185 PRT( "Bdd", clock() - clk2 ); 00186 printf( "\n" ); 00187 } 00188 */ 00189 // return SAT proof 00190 p->nSatProof++; 00191 return 1; 00192 }
Function*************************************************************
Synopsis [Runs the result of test for pObj => pNew.]
Description []
SideEffects []
SeeAlso []
Definition at line 205 of file fraSat.c.
00206 { 00207 int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock(); 00208 int status; 00209 00210 // make sure the nodes are not complemented 00211 assert( !Aig_IsComplement(pNew) ); 00212 assert( !Aig_IsComplement(pOld) ); 00213 assert( pNew != pOld ); 00214 00215 // if at least one of the nodes is a failed node, perform adjustments: 00216 // if the backtrack limit is small, simply skip this node 00217 // if the backtrack limit is > 10, take the quare root of the limit 00218 nBTLimit = p->pPars->nBTLimitNode; 00219 /* 00220 if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) ) 00221 { 00222 p->nSatFails++; 00223 // fail immediately 00224 // return -1; 00225 if ( nBTLimit <= 10 ) 00226 return -1; 00227 nBTLimit = (int)pow(nBTLimit, 0.7); 00228 } 00229 */ 00230 p->nSatCalls++; 00231 00232 // make sure the solver is allocated and has enough variables 00233 if ( p->pSat == NULL ) 00234 { 00235 p->pSat = sat_solver_new(); 00236 p->nSatVars = 1; 00237 sat_solver_setnvars( p->pSat, 1000 ); 00238 // var 0 is reserved for const1 node - add the clause 00239 pLits[0] = toLit( 0 ); 00240 sat_solver_addclause( p->pSat, pLits, pLits + 1 ); 00241 } 00242 00243 // if the nodes do not have SAT variables, allocate them 00244 Fra_CnfNodeAddToSolver( p, pOld, pNew ); 00245 00246 if ( p->pSat->qtail != p->pSat->qhead ) 00247 { 00248 status = sat_solver_simplify(p->pSat); 00249 assert( status != 0 ); 00250 assert( p->pSat->qtail == p->pSat->qhead ); 00251 } 00252 00253 // prepare variable activity 00254 if ( p->pPars->fConeBias ) 00255 Fra_SetActivityFactors( p, pOld, pNew ); 00256 00257 // solve under assumptions 00258 // A = 1; B = 0 OR A = 1; B = 1 00259 clk = clock(); 00260 // pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 ); 00261 // pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase ); 00262 pLits[0] = toLitCond( Fra_ObjSatNum(pOld), fComplL ); 00263 pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR ); 00264 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); 00265 RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 00266 (sint64)nBTLimit, (sint64)0, 00267 p->nBTLimitGlobal, p->nInsLimitGlobal ); 00268 p->timeSat += clock() - clk; 00269 if ( RetValue1 == l_False ) 00270 { 00271 p->timeSatUnsat += clock() - clk; 00272 pLits[0] = lit_neg( pLits[0] ); 00273 pLits[1] = lit_neg( pLits[1] ); 00274 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); 00275 assert( RetValue ); 00276 // continue solving the other implication 00277 p->nSatCallsUnsat++; 00278 } 00279 else if ( RetValue1 == l_True ) 00280 { 00281 p->timeSatSat += clock() - clk; 00282 Fra_SmlSavePattern( p ); 00283 p->nSatCallsSat++; 00284 return 0; 00285 } 00286 else // if ( RetValue1 == l_Undef ) 00287 { 00288 p->timeSatFail += clock() - clk; 00289 // mark the node as the failed node 00290 if ( pOld != p->pManFraig->pConst1 ) 00291 pOld->fMarkB = 1; 00292 pNew->fMarkB = 1; 00293 p->nSatFailsReal++; 00294 return -1; 00295 } 00296 // return SAT proof 00297 p->nSatProof++; 00298 return 1; 00299 }
Definition at line 205 of file fra.h.
00205 { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; }
Definition at line 206 of file fra.h.
00206 { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; }
| static unsigned Fra_ObjRandomSim | ( | ) | [inline, static] |
| static int Fra_ObjSatNum | ( | Aig_Obj_t * | pObj | ) | [inline, static] |
| static void Fra_ObjSetSatNum | ( | Aig_Obj_t * | pObj, | |
| int | Num | |||
| ) | [inline, static] |
| static unsigned* Fra_ObjSim | ( | Fra_Sml_t * | p, | |
| int | Id | |||
| ) | [inline, static] |
MACRO DEFINITIONS ///
Definition at line 190 of file fra.h.
00190 { return p->pData + p->nWordsTotal * Id; }
| void Fra_ParamsDefault | ( | Fra_Par_t * | pPars | ) |
CFile****************************************************************
FileName [fraMan.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis [Starts the FRAIG manager.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [
- Id
- fraMan.c,v 1.00 2007/06/30 00:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Sets the default solving parameters.]
Description []
SideEffects []
SeeAlso []
Definition at line 42 of file fraMan.c.
00043 { 00044 memset( pPars, 0, sizeof(Fra_Par_t) ); 00045 pPars->nSimWords = 32; // the number of words in the simulation info 00046 pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached 00047 pPars->fPatScores = 0; // enables simulation pattern scoring 00048 pPars->MaxScore = 25; // max score after which resimulation is used 00049 pPars->fDoSparse = 1; // skips sparse functions 00050 // pPars->dActConeRatio = 0.05; // the ratio of cone to be bumped 00051 // pPars->dActConeBumpMax = 5.0; // the largest bump of activity 00052 pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped 00053 pPars->dActConeBumpMax = 10.0; // the largest bump of activity 00054 pPars->nBTLimitNode = 100; // conflict limit at a node 00055 pPars->nBTLimitMiter = 500000; // conflict limit at an output 00056 pPars->nFramesK = 0; // the number of timeframes to unroll 00057 pPars->fConeBias = 1; 00058 pPars->fRewrite = 0; 00059 }
| void Fra_ParamsDefaultSeq | ( | Fra_Par_t * | pPars | ) |
Function*************************************************************
Synopsis [Sets the default solving parameters.]
Description []
SideEffects []
SeeAlso []
Definition at line 72 of file fraMan.c.
00073 { 00074 memset( pPars, 0, sizeof(Fra_Par_t) ); 00075 pPars->nSimWords = 1; // the number of words in the simulation info 00076 pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached 00077 pPars->fPatScores = 0; // enables simulation pattern scoring 00078 pPars->MaxScore = 25; // max score after which resimulation is used 00079 pPars->fDoSparse = 1; // skips sparse functions 00080 pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped 00081 pPars->dActConeBumpMax = 10.0; // the largest bump of activity 00082 pPars->nBTLimitNode = 10000000; // conflict limit at a node 00083 pPars->nBTLimitMiter = 500000; // conflict limit at an output 00084 pPars->nFramesK = 1; // the number of timeframes to unroll 00085 pPars->fConeBias = 0; 00086 pPars->fRewrite = 0; 00087 pPars->fLatchCorr = 0; 00088 }
| int Fra_SmlCheckOutput | ( | Fra_Man_t * | p | ) |
Function*************************************************************
Synopsis [Returns 1 if the one of the output is already non-constant 0.]
Description []
SideEffects []
SeeAlso []
Definition at line 297 of file fraSim.c.
00298 { 00299 Aig_Obj_t * pObj; 00300 int i; 00301 // make sure the reference simulation pattern does not detect the bug 00302 pObj = Aig_ManPo( p->pManAig, 0 ); 00303 assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 00304 Aig_ManForEachPo( p->pManAig, pObj, i ) 00305 { 00306 if ( !Fra_SmlNodeIsConst( Aig_ObjFanin0(pObj) ) ) 00307 { 00308 // create the counter-example from this pattern 00309 Fra_SmlCheckOutputSavePattern( p, Aig_ObjFanin0(pObj) ); 00310 return 1; 00311 } 00312 } 00313 return 0; 00314 }
| int Fra_SmlNodeHash | ( | Aig_Obj_t * | pObj, | |
| int | nTableSize | |||
| ) |
CFile****************************************************************
FileName [fraSim.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [
- Id
- fraSim.c,v 1.00 2007/06/30 00:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Computes hash value of the node using its simulation info.]
Description []
SideEffects []
SeeAlso []
Definition at line 42 of file fraSim.c.
00043 { 00044 Fra_Man_t * p = pObj->pData; 00045 static int s_FPrimes[128] = { 00046 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 00047 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 00048 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 00049 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 00050 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 00051 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 00052 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 00053 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 00054 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 00055 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 00056 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 00057 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 00058 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147 00059 }; 00060 unsigned * pSims; 00061 unsigned uHash; 00062 int i; 00063 // assert( p->pSml->nWordsTotal <= 128 ); 00064 uHash = 0; 00065 pSims = Fra_ObjSim(p->pSml, pObj->Id); 00066 for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ ) 00067 uHash ^= pSims[i] * s_FPrimes[i & 0x7F]; 00068 return uHash % nTableSize; 00069 }
| int Fra_SmlNodeIsConst | ( | Aig_Obj_t * | pObj | ) |
Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
Definition at line 82 of file fraSim.c.
00083 { 00084 Fra_Man_t * p = pObj->pData; 00085 unsigned * pSims; 00086 int i; 00087 pSims = Fra_ObjSim(p->pSml, pObj->Id); 00088 for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ ) 00089 if ( pSims[i] ) 00090 return 0; 00091 return 1; 00092 }
| int Fra_SmlNodeNotEquWeight | ( | Fra_Sml_t * | p, | |
| int | Left, | |||
| int | Right | |||
| ) |
Function*************************************************************
Synopsis [Counts the number of 1s in the XOR of simulation data.]
Description []
SideEffects []
SeeAlso []
Definition at line 129 of file fraSim.c.
00130 { 00131 unsigned * pSimL, * pSimR; 00132 int k, Counter = 0; 00133 pSimL = Fra_ObjSim( p, Left ); 00134 pSimR = Fra_ObjSim( p, Right ); 00135 for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) 00136 Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] ); 00137 return Counter; 00138 }
Function*************************************************************
Synopsis [Returns 1 if simulation infos are equal.]
Description []
SideEffects []
SeeAlso []
Definition at line 105 of file fraSim.c.
00106 { 00107 Fra_Man_t * p = pObj0->pData; 00108 unsigned * pSims0, * pSims1; 00109 int i; 00110 pSims0 = Fra_ObjSim(p->pSml, pObj0->Id); 00111 pSims1 = Fra_ObjSim(p->pSml, pObj1->Id); 00112 for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ ) 00113 if ( pSims0[i] != pSims1[i] ) 00114 return 0; 00115 return 1; 00116 }
| void Fra_SmlResimulate | ( | Fra_Man_t * | p | ) |
Function*************************************************************
Synopsis [Resimulates fraiging manager after finding a counter-example.]
Description []
SideEffects []
SeeAlso []
Definition at line 643 of file fraSim.c.
00644 { 00645 int nChanges, clk; 00646 Fra_SmlAssignDist1( p->pSml, p->pPatWords ); 00647 Fra_SmlSimulateOne( p->pSml ); 00648 // if ( p->pPars->fPatScores ) 00649 // Fra_CleanPatScores( p ); 00650 if ( p->pPars->fProve && Fra_SmlCheckOutput(p) ) 00651 return; 00652 clk = clock(); 00653 nChanges = Fra_ClassesRefine( p->pCla ); 00654 nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL ); 00655 if ( p->pCla->vImps ) 00656 nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps ); 00657 p->timeRef += clock() - clk; 00658 if ( !p->pPars->nFramesK && nChanges < 1 ) 00659 printf( "Error: A counter-example did not refine classes!\n" ); 00660 // assert( nChanges >= 1 ); 00661 //printf( "Refined classes = %5d. Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges ); 00662 }
| void Fra_SmlSavePattern | ( | Fra_Man_t * | p | ) |
Function*************************************************************
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
SideEffects []
SeeAlso []
Definition at line 216 of file fraSim.c.
00217 { 00218 Aig_Obj_t * pObj; 00219 int i; 00220 memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); 00221 Aig_ManForEachPi( p->pManFraig, pObj, i ) 00222 if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True ) 00223 Aig_InfoSetBit( p->pPatWords, i ); 00224 00225 if ( p->vCex ) 00226 { 00227 Vec_IntClear( p->vCex ); 00228 for ( i = 0; i < Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ ) 00229 Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) ); 00230 for ( i = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManPiNum(p->pManFraig); i++ ) 00231 Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) ); 00232 } 00233 00234 /* 00235 printf( "Pattern: " ); 00236 Aig_ManForEachPi( p->pManFraig, pObj, i ) 00237 printf( "%d", Aig_InfoHasBit( p->pPatWords, i ) ); 00238 printf( "\n" ); 00239 */ 00240 }
| void Fra_SmlSimulate | ( | Fra_Man_t * | p, | |
| int | fInit | |||
| ) |
Function*************************************************************
Synopsis [Performs simulation of the manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 675 of file fraSim.c.
00676 { 00677 int fVerbose = 0; 00678 int nChanges, nClasses, clk; 00679 assert( !fInit || Aig_ManRegNum(p->pManAig) ); 00680 // start the classes 00681 Fra_SmlInitialize( p->pSml, fInit ); 00682 Fra_SmlSimulateOne( p->pSml ); 00683 Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr ); 00684 // Fra_ClassesPrint( p->pCla, 0 ); 00685 if ( fVerbose ) 00686 printf( "Starting classes = %5d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) ); 00687 00688 //return; 00689 00690 // refine classes by walking 0/1 patterns 00691 Fra_SmlSavePattern0( p, fInit ); 00692 Fra_SmlAssignDist1( p->pSml, p->pPatWords ); 00693 Fra_SmlSimulateOne( p->pSml ); 00694 if ( p->pPars->fProve && Fra_SmlCheckOutput(p) ) 00695 return; 00696 clk = clock(); 00697 nChanges = Fra_ClassesRefine( p->pCla ); 00698 nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL ); 00699 p->timeRef += clock() - clk; 00700 if ( fVerbose ) 00701 printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) ); 00702 Fra_SmlSavePattern1( p, fInit ); 00703 Fra_SmlAssignDist1( p->pSml, p->pPatWords ); 00704 Fra_SmlSimulateOne( p->pSml ); 00705 if ( p->pPars->fProve && Fra_SmlCheckOutput(p) ) 00706 return; 00707 clk = clock(); 00708 nChanges = Fra_ClassesRefine( p->pCla ); 00709 nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL ); 00710 p->timeRef += clock() - clk; 00711 00712 if ( fVerbose ) 00713 printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) ); 00714 // refine classes by random simulation 00715 do { 00716 Fra_SmlInitialize( p->pSml, fInit ); 00717 Fra_SmlSimulateOne( p->pSml ); 00718 nClasses = Vec_PtrSize(p->pCla->vClasses); 00719 if ( p->pPars->fProve && Fra_SmlCheckOutput(p) ) 00720 return; 00721 clk = clock(); 00722 nChanges = Fra_ClassesRefine( p->pCla ); 00723 nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL ); 00724 p->timeRef += clock() - clk; 00725 if ( fVerbose ) 00726 printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) ); 00727 } while ( (double)nChanges / nClasses > p->pPars->dSimSatur ); 00728 00729 // if ( p->pPars->fVerbose ) 00730 // printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", 00731 // Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) ); 00732 // Fra_ClassesPrint( p->pCla, 0 ); 00733 }
Function*************************************************************
Synopsis [Performs simulation of the uninitialized circuit.]
Description []
SideEffects []
SeeAlso []
Definition at line 789 of file fraSim.c.
00790 { 00791 Fra_Sml_t * p; 00792 p = Fra_SmlStart( pAig, 0, 1, nWords ); 00793 Fra_SmlInitialize( p, 0 ); 00794 Fra_SmlSimulateOne( p ); 00795 return p; 00796 }
Function*************************************************************
Synopsis [Performs simulation of the initialized circuit.]
Description []
SideEffects []
SeeAlso []
Definition at line 809 of file fraSim.c.
00810 { 00811 Fra_Sml_t * p; 00812 p = Fra_SmlStart( pAig, nPref, nFrames, nWords ); 00813 Fra_SmlInitialize( p, 1 ); 00814 Fra_SmlSimulateOne( p ); 00815 p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p ); 00816 return p; 00817 }
Function*************************************************************
Synopsis [Allocates simulation manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 747 of file fraSim.c.
00748 { 00749 Fra_Sml_t * p; 00750 p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame ); 00751 memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame ); 00752 p->pAig = pAig; 00753 p->nPref = nPref; 00754 p->nFrames = nPref + nFrames; 00755 p->nWordsFrame = nWordsFrame; 00756 p->nWordsTotal = (nPref + nFrames) * nWordsFrame; 00757 p->nWordsPref = nPref * nWordsFrame; 00758 return p; 00759 }
