merge

abclib.dsp

@@ -271,6 +271,10 @@ SOURCE=.\src\base\abci\abcDsd.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcEco.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcExact.c
 # End Source File
 # Begin Source File
@@ -695,6 +699,10 @@ SOURCE=.\src\base\io\ioWriteVerilog.c
 # PROP Default_Filter ""
 # Begin Source File
 
+SOURCE=.\src\base\main\abcapis.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\main\libSupport.c
 # End Source File
 # Begin Source File

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 );
     }

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,

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,

src/aig/miniaig/ndr.h

+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+

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] = 
 {

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 );

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);

src/base/abci/abcEco.c

+/**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
+

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 )
     {

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;
 }
 

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 \

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 );

src/base/main/abcapis.h

+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+

src/aig/miniaig/abcapis.h → 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                                ///

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 );  

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;    }        

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 );
     }

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)

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;

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-- )
     {

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)
 {

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);