src/aig/fra/fraSec.c File Reference
#include "fra.h"#include "ioa.h"
Include dependency graph for fraSec.c:
Go to the source code of this file.
Functions | |
| int | Fra_FraigSec2 (Aig_Man_t *p, int nFramesFix, int fVerbose, int fVeryVerbose) |
| int | Fra_FraigSec (Aig_Man_t *p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose) |
Function Documentation
| 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 }
| int Fra_FraigSec2 | ( | Aig_Man_t * | p, | |
| int | nFramesFix, | |||
| int | fVerbose, | |||
| int | fVeryVerbose | |||
| ) |
CFile****************************************************************
FileName [fraSec.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis [Performs SEC based on seq sweeping.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [
- Id
- fraSec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 43 of file fraSec.c.
00044 { 00045 Aig_Man_t * pNew; 00046 int nFrames, RetValue, nIter, clk, clkTotal = clock(); 00047 int fLatchCorr = 0; 00048 if ( nFramesFix ) 00049 { 00050 nFrames = nFramesFix; 00051 // perform seq sweeping for one frame number 00052 pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter ); 00053 } 00054 else 00055 { 00056 // perform seq sweeping while increasing the number of frames 00057 for ( nFrames = 1; ; nFrames++ ) 00058 { 00059 clk = clock(); 00060 pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter ); 00061 RetValue = Fra_FraigMiterStatus( pNew ); 00062 if ( fVerbose ) 00063 { 00064 printf( "FRAMES %3d : Iters = %3d. ", nFrames, nIter ); 00065 if ( RetValue == 1 ) 00066 printf( "UNSAT " ); 00067 else 00068 printf( "UNDECIDED " ); 00069 PRT( "Time", clock() - clk ); 00070 } 00071 if ( RetValue != -1 ) 00072 break; 00073 Aig_ManStop( pNew ); 00074 } 00075 } 00076 00077 // get the miter status 00078 RetValue = Fra_FraigMiterStatus( pNew ); 00079 Aig_ManStop( pNew ); 00080 00081 // report the miter 00082 if ( RetValue == 1 ) 00083 printf( "Networks are equivalent after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter ); 00084 else if ( RetValue == 0 ) 00085 printf( "Networks are NOT EQUIVALENT. " ); 00086 else 00087 printf( "Networks are UNDECIDED after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter ); 00088 PRT( "Time", clock() - clkTotal ); 00089 return RetValue; 00090 }
