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

merge

This commit is contained in:
Yen-Sheng Ho 2017-02-28 19:21:31 -08:00
parent 902a78eeb8 9957736777
commit 777c77785d
10 changed files with 197 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/base/abci/abc.c
View File

@ -61,6 +61,7 @@
#include "bool/rpo/rpo.h"
#include "map/mpm/mpm.h"
#include "opt/fret/fretime.h"
#include "opt/nwk/nwkMerge.h"
#ifndef _WIN32
#include <unistd.h>
@ -124,7 +125,7 @@ static int Abc_CommandTrace ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandSpeedup ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPowerdown ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAddBuffs ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandMerge ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMerge ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTestDec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTestNpn ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTestRPO ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -774,7 +775,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "speedup", Abc_CommandSpeedup, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "powerdown", Abc_CommandPowerdown, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "addbuffs", Abc_CommandAddBuffs, 1 );
// Cmd_CommandAdd( pAbc, "Synthesis", "merge", Abc_CommandMerge, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "merge", Abc_CommandMerge, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "testdec", Abc_CommandTestDec, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "testnpn", Abc_CommandTestNpn, 0 );
Cmd_CommandAdd( pAbc, "LogiCS", "testrpo", Abc_CommandTestRPO, 0 );
@ -6011,7 +6012,7 @@ usage:
return 1;
}
#if 0
//#if 0
/**Function*************************************************************
Synopsis []
@ -6144,7 +6145,7 @@ usage:
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
#endif
//#endif

34
src/map/scl/scl.c
View File

@ -1823,13 +1823,17 @@ int Scl_CommandReadConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
FILE * pFile;
char * pFileName;
int fUseNewFormat = 0;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "nvh" ) ) != EOF )
{
switch ( c )
{
case 'n':
fVerbose ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -1850,25 +1854,29 @@ int Scl_CommandReadConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
fclose( pFile );
// Abc_SclReadTimingConstr( pAbc, pFileName, fVerbose );
if ( pNtk == NULL )
if ( !fUseNewFormat )
Abc_SclReadTimingConstr( pAbc, pFileName, fVerbose );
else
{
fprintf( pAbc->Err, "There is no current network.\n" );
return 1;
}
// input constraint manager
if ( pNtk )
{
Scl_Con_t * pCon = Scl_ConRead( pFileName, Abc_NtkNameMan(pNtk, 0), Abc_NtkNameMan(pNtk, 1) );
if ( pCon ) Scl_ConUpdateMan( pAbc, pCon );
if ( pNtk == NULL )
{
fprintf( pAbc->Err, "There is no current network.\n" );
return 1;
}
// input constraint manager
if ( pNtk )
{
Scl_Con_t * pCon = Scl_ConRead( pFileName, Abc_NtkNameMan(pNtk, 0), Abc_NtkNameMan(pNtk, 1) );
if ( pCon ) Scl_ConUpdateMan( pAbc, pCon );
}
}
return 0;
usage:
fprintf( pAbc->Err, "usage: read_constr [-vh] <file>\n" );
fprintf( pAbc->Err, "usage: read_constr [-nvh] <file>\n" );
fprintf( pAbc->Err, "\t read file with timing constraints for standard-cell designs\n" );
fprintf( pAbc->Err, "\t-n : toggle using new constraint file format [default = %s]\n", fUseNewFormat? "yes": "no" );
fprintf( pAbc->Err, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\t<file> : the name of a file to read\n" );

10
src/map/scl/sclUtil.c
View File

@ -254,21 +254,21 @@ void Abc_SclReadTimingConstr( Abc_Frame_t * pAbc, char * pFileName, int fVerbose
pToken = strtok( Buffer, " \t\r\n" );
if ( pToken == NULL )
continue;
// if ( !strcmp(pToken, "set_driving_cell") )
if ( !strcmp(pToken, "default_input_cell") )
if ( !strcmp(pToken, "set_driving_cell") )
// if ( !strcmp(pToken, "default_input_cell") )
{
Abc_FrameSetDrivingCell( Abc_UtilStrsav(strtok(NULL, " \t\r\n")) );
if ( fVerbose )
printf( "Setting driving cell to be \"%s\".\n", Abc_FrameReadDrivingCell() );
}
// else if ( !strcmp(pToken, "set_load") )
else if ( !strcmp(pToken, "default_output_load") )
else if ( !strcmp(pToken, "set_load") )
// else if ( !strcmp(pToken, "default_output_load") )
{
Abc_FrameSetMaxLoad( atof(strtok(NULL, " \t\r\n")) );
if ( fVerbose )
printf( "Setting driving cell to be %f.\n", Abc_FrameReadMaxLoad() );
}
// else printf( "Unrecognized token \"%s\".\n", pToken );
else printf( "Unrecognized token \"%s\".\n", pToken );
}
fclose( pFile );
}

63
src/opt/sbd/sbd.c
View File

@ -19,6 +19,7 @@
***********************************************************************/
#include "sbdInt.h"
#include "misc/vec/vecHsh.h"
ABC_NAMESPACE_IMPL_START
@ -42,6 +43,68 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
int Sbd_CountConfigVars( Vec_Int_t * vSet, int nVars )
{
int i, k, Entry = 0, Entry2, Count = 0, Below;
int Prev = Vec_IntEntry( vSet, 0 );
Vec_IntForEachEntryStart( vSet, Entry, i, 1 )
{
assert( 2*Prev >= Entry );
if ( 2*Prev == Entry )
{
Prev = Entry;
continue;
}
Below = nVars;
Vec_IntForEachEntryStart( vSet, Entry2, k, i )
Below += Entry2;
Count += Below * (2*Prev - 1);
Prev = Entry;
}
Count += nVars * 2*Prev;
return Vec_IntSum(vSet) < nVars - 1 ? 0 : Count;
}
void Sbd_CountTopos()
{
Hsh_VecMan_t * p = Hsh_VecManStart( 100000 ); // hash table for arrays
Vec_Int_t * vSet = Vec_IntAlloc( 100 );
int i, k, e, Start, Stop;
Start = Hsh_VecManAdd( p, vSet );
for ( i = 1; i < 9; i++ )
{
Stop = Hsh_VecSize( p );
for ( e = Start; e < Stop; e++ )
{
Vec_Int_t * vTemp = Hsh_VecReadEntry( p, e );
Vec_IntClear( vSet );
Vec_IntAppend( vSet, vTemp );
for ( k = 0; k < Vec_IntSize(vSet); k++ )
{
// skip if the number of entries on this level is equal to the number of fanins on the previous level
if ( k ? (Vec_IntEntry(vSet, k) == 2*Vec_IntEntry(vSet, k-1)) : (Vec_IntEntry(vSet, 0) > 0) )
continue;
Vec_IntAddToEntry( vSet, k, 1 );
Hsh_VecManAdd( p, vSet );
Vec_IntAddToEntry( vSet, k, -1 );
}
Vec_IntPush( vSet, 1 );
Hsh_VecManAdd( p, vSet );
}
printf( "%2d : This = %8d All = %8d\n", i, Hsh_VecSize(p) - Stop, Hsh_VecSize(p) );
if ( 0 )
{
for ( e = Stop; e < Hsh_VecSize(p); e++ )
{
Vec_Int_t * vTemp = Hsh_VecReadEntry( p, e );
printf( "Params = %3d. ", Sbd_CountConfigVars(vTemp, 5) );
Vec_IntPrint( vTemp );
}
}
Start = Stop;
}
Vec_IntFree( vSet );
Hsh_VecManStop( p );
}
////////////////////////////////////////////////////////////////////////

