abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Macros | Functions
utilBridge.c File Reference
#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include <assert.h>
#include "aig/gia/gia.h"

Go to the source code of this file.

Macros

#define BRIDGE_TEXT_MESSAGE   999996
 DECLARATIONS ///. More...
 
#define BRIDGE_ABORT   5
 
#define BRIDGE_PROGRESS   3
 
#define BRIDGE_RESULTS   101
 
#define BRIDGE_BAD_ABS   105
 
#define BRIDGE_VALUE_X   0
 
#define BRIDGE_VALUE_0   2
 
#define BRIDGE_VALUE_1   3
 

Functions

Vec_Str_t * Gia_ManToBridgeVec (Gia_Man_t *p)
 FUNCTION DEFINITIONS ///. More...
 
void Gia_CreateHeader (FILE *pFile, int Type, int Size, unsigned char *pBuffer)
 
int Gia_ManToBridgeText (FILE *pFile, int Size, unsigned char *pBuffer)
 
int Gia_ManToBridgeAbort (FILE *pFile, int Size, unsigned char *pBuffer)
 
int Gia_ManToBridgeProgress (FILE *pFile, int Size, unsigned char *pBuffer)
 
int Gia_ManToBridgeAbsNetlist (FILE *pFile, void *p, int pkg_type)
 
int Gia_ManToBridgeBadAbs (FILE *pFile)
 
static int aigerNumSize (unsigned x)
 
void Gia_ManFromBridgeHolds (FILE *pFile, int iPoProved)
 
void Gia_ManFromBridgeUnknown (FILE *pFile, int iPoUnknown)
 
void Gia_ManFromBridgeCex (FILE *pFile, Abc_Cex_t *pCex)
 
int Gia_ManToBridgeResult (FILE *pFile, int Result, Abc_Cex_t *pCex, int iPoProved)
 DECLARATIONS ///. More...
 
Gia_Man_t * Gia_ManFromBridgeReadBody (int Size, unsigned char *pBuffer, Vec_Int_t **pvInits)
 
int Gia_ManFromBridgeReadPackage (FILE *pFile, int *pType, int *pSize, unsigned char **ppBuffer)
 
Gia_Man_t * Gia_ManFromBridge (FILE *pFile, Vec_Int_t **pvInit)
 
void Gia_ManToBridgeAbsNetlistTest (char *pFileName, Gia_Man_t *p, int msg_type)
 
void Gia_ManFromBridgeTest (char *pFileName)
 

Macro Definition Documentation

#define BRIDGE_ABORT   5

Definition at line 39 of file utilBridge.c.

#define BRIDGE_BAD_ABS   105

Definition at line 42 of file utilBridge.c.

#define BRIDGE_PROGRESS   3

Definition at line 40 of file utilBridge.c.

#define BRIDGE_RESULTS   101

Definition at line 41 of file utilBridge.c.

#define BRIDGE_TEXT_MESSAGE   999996

DECLARATIONS ///.

CFile****************************************************************

