summaryrefslogtreecommitdiffstats
path: root/src/aig/gia/giaTim.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia/giaTim.c')
-rw-r--r--src/aig/gia/giaTim.c64
1 files changed, 35 insertions, 29 deletions
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index 1d5a2f36..5640baa4 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -822,53 +822,59 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit, char * pFileSpec
printf( "Spec file is not given. Use standard flow.\n" );
return Status;
}
- if ( pGia->pManTime == NULL )
- {
- printf( "Design has no tim manager. Use standard flow.\n" );
- return Status;
- }
- if ( pGia->pAigExtra == NULL )
+ if ( Gia_ManBoxNum(pGia) && pGia->pAigExtra == NULL )
{
printf( "Design has no box logic. Use standard flow.\n" );
return Status;
}
// read original AIG
pSpec = Gia_AigerRead( pFileSpec ? pFileSpec : pGia->pSpec, 0, 0 );
- if ( pSpec->pManTime == NULL )
+ if ( Gia_ManBoxNum(pSpec) && pSpec->pAigExtra == NULL )
{
- printf( "Spec has no tim manager. Use standard flow.\n" );
+ Gia_ManStop( pSpec );
+ printf( "Spec has no box logic. Use standard flow.\n" );
return Status;
}
- if ( pSpec->pAigExtra == NULL )
+ // prepare miter
+ if ( pGia->pManTime == NULL && pSpec->pManTime == NULL )
{
- printf( "Spec has no box logic. Use standard flow.\n" );
- return Status;
+ pGia0 = Gia_ManDup( pSpec );
+ pGia1 = Gia_ManDup( pGia );
}
- // if timing managers have different number of black boxes,
- // it is possible that some of the boxes are swept away
- if ( Tim_ManBlackBoxNum( (Tim_Man_t *)pSpec->pManTime ) > 0 )
+ else
{
- // specification cannot have fewer boxes than implementation
- if ( Tim_ManBoxNum( (Tim_Man_t *)pSpec->pManTime ) < Tim_ManBoxNum( (Tim_Man_t *)pGia->pManTime ) )
+ // if timing managers have different number of black boxes,
+ // it is possible that some of the boxes are swept away
+ if ( pSpec->pManTime && Tim_ManBlackBoxNum((Tim_Man_t *)pSpec->pManTime) > 0 && Gia_ManBoxNum(pGia) > 0 )
{
- printf( "Spec has more boxes than the design. Cannot proceed.\n" );
- return Status;
- }
- // to align the boxes, find what boxes of pSpec are dropped in pGia
- if ( Tim_ManBoxNum( (Tim_Man_t *)pSpec->pManTime ) != Tim_ManBoxNum( (Tim_Man_t *)pGia->pManTime ) )
- {
- vBoxPres = Tim_ManAlignTwo( (Tim_Man_t *)pSpec->pManTime, (Tim_Man_t *)pGia->pManTime );
- if ( vBoxPres == NULL )
+ // specification cannot have fewer boxes than implementation
+ if ( Gia_ManBoxNum(pSpec) < Gia_ManBoxNum(pGia) )
{
- printf( "Boxes of spec and design cannot be aligned. Cannot proceed.\n" );
+ printf( "Spec has less boxes than the design. Cannot proceed.\n" );
return Status;
}
+ // to align the boxes, find what boxes of pSpec are dropped in pGia
+ if ( Gia_ManBoxNum(pSpec) > Gia_ManBoxNum(pGia) )
+ {
+ vBoxPres = Tim_ManAlignTwo( (Tim_Man_t *)pSpec->pManTime, (Tim_Man_t *)pGia->pManTime );
+ if ( vBoxPres == NULL )
+ {
+ printf( "Boxes of spec and design cannot be aligned. Cannot proceed.\n" );
+ return Status;
+ }
+ }
}
+ // collapse two designs
+ if ( Gia_ManBoxNum(pSpec) > 0 )
+ pGia0 = Gia_ManDupCollapse( pSpec, pSpec->pAigExtra, vBoxPres );
+ else
+ pGia0 = Gia_ManDup( pSpec );
+ if ( Gia_ManBoxNum(pGia) > 0 )
+ pGia1 = Gia_ManDupCollapse( pGia, pGia->pAigExtra, NULL );
+ else
+ pGia1 = Gia_ManDup( pGia );
+ Vec_IntFreeP( &vBoxPres );
}
- // collapse two designs
- pGia0 = Gia_ManDupCollapse( pSpec, pSpec->pAigExtra, vBoxPres );
- pGia1 = Gia_ManDupCollapse( pGia, pGia->pAigExtra, NULL );
- Vec_IntFreeP( &vBoxPres );
// compute the miter
pMiter = Gia_ManMiter( pGia0, pGia1, 0, 1, 0, 0, fVerbose );
if ( pMiter )