1 /**CFile****************************************************************
2
3 FileName [sswPart.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Inductive prover with constraints.]
8
9 Synopsis [Partitioned signal correspondence.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - September 1, 2008.]
16
17 Revision [$Id: sswPart.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "sswInt.h"
22 #include "aig/ioa/ioa.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34
35 /**Function*************************************************************
36
37 Synopsis [Performs partitioned sequential SAT sweeping.]
38
39 Description []
40
41 SideEffects []
42
43 SeeAlso []
44
45 ***********************************************************************/
Ssw_SignalCorrespondencePart(Aig_Man_t * pAig,Ssw_Pars_t * pPars)46 Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
47 {
48 int fPrintParts = 0;
49 char Buffer[100];
50 Aig_Man_t * pTemp, * pNew;
51 Vec_Ptr_t * vResult;
52 Vec_Int_t * vPart;
53 int * pMapBack;
54 int i, nCountPis, nCountRegs;
55 int nClasses, nPartSize, fVerbose;
56 abctime clk = Abc_Clock();
57 if ( pPars->fConstrs )
58 {
59 Abc_Print( 1, "Cannot use partitioned computation with constraints.\n" );
60 return NULL;
61 }
62 // save parameters
63 nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
64 fVerbose = pPars->fVerbose; pPars->fVerbose = 0;
65 // generate partitions
66 if ( pAig->vClockDoms )
67 {
68 // divide large clock domains into separate partitions
69 vResult = Vec_PtrAlloc( 100 );
70 Vec_PtrForEachEntry( Vec_Int_t *, (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
71 {
72 if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
73 Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
74 else
75 Vec_PtrPush( vResult, Vec_IntDup(vPart) );
76 }
77 }
78 else
79 vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
80 // vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 );
81 // vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
82 if ( fPrintParts )
83 {
84 // print partitions
85 Abc_Print( 1, "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
86 Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
87 {
88 // extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
89 sprintf( Buffer, "part%03d.aig", i );
90 pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
91 Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
92 Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
93 i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
94 Aig_ManStop( pTemp );
95 }
96 }
97
98 // perform SSW with partitions
99 Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
100 Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
101 {
102 pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
103 Aig_ManSetRegNum( pTemp, pTemp->nRegs );
104 // create the projection of 1-hot registers
105 if ( pAig->vOnehots )
106 pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose );
107 // run SSW
108 if (nCountPis>0) {
109 pNew = Ssw_SignalCorrespondence( pTemp, pPars );
110 nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
111 if ( fVerbose )
112 Abc_Print( 1, "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
113 i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
114 Aig_ManStop( pNew );
115 }
116 Aig_ManStop( pTemp );
117 ABC_FREE( pMapBack );
118 }
119 // remap the AIG
120 pNew = Aig_ManDupRepr( pAig, 0 );
121 Aig_ManSeqCleanup( pNew );
122 // Aig_ManPrintStats( pAig );
123 // Aig_ManPrintStats( pNew );
124 Vec_VecFree( (Vec_Vec_t *)vResult );
125 pPars->nPartSize = nPartSize;
126 pPars->fVerbose = fVerbose;
127 if ( fVerbose )
128 {
129 ABC_PRT( "Total time", Abc_Clock() - clk );
130 }
131 return pNew;
132 }
133
134
135 ////////////////////////////////////////////////////////////////////////
136 /// END OF FILE ///
137 ////////////////////////////////////////////////////////////////////////
138
139
140 ABC_NAMESPACE_IMPL_END
141