summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaGlitch.c19
-rw-r--r--src/aig/gia/giaIso.c2
-rw-r--r--src/aig/gia/giaIso2.c2
-rw-r--r--src/aig/miniaig/ndr.h614
-rw-r--r--src/aig/saig/saigIsoSlow.c2
-rw-r--r--src/base/abc/abc.h1
-rw-r--r--src/base/abci/abc.c130
-rw-r--r--src/base/abci/abcEco.c58
-rw-r--r--src/base/abci/abcMap.c16
-rw-r--r--src/base/abci/abcPrint.c79
-rw-r--r--src/base/abci/module.make1
-rw-r--r--src/base/cmd/cmdHist.c8
-rw-r--r--src/base/main/abcapis.h105
-rw-r--r--src/base/main/abcapis_old.h (renamed from src/aig/miniaig/abcapis.h)4
-rw-r--r--src/base/main/main.h8
-rw-r--r--src/base/main/mainFrame.c2
-rw-r--r--src/base/wlc/wlcStdin.c2
-rw-r--r--src/map/scl/sclCon.h4
-rw-r--r--src/proof/pdr/pdrCore.c195
-rw-r--r--src/sat/bmc/bmcClp.c26
-rw-r--r--src/sat/bsat/satSolver.c147
-rw-r--r--src/sat/bsat/satSolver.h2
22 files changed, 1377 insertions, 50 deletions
diff --git a/src/aig/gia/giaGlitch.c b/src/aig/gia/giaGlitch.c
index cc69f6b3..8c0cc161 100644
--- a/src/aig/gia/giaGlitch.c
+++ b/src/aig/gia/giaGlitch.c
@@ -37,7 +37,7 @@ struct Gli_Obj_t_
unsigned nFanins : 3; // the number of fanins
unsigned nFanouts : 25; // total number of fanouts
unsigned Handle; // ID of the node
- unsigned uTruth[2]; // truth table of the node
+ word * pTruth; // truth table of the node
unsigned uSimInfo; // simulation info of the node
union
{
@@ -333,7 +333,7 @@ static inline int Gli_NodeComputeValue( Gli_Obj_t * pNode )
int i, Phase = 0;
for ( i = 0; i < (int)pNode->nFanins; i++ )
Phase |= (Gli_ObjFanin(pNode, i)->fPhase << i);
- return Abc_InfoHasBit( pNode->uTruth, Phase );
+ return Abc_InfoHasBit( (unsigned *)pNode->pTruth, Phase );
}
/**Function*************************************************************
@@ -352,7 +352,7 @@ static inline int Gli_NodeComputeValue2( Gli_Obj_t * pNode )
int i, Phase = 0;
for ( i = 0; i < (int)pNode->nFanins; i++ )
Phase |= (Gli_ObjFanin(pNode, i)->fPhase2 << i);
- return Abc_InfoHasBit( pNode->uTruth, Phase );
+ return Abc_InfoHasBit( (unsigned *)pNode->pTruth, Phase );
}
/**Function*************************************************************
@@ -366,16 +366,15 @@ static inline int Gli_NodeComputeValue2( Gli_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-int Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, unsigned * puTruth )
+int Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, word * pGateTruth )
{
Gli_Obj_t * pObj, * pFanin;
int i;
- assert( Vec_IntSize(vFanins) <= 6 );
+ assert( Vec_IntSize(vFanins) <= 16 );
pObj = Gli_ObjAlloc( p, Vec_IntSize(vFanins), nFanouts );
Gli_ManForEachEntry( vFanins, p, pFanin, i )
Gli_ObjAddFanin( pObj, pFanin );
- pObj->uTruth[0] = puTruth[0];
- pObj->uTruth[1] = puTruth[Vec_IntSize(vFanins) == 6];
+ pObj->pTruth = pGateTruth;
pObj->fPhase = pObj->fPhase2 = Gli_NodeComputeValue( pObj );
return pObj->Handle;
}
@@ -584,7 +583,7 @@ unsigned Gli_ManSimulateSeqNode( Gli_Man_t * p, Gli_Obj_t * pNode )
int nFanins = Gli_ObjFaninNum(pNode);
int i, k, Phase;
Gli_Obj_t * pFanin;
- assert( nFanins <= 6 );
+ assert( nFanins <= 16 );
Gli_ObjForEachFanin( pNode, pFanin, i )
pSimInfos[i] = pFanin->uSimInfo;
for ( i = 0; i < 32; i++ )
@@ -593,7 +592,7 @@ unsigned Gli_ManSimulateSeqNode( Gli_Man_t * p, Gli_Obj_t * pNode )
for ( k = 0; k < nFanins; k++ )
if ( (pSimInfos[k] >> i) & 1 )
Phase |= (1 << k);
- if ( Abc_InfoHasBit( pNode->uTruth, Phase ) )
+ if ( Abc_InfoHasBit( (unsigned *)pNode->pTruth, Phase ) )
Result |= (1 << i);
}
return Result;
@@ -772,7 +771,7 @@ void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb
}
if ( fVerbose )
{
- printf( "\nSimulated %d patterns. ", nPatterns );
+ printf( "Simulated %d patterns. Input transition probability %.2f. ", nPatterns, PiTransProb );
ABC_PRMn( "Memory", 4*p->nObjData );
ABC_PRT( "Time", Abc_Clock() - clk );
}
diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c
index baf7bc93..0e040b6c 100644
--- a/src/aig/gia/giaIso.c
+++ b/src/aig/gia/giaIso.c
@@ -24,7 +24,7 @@ ABC_NAMESPACE_IMPL_START
#define ISO_MASK 0xFF
-static int s_256Primes[ISO_MASK+1] =
+static unsigned int s_256Primes[ISO_MASK+1] =
{
0x984b6ad9,0x18a6eed3,0x950353e2,0x6222f6eb,0xdfbedd47,0xef0f9023,0xac932a26,0x590eaf55,
0x97d0a034,0xdc36cd2e,0x22736b37,0xdc9066b0,0x2eb2f98b,0x5d9c7baf,0x85747c9e,0x8aca1055,
diff --git a/src/aig/gia/giaIso2.c b/src/aig/gia/giaIso2.c
index e1ea7690..576b118f 100644
--- a/src/aig/gia/giaIso2.c
+++ b/src/aig/gia/giaIso2.c
@@ -27,7 +27,7 @@ ABC_NAMESPACE_IMPL_START
#define ISO_MASK 0xFF
-static int s_256Primes[ISO_MASK+1] =
+static unsigned int s_256Primes[ISO_MASK+1] =
{
0x984b6ad9,0x18a6eed3,0x950353e2,0x6222f6eb,0xdfbedd47,0xef0f9023,0xac932a26,0x590eaf55,
0x97d0a034,0xdc36cd2e,0x22736b37,0xdc9066b0,0x2eb2f98b,0x5d9c7baf,0x85747c9e,0x8aca1055,
diff --git a/src/aig/miniaig/ndr.h b/src/aig/miniaig/ndr.h
new file mode 100644
index 00000000..d7f425e8
--- /dev/null
+++ b/src/aig/miniaig/ndr.h
@@ -0,0 +1,614 @@
+/**CFile****************************************************************
+
+ FileName [ndr.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Format for word-level design representation.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - August 22, 2014.]
+
+ Revision [$Id: ndr.h,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__base__ndr__ndr_h
+#define ABC__base__ndr__ndr_h
+
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+//ABC_NAMESPACE_HEADER_START
+
+#ifdef _WIN32
+#define inline __inline
+#endif
+
+/*
+ For the lack of a better name, this format is called New Data Representation (NDR).
+
+ NDR is based on the following principles:
+ - complex data is composed of individual records
+ - a record has one of several known types (module, name, range, fanins, etc)
+ - a record can be atomic, for example, a name or an operator type
+ - a record can be composed of other records (for example, a module is composed of objects, etc)
+ - the stored data should be easy to write into and read from a file, or pass around as a memory buffer
+ - the format should be simple, easy to use, low-memory, and extensible
+ - new record types can be added by the user as needed
+
+ The implementation is based on the following ideas:
+ - a record is composed of two parts (the header followed by the body)
+ - the header contains two items (the record type and the body size, measured in terms of 4-byte integers)
+ - the body contains as many entries as stated in the record size
+ - if a record is composed of other records, its body contains these records
+
+ As an example, consider a name. It can be a module name, an object name, or a net name.
+ A record storing one name has a header {NDR_NAME, 1} containing record type (NDR_NAME) and size (1),
+ The body of the record is composed of one unsigned integer representing the name (say, 357).
+ So the complete record looks as follows: { <header>, <body> } = { {NDR_NAME, 1}, {357} }.
+
+ As another example, consider a two-input AND-gate. In this case, the recent is composed
+ of a header {NDR_OBJECT, 4} containing record type (NDR_OBJECT) and the body size (4), followed
+ by an array of records creating the AND-gate: (a) name, (b) operation type, (c) fanins.
+ The complete record looks as follows: { {NDR_OBJECT, 5}, {{{NDR_NAME, 1}, 357}, {{NDR_OPERTYPE, 1}, WLC_OBJ_LOGIC_AND},
+ {{NDR_INPUT, 2}, {<id_fanin1>, <id_fanin2>}}} }. Please note that only body entries are counted towards size.
+ In the case of one name, there is only one body entry. In the case of the AND-gate, there are 4 body entries
+ (name ID, gate type, first fanin, second fanin).
+
+ Headers and bodies of all objects are stored differently. Headers are stored in an array of unsigned chars,
+ while bodies are stored in the array of 4-byte unsigned integers. This is important for memory efficiency.
+ However, the user does not see these details.
+
+ To estimate memory usage, we can assume that each header takes 1 byte and each body entry contains 4 bytes.
+ A name takes 5 bytes, and an AND-gate takes 1 * NumHeaders + 4 * NumBodyEntries = 1 * 4 + 4 * 4 = 20 bytes.
+ Not bad. The same as memory usage in a well-designed AIG package with structural hashing.
+
+ Comments:
+ - it is assumed that all port names, net names, and instance names are hashed into 1-based integer numbers called name IDs
+ - nets are not explicitly represented but their name ID are used to establish connectivity between the objects
+ - primary input and primary output objects have to be explicitly created (as shown in the example below)
+ - object inputs are name IDs of the driving nets; object outputs are name IDs of the driven nets
+ - objects can be added to a module in any order
+ - if the ordering of inputs/outputs/flops of a module is not provided as a separate record,
+ their ordering is determined by the order of their appearance of their records in the body of the module
+ - if range limits and signedness are all 0, it is assumed that it is a Boolean object
+ - if left limit and right limit of a range are equal, it is assumed that the range contains one bit
+ - instances of known operators can have types defined by Wlc_ObjType_t below
+ - instances of user modules have type equal to the name ID of the module plus 1000
+ - initial states of the flops are given as char-strings containing 0, 1, and 'x'
+ (for example, "4'b10XX" is an init state of a 4-bit flop with bit-level init states const1, const0, unknown, unknown)
+ - word-level constants are represented as char-strings given in the same way as they would appear in a Verilog file
+ (for example, the 16-bit constant 10 is represented as a string "4'b1010". This string contains 8 bytes,
+ including the char '\0' to denote the end of the string. It will take 2 unsigned ints, therefore
+ its record will look as follows { {NDR_FUNCTION, 2}, {"4'b1010"} }, but the user does not see these details.
+ The user only gives "4'b1010" as an argument (char * pFunction) to the above procedure Ndr_ModuleAddObject().
+*/
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+// record types
+typedef enum {
+ NDR_NONE = 0, // 0: unused
+ NDR_DESIGN, // 1: design (or library of modules)
+ NDR_MODULE, // 2: one module
+ NDR_OBJECT, // 3: object
+ NDR_INPUT, // 4: input
+ NDR_OUTPUT, // 5: output
+ NDR_OPERTYPE, // 6: operator type (buffer, shifter, adder, etc)
+ NDR_NAME, // 7: name
+ NDR_RANGE, // 8: bit range
+ NDR_FUNCTION, // 9: specified for some operators (PLAs, etc)
+ NDR_UNKNOWN // 10: unknown
+} Ndr_RecordType_t;
+
+// operator types
+typedef enum {
+ WLC_OBJ_NONE = 0, // 00: unknown
+ WLC_OBJ_PI, // 01: primary input
+ WLC_OBJ_PO, // 02: primary output
+ WLC_OBJ_FO, // 03: flop output (unused)
+ WLC_OBJ_FI, // 04: flop input (unused)
+ WLC_OBJ_FF, // 05: flop
+ WLC_OBJ_CONST, // 06: constant
+ WLC_OBJ_BUF, // 07: buffer
+ WLC_OBJ_MUX, // 08: multiplexer
+ WLC_OBJ_SHIFT_R, // 09: shift right
+ WLC_OBJ_SHIFT_RA, // 10: shift right (arithmetic)
+ WLC_OBJ_SHIFT_L, // 11: shift left
+ WLC_OBJ_SHIFT_LA, // 12: shift left (arithmetic)
+ WLC_OBJ_ROTATE_R, // 13: rotate right
+ WLC_OBJ_ROTATE_L, // 14: rotate left
+ WLC_OBJ_BIT_NOT, // 15: bitwise NOT
+ WLC_OBJ_BIT_AND, // 16: bitwise AND
+ WLC_OBJ_BIT_OR, // 17: bitwise OR
+ WLC_OBJ_BIT_XOR, // 18: bitwise XOR
+ WLC_OBJ_BIT_NAND, // 19: bitwise AND
+ WLC_OBJ_BIT_NOR, // 20: bitwise OR
+ WLC_OBJ_BIT_NXOR, // 21: bitwise NXOR
+ WLC_OBJ_BIT_SELECT, // 22: bit selection
+ WLC_OBJ_BIT_CONCAT, // 23: bit concatenation
+ WLC_OBJ_BIT_ZEROPAD, // 24: zero padding
+ WLC_OBJ_BIT_SIGNEXT, // 25: sign extension
+ WLC_OBJ_LOGIC_NOT, // 26: logic NOT
+ WLC_OBJ_LOGIC_IMPL, // 27: logic implication
+ WLC_OBJ_LOGIC_AND, // 28: logic AND
+ WLC_OBJ_LOGIC_OR, // 29: logic OR
+ WLC_OBJ_LOGIC_XOR, // 30: logic XOR
+ WLC_OBJ_COMP_EQU, // 31: compare equal
+ WLC_OBJ_COMP_NOTEQU, // 32: compare not equal
+ WLC_OBJ_COMP_LESS, // 33: compare less
+ WLC_OBJ_COMP_MORE, // 34: compare more
+ WLC_OBJ_COMP_LESSEQU, // 35: compare less or equal
+ WLC_OBJ_COMP_MOREEQU, // 36: compare more or equal
+ WLC_OBJ_REDUCT_AND, // 37: reduction AND
+ WLC_OBJ_REDUCT_OR, // 38: reduction OR
+ WLC_OBJ_REDUCT_XOR, // 39: reduction XOR
+ WLC_OBJ_REDUCT_NAND, // 40: reduction NAND
+ WLC_OBJ_REDUCT_NOR, // 41: reduction NOR
+ WLC_OBJ_REDUCT_NXOR, // 42: reduction NXOR
+ WLC_OBJ_ARI_ADD, // 43: arithmetic addition
+ WLC_OBJ_ARI_SUB, // 44: arithmetic subtraction
+ WLC_OBJ_ARI_MULTI, // 45: arithmetic multiplier
+ WLC_OBJ_ARI_DIVIDE, // 46: arithmetic division
+ WLC_OBJ_ARI_REM, // 47: arithmetic remainder
+ WLC_OBJ_ARI_MODULUS, // 48: arithmetic modulus
+ WLC_OBJ_ARI_POWER, // 49: arithmetic power
+ WLC_OBJ_ARI_MINUS, // 50: arithmetic minus
+ WLC_OBJ_ARI_SQRT, // 51: integer square root
+ WLC_OBJ_ARI_SQUARE, // 52: integer square
+ WLC_OBJ_TABLE, // 53: bit table
+ WLC_OBJ_NUMBER // 54: unused
+} Wlc_ObjType_t;
+
+// printing operator types
+static inline char * Ndr_OperName( int Type )
+{
+ if ( Type == WLC_OBJ_NONE ) return NULL;
+ if ( Type == WLC_OBJ_PI ) return "pi"; // 01: primary input
+ if ( Type == WLC_OBJ_PO ) return "po"; // 02: primary output (unused)
+ if ( Type == WLC_OBJ_FO ) return "ff"; // 03: flop output
+ if ( Type == WLC_OBJ_FI ) return "bi"; // 04: flop input (unused)
+ if ( Type == WLC_OBJ_FF ) return "ff"; // 05: flop (unused)
+ if ( Type == WLC_OBJ_CONST ) return "const"; // 06: constant
+ if ( Type == WLC_OBJ_BUF ) return "buf"; // 07: buffer
+ if ( Type == WLC_OBJ_MUX ) return "mux"; // 08: multiplexer
+ if ( Type == WLC_OBJ_SHIFT_R ) return ">>"; // 09: shift right
+ if ( Type == WLC_OBJ_SHIFT_RA ) return ">>>"; // 10: shift right (arithmetic)
+ if ( Type == WLC_OBJ_SHIFT_L ) return "<<"; // 11: shift left
+ if ( Type == WLC_OBJ_SHIFT_LA ) return "<<<"; // 12: shift left (arithmetic)
+ if ( Type == WLC_OBJ_ROTATE_R ) return "rotR"; // 13: rotate right
+ if ( Type == WLC_OBJ_ROTATE_L ) return "rotL"; // 14: rotate left
+ if ( Type == WLC_OBJ_BIT_NOT ) return "~"; // 15: bitwise NOT
+ if ( Type == WLC_OBJ_BIT_AND ) return "&"; // 16: bitwise AND
+ if ( Type == WLC_OBJ_BIT_OR ) return "|"; // 17: bitwise OR
+ if ( Type == WLC_OBJ_BIT_XOR ) return "^"; // 18: bitwise XOR
+ if ( Type == WLC_OBJ_BIT_NAND ) return "~&"; // 19: bitwise NAND
+ if ( Type == WLC_OBJ_BIT_NOR ) return "~|"; // 20: bitwise NOR
+ if ( Type == WLC_OBJ_BIT_NXOR ) return "~^"; // 21: bitwise NXOR
+ if ( Type == WLC_OBJ_BIT_SELECT ) return "[:]"; // 22: bit selection
+ if ( Type == WLC_OBJ_BIT_CONCAT ) return "{}"; // 23: bit concatenation
+ if ( Type == WLC_OBJ_BIT_ZEROPAD ) return "zPad"; // 24: zero padding
+ if ( Type == WLC_OBJ_BIT_SIGNEXT ) return "sExt"; // 25: sign extension
+ if ( Type == WLC_OBJ_LOGIC_NOT ) return "!"; // 26: logic NOT
+ if ( Type == WLC_OBJ_LOGIC_IMPL ) return "=>"; // 27: logic implication
+ if ( Type == WLC_OBJ_LOGIC_AND ) return "&&"; // 28: logic AND
+ if ( Type == WLC_OBJ_LOGIC_OR ) return "||"; // 29: logic OR
+ if ( Type == WLC_OBJ_LOGIC_XOR ) return "^^"; // 30: logic XOR
+ if ( Type == WLC_OBJ_COMP_EQU ) return "=="; // 31: compare equal
+ if ( Type == WLC_OBJ_COMP_NOTEQU ) return "!="; // 32: compare not equal
+ if ( Type == WLC_OBJ_COMP_LESS ) return "<"; // 33: compare less
+ if ( Type == WLC_OBJ_COMP_MORE ) return ">"; // 34: compare more
+ if ( Type == WLC_OBJ_COMP_LESSEQU ) return "<="; // 35: compare less or equal
+ if ( Type == WLC_OBJ_COMP_MOREEQU ) return ">="; // 36: compare more or equal
+ if ( Type == WLC_OBJ_REDUCT_AND ) return "&"; // 37: reduction AND
+ if ( Type == WLC_OBJ_REDUCT_OR ) return "|"; // 38: reduction OR
+ if ( Type == WLC_OBJ_REDUCT_XOR ) return "^"; // 39: reduction XOR
+ if ( Type == WLC_OBJ_REDUCT_NAND ) return "~&"; // 40: reduction NAND
+ if ( Type == WLC_OBJ_REDUCT_NOR ) return "~|"; // 41: reduction NOR
+ if ( Type == WLC_OBJ_REDUCT_NXOR ) return "~^"; // 42: reduction NXOR
+ if ( Type == WLC_OBJ_ARI_ADD ) return "+"; // 43: arithmetic addition
+ if ( Type == WLC_OBJ_ARI_SUB ) return "-"; // 44: arithmetic subtraction
+ if ( Type == WLC_OBJ_ARI_MULTI ) return "*"; // 45: arithmetic multiplier
+ if ( Type == WLC_OBJ_ARI_DIVIDE ) return "/"; // 46: arithmetic division
+ if ( Type == WLC_OBJ_ARI_REM ) return "%"; // 47: arithmetic reminder
+ if ( Type == WLC_OBJ_ARI_MODULUS ) return "mod"; // 48: arithmetic modulus
+ if ( Type == WLC_OBJ_ARI_POWER ) return "**"; // 49: arithmetic power
+ if ( Type == WLC_OBJ_ARI_MINUS ) return "-"; // 50: arithmetic minus
+ if ( Type == WLC_OBJ_ARI_SQRT ) return "sqrt"; // 51: integer square root
+ if ( Type == WLC_OBJ_ARI_SQUARE ) return "squar"; // 52: integer square
+ if ( Type == WLC_OBJ_TABLE ) return "table"; // 53: bit table
+ if ( Type == WLC_OBJ_NUMBER ) return NULL; // 54: unused
+ return NULL;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+// this is an internal procedure, which is not seen by the user
+typedef struct Ndr_Data_t_ Ndr_Data_t;
+struct Ndr_Data_t_
+{
+ int nSize;
+ int nCap;
+ unsigned char * pHead;
+ unsigned int * pBody;
+};
+
+static inline int Ndr_DataType( Ndr_Data_t * p, int i ) { assert( p->pHead[i] ); return (int)p->pHead[i]; }
+static inline int Ndr_DataSize( Ndr_Data_t * p, int i ) { return Ndr_DataType(p, i) > NDR_OBJECT ? 1 : p->pBody[i]; }
+static inline int Ndr_DataEntry( Ndr_Data_t * p, int i ) { return (int)p->pBody[i]; }
+static inline int * Ndr_DataEntryP( Ndr_Data_t * p, int i ) { return (int *)p->pBody + i; }
+static inline int Ndr_DataEnd( Ndr_Data_t * p, int i ) { return i + p->pBody[i]; }
+static inline void Ndr_DataAddTo( Ndr_Data_t * p, int i, int Add ) { assert(Ndr_DataType(p, i) <= NDR_OBJECT); p->pBody[i] += Add; }
+static inline void Ndr_DataPush( Ndr_Data_t * p, int Type, int Entry ) { p->pHead[p->nSize] = Type; p->pBody[p->nSize++] = Entry; }
+
+////////////////////////////////////////////////////////////////////////
+/// ITERATORS ///
+////////////////////////////////////////////////////////////////////////
+
+// iterates over modules in the design
+#define Ndr_DesForEachMod( p, Mod ) \
+ for ( Mod = 1; Mod < Ndr_DataEntry(p, 0); Mod += Ndr_DataSize(p, Mod) ) if (Ndr_DataType(p, Mod) != NDR_MODULE) {} else
+
+// iterates over objects in a module
+#define Ndr_ModForEachObj( p, Mod, Obj ) \
+ for ( Obj = Mod + 1; Obj < Ndr_DataEnd(p, Mod); Obj += Ndr_DataSize(p, Obj) ) if (Ndr_DataType(p, Obj) != NDR_OBJECT) {} else
+
+// iterates over records in an object
+#define Ndr_ObjForEachEntry( p, Obj, Ent ) \
+ for ( Ent = Obj + 1; Ent < Ndr_DataEnd(p, Obj); Ent += Ndr_DataSize(p, Ent) )
+
+// iterates over primary inputs of a module
+#define Ndr_ModForEachPi( p, Mod, Obj ) \
+ Ndr_ModForEachObj( p, 0, Obj ) if ( !Ndr_ObjIsType(p, Obj, WLC_OBJ_PI) ) {} else
+
+// iteraots over primary outputs of a module
+#define Ndr_ModForEachPo( p, Mod, Obj ) \
+ Ndr_ModForEachObj( p, 0, Obj ) if ( !Ndr_ObjIsType(p, Obj, WLC_OBJ_PO) ) {} else
+
+// iterates over internal nodes of a module
+#define Ndr_ModForEachNode( p, Mod, Obj ) \
+ Ndr_ModForEachObj( p, 0, Obj ) if ( Ndr_ObjIsType(p, Obj, WLC_OBJ_PI) || Ndr_ObjIsType(p, Obj, WLC_OBJ_PO) ) {} else
+
+
+////////////////////////////////////////////////////////////////////////
+/// INTERNAL PROCEDURES ///
+////////////////////////////////////////////////////////////////////////
+
+
+static inline void Ndr_DataResize( Ndr_Data_t * p, int Add )
+{
+ if ( p->nSize + Add <= p->nCap )
+ return;
+ p->nCap *= 2;
+ p->pHead = (unsigned char*)realloc( p->pHead, p->nCap );
+ p->pBody = (unsigned int *)realloc( p->pBody, 4*p->nCap );
+}
+static inline void Ndr_DataPushRange( Ndr_Data_t * p, int RangeLeft, int RangeRight, int fSignedness )
+{
+ if ( fSignedness )
+ {
+ Ndr_DataPush( p, NDR_RANGE, RangeLeft );
+ Ndr_DataPush( p, NDR_RANGE, RangeRight );
+ Ndr_DataPush( p, NDR_RANGE, fSignedness );
+ return;
+ }
+ if ( !RangeLeft && !RangeRight )
+ return;
+ if ( RangeLeft == RangeRight )
+ Ndr_DataPush( p, NDR_RANGE, RangeLeft );
+ else
+ {
+ Ndr_DataPush( p, NDR_RANGE, RangeLeft );
+ Ndr_DataPush( p, NDR_RANGE, RangeRight );
+ }
+}
+static inline void Ndr_DataPushArray( Ndr_Data_t * p, int Type, int nArray, int * pArray )
+{
+ if ( !nArray )
+ return;
+ assert( nArray > 0 );
+ Ndr_DataResize( p, nArray );
+ memset( p->pHead + p->nSize, Type, nArray );
+ memcpy( p->pBody + p->nSize, pArray, 4*nArray );
+ p->nSize += nArray;
+}
+static inline void Ndr_DataPushString( Ndr_Data_t * p, int Type, char * pFunc )
+{
+ if ( !pFunc )
+ return;
+ Ndr_DataPushArray( p, Type, (strlen(pFunc) + 4) / 4, (int *)pFunc );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// VERILOG WRITING ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int Ndr_ObjReadEntry( Ndr_Data_t * p, int Obj, int Type )
+{
+ int Ent;
+ Ndr_ObjForEachEntry( p, Obj, Ent )
+ if ( Ndr_DataType(p, Ent) == Type )
+ return Ndr_DataEntry(p, Ent);
+ return -1;
+}
+static inline int Ndr_ObjReadArray( Ndr_Data_t * p, int Obj, int Type, int ** ppStart )
+{
+ int Ent, Counter = 0; *ppStart = NULL;
+ Ndr_ObjForEachEntry( p, Obj, Ent )
+ if ( Ndr_DataType(p, Ent) == Type )
+ {
+ Counter++;
+ if ( *ppStart == NULL )
+ *ppStart = (int *)p->pBody + Ent;
+ }
+ else if ( *ppStart )
+ return Counter;
+ return Counter;
+}
+static inline int Ndr_ObjIsType( Ndr_Data_t * p, int Obj, int Type )
+{
+ int Ent;
+ Ndr_ObjForEachEntry( p, Obj, Ent )
+ if ( Ndr_DataType(p, Ent) == NDR_OPERTYPE )
+ return (int)(Ndr_DataEntry(p, Ent) == Type);
+ return -1;
+}
+static inline int Ndr_ObjReadBody( Ndr_Data_t * p, int Obj, int Type )
+{
+ int Ent;
+ Ndr_ObjForEachEntry( p, Obj, Ent )
+ if ( Ndr_DataType(p, Ent) == Type )
+ return Ndr_DataEntry(p, Ent);
+ return -1;
+}
+static inline int * Ndr_ObjReadBodyP( Ndr_Data_t * p, int Obj, int Type )
+{
+ int Ent;
+ Ndr_ObjForEachEntry( p, Obj, Ent )
+ if ( Ndr_DataType(p, Ent) == Type )
+ return Ndr_DataEntryP(p, Ent);
+ return NULL;
+}
+static inline void Ndr_ObjWriteRange( Ndr_Data_t * p, int Obj, FILE * pFile )
+{
+ int * pArray, nArray = Ndr_ObjReadArray( p, Obj, NDR_RANGE, &pArray );
+ if ( nArray == 0 )
+ return;
+ if ( nArray == 3 )
+ fprintf( pFile, "signed " );
+ if ( nArray == 1 )
+ fprintf( pFile, "[%d] ", pArray[0] );
+ else
+ fprintf( pFile, "[%d:%d] ", pArray[0], pArray[1] );
+}
+static inline char * Ndr_ObjReadOutName( Ndr_Data_t * p, int Obj, char ** pNames )
+{
+ return pNames[Ndr_ObjReadBody(p, Obj, NDR_OUTPUT)];
+}
+static inline char * Ndr_ObjReadInName( Ndr_Data_t * p, int Obj, char ** pNames )
+{
+ return pNames[Ndr_ObjReadBody(p, Obj, NDR_INPUT)];
+}
+
+// to write signal names, this procedure takes a mapping of name IDs into actual char-strings (pNames)
+static inline void Ndr_ModuleWriteVerilog( char * pFileName, void * pModule, char ** pNames )
+{
+ Ndr_Data_t * p = (Ndr_Data_t *)pModule;
+ int Mod = 0, Obj, nArray, * pArray, fFirst = 1;
+
+ FILE * pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
+ if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for writing.\n", pFileName ); return; }
+
+ fprintf( pFile, "\nmodule %s (\n ", pNames[Ndr_ObjReadEntry(p, 0, NDR_NAME)] );
+
+ Ndr_ModForEachPi( p, Mod, Obj )
+ fprintf( pFile, "%s, ", Ndr_ObjReadOutName(p, Obj, pNames) );
+
+ fprintf( pFile, "\n " );
+
+ Ndr_ModForEachPo( p, Mod, Obj )
+ fprintf( pFile, "%s%s", fFirst ? "":", ", Ndr_ObjReadInName(p, Obj, pNames) ), fFirst = 0;
+
+ fprintf( pFile, "\n);\n\n" );
+
+ Ndr_ModForEachPi( p, Mod, Obj )
+ {
+ fprintf( pFile, " input " );
+ Ndr_ObjWriteRange( p, Obj, pFile );
+ fprintf( pFile, "%s;\n", Ndr_ObjReadOutName(p, Obj, pNames) );
+ }
+
+ Ndr_ModForEachPo( p, Mod, Obj )
+ {
+ fprintf( pFile, " output " );
+ Ndr_ObjWriteRange( p, Obj, pFile );
+ fprintf( pFile, "%s;\n", Ndr_ObjReadInName(p, Obj, pNames) );
+ }
+
+ Ndr_ModForEachNode( p, Mod, Obj )
+ {
+ fprintf( pFile, " wire " );
+ Ndr_ObjWriteRange( p, Obj, pFile );
+ fprintf( pFile, "%s;\n", Ndr_ObjReadOutName(p, Obj, pNames) );
+ }
+
+ fprintf( pFile, "\n" );
+
+ Ndr_ModForEachNode( p, Mod, Obj )
+ {
+ fprintf( pFile, " assign %s = ", Ndr_ObjReadOutName(p, Obj, pNames) );
+ nArray = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray );
+ if ( nArray == 0 )
+ fprintf( pFile, "%s;\n", (char *)Ndr_ObjReadBodyP(p, Obj, NDR_FUNCTION) );
+ else if ( nArray == 1 && Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE) == WLC_OBJ_BUF )
+ fprintf( pFile, "%s;\n", pNames[pArray[0]] );
+ else if ( nArray == 1 )
+ fprintf( pFile, "%s %s;\n", Ndr_OperName(Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE)), pNames[pArray[0]] );
+ else if ( nArray == 2 )
+ fprintf( pFile, "%s %s %s;\n", pNames[pArray[0]], Ndr_OperName(Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE)), pNames[pArray[1]] );
+ else if ( Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE) == WLC_OBJ_MUX )
+ fprintf( pFile, "%s ? %s : %s;\n", pNames[pArray[0]], pNames[pArray[1]], pNames[pArray[2]] );
+ else
+ fprintf( pFile, "<cannot write operation %s>;\n", Ndr_OperName(Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE)) );
+ }
+
+ fprintf( pFile, "\nendmodule\n\n" );
+ fclose( pFile );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// EXTERNAL PROCEDURES ///
+////////////////////////////////////////////////////////////////////////
+
+// creating a new module (returns pointer to the memory buffer storing the module info)
+static inline void * Ndr_ModuleCreate( int Name )
+{
+ Ndr_Data_t * p = malloc( sizeof(Ndr_Data_t) );
+ p->nSize = 0;
+ p->nCap = 16;
+ p->pHead = malloc( p->nCap );
+ p->pBody = malloc( p->nCap * 4 );
+ Ndr_DataPush( p, NDR_MODULE, 0 );
+ Ndr_DataPush( p, NDR_NAME, Name );
+ Ndr_DataAddTo( p, 0, p->nSize );
+ assert( p->nSize == 2 );
+ assert( Name );
+ return p;
+}
+
+// adding a new object (input/output/flop/intenal node) to an already module module
+static inline void Ndr_ModuleAddObject( void * pModule, int Type, int InstName,
+ int RangeLeft, int RangeRight, int fSignedness,
+ int nInputs, int * pInputs,
+ int nOutputs, int * pOutputs,
+ char * pFunction )
+{
+ Ndr_Data_t * p = (Ndr_Data_t *)pModule;
+ int Obj = p->nSize; assert( Type != 0 );
+ Ndr_DataResize( p, 6 );
+ Ndr_DataPush( p, NDR_OBJECT, 0 );
+ Ndr_DataPush( p, NDR_OPERTYPE, Type );
+ Ndr_DataPushRange( p, RangeLeft, RangeRight, fSignedness );
+ if ( InstName )
+ Ndr_DataPush( p, NDR_NAME, InstName );
+ Ndr_DataPushArray( p, NDR_INPUT, nInputs, pInputs );
+ Ndr_DataPushArray( p, NDR_OUTPUT, nOutputs, pOutputs );
+ Ndr_DataPushString( p, NDR_FUNCTION, pFunction );
+ Ndr_DataAddTo( p, Obj, p->nSize - Obj );
+ Ndr_DataAddTo( p, 0, p->nSize - Obj );
+ assert( (int)p->pBody[0] == p->nSize );
+}
+
+// deallocate the memory buffer
+static inline void Ndr_ModuleDelete( void * pModule )
+{
+ Ndr_Data_t * p = (Ndr_Data_t *)pModule;
+ if ( !p ) return;
+ free( p->pHead );
+ free( p->pBody );
+ free( p );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// FILE READING AND WRITING ///
+////////////////////////////////////////////////////////////////////////
+
+// file reading/writing
+static inline void * Ndr_ModuleRead( char * pFileName )
+{
+ Ndr_Data_t * p; int nFileSize, RetValue;
+ FILE * pFile = fopen( pFileName, "rb" );
+ if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for reading.\n", pFileName ); return NULL; }
+ // check file size
+ fseek( pFile, 0, SEEK_END );
+ nFileSize = ftell( pFile );
+ assert( nFileSize % 5 == 0 );
+ rewind( pFile );
+ // create structure
+ p = malloc( sizeof(Ndr_Data_t) );
+ p->nSize = p->nCap = nFileSize / 5;
+ p->pHead = malloc( p->nCap );
+ p->pBody = malloc( p->nCap * 4 );
+ RetValue = fread( p->pBody, 4, p->nCap, pFile );
+ RetValue = fread( p->pHead, 1, p->nCap, pFile );
+ assert( p->nSize == (int)p->pBody[0] );
+ fclose( pFile );
+ return p;
+}
+static inline void Ndr_ModuleWrite( char * pFileName, void * pModule )
+{
+ Ndr_Data_t * p = (Ndr_Data_t *)pModule; int RetValue;
+ FILE * pFile = fopen( pFileName, "wb" );
+ if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for writing.\n", pFileName ); return; }
+ RetValue = fwrite( p->pBody, 4, p->pBody[0], pFile );
+ RetValue = fwrite( p->pHead, 1, p->pBody[0], pFile );
+ fclose( pFile );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// TESTING PROCEDURE ///
+////////////////////////////////////////////////////////////////////////
+
+// This testing procedure creates and writes into a Verilog file the following module
+
+// module add10 ( input [3:0] a, output [3:0] s );
+// wire [3:0] const10 = 4'b1010;
+// assign s = a + const10;
+// endmodule
+
+static inline void Ndr_ModuleTest()
+{
+ // name IDs
+ int NameIdA = 2;
+ int NameIdS = 3;
+ int NameIdC = 4;
+ // array of fanins of node s
+ int Fanins[2] = { NameIdA, NameIdC };
+ // map name IDs into char strings
+ char * ppNames[5] = { NULL, "add10", "a", "s", "const10" };
+
+ // create a new module
+ void * pModule = Ndr_ModuleCreate( 1 );
+
+ // add objects to the modele
+ Ndr_ModuleAddObject( pModule, WLC_OBJ_PI, 0, 3, 0, 0, 0, NULL, 1, &NameIdA, NULL ); // no fanins
+ Ndr_ModuleAddObject( pModule, WLC_OBJ_CONST, 0, 3, 0, 0, 0, NULL, 1, &NameIdC, "4'b1010" ); // no fanins
+ Ndr_ModuleAddObject( pModule, WLC_OBJ_ARI_ADD, 0, 3, 0, 0, 2, Fanins, 1, &NameIdS, NULL ); // fanins are a and const10
+ Ndr_ModuleAddObject( pModule, WLC_OBJ_PO, 0, 3, 0, 0, 1, &NameIdS, 0, NULL, NULL ); // fanin is a
+
+ // write Verilog for verification
+ Ndr_ModuleWriteVerilog( NULL, pModule, ppNames );
+ Ndr_ModuleDelete( pModule );
+}
+
+
+//ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/saig/saigIsoSlow.c b/src/aig/saig/saigIsoSlow.c
index 58dc6596..a0e2d1d0 100644
--- a/src/aig/saig/saigIsoSlow.c
+++ b/src/aig/saig/saigIsoSlow.c
@@ -120,7 +120,7 @@ static int s_1kPrimes[ISO_MASK+1] = {
*/
#define ISO_MASK 0x3FF
-static int s_1kPrimes[ISO_MASK+1] =
+static unsigned int s_1kPrimes[ISO_MASK+1] =
//#define ISO_MASK 0xFF
//static int s_1kPrimes[0x3FF+1] =
{
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 6c0d96d1..fad0b804 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -825,6 +825,7 @@ extern ABC_DLL void Abc_NtkDontCareFree( Odc_Man_t * p );
extern ABC_DLL int Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth );
/*=== abcPrint.c ==========================================================*/
extern ABC_DLL float Abc_NtkMfsTotalSwitching( Abc_Ntk_t * pNtk );
+extern ABC_DLL float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk, int nPats, int Prob, int fVerbose );
extern ABC_DLL void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes, int fPower, int fGlitch, int fSkipBuf, int fSkipSmall, int fPrintMem );
extern ABC_DLL void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintFlops );
extern ABC_DLL void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2efa041c..7fc45f48 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -122,6 +122,7 @@ static int Abc_CommandMfs ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandMfs2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMfs3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTrace ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandGlitch ( Abc_Frame_t * pAbc, int argc, char ** argv );
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 );
@@ -316,6 +317,7 @@ static int Abc_CommandPSat ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDebug ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandEco ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmc2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmc3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -772,6 +774,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "mfs2", Abc_CommandMfs2, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "mfs3", Abc_CommandMfs3, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "trace", Abc_CommandTrace, 0 );
+ Cmd_CommandAdd( pAbc, "Synthesis", "glitch", Abc_CommandGlitch, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "speedup", Abc_CommandSpeedup, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "powerdown", Abc_CommandPowerdown, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "addbuffs", Abc_CommandAddBuffs, 1 );
@@ -966,6 +969,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 );
Cmd_CommandAdd( pAbc, "Verification", "iprove", Abc_CommandIProve, 1 );
Cmd_CommandAdd( pAbc, "Verification", "debug", Abc_CommandDebug, 0 );
+ Cmd_CommandAdd( pAbc, "Verification", "eco", Abc_CommandEco, 0 );
Cmd_CommandAdd( pAbc, "Verification", "bmc", Abc_CommandBmc, 0 );
Cmd_CommandAdd( pAbc, "Verification", "bmc2", Abc_CommandBmc2, 0 );
Cmd_CommandAdd( pAbc, "Verification", "bmc3", Abc_CommandBmc3, 1 );
@@ -5718,6 +5722,88 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandGlitch( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+ int nPats = 4000;
+ int Prob = 8;
+ int fVerbose = 1;
+ int c;
+
+ // set defaults
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NPvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nPats = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nPats < 1 )
+ goto usage;
+ break;
+ case 'P':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ Prob = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( Prob < 1 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( -1, "Empty network.\n" );
+ return 1;
+ }
+ if ( !Abc_NtkIsLogic(pNtk) )
+ {
+ Abc_Print( -1, "This command can only be applied to a mapped logic network.\n" );
+ return 1;
+ }
+ if ( Abc_NtkIsMappedLogic(pNtk) || Abc_NtkGetFaninMax(pNtk) <= 6 )
+ Abc_Print( 1, "Glitching adds %7.2f %% of signal transitions, compared to switching.\n", Abc_NtkMfsTotalGlitching(pNtk, nPats, Prob, fVerbose) );
+ else
+ printf( "Currently computes glitching only for K-LUT networks with K <= 6.\n" );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: glitch [-NP <num>] [-vh]\n" );
+ Abc_Print( -2, "\t comparing glitching activity to switching activity\n" );
+ Abc_Print( -2, "\t-N <num> : the number of random patterns to use (0 < num < 1000000) [default = %d]\n", nPats );
+ Abc_Print( -2, "\t-P <num> : once in how many cycles an input changes its value [default = %d]\n", Prob );
+ Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandSpeedup( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pNtkRes;
@@ -23865,6 +23951,50 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandEco( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Abc_NtkEco( char * pFileNames[3] );
+ char * pFileNames[3] = {NULL}; int c;
+ // set defaults
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( globalUtilOptind + 3 != argc )
+ {
+ Abc_Print( -1, "Expecting three file names on the command line.\n" );
+ return 1;
+ }
+ for ( c = 0; c < 3; c++ )
+ pFileNames[c] = argv[globalUtilOptind+c];
+ Abc_NtkEco( pFileNames );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: eco [-h]\n" );
+ Abc_Print( -2, "\t performs experimental ECO computation\n" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
diff --git a/src/base/abci/abcEco.c b/src/base/abci/abcEco.c
new file mode 100644
index 00000000..70a76729
--- /dev/null
+++ b/src/base/abci/abcEco.c
@@ -0,0 +1,58 @@
+/**CFile****************************************************************
+
+ FileName [abcEco.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Experimental procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcEco.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "base/abc/abc.h"
+#include "base/main/main.h"
+#include "map/mio/mio.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkEco( char * pFileNames[3] )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 4e588e2d..f758d0f0 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -923,9 +923,9 @@ void Abc_NtkPrintMiniMapping( int * pArray )
SeeAlso []
***********************************************************************/
-int * Abc_NtkOutputMiniMapping( void * pAbc0 )
+int * Abc_NtkOutputMiniMapping( Abc_Frame_t * pAbc )
{
- Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
+ //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
Abc_Ntk_t * pNtk;
Vec_Int_t * vMapping;
int * pArray;
@@ -977,9 +977,9 @@ void Abc_NtkTestMiniMapping( Abc_Ntk_t * p )
SeeAlso []
***********************************************************************/
-void Abc_NtkSetCiArrivalTime( void * pAbc0, int iCi, float Rise, float Fall )
+void Abc_NtkSetCiArrivalTime( Abc_Frame_t * pAbc, int iCi, float Rise, float Fall )
{
- Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
+ //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
Abc_Ntk_t * pNtk;
Abc_Obj_t * pNode;
if ( pAbc == NULL )
@@ -1001,9 +1001,9 @@ void Abc_NtkSetCiArrivalTime( void * pAbc0, int iCi, float Rise, float Fall )
pNode = Abc_NtkCi( pNtk, iCi );
Abc_NtkTimeSetArrival( pNtk, Abc_ObjId(pNode), Rise, Fall );
}
-void Abc_NtkSetCoRequiredTime( void * pAbc0, int iCo, float Rise, float Fall )
+void Abc_NtkSetCoRequiredTime( Abc_Frame_t * pAbc, int iCo, float Rise, float Fall )
{
- Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
+ //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
Abc_Ntk_t * pNtk;
Abc_Obj_t * pNode;
if ( pAbc == NULL )\
@@ -1037,9 +1037,9 @@ void Abc_NtkSetCoRequiredTime( void * pAbc0, int iCo, float Rise, float Fall )
SeeAlso []
***********************************************************************/
-void Abc_NtkSetAndGateDelay( void * pAbc0, float Delay )
+void Abc_NtkSetAndGateDelay( Abc_Frame_t * pAbc, float Delay )
{
- Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
+ //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
Abc_Ntk_t * pNtk;
if ( pAbc == NULL )
{
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 2129782f..ea91619c 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -351,9 +351,8 @@ void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDum
Abc_Print( 1," power =%7.2f", Abc_NtkMfsTotalSwitching(pNtk) );
if ( fGlitch )
{
- extern float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk );
if ( Abc_NtkIsLogic(pNtk) && Abc_NtkGetFaninMax(pNtk) <= 6 )
- Abc_Print( 1," glitch =%7.2f %%", Abc_NtkMfsTotalGlitching(pNtk) );
+ Abc_Print( 1," glitch =%7.2f %%", Abc_NtkMfsTotalGlitching(pNtk, 4000, 8, 0) );
else
printf( "\nCurrently computes glitching only for K-LUT networks with K <= 6." );
}
@@ -1744,7 +1743,7 @@ extern Gli_Man_t * Gli_ManAlloc( int nObjs, int nRegs, int nFanioPairs );
extern void Gli_ManStop( Gli_Man_t * p );
extern int Gli_ManCreateCi( Gli_Man_t * p, int nFanouts );
extern int Gli_ManCreateCo( Gli_Man_t * p, int iFanin );
-extern int Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, unsigned * puTruth );
+extern int Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, word * pGateTruth );
extern void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb, int fVerbose );
extern int Gli_ObjNumSwitches( Gli_Man_t * p, int iNode );
@@ -1761,13 +1760,14 @@ extern int Gli_ObjNumGlitches( Gli_Man_t * p, int iNode );
SeeAlso []
***********************************************************************/
-float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
+float Abc_NtkMfsTotalGlitchingLut( Abc_Ntk_t * pNtk, int nPats, int Prob, int fVerbose )
{
int nSwitches, nGlitches;
Gli_Man_t * p;
Vec_Ptr_t * vNodes;
Vec_Int_t * vFanins, * vTruth;
Abc_Obj_t * pObj, * pFanin;
+ Vec_Wrd_t * vTruths; word * pTruth;
unsigned * puTruth;
int i, k;
assert( Abc_NtkIsLogic(pNtk) );
@@ -1781,6 +1781,7 @@ float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
vNodes = Abc_NtkDfs( pNtk, 0 );
vFanins = Vec_IntAlloc( 6 );
vTruth = Vec_IntAlloc( 1 << 12 );
+ vTruths = Vec_WrdStart( Abc_NtkObjNumMax(pNtk) );
// derive network for glitch computation
p = Gli_ManAlloc( Vec_PtrSize(vNodes) + Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk),
@@ -1795,7 +1796,9 @@ float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
Abc_ObjForEachFanin( pObj, pFanin, k )
Vec_IntPush( vFanins, pFanin->iTemp );
puTruth = Hop_ManConvertAigToTruth( (Hop_Man_t *)pNtk->pManFunc, (Hop_Obj_t *)pObj->pData, Abc_ObjFaninNum(pObj), vTruth, 0 );
- pObj->iTemp = Gli_ManCreateNode( p, vFanins, Abc_ObjFanoutNum(pObj), puTruth );
+ pTruth = Vec_WrdEntryP( vTruths, Abc_ObjId(pObj) );
+ *pTruth = ((word)puTruth[Abc_ObjFaninNum(pObj) == 6] << 32) | (word)puTruth[0];
+ pObj->iTemp = Gli_ManCreateNode( p, vFanins, Abc_ObjFanoutNum(pObj), pTruth );
}
Abc_NtkForEachCo( pNtk, pObj, i )
Gli_ManCreateCo( p, Abc_ObjFanin0(pObj)->iTemp );
@@ -1816,6 +1819,72 @@ float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
Vec_PtrFree( vNodes );
Vec_IntFree( vTruth );
Vec_IntFree( vFanins );
+ Vec_WrdFree( vTruths );
+ return nSwitches ? 100.0*(nGlitches-nSwitches)/nSwitches : 0.0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the percentable of increased power due to glitching.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk, int nPats, int Prob, int fVerbose )
+{
+ int nSwitches, nGlitches;
+ Gli_Man_t * p;
+ Vec_Ptr_t * vNodes;
+ Vec_Int_t * vFanins;
+ Abc_Obj_t * pObj, * pFanin;
+ int i, k, nFaninMax = Abc_NtkGetFaninMax(pNtk);
+ if ( !Abc_NtkIsMappedLogic(pNtk) )
+ return Abc_NtkMfsTotalGlitchingLut( pNtk, nPats, Prob, fVerbose );
+ assert( Abc_NtkIsMappedLogic(pNtk) );
+ if ( nFaninMax > 16 )
+ {
+ printf( "Abc_NtkMfsTotalGlitching() This procedure works only for mapped networks with LUTs size up to 6 inputs.\n" );
+ return -1.0;
+ }
+ vNodes = Abc_NtkDfs( pNtk, 0 );
+ vFanins = Vec_IntAlloc( 6 );
+
+ // derive network for glitch computation
+ p = Gli_ManAlloc( Vec_PtrSize(vNodes) + Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk),
+ Abc_NtkLatchNum(pNtk), Abc_NtkGetTotalFanins(pNtk) + Abc_NtkCoNum(pNtk) );
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ pObj->iTemp = -1;
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ pObj->iTemp = Gli_ManCreateCi( p, Abc_ObjFanoutNum(pObj) );
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+ {
+ Vec_IntClear( vFanins );
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ Vec_IntPush( vFanins, pFanin->iTemp );
+ pObj->iTemp = Gli_ManCreateNode( p, vFanins, Abc_ObjFanoutNum(pObj), Mio_GateReadTruthP((Mio_Gate_t *)pObj->pData) );
+ }
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ Gli_ManCreateCo( p, Abc_ObjFanin0(pObj)->iTemp );
+
+ // compute glitching
+ Gli_ManSwitchesAndGlitches( p, nPats, 1.0/Prob, fVerbose );
+
+ // compute the ratio
+ nSwitches = nGlitches = 0;
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ if ( pObj->iTemp >= 0 )
+ {
+ nSwitches += Abc_ObjFanoutNum(pObj) * Gli_ObjNumSwitches(p, pObj->iTemp);
+ nGlitches += Abc_ObjFanoutNum(pObj) * Gli_ObjNumGlitches(p, pObj->iTemp);
+ }
+
+ Gli_ManStop( p );
+ Vec_PtrFree( vNodes );
+ Vec_IntFree( vFanins );
return nSwitches ? 100.0*(nGlitches-nSwitches)/nSwitches : 0.0;
}
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index b97f526f..abf56716 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -17,6 +17,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcDress2.c \
src/base/abci/abcDress3.c \
src/base/abci/abcDsd.c \
+ src/base/abci/abcEco.c \
src/base/abci/abcExact.c \
src/base/abci/abcExtract.c \
src/base/abci/abcFraig.c \
diff --git a/src/base/cmd/cmdHist.c b/src/base/cmd/cmdHist.c
index d1ff0a9d..36e546a7 100644
--- a/src/base/cmd/cmdHist.c
+++ b/src/base/cmd/cmdHist.c
@@ -30,6 +30,8 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+#define ABC_USE_HISTORY 1
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -99,7 +101,7 @@ void Cmd_HistoryAddCommand( Abc_Frame_t * p, const char * command )
***********************************************************************/
void Cmd_HistoryRead( Abc_Frame_t * p )
{
-#if defined(WIN32)
+#if defined(WIN32) && defined(ABC_USE_HISTORY)
char Buffer[ABC_MAX_STR];
FILE * pFile;
assert( Vec_PtrSize(p->aHistory) == 0 );
@@ -130,7 +132,7 @@ void Cmd_HistoryRead( Abc_Frame_t * p )
***********************************************************************/
void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit )
{
-#if defined(WIN32)
+#if defined(WIN32) && defined(ABC_USE_HISTORY)
FILE * pFile;
char * pStr;
int i;
@@ -160,7 +162,7 @@ void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit )
***********************************************************************/
void Cmd_HistoryPrint( Abc_Frame_t * p, int Limit )
{
-#if defined(WIN32)
+#if defined(WIN32) && defined(ABC_USE_HISTORY)
char * pStr;
int i;
Limit = Abc_MaxInt( 0, Vec_PtrSize(p->aHistory)-Limit );
diff --git a/src/base/main/abcapis.h b/src/base/main/abcapis.h
new file mode 100644
index 00000000..8c188b67
--- /dev/null
+++ b/src/base/main/abcapis.h
@@ -0,0 +1,105 @@
+/**CFile****************************************************************
+
+ FileName [abcapis.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Include this file in the external code calling ABC.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - September 29, 2012.]
+
+ Revision [$Id: abcapis.h,v 1.00 2012/09/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef MINI_AIG__abc_apis_h
+#define MINI_AIG__abc_apis_h
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+typedef struct Abc_Frame_t_ Abc_Frame_t;
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#ifdef WIN32
+ #ifdef WIN32_NO_DLL
+ #define ABC_DLLEXPORT
+ #define ABC_DLLIMPORT
+ #else
+ #define ABC_DLLEXPORT __declspec(dllexport)
+ #define ABC_DLLIMPORT __declspec(dllimport)
+ #endif
+#else /* defined(WIN32) */
+#define ABC_DLLIMPORT
+#endif /* defined(WIN32) */
+
+#ifndef ABC_DLL
+#define ABC_DLL ABC_DLLIMPORT
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// procedures to start and stop the ABC framework
+extern ABC_DLL void Abc_Start();
+extern ABC_DLL void Abc_Stop();
+
+// procedures to get the ABC framework (pAbc) and execute commands in it
+extern ABC_DLL Abc_Frame_t * Abc_FrameGetGlobalFrame();
+extern ABC_DLL int Cmd_CommandExecute( Abc_Frame_t * pAbc, const char * pCommandLine );
+
+// procedures to input/output 'mini AIG'
+extern ABC_DLL void Abc_NtkInputMiniAig( Abc_Frame_t * pAbc, void * pMiniAig );
+extern ABC_DLL void * Abc_NtkOutputMiniAig( Abc_Frame_t * pAbc );
+extern ABC_DLL void Abc_FrameGiaInputMiniAig( Abc_Frame_t * pAbc, void * p );
+extern ABC_DLL void * Abc_FrameGiaOutputMiniAig( Abc_Frame_t * pAbc );
+extern ABC_DLL void Abc_NtkSetFlopNum( Abc_Frame_t * pAbc, int nFlops );
+
+// procedures to input/output 'mini LUT'
+extern ABC_DLL void Abc_FrameGiaInputMiniLut( Abc_Frame_t * pAbc, void * pMiniLut );
+extern ABC_DLL void * Abc_FrameGiaOutputMiniLut( Abc_Frame_t * pAbc );
+
+// procedures to set CI/CO arrival/required times
+extern ABC_DLL void Abc_NtkSetCiArrivalTime( Abc_Frame_t * pAbc, int iCi, float Rise, float Fall );
+extern ABC_DLL void Abc_NtkSetCoRequiredTime( Abc_Frame_t * pAbc, int iCo, float Rise, float Fall );
+
+// procedure to set AND-gate delay to tech-independent synthesis and mapping
+extern ABC_DLL void Abc_NtkSetAndGateDelay( Abc_Frame_t * pAbc, float Delay );
+
+// procedures to return the mapped network
+extern ABC_DLL int * Abc_NtkOutputMiniMapping( Abc_Frame_t * pAbc );
+extern ABC_DLL void Abc_NtkPrintMiniMapping( int * pArray );
+
+// procedures to access verifization status and a counter-example
+extern ABC_DLL int Abc_FrameReadProbStatus( Abc_Frame_t * pAbc );
+extern ABC_DLL void * Abc_FrameReadCex( Abc_Frame_t * pAbc );
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/miniaig/abcapis.h b/src/base/main/abcapis_old.h
index eb8586fe..b2703bea 100644
--- a/src/aig/miniaig/abcapis.h
+++ b/src/base/main/abcapis_old.h
@@ -18,8 +18,8 @@
***********************************************************************/
-#ifndef MINI_AIG__abc_apis_h
-#define MINI_AIG__abc_apis_h
+#ifndef MINI_AIG__abc_apis_old_h
+#define MINI_AIG__abc_apis_old_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 89353fa6..a59a9a40 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -34,10 +34,8 @@
#include "misc/vec/vec.h"
#include "misc/st/st.h"
-ABC_NAMESPACE_HEADER_START
-// the framework containing all data
-typedef struct Abc_Frame_t_ Abc_Frame_t;
-ABC_NAMESPACE_HEADER_END
+// the framework containing all data is defined here
+#include "abcapis.h"
#include "base/cmd/cmd.h"
#include "base/io/ioAbc.h"
@@ -116,7 +114,7 @@ extern ABC_DLL void Abc_FrameSetBridgeMode();
extern ABC_DLL int Abc_FrameReadBmcFrames( Abc_Frame_t * p );
extern ABC_DLL int Abc_FrameReadProbStatus( Abc_Frame_t * p );
-extern ABC_DLL Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p );
+extern ABC_DLL void * Abc_FrameReadCex( Abc_Frame_t * p );
extern ABC_DLL Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p );
extern ABC_DLL Vec_Int_t * Abc_FrameReadStatusVec( Abc_Frame_t * p );
extern ABC_DLL Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p );
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 9647d020..cd4ff2c7 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -69,7 +69,7 @@ char * Abc_FrameReadFlag( char * pFlag ) { return Cmd_FlagRe
int Abc_FrameReadBmcFrames( Abc_Frame_t * p ) { return s_GlobalFrame->nFrames; }
int Abc_FrameReadProbStatus( Abc_Frame_t * p ) { return s_GlobalFrame->Status; }
-Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p ) { return s_GlobalFrame->pCex; }
+void * Abc_FrameReadCex( Abc_Frame_t * p ) { return s_GlobalFrame->pCex; }
Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ) { return s_GlobalFrame->vCexVec; }
Vec_Int_t * Abc_FrameReadStatusVec( Abc_Frame_t * p ) { return s_GlobalFrame->vStatuses; }
Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p ) { return s_GlobalFrame->vPoEquivs; }
diff --git a/src/base/wlc/wlcStdin.c b/src/base/wlc/wlcStdin.c
index 49c25ad0..3b747cc5 100644
--- a/src/base/wlc/wlcStdin.c
+++ b/src/base/wlc/wlcStdin.c
@@ -239,7 +239,7 @@ int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd )
return 0;
}
// report value of this variable
- Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, Abc_FrameReadCex(pAbc), pName, 16 );
+ Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, (Abc_Cex_t *)Abc_FrameReadCex(pAbc), pName, 16 );
Vec_StrFree( vInput );
fflush( stdout );
}
diff --git a/src/map/scl/sclCon.h b/src/map/scl/sclCon.h
index aeeffbf2..fe7776c1 100644
--- a/src/map/scl/sclCon.h
+++ b/src/map/scl/sclCon.h
@@ -56,8 +56,8 @@ struct Scl_Con_t_
#define SCL_OUTPUT_REQ "output_required"
#define SCL_OUTPUT_LOAD "output_load"
-#define SCL_DIRECTIVE(ITEM) "."ITEM
-#define SCL_DEF_DIRECTIVE(ITEM) ".default_"ITEM
+#define SCL_DIRECTIVE(ITEM) "."#ITEM
+#define SCL_DEF_DIRECTIVE(ITEM) ".default_"#ITEM
#define SCL_NUM 1000
#define SCL_INFINITY (0x3FFFFFFF)
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 501f9be6..60454752 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -288,7 +288,7 @@ int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
best_i = i;
for ( j = i+1; j < nSize; j++ )
// if ( pArray[j] < pArray[best_i] )
- if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] )
+ if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] ) // list lower priority first (these will be removed first)
best_i = j;
temp = pArray[i];
pArray[i] = pArray[best_i];
@@ -488,7 +488,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
/**Function*************************************************************
- Synopsis [Specialized sorting of flops based on cost.]
+ Synopsis [Specialized sorting of flops based on priority.]
Description []
@@ -497,17 +497,171 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
SeeAlso []
***********************************************************************/
-static inline void Vec_IntSelectSortCostReverseLit( int * pArray, int nSize, Vec_Int_t * vCosts )
+static inline int Vec_IntSelectSortPrioReverseLit( int * pArray, int nSize, Vec_Int_t * vPrios )
{
int i, j, best_i;
for ( i = 0; i < nSize-1; i++ )
{
best_i = i;
for ( j = i+1; j < nSize; j++ )
- if ( Vec_IntEntry(vCosts, Abc_Lit2Var(pArray[j])) > Vec_IntEntry(vCosts, Abc_Lit2Var(pArray[best_i])) )
+ if ( Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[j])) > Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[best_i])) ) // prefer higher priority
best_i = j;
ABC_SWAP( int, pArray[i], pArray[best_i] );
}
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs generalization using a different idea.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppCubeMin )
+{
+ int fUseMinAss = 0;
+ sat_solver * pSat = Pdr_ManFetchSolver( p, k );
+ int Order = Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
+ Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
+ int RetValue, Count = 0, iLit, Lits[2], nLits = Vec_IntSize( vLits1 );
+ // create free variables
+ int i, iUseVar, iAndVar;
+ iAndVar = Pdr_ManFreeVar(p, k);
+ for ( i = 1; i < nLits; i++ )
+ Pdr_ManFreeVar(p, k);
+ iUseVar = Pdr_ManFreeVar(p, k);
+ for ( i = 1; i < nLits; i++ )
+ Pdr_ManFreeVar(p, k);
+ assert( iUseVar == iAndVar + nLits );
+ // if there is only one positive literal, put it in front and always assume
+ if ( fUseMinAss )
+ {
+ for ( i = 0; i < pCube->nLits && Count < 2; i++ )
+ Count += !Abc_LitIsCompl(pCube->Lits[i]);
+ if ( Count == 1 )
+ {
+ for ( i = 0; i < pCube->nLits; i++ )
+ if ( !Abc_LitIsCompl(pCube->Lits[i]) )
+ break;
+ assert( i < pCube->nLits );
+ iLit = pCube->Lits[i];
+ for ( ; i > 0; i-- )
+ pCube->Lits[i] = pCube->Lits[i-1];
+ pCube->Lits[0] = iLit;
+ }
+ }
+ // add clauses for the additional AND-gates
+ Vec_IntForEachEntry( vLits1, iLit, i )
+ {
+ sat_solver_add_buffer_enable( pSat, iAndVar + i, Abc_Lit2Var(iLit), iUseVar + i, Abc_LitIsCompl(iLit) );
+ Vec_IntWriteEntry( vLits1, i, Abc_Var2Lit(iAndVar + i, 0) );
+ }
+ // add clauses for the additional OR-gate
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits1), Vec_IntLimit(vLits1) );
+ assert( RetValue == 1 );
+ // add implications
+ vLits1 = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
+ assert( Vec_IntSize(vLits1) == nLits );
+ Vec_IntForEachEntry( vLits1, iLit, i )
+ {
+ Lits[0] = Abc_Var2Lit(iUseVar + i, 1);
+ Lits[1] = iLit;
+ RetValue = sat_solver_addclause( pSat, Lits, Lits+2 );
+ assert( RetValue == 1 );
+ Vec_IntWriteEntry( vLits1, i, Abc_Var2Lit(iUseVar + i, 0) );
+ }
+ sat_solver_compress( pSat );
+ // perform minimization
+ if ( fUseMinAss )
+ {
+ if ( Count == 1 ) // always assume the only positive literal
+ {
+ if ( !sat_solver_push(pSat, Vec_IntEntry(vLits1, 0)) ) // UNSAT with the first (mandatory) literal
+ nLits = 1;
+ else
+ nLits = 1 + sat_solver_minimize_assumptions2( pSat, Vec_IntArray(vLits1)+1, nLits-1, p->pPars->nConfLimit );
+ sat_solver_pop(pSat); // unassume the first literal
+ }
+ else
+ nLits = sat_solver_minimize_assumptions2( pSat, Vec_IntArray(vLits1), nLits, p->pPars->nConfLimit );
+ Vec_IntShrink( vLits1, nLits );
+ }
+ else
+ {
+ // try removing one literal at a time in the old-fashioned way
+ int k, Entry;
+ Vec_Int_t * vTemp = Vec_IntAlloc( nLits );
+ for ( i = nLits - 1; i >= 0; i-- )
+ {
+ // if we are about to remove a positive lit, make sure at least one positive lit remains
+ if ( !Abc_LitIsCompl(Vec_IntEntry(vLits1, i)) )
+ {
+ Vec_IntForEachEntry( vLits1, iLit, k )
+ if ( iLit != -1 && k != i && !Abc_LitIsCompl(iLit) )
+ break;
+ if ( k == Vec_IntSize(vLits1) ) // no other positive literals, except the i-th one
+ continue;
+ }
+ // load remaining literals
+ Vec_IntClear( vTemp );
+ Vec_IntForEachEntry( vLits1, Entry, k )
+ if ( Entry != -1 && k != i )
+ Vec_IntPush( vTemp, Entry );
+ else if ( Entry != -1 ) // assume opposite literal
+ Vec_IntPush( vTemp, Abc_LitNot(Entry) );
+ // solve with assumptions
+ RetValue = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), p->pPars->nConfLimit, 0, 0, 0 );
+ // commit the literal
+ if ( RetValue == l_False )
+ {
+ int LitNot = Abc_LitNot(Vec_IntEntry(vLits1, i));
+ int RetValue = sat_solver_addclause( pSat, &LitNot, &LitNot+1 );
+ assert( RetValue );
+ }
+ // update the clause
+ if ( RetValue == l_False )
+ Vec_IntWriteEntry( vLits1, i, -1 );
+ }
+ Vec_IntFree( vTemp );
+ // compact
+ k = 0;
+ Vec_IntForEachEntry( vLits1, Entry, i )
+ if ( Entry != -1 )
+ Vec_IntWriteEntry( vLits1, k++, Entry );
+ Vec_IntShrink( vLits1, k );
+ }
+ // remap auxiliary literals into original literals
+ Vec_IntForEachEntry( vLits1, iLit, i )
+ Vec_IntWriteEntry( vLits1, i, pCube->Lits[Abc_Lit2Var(iLit)-iUseVar] );
+ // make sure the cube has at least one positive literal
+ if ( fUseMinAss )
+ {
+ Vec_IntForEachEntry( vLits1, iLit, i )
+ if ( !Abc_LitIsCompl(iLit) )
+ break;
+ if ( i == Vec_IntSize(vLits1) ) // has no positive literals
+ {
+ // find positive lit in the cube
+ for ( i = 0; i < pCube->nLits; i++ )
+ if ( !Abc_LitIsCompl(pCube->Lits[i]) )
+ break;
+ assert( i < pCube->nLits );
+ Vec_IntPush( vLits1, pCube->Lits[i] );
+// printf( "-" );
+ }
+// else
+// printf( "+" );
+ }
+ // create a subset cube
+ *ppCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits1), Vec_IntSize(vLits1) );
+ assert( !Pdr_SetIsInit(*ppCubeMin, -1) );
+ Order = 0;
+ return 0;
}
/**Function*************************************************************
@@ -532,7 +686,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
// if there is no induction, return
*ppCubeMin = NULL;
if ( p->pPars->fFlopOrder )
- Vec_IntSelectSortCostReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
+ Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0, 1 );
if ( p->pPars->fFlopOrder )
Vec_IntSelectSort( pCube->Lits, pCube->nLits );
@@ -543,8 +697,6 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
p->tGeneral += clock() - clk;
return 0;
}
-
- keep = p->pPars->fSkipDown ? NULL : Hash_IntAlloc( 1 );
// reduce clause using assumptions
// pCubeMin = Pdr_SetDup( pCube );
@@ -552,6 +704,31 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
if ( pCubeMin == NULL )
pCubeMin = Pdr_SetDup( pCube );
+ // perform simplified generalization
+ if ( p->pPars->fSimpleGeneral )
+ {
+ assert( pCubeMin->nLits > 0 );
+ if ( pCubeMin->nLits > 1 )
+ {
+ RetValue = Pdr_ManGeneralize2( p, k, pCubeMin, ppCubeMin );
+ Pdr_SetDeref( pCubeMin );
+ assert( ppCubeMin != NULL );
+ pCubeMin = *ppCubeMin;
+ }
+ *ppCubeMin = pCubeMin;
+ if ( p->pPars->fVeryVerbose )
+ {
+ printf("Cube:\n");
+ for ( i = 0; i < pCubeMin->nLits; i++)
+ printf ("%d ", pCubeMin->Lits[i]);
+ printf("\n");
+ }
+ p->tGeneral += Abc_Clock() - clk;
+ return 1;
+ }
+
+ keep = p->pPars->fSkipDown ? NULL : Hash_IntAlloc( 1 );
+
// perform generalization
if ( !p->pPars->fSkipGeneral )
{
@@ -691,9 +868,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
{
printf("Cube:\n");
for ( i = 0; i < pCubeMin->nLits; i++)
- {
- printf ("%d ", pCubeMin->Lits[i]);
- }
+ printf ("%d ", pCubeMin->Lits[i]);
printf("\n");
}
*ppCubeMin = pCubeMin;
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c
index cfc608b1..2ac94da5 100644
--- a/src/sat/bmc/bmcClp.c
+++ b/src/sat/bmc/bmcClp.c
@@ -353,11 +353,37 @@ int Bmc_CollapseIrredundantFull( Vec_Str_t * vSop, int nCubes, int nVars )
SeeAlso []
***********************************************************************/
+int Bmc_CollapseExpandRound2( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTemp, int nBTLimit, int fOnOffSetLit )
+{
+ // put into new array
+ int i, iLit, nLits;
+ Vec_IntClear( vTemp );
+ Vec_IntForEachEntry( vLits, iLit, i )
+ if ( iLit != -1 )
+ Vec_IntPush( vTemp, iLit );
+ assert( Vec_IntSize(vTemp) > 0 );
+ // assume condition literal
+ if ( fOnOffSetLit >= 0 )
+ sat_solver_push( pSat, fOnOffSetLit );
+ // minimize
+ nLits = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vTemp), Vec_IntSize(vTemp), nBTLimit );
+ Vec_IntShrink( vTemp, nLits );
+ // assume conditional literal
+ if ( fOnOffSetLit >= 0 )
+ sat_solver_pop( pSat );
+ // modify output literas
+ Vec_IntForEachEntry( vLits, iLit, i )
+ if ( iLit != -1 && Vec_IntFind(vTemp, iLit) == -1 )
+ Vec_IntWriteEntry( vLits, i, -1 );
+ return 0;
+}
+
int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon, int fOnOffSetLit )
{
int fProfile = 0;
int k, n, iLit, status;
abctime clk;
+ //return Bmc_CollapseExpandRound2( pSat, vLits, vTemp, nBTLimit, fOnOffSetLit );
// try removing one literal at a time
for ( k = Vec_IntSize(vLits) - 1; k >= 0; k-- )
{
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index df9ada8e..fe7e65fe 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -2168,6 +2168,153 @@ int sat_solver_solve_lexsat( sat_solver* s, int * pLits, int nLits )
return status;
}
+// This procedure is called on a set of assumptions to minimize their number.
+// The procedure relies on the fact that the current set of assumptions is UNSAT.
+// It receives and returns SAT solver without assumptions. It returns the number
+// of assumptions after minimization. The set of assumptions is returned in pLits.
+int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int nConfLimit )
+{
+ int i, k, nLitsL, nLitsR, nResL, nResR;
+ if ( nLits == 1 )
+ {
+ // since the problem is UNSAT, we will try to solve it without assuming the last literal
+ // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
+ int status = l_False;
+ int Temp = s->nConfLimit;
+ s->nConfLimit = nConfLimit;
+ status = sat_solver_solve_internal( s );
+ s->nConfLimit = Temp;
+ return (int)(status != l_False); // return 1 if the problem is not UNSAT
+ }
+ assert( nLits >= 2 );
+ nLitsL = nLits / 2;
+ nLitsR = nLits - nLitsL;
+ // assume the left lits
+ for ( i = 0; i < nLitsL; i++ )
+ if ( !sat_solver_push(s, pLits[i]) )
+ {
+ for ( k = i; k >= 0; k-- )
+ sat_solver_pop(s);
+ return sat_solver_minimize_assumptions( s, pLits, i+1, nConfLimit );
+ }
+ // solve for the right lits
+ nResL = sat_solver_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit );
+ for ( i = 0; i < nLitsL; i++ )
+ sat_solver_pop(s);
+ // swap literals
+// assert( nResL <= nLitsL );
+// for ( i = 0; i < nResL; i++ )
+// ABC_SWAP( int, pLits[i], pLits[nLitsL+i] );
+ veci_resize( &s->temp_clause, 0 );
+ for ( i = 0; i < nLitsL; i++ )
+ veci_push( &s->temp_clause, pLits[i] );
+ for ( i = 0; i < nResL; i++ )
+ pLits[i] = pLits[nLitsL+i];
+ for ( i = 0; i < nLitsL; i++ )
+ pLits[nResL+i] = veci_begin(&s->temp_clause)[i];
+ // assume the right lits
+ for ( i = 0; i < nResL; i++ )
+ if ( !sat_solver_push(s, pLits[i]) )
+ {
+ for ( k = i; k >= 0; k-- )
+ sat_solver_pop(s);
+ return sat_solver_minimize_assumptions( s, pLits, i+1, nConfLimit );
+ }
+ // solve for the left lits
+ nResR = sat_solver_minimize_assumptions( s, pLits + nResL, nLitsL, nConfLimit );
+ for ( i = 0; i < nResL; i++ )
+ sat_solver_pop(s);
+ return nResL + nResR;
+}
+
+// This is a specialized version of the above procedure with several custom changes:
+// - makes sure that at least one of the marked literals is preserved in the clause
+// - sets literals to zero when they do not have to be used
+// - sets literals to zero for disproved variables
+int sat_solver_minimize_assumptions2( sat_solver* s, int * pLits, int nLits, int nConfLimit )
+{
+ int i, k, nLitsL, nLitsR, nResL, nResR;
+ if ( nLits == 1 )
+ {
+ // since the problem is UNSAT, we will try to solve it without assuming the last literal
+ // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
+ int RetValue = 1, LitNot = Abc_LitNot(pLits[0]);
+ int status = l_False;
+ int Temp = s->nConfLimit;
+ s->nConfLimit = nConfLimit;
+
+ RetValue = sat_solver_push( s, LitNot ); assert( RetValue );
+ status = sat_solver_solve_internal( s );
+ sat_solver_pop( s );
+
+ // if the problem is UNSAT, add clause
+ if ( status == l_False )
+ {
+ RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
+ assert( RetValue );
+ }
+
+ s->nConfLimit = Temp;
+ return (int)(status != l_False); // return 1 if the problem is not UNSAT
+ }
+ assert( nLits >= 2 );
+ nLitsL = nLits / 2;
+ nLitsR = nLits - nLitsL;
+ // assume the left lits
+ for ( i = 0; i < nLitsL; i++ )
+ if ( !sat_solver_push(s, pLits[i]) )
+ {
+ for ( k = i; k >= 0; k-- )
+ sat_solver_pop(s);
+
+ // add clauses for these literal
+ for ( k = i+1; k > nLitsL; k++ )
+ {
+ int LitNot = Abc_LitNot(pLits[i]);
+ int RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
+ assert( RetValue );
+ }
+
+ return sat_solver_minimize_assumptions2( s, pLits, i+1, nConfLimit );
+ }
+ // solve for the right lits
+ nResL = sat_solver_minimize_assumptions2( s, pLits + nLitsL, nLitsR, nConfLimit );
+ for ( i = 0; i < nLitsL; i++ )
+ sat_solver_pop(s);
+ // swap literals
+// assert( nResL <= nLitsL );
+ veci_resize( &s->temp_clause, 0 );
+ for ( i = 0; i < nLitsL; i++ )
+ veci_push( &s->temp_clause, pLits[i] );
+ for ( i = 0; i < nResL; i++ )
+ pLits[i] = pLits[nLitsL+i];
+ for ( i = 0; i < nLitsL; i++ )
+ pLits[nResL+i] = veci_begin(&s->temp_clause)[i];
+ // assume the right lits
+ for ( i = 0; i < nResL; i++ )
+ if ( !sat_solver_push(s, pLits[i]) )
+ {
+ for ( k = i; k >= 0; k-- )
+ sat_solver_pop(s);
+
+ // add clauses for these literal
+ for ( k = i+1; k > nResL; k++ )
+ {
+ int LitNot = Abc_LitNot(pLits[i]);
+ int RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
+ assert( RetValue );
+ }
+
+ return sat_solver_minimize_assumptions2( s, pLits, i+1, nConfLimit );
+ }
+ // solve for the left lits
+ nResR = sat_solver_minimize_assumptions2( s, pLits + nResL, nLitsL, nConfLimit );
+ for ( i = 0; i < nResL; i++ )
+ sat_solver_pop(s);
+ return nResL + nResR;
+}
+
+
int sat_solver_nvars(sat_solver* s)
{
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 5a8483c1..5191b2cd 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -50,6 +50,8 @@ extern int sat_solver_simplify(sat_solver* s);
extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
extern int sat_solver_solve_internal(sat_solver* s);
extern int sat_solver_solve_lexsat(sat_solver* s, int * pLits, int nLits);
+extern int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int nConfLimit );
+extern int sat_solver_minimize_assumptions2( sat_solver* s, int * pLits, int nLits, int nConfLimit );
extern int sat_solver_push(sat_solver* s, int p);
extern void sat_solver_pop(sat_solver* s);
extern void sat_solver_set_resource_limits(sat_solver* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-05 08:16:38 +0000