30
src/proof/abs/absGla.c
View File

@ -1539,9 +1539,37 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
Abc_Print( 1, "LrnStart = %d LrnDelta = %d LrnRatio = %d %% Skip = %d SimpleCNF = %d Dump = %d\n",
pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs );
if ( pPars->fDumpVabs || pPars->fDumpMabs )
Abc_Print( 1, "%s will be dumped into file \"%s\".\n",
Abc_Print( 1, "%s will be continously dumped into file \"%s\".\n",
pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map",
Ga2_GlaGetFileName(p, pPars->fDumpVabs) );
if ( pPars->fDumpMabs )
{
{
char Command[1000];
Abc_FrameSetStatus( -1 );
Abc_FrameSetCex( NULL );
Abc_FrameSetNFrames( -1 );
sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status"));
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
}
{
// create trivial abstraction map
Gia_Obj_t * pObj;
char * pFileName = Ga2_GlaGetFileName(p, 0);
Vec_Int_t * vMap = pAig->vGateClasses; pAig->vGateClasses = NULL;
pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
Gia_ManForEachAnd( pAig, pObj, i )
Vec_IntWriteEntry( pAig->vGateClasses, i, 1 );
Gia_ManForEachRo( pAig, pObj, i )
Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjId(pAig, pObj), 1 );
Gia_AigerWrite( pAig, pFileName, 0, 0 );
Vec_IntFree( pAig->vGateClasses );
pAig->vGateClasses = vMap;
if ( p->pPars->fVerbose )
Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
}
}
Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" );
}
// iterate unrolling

14
src/sat/satoko/clause.h
View File

@ -59,5 +59,19 @@ static inline void clause_print(struct clause *clause)
printf("}\n");
}
static inline void clause_dump(FILE *file, struct clause *clause, int no_zero_var)
{
unsigned i;
for (i = 0; i < clause->size; i++) {
int var = (clause->data[i].lit >> 1);
char pol = (clause->data[i].lit & 1);
fprintf(file, "%d ", pol ? -(var + no_zero_var) : (var + no_zero_var));
}
if (no_zero_var)
fprintf(file, "0\n");
else
fprintf(file, "\n");
}
ABC_NAMESPACE_HEADER_END
#endif /* satoko__clause_h */

2
src/sat/satoko/cnf_reader.c
View File

@ -150,7 +150,7 @@ int satoko_parse_dimacs(char *fname, satoko_t **solver)
vec_uint_free(lits);
satoko_free(buffer);
*solver = p;
return satoko_simplify(p);
return SATOKO_OK;
}
ABC_NAMESPACE_IMPL_END

