luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Supporting new resub problem format.

This commit is contained in:
Alan Mishchenko 2022-06-02 07:47:33 -07:00
parent 5a3e0a1f15
commit 94ab17c39e
6 changed files with 200 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

50
src/aig/gia/giaUtil.c
View File

@ -3080,7 +3080,55 @@ Gia_Man_t * Gia_ManTransformCond( Gia_Man_t * p )
Abc_PrintTime( 0, "Time", Abc_Clock() - clk );
return NULL;
}
void Gia_ManWriteSol( Gia_Man_t * p, char * pFileName )
{
char * pBasicName = Extra_FileNameGeneric( pFileName );
char * pFileName2 = Abc_UtilStrsavTwo( pBasicName, ".sol" );
FILE * pFile = fopen( pFileName2, "wb" );
ABC_FREE( pBasicName );
if ( pFile == NULL )
printf( "Cannot open output file \"%s\".\n", pFileName2 );
else
{
Gia_Obj_t * pObj; int i;
Gia_ManForEachAnd( p, pObj, i )
fprintf( pFile, "%d %d ", Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i) );
Gia_ManForEachCo( p, pObj, i )
fprintf( pFile, "%d %d ", Gia_ObjFaninLit0p(p, pObj), Gia_ObjFaninLit0p(p, pObj) );
fclose( pFile );
printf( "Finished writing solution file \"%s\".\n", pFileName2 );
}
ABC_FREE( pFileName2 );
}
void Gia_ManWriteResub( Gia_Man_t * p, char * pFileName )
{
FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
printf( "Cannot open output file \"%s\".\n", pFileName );
else
{
Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
Vec_Wrd_t * vSimsPo = Gia_ManSimPatSimOut( p, vSimsPi, 1 );
int i, k, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p);
word * pTemp = ABC_ALLOC( word, nWords );
fprintf( pFile, "%d %d %d %d\n", Gia_ManCiNum(p), 0, Gia_ManCoNum(p), 1 << Gia_ManCiNum(p) );
for ( i = 0; i < Gia_ManCiNum(p); i++ )
Abc_TtPrintBinary1( pFile, Vec_WrdEntryP(vSimsPi, i*nWords), Gia_ManCiNum(p) ), fprintf(pFile, "\n");
for ( i = 0; i < (1 << Gia_ManCoNum(p)); i++ )
{
Abc_TtFill( pTemp, nWords );
for ( k = 0; k < Gia_ManCoNum(p); k++ )
Abc_TtAndCompl( pTemp, pTemp, 0, Vec_WrdEntryP(vSimsPo, k*nWords), !((i>>k)&1), nWords );
Abc_TtPrintBinary1( pFile, pTemp, Gia_ManCiNum(p) ), fprintf(pFile, "\n");
}
ABC_FREE( pTemp );
fclose( pFile );
Vec_WrdFree( vSimsPi );
Vec_WrdFree( vSimsPo );
printf( "Finished writing resub file \"%s\".\n", pFileName );
Gia_ManWriteSol( p, pFileName );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

53
src/base/io/io.c
View File

@ -84,6 +84,7 @@ static int IoCommandWriteTruths ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteStatus ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteSmv ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteJson ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteResub ( Abc_Frame_t * pAbc, int argc, char **argv );
extern void Abc_FrameCopyLTLDataBase( Abc_Frame_t *pAbc, Abc_Ntk_t * pNtk );
@ -155,6 +156,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "write_status", IoCommandWriteStatus, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_smv", IoCommandWriteSmv, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_json", IoCommandWriteJson, 0 );
Cmd_CommandAdd( pAbc, "I/O", "&write_resub", IoCommandWriteResub, 0 );
}
/**Function*************************************************************
@ -3480,6 +3482,57 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandWriteResub( Abc_Frame_t * pAbc, int argc, char **argv )
{
extern void Gia_ManWriteResub( Gia_Man_t * p, char * pFileName );
char * pFileName;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
goto usage;
pFileName = argv[globalUtilOptind];
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "IoCommandWriteResub(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManCiNum(pAbc->pGia) > 20 )
{
Abc_Print( -1, "IoCommandWriteResub(): The number of inputs is wrong.\n" );
return 1;
}
Gia_ManWriteResub( pAbc->pGia, pFileName );
return 0;
usage:
fprintf( pAbc->Err, "usage: &write_resub [-ch] <file>\n" );
fprintf( pAbc->Err, "\t write the network in resub format\n" );
fprintf( pAbc->Err, "\t-h : print the help message\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .json)\n" );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

2
src/base/main/mainUtils.c
View File

@ -160,7 +160,7 @@ void Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName )
void Abc_UtilsSource( Abc_Frame_t * pAbc )
{
#ifdef WIN32
if ( Cmd_CommandExecute(pAbc, "source -s abc.rc") )
if ( Cmd_CommandExecute(pAbc, "source abc.rc") )
{
if ( Cmd_CommandExecute(pAbc, "source ..\\abc.rc") == 0 )
printf( "Loaded \"abc.rc\" from the parent directory.\n" );

18
src/misc/util/utilTruth.h
View File

@ -1471,6 +1471,24 @@ static inline void Abc_TtPrintBinary( word * pTruth, int nVars )
printf( "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) );
printf( "\n" );
}
static inline void Abc_TtPrintBinary1( FILE * pFile, word * pTruth, int nVars )
{
word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
int k, Limit = Abc_MinInt( 64, (1 << nVars) );
assert( nVars >= 2 );
for ( pThis = pTruth; pThis < pLimit; pThis++ )
for ( k = 0; k < Limit; k++ )
fprintf( pFile, "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) );
}
static inline void Abc_TtPrintBinary2( FILE * pFile, word * pTruth, int nVars )
{
word * pThis;
int k, Limit = Abc_MinInt( 64, (1 << nVars) );
assert( nVars >= 2 );
for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
for ( k = Limit-1; k >= 0; k-- )
fprintf( pFile, "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) );
}
/**Function*************************************************************

2
src/misc/vec/vecInt.h
View File

@ -61,6 +61,8 @@ struct Vec_Int_t_
for ( i = Start; (i < Stop) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
#define Vec_IntForEachEntryReverse( vVec, pEntry, i ) \
for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && (((pEntry) = Vec_IntEntry(vVec, i)), 1); i-- )
#define Vec_IntForEachEntryReverseStart( vVec, pEntry, i, Start ) \
for ( i = Start; (i >= 0) && (((pEntry) = Vec_IntEntry(vVec, i)), 1); i-- )
#define Vec_IntForEachEntryTwo( vVec1, vVec2, Entry1, Entry2, i ) \
for ( i = 0; (i < Vec_IntSize(vVec1)) && (((Entry1) = Vec_IntEntry(vVec1, i)), 1) && (((Entry2) = Vec_IntEntry(vVec2, i)), 1); i++ )
#define Vec_IntForEachEntryTwoStart( vVec1, vVec2, Entry1, Entry2, i, Start ) \

77
src/proof/acec/acecBo.c
View File

@ -21,6 +21,7 @@
#include "acecInt.h"
#include "misc/vec/vecWec.h"
#include "misc/extra/extra.h"
#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
@ -207,6 +208,82 @@ void Acec_DetectBoothTest( Gia_Man_t * p )
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManResubTest4()
{
Vec_Int_t * vRes = Vec_IntAlloc( 100 );
unsigned T = 0xF335ACC0;
int a, b, c;
int i, k, f, y;
int Count = 0;
for ( a = 0; a < 2; a++ )
{
unsigned A = s_Truths5[a];
for ( b = 0; b < 3; b++ )
{
unsigned B = s_Truths5[2+b];
for ( c = 0; c < 3; c++ ) if ( c != b )
{
unsigned C = s_Truths5[2+c];
Vec_IntPush( vRes, A & B & C );
Vec_IntPush( vRes, A & B & ~C );
}
}
}
printf( "Size = %d.\n", Vec_IntSize(vRes) );
for ( i = 0; i < (1 << Vec_IntSize(vRes)); i++ )
{
unsigned F[7] = {0};
unsigned Y[3] = {0};
if ( Abc_TtCountOnes( (word)i ) >= 8 )
continue;
for ( f = k = 0; k < Vec_IntSize(vRes); k++ )
if ( ((i >> k) & 1) )
F[f++] = Vec_IntEntry(vRes, k);
{
unsigned S1 = (F[0] & F[1]) | (F[0] & F[2]) | (F[1] & F[2]);
unsigned C1 = F[0] ^ F[1] ^ F[2];
unsigned S2 = (F[3] & F[4]) | (F[3] & F[5]) | (F[4] & F[5]);
unsigned C2 = F[3] ^ F[4] ^ F[5];
unsigned S3 = (F[6] & S1) | (F[6] & S2) | (S1 & S2);
unsigned C3 = F[6] ^ S1 ^ S2;
unsigned S4 = (C1 & C2) | (C1 & C3) | (C2 & C3);
unsigned C4 = C1 ^ C2 ^ C3;
Y[0] = S3;
Y[1] = S4;
Y[2] = C4;
}
for ( y = 0; y < 3; y++ )
if ( Y[y] == T )
printf( "Found!\n" );
Count++;
}
printf( "Tried = %d.\n", Count );
Vec_IntFree( vRes );
}
void Gia_ManResubTest5()
{
unsigned T = 0xF335ACC0;
int i;
for ( i = 0; i < 4; i++ )
{
unsigned x = i%2 ? Abc_Tt5Cofactor1(T, 0) : Abc_Tt5Cofactor0(T, 0);
unsigned y = i/2 ? Abc_Tt5Cofactor1(x, 1) : Abc_Tt5Cofactor0(x, 1);
word F = y;
F |= F << 32;
//Dau_DsdPrintFromTruth2( &F, 6 ); printf( "\n" );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////