FileName [utilBridge.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName []

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
utilBridge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 37 of file utilBridge.c.

#define BRIDGE_VALUE_0   2

Definition at line 47 of file utilBridge.c.

#define BRIDGE_VALUE_1   3

Definition at line 48 of file utilBridge.c.

#define BRIDGE_VALUE_X   0

Definition at line 46 of file utilBridge.c.

Function Documentation

static int aigerNumSize ( unsigned  x)
static

Definition at line 206 of file utilBridge.c.

207 {
208  int sz = 1;
209  while (x & ~0x7f)
210  {
211  sz++;
212  x >>= 7;
213  }
214  return sz;
215 }
void Gia_CreateHeader ( FILE *  pFile,
int  Type,
int  Size,
unsigned char *  pBuffer 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 127 of file utilBridge.c.

128 {
129  fprintf( pFile, "%.6d", Type );
130  fprintf( pFile, " " );
131  fprintf( pFile, "%.16d", Size );
132  fprintf( pFile, " " );
133 #if !defined(LIN) && !defined(LIN64)
134  {
135  int RetValue;
136  RetValue = fwrite( pBuffer, Size, 1, pFile );
137  assert( RetValue == 1 || Size == 0);
138  fflush( pFile );
139  }
140 #else
141  fflush(pFile);
142  int fd = fileno(pFile);
143 
144  ssize_t bytes_written = 0;
145  while (bytes_written < Size){
146  ssize_t n = write(fd, &pBuffer[bytes_written], Size - bytes_written);
147  if (n < 0){
148  fprintf(stderr, "BridgeMode: failed to send package; aborting\n"); fflush(stderr);
149  _exit(255);
150  }
151  bytes_written += n;
152  }
153 #endif
154 }
assert
#define assert(ex)
Definition: util_old.h:213
Gia_Man_t* Gia_ManFromBridge ( FILE *  pFile,
Vec_Int_t **  pvInit 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 457 of file utilBridge.c.

458 {
459  unsigned char * pBuffer;
460  int Type, Size, RetValue;
461  Gia_Man_t * p = NULL;
462 
463  RetValue = Gia_ManFromBridgeReadPackage( pFile, &Type, &Size, &pBuffer );
464  ABC_FREE( pBuffer );
465  if ( !RetValue )
466  return NULL;
467 
468  RetValue = Gia_ManFromBridgeReadPackage( pFile, &Type, &Size, &pBuffer );
469  if ( !RetValue )
470  return NULL;
471 
472  p = Gia_ManFromBridgeReadBody( Size, pBuffer, pvInit );
473  ABC_FREE( pBuffer );
474  if ( p == NULL )
475  return NULL;
476 
477  RetValue = Gia_ManFromBridgeReadPackage( pFile, &Type, &Size, &pBuffer );
478  ABC_FREE( pBuffer );
479  if ( !RetValue )
480  return NULL;
481 
482  return p;
483 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_ManFromBridgeReadBody
Gia_Man_t * Gia_ManFromBridgeReadBody(int Size, unsigned char *pBuffer, Vec_Int_t **pvInits)
Definition: utilBridge.c:308
Gia_ManFromBridgeReadPackage
int Gia_ManFromBridgeReadPackage(FILE *pFile, int *pType, int *pSize, unsigned char **ppBuffer)
Definition: utilBridge.c:419
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
void Gia_ManFromBridgeCex ( FILE *  pFile,
Abc_Cex_t *  pCex 
)

Definition at line 254 of file utilBridge.c.

255 {
256  int i, f, iBit;//, RetValue;
257  Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
258  Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // false
259  Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
260  Gia_AigerWriteUnsigned( vStr, pCex->iPo ); // number of the property (Armin's encoding)
261  Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
262  Gia_AigerWriteUnsigned( vStr, pCex->iFrame ); // depth
263 
264  Gia_AigerWriteUnsigned( vStr, 1 ); // concrete
265  Gia_AigerWriteUnsigned( vStr, pCex->iFrame + 1 ); // number of frames (1 more than depth)
266  iBit = pCex->nRegs;
267  for ( f = 0; f <= pCex->iFrame; f++ )
268  {
269  Gia_AigerWriteUnsigned( vStr, pCex->nPis ); // num of inputs
270  for ( i = 0; i < pCex->nPis; i++, iBit++ )
271  Vec_StrPush( vStr, (char)(Abc_InfoHasBit(pCex->pData, iBit) ? BRIDGE_VALUE_1:BRIDGE_VALUE_0) ); // value
272  }
273  assert( iBit == pCex->nBits );
274  Vec_StrPush( vStr, (char)1 ); // the number of frames (for a concrete counter-example)
275  Gia_AigerWriteUnsigned( vStr, pCex->nRegs ); // num of flops
276  for ( i = 0; i < pCex->nRegs; i++ )
277  Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // always zero!!!
278 // RetValue = fwrite( Vec_StrArray(vStr), Vec_StrSize(vStr), 1, pFile );
279  Gia_CreateHeader(pFile, 101/*type=Result*/, Vec_StrSize(vStr), (unsigned char*)Vec_StrArray(vStr));
280 
281  Vec_StrFree( vStr );
282  fflush(pFile);
283 }
BRIDGE_VALUE_1
#define BRIDGE_VALUE_1
Definition: utilBridge.c:48
Gia_CreateHeader
void Gia_CreateHeader(FILE *pFile, int Type, int Size, unsigned char *pBuffer)
Definition: utilBridge.c:127
Vec_StrArray
static char * Vec_StrArray(Vec_Str_t *p)
Definition: vecStr.h:272
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Vec_StrAlloc
static Vec_Str_t * Vec_StrAlloc(int nCap)
Definition: bblif.c:495
Gia_AigerWriteUnsigned
static void Gia_AigerWriteUnsigned(Vec_Str_t *vStr, unsigned x)
Definition: gia.h:848
Vec_StrPush
static void Vec_StrPush(Vec_Str_t *p, char Entry)
Definition: vecStr.h:535
Vec_StrFree
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
BRIDGE_VALUE_0
#define BRIDGE_VALUE_0
Definition: utilBridge.c:47
Vec_StrSize
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
Vec_Str_t_
Definition: bblif.c:47
assert
#define assert(ex)
Definition: util_old.h:213
void Gia_ManFromBridgeHolds ( FILE *  pFile,
int  iPoProved 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 229 of file utilBridge.c.

230 {
231  fprintf( pFile, "%.6d", 101 /*message type = Result*/);
232  fprintf( pFile, " " );
233  fprintf( pFile, "%.16d", 3 + aigerNumSize(iPoProved) /*size in bytes*/);
234  fprintf( pFile, " " );
235 
236  fputc( (char)BRIDGE_VALUE_1, pFile ); // true
237  fputc( (char)1, pFile ); // size of vector (Armin's encoding)
238  Gia_AigerWriteUnsignedFile( pFile, iPoProved ); // number of the property (Armin's encoding)
239  fputc( (char)0, pFile ); // no invariant
240  fflush(pFile);
241 }
aigerNumSize
static int aigerNumSize(unsigned x)
Definition: utilBridge.c:206
BRIDGE_VALUE_1
#define BRIDGE_VALUE_1
Definition: utilBridge.c:48
Gia_AigerWriteUnsignedFile
static void Gia_AigerWriteUnsignedFile(FILE *pFile, unsigned x)
Definition: gia.h:860
Gia_Man_t* Gia_ManFromBridgeReadBody ( int  Size,
unsigned char *  pBuffer,
Vec_Int_t **  pvInits 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 308 of file utilBridge.c.

309 {
310  int fHash = 0;
311  Vec_Int_t * vLits, * vInits;
312  Gia_Man_t * p = NULL;
313  unsigned char * pBufferPivot, * pBufferEnd = pBuffer + Size;
314  int i, nInputs, nFlops, nGates, nProps;
315  unsigned iFan0, iFan1;
316 
317  nInputs = Gia_AigerReadUnsigned( &pBuffer );
318  nFlops = Gia_AigerReadUnsigned( &pBuffer );
319  nGates = Gia_AigerReadUnsigned( &pBuffer );
320 
321  vLits = Vec_IntAlloc( 1000 );
322  Vec_IntPush( vLits, -999 );
323  Vec_IntPush( vLits, 1 );
324 
325  // start the AIG package
326  p = Gia_ManStart( nInputs + nFlops * 2 + nGates + 1 + 1 ); // PI+FO+FI+AND+PO+1
327  p->pName = Abc_UtilStrsav( "temp" );
328 
329  // create PIs
330  for ( i = 0; i < nInputs; i++ )
331  Vec_IntPush( vLits, Gia_ManAppendCi( p ) );
332 
333  // create flop outputs
334  for ( i = 0; i < nFlops; i++ )
335  Vec_IntPush( vLits, Gia_ManAppendCi( p ) );
336 
337  // create nodes
338  if ( fHash )
339  Gia_ManHashAlloc( p );
340  for ( i = 0; i < nGates; i++ )
341  {
342  iFan0 = Gia_AigerReadUnsigned( &pBuffer );
343  iFan1 = Gia_AigerReadUnsigned( &pBuffer );
344  assert( !(iFan0 & 1) );
345  iFan0 >>= 1;
346  iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 );
347  iFan1 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan1 >> 1), iFan1 & 1 );
348  if ( fHash )
349  Vec_IntPush( vLits, Gia_ManHashAnd(p, iFan0, iFan1) );
350  else
351  Vec_IntPush( vLits, Gia_ManAppendAnd(p, iFan0, iFan1) );
352 
353  }
354  if ( fHash )
355  Gia_ManHashStop( p );
356 
357  // remember where flops begin
358  pBufferPivot = pBuffer;
359  // scroll through flops
360  for ( i = 0; i < nFlops; i++ )
361  Gia_AigerReadUnsigned( &pBuffer );
362 
363  // create POs
364  nProps = Gia_AigerReadUnsigned( &pBuffer );
365 // assert( nProps == 1 );
366  for ( i = 0; i < nProps; i++ )
367  {
368  iFan0 = Gia_AigerReadUnsigned( &pBuffer );
369  iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 );
370  // complement property output!!!
371  Gia_ManAppendCo( p, Abc_LitNot(iFan0) );
372  }
373  // make sure the end of buffer is reached
374  assert( pBufferEnd == pBuffer );
375 
376  // resetting to flops
377  pBuffer = pBufferPivot;
378  vInits = Vec_IntAlloc( nFlops );
379  for ( i = 0; i < nFlops; i++ )
380  {
381  iFan0 = Gia_AigerReadUnsigned( &pBuffer );
382  assert( (iFan0 & 3) == BRIDGE_VALUE_0 );
383  Vec_IntPush( vInits, iFan0 & 3 ); // 0 = X value; 1 = not used; 2 = false; 3 = true
384  iFan0 >>= 2;
385  iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 );
386  Gia_ManAppendCo( p, iFan0 );
387  }
388  Gia_ManSetRegNum( p, nFlops );
389  Vec_IntFree( vLits );
390 
391  // remove wholes in the node list
392  if ( fHash )
393  {
394  Gia_Man_t * pTemp;
395  p = Gia_ManCleanup( pTemp = p );
396  Gia_ManStop( pTemp );
397  }
398 
399  // return
400  if ( pvInits )
401  *pvInits = vInits;
402  else
403  Vec_IntFree( vInits );
404  return p;
405 }
Gia_ManAppendAnd
static int Gia_ManAppendAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: gia.h:592
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManAppendCo
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
BRIDGE_VALUE_0
#define BRIDGE_VALUE_0
Definition: utilBridge.c:47
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
Gia_Man_t_
Definition: gia.h:95
assert
#define assert(ex)
Definition: util_old.h:213
Gia_AigerReadUnsigned
static unsigned Gia_AigerReadUnsigned(unsigned char **ppPos)
Definition: gia.h:840
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
int Gia_ManFromBridgeReadPackage ( FILE *  pFile,
int *  pType,
int *  pSize,
unsigned char **  ppBuffer 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 419 of file utilBridge.c.

420 {
421  char Temp[24];
422  int RetValue;
423  RetValue = fread( Temp, 24, 1, pFile );
424  if ( RetValue != 1 )
425  {
426  printf( "Gia_ManFromBridgeReadPackage(); Error 1: Something is wrong!\n" );
427  return 0;
428  }
429  Temp[6] = 0;
430  Temp[23]= 0;
431 
432  *pType = atoi( Temp );
433  *pSize = atoi( Temp + 7 );
434 
435  *ppBuffer = ABC_ALLOC( unsigned char, *pSize );
436  RetValue = fread( *ppBuffer, *pSize, 1, pFile );
437  if ( RetValue != 1 && *pSize != 0 )
438  {
439  ABC_FREE( *ppBuffer );
440  printf( "Gia_ManFromBridgeReadPackage(); Error 2: Something is wrong!\n" );
441  return 0;
442  }
443  return 1;
444 }
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
void Gia_ManFromBridgeTest ( char *  pFileName)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 526 of file utilBridge.c.

527 {
528  Gia_Man_t * p;
529  FILE * pFile = fopen( pFileName, "rb" );
530  if ( pFile == NULL )
531  {
532  printf( "Cannot open input file \"%s\".\n", pFileName );
533  return;
534  }
535 
536  p = Gia_ManFromBridge( pFile, NULL );
537  fclose ( pFile );
538 
539  Gia_ManPrintStats( p, NULL );
540  Gia_AigerWrite( p, "temp.aig", 0, 0 );
541 
542  Gia_ManToBridgeAbsNetlistTest( "par_.dump", p, BRIDGE_ABS_NETLIST );
543  Gia_ManStop( p );
544 }
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManPrintStats
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition: giaMan.c:389
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_ManToBridgeAbsNetlistTest
void Gia_ManToBridgeAbsNetlistTest(char *pFileName, Gia_Man_t *p, int msg_type)
Definition: utilBridge.c:503
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact)
Definition: giaAiger.c:1024
Gia_Man_t_
Definition: gia.h:95
Gia_ManFromBridge
Gia_Man_t * Gia_ManFromBridge(FILE *pFile, Vec_Int_t **pvInit)
Definition: utilBridge.c:457
BRIDGE_ABS_NETLIST
#define BRIDGE_ABS_NETLIST
Definition: abc_global.h:295
void Gia_ManFromBridgeUnknown ( FILE *  pFile,
int  iPoUnknown 
)

Definition at line 242 of file utilBridge.c.

243 {
244  fprintf( pFile, "%.6d", 101 /*message type = Result*/);
245  fprintf( pFile, " " );
246  fprintf( pFile, "%.16d", 2 + aigerNumSize(iPoUnknown) /*size in bytes*/);
247  fprintf( pFile, " " );
248 
249  fputc( (char)BRIDGE_VALUE_X, pFile ); // undef
250  fputc( (char)1, pFile ); // size of vector (Armin's encoding)
251  Gia_AigerWriteUnsignedFile( pFile, iPoUnknown ); // number of the property (Armin's encoding)
252  fflush(pFile);
253 }
aigerNumSize
static int aigerNumSize(unsigned x)
Definition: utilBridge.c:206
BRIDGE_VALUE_X
#define BRIDGE_VALUE_X
Definition: utilBridge.c:46
Gia_AigerWriteUnsignedFile
static void Gia_AigerWriteUnsignedFile(FILE *pFile, unsigned x)
Definition: gia.h:860
int Gia_ManToBridgeAbort ( FILE *  pFile,
int  Size,
unsigned char *  pBuffer 
)

Definition at line 175 of file utilBridge.c.

176 {
177  Gia_CreateHeader( pFile, BRIDGE_ABORT, Size, pBuffer );
178  return 1;
179 }
Gia_CreateHeader
void Gia_CreateHeader(FILE *pFile, int Type, int Size, unsigned char *pBuffer)
Definition: utilBridge.c:127
BRIDGE_ABORT
#define BRIDGE_ABORT
Definition: utilBridge.c:39
int Gia_ManToBridgeAbsNetlist ( FILE *  pFile,
void *  p,
int  pkg_type 
)

Definition at line 189 of file utilBridge.c.

190 {
191  Vec_Str_t * vBuffer;
192  vBuffer = Gia_ManToBridgeVec( (Gia_Man_t *)p );
193  Gia_CreateHeader( pFile, pkg_type, Vec_StrSize(vBuffer), (unsigned char *)Vec_StrArray(vBuffer) );
194  Vec_StrFree( vBuffer );
195  return 1;
196 }
Gia_CreateHeader
void Gia_CreateHeader(FILE *pFile, int Type, int Size, unsigned char *pBuffer)
Definition: utilBridge.c:127
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_StrArray
static char * Vec_StrArray(Vec_Str_t *p)
Definition: vecStr.h:272
Vec_StrFree
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
Vec_StrSize
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
Gia_ManToBridgeVec
Vec_Str_t * Gia_ManToBridgeVec(Gia_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: utilBridge.c:66
Vec_Str_t_
Definition: bblif.c:47
Gia_Man_t_
Definition: gia.h:95
void Gia_ManToBridgeAbsNetlistTest ( char *  pFileName,
Gia_Man_t *  p,
int  msg_type 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 503 of file utilBridge.c.

504 {
505  FILE * pFile = fopen( pFileName, "wb" );
506  if ( pFile == NULL )
507  {
508  printf( "Cannot open output file \"%s\".\n", pFileName );
509  return;
510  }
511  Gia_ManToBridgeAbsNetlist( pFile, p, msg_type );
512  fclose ( pFile );
513 }
Gia_ManToBridgeAbsNetlist
int Gia_ManToBridgeAbsNetlist(FILE *pFile, void *p, int pkg_type)
Definition: utilBridge.c:189
int Gia_ManToBridgeBadAbs ( FILE *  pFile)

Definition at line 199 of file utilBridge.c.

200 {
201  Gia_CreateHeader( pFile, BRIDGE_BAD_ABS, 0, NULL );
202  return 1;
203 }
Gia_CreateHeader
void Gia_CreateHeader(FILE *pFile, int Type, int Size, unsigned char *pBuffer)
Definition: utilBridge.c:127
BRIDGE_BAD_ABS
#define BRIDGE_BAD_ABS
Definition: utilBridge.c:42
int Gia_ManToBridgeProgress ( FILE *  pFile,
int  Size,
unsigned char *  pBuffer 
)

Definition at line 182 of file utilBridge.c.

183 {
184  Gia_CreateHeader( pFile, BRIDGE_PROGRESS, Size, pBuffer );
185  return 1;
186 }
Gia_CreateHeader
void Gia_CreateHeader(FILE *pFile, int Type, int Size, unsigned char *pBuffer)
Definition: utilBridge.c:127
BRIDGE_PROGRESS
#define BRIDGE_PROGRESS
Definition: utilBridge.c:40
int Gia_ManToBridgeResult ( FILE *  pFile,
int  Result,
Abc_Cex_t *  pCex,
int  iPoProved 
)

DECLARATIONS ///.

CFile****************************************************************

FileName [pdrCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Property driven reachability.]

Synopsis [Core procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - November 20, 2010.]

Revision [

Id:
pdrCore.c,v 1.00 2010/11/20 00:00:00 alanmi Exp

]

Definition at line 284 of file utilBridge.c.

285 {
286  if ( Result == 0 ) // sat
287  Gia_ManFromBridgeCex( pFile, pCex );
288  else if ( Result == 1 ) // unsat
289  Gia_ManFromBridgeHolds( pFile, iPoProved );
290  else if ( Result == -1 ) // undef
291  Gia_ManFromBridgeUnknown( pFile, iPoProved );
292  else assert( 0 );
293  return 1;
294 }
Gia_ManFromBridgeUnknown
void Gia_ManFromBridgeUnknown(FILE *pFile, int iPoUnknown)
Definition: utilBridge.c:242
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManFromBridgeHolds
void Gia_ManFromBridgeHolds(FILE *pFile, int iPoProved)
Definition: utilBridge.c:229
Gia_ManFromBridgeCex
void Gia_ManFromBridgeCex(FILE *pFile, Abc_Cex_t *pCex)
Definition: utilBridge.c:254
int Gia_ManToBridgeText ( FILE *  pFile,
int  Size,
unsigned char *  pBuffer 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 168 of file utilBridge.c.

169 {
170  Gia_CreateHeader( pFile, BRIDGE_TEXT_MESSAGE, Size, pBuffer );
171  return 1;
172 }
Gia_CreateHeader
void Gia_CreateHeader(FILE *pFile, int Type, int Size, unsigned char *pBuffer)
Definition: utilBridge.c:127
BRIDGE_TEXT_MESSAGE
#define BRIDGE_TEXT_MESSAGE
DECLARATIONS ///.
Definition: utilBridge.c:37
Vec_Str_t* Gia_ManToBridgeVec ( Gia_Man_t *  p)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 66 of file utilBridge.c.

67 {
68  Vec_Str_t * vStr;
69  Gia_Obj_t * pObj;
70  int i, uLit0, uLit1, nNodes;
71  assert( Gia_ManPoNum(p) > 0 );
72 
73  // start with const1 node (number 1)
74  nNodes = 1;
75  // assign literals(!!!) to the value field
76  Gia_ManConst0(p)->Value = Abc_Var2Lit( nNodes++, 1 );
77  Gia_ManForEachCi( p, pObj, i )
78  pObj->Value = Abc_Var2Lit( nNodes++, 0 );
79  Gia_ManForEachAnd( p, pObj, i )
80  pObj->Value = Abc_Var2Lit( nNodes++, 0 );
81 
82  // write header
83  vStr = Vec_StrAlloc( 1000 );
84  Gia_AigerWriteUnsigned( vStr, Gia_ManPiNum(p) );
85  Gia_AigerWriteUnsigned( vStr, Gia_ManRegNum(p) );
86  Gia_AigerWriteUnsigned( vStr, Gia_ManAndNum(p) );
87 
88  // write the nodes
89  Gia_ManForEachAnd( p, pObj, i )
90  {
91  uLit0 = Gia_ObjFanin0Copy( pObj );
92  uLit1 = Gia_ObjFanin1Copy( pObj );
93  assert( uLit0 != uLit1 );
94  Gia_AigerWriteUnsigned( vStr, uLit0 << 1 );
95  Gia_AigerWriteUnsigned( vStr, uLit1 );
96  }
97 
98  // write latch drivers
99  Gia_ManForEachRi( p, pObj, i )
100  {
101  uLit0 = Gia_ObjFanin0Copy( pObj );
102  Gia_AigerWriteUnsigned( vStr, (uLit0 << 2) | BRIDGE_VALUE_0 );
103  }
104 
105  // write PO drivers
106  Gia_AigerWriteUnsigned( vStr, Gia_ManPoNum(p) );
107  Gia_ManForEachPo( p, pObj, i )
108  {
109  uLit0 = Gia_ObjFanin0Copy( pObj );
110  // complement property output!!!
111  Gia_AigerWriteUnsigned( vStr, Abc_LitNot(uLit0) );
112  }
113  return vStr;
114 }
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Vec_StrAlloc
static Vec_Str_t * Vec_StrAlloc(int nCap)
Definition: bblif.c:495
Gia_AigerWriteUnsigned
static void Gia_AigerWriteUnsigned(Vec_Str_t *vStr, unsigned x)
Definition: gia.h:848
Gia_Obj_t_
Definition: gia.h:75
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Gia_ObjFanin1Copy
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
BRIDGE_VALUE_0
#define BRIDGE_VALUE_0
Definition: utilBridge.c:47
Gia_ObjFanin0Copy
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
Vec_Str_t_
Definition: bblif.c:47
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
assert
#define assert(ex)
Definition: util_old.h:213
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387