11
src/sat/satoko/satoko.h
View File

@ -60,6 +60,7 @@ struct satoko_opts {
unsigned clause_min_lbd_bin_resol;
float garbage_max_ratio;
char verbose;
char no_simplify;
};
typedef struct satoko_stats satoko_stats_t;
@ -108,6 +109,16 @@ extern void satoko_unbookmark(satoko_t *);
*/
extern int satoko_final_conflict(satoko_t *, unsigned *);
/* Procedure to dump a DIMACS file.
* - It receives as input the solver, a file name string and two integers.
* - If the file name string is NULL the solver will dump in stdout.
* - The first argument can be either 0 or 1 and is an option to dump learnt
* clauses. (value 1 will dump them).
* - The seccond argument can be either 0 or 1 and is an option to use 0 as a
* variable ID or not. Keep in mind that if 0 is used as an ID the generated
* file will not be a DIMACS. (value 1 will use 0 as ID).
*/
extern void satoko_write_dimacs(satoko_t *, char *, int, int);
extern satoko_stats_t satoko_stats(satoko_t *);
ABC_NAMESPACE_HEADER_END

2
src/sat/satoko/solver.c
View File

@ -644,7 +644,7 @@ char solver_search(solver_t *s)
solver_cancel_until(s, 0);
return SATOKO_UNDEC;
}
if (solver_dlevel(s) == 0)
if (!s->opts.no_simplify && solver_dlevel(s) == 0)
satoko_simplify(s);
/* Reduce the set of learnt clauses */

48
src/sat/satoko/solver_api.c
View File

@ -152,6 +152,7 @@ void satoko_default_opts(satoko_opts_t *opts)
{
memset(opts, 0, sizeof(satoko_opts_t));
opts->verbose = 0;
opts->no_simplify = 0;
/* Limits */
opts->conf_limit = 0;
opts->prop_limit = 0;
@ -290,6 +291,10 @@ int satoko_solve(solver_t *s)
//if (s->opts.verbose)
// print_opts(s);
if (!s->opts.no_simplify)
if (satoko_simplify(s) != SATOKO_OK)
return SATOKO_UNDEC;
while (status == SATOKO_UNDEC) {
status = solver_search(s);
if (solver_check_limits(s) == 0)
@ -297,6 +302,7 @@ int satoko_solve(solver_t *s)
}
if (s->opts.verbose)
print_stats(s);
solver_cancel_until(s, vec_uint_size(s->assumptions));
return status;
}
@ -309,7 +315,6 @@ int satoko_final_conflict(solver_t *s, unsigned *out)
memcpy(out, vec_uint_data(s->final_conflict),
sizeof(unsigned) * vec_uint_size(s->final_conflict));
return vec_uint_size(s->final_conflict);
}
satoko_stats_t satoko_stats(satoko_t *s)
@ -324,6 +329,7 @@ void satoko_bookmark(satoko_t *s)
s->book_cl_lrnt = vec_uint_size(s->learnts);
s->book_vars = vec_char_size(s->assigns);
s->book_trail = vec_uint_size(s->trail);
s->opts.no_simplify = 1;
}
void satoko_unbookmark(satoko_t *s)
@ -333,6 +339,7 @@ void satoko_unbookmark(satoko_t *s)
s->book_cdb = 0;
s->book_vars = 0;
s->book_trail = 0;
s->opts.no_simplify = 0;
}
void satoko_reset(satoko_t *s)
@ -442,4 +449,43 @@ void satoko_unmark_cone(satoko_t *s, int *pvars, int n_vars)
var_clean_mark(s, pvars[i]);
}
void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var)
{
FILE *file;
unsigned i;
unsigned n_vars = vec_act_size(s->activity);
unsigned n_orig = vec_uint_size(s->originals) + vec_uint_size(s->assumptions);
unsigned n_lrnts = vec_uint_size(s->learnts);
unsigned *array;
assert(wrt_lrnt == 0 || wrt_lrnt == 1);
assert(zero_var == 0 || zero_var == 1);
if (fname != NULL)
file = fopen(fname, "w");
else
file = stdout;
if (file == NULL) {
printf( "Error: Cannot open output file.\n");
return;
}
fprintf(file, "p cnf %d %d\n", n_vars, wrt_lrnt ? n_orig + n_lrnts : n_orig);
array = vec_uint_data(s->assumptions);
for (i = 0; i < vec_uint_size(s->assumptions); i++)
fprintf(file, "%d\n", array[i] & 1 ? -(array[i] + !zero_var) : array[i] + !zero_var);
array = vec_uint_data(s->originals);
for (i = 0; i < vec_uint_size(s->originals); i++)
clause_dump(file, clause_read(s, array[i]), !zero_var);
if (wrt_lrnt) {
printf(" Lertns %u", n_lrnts);
array = vec_uint_data(s->learnts);
for (i = 0; i < n_lrnts; i++)
clause_dump(file, clause_read(s, array[i]), !zero_var);
}
}
ABC_NAMESPACE_IMPL_END