1
2 /**Function*************************************************************
3
4 Synopsis []
5
6 Description []
7
8 SideEffects []
9
10 SeeAlso []
11
12 ***********************************************************************/
Abc_CommandUnfold2(Abc_Frame_t * pAbc,int argc,char ** argv)13 int Abc_CommandUnfold2( Abc_Frame_t * pAbc, int argc, char ** argv )
14 {
15 Abc_Ntk_t * pNtk, * pNtkRes;
16 int nFrames;
17 int nConfs;
18 int nProps;
19 int fStruct = 0;
20 int fOldAlgo = 0;
21 int fVerbose;
22 int c;
23 extern Abc_Ntk_t * Abc_NtkDarUnfold2( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose );
24 pNtk = Abc_FrameReadNtk(pAbc);
25 // set defaults
26 nFrames = 1;
27 nConfs = 1000;
28 nProps = 1000;
29 fVerbose = 0;
30 Extra_UtilGetoptReset();
31 while ( ( c = Extra_UtilGetopt( argc, argv, "CPvh" ) ) != EOF )
32 {
33 switch ( c )
34 {
35 /* case 'F': */
36 /* if ( globalUtilOptind >= argc ) */
37 /* { */
38 /* Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); */
39 /* goto usage; */
40 /* } */
41 /* nFrames = atoi(argv[globalUtilOptind]); */
42 /* globalUtilOptind++; */
43 /* if ( nFrames < 0 ) */
44 /* goto usage; */
45 /* break; */
46 case 'C':
47 if ( globalUtilOptind >= argc )
48 {
49 Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
50 goto usage;
51 }
52 nConfs = atoi(argv[globalUtilOptind]);
53 globalUtilOptind++;
54 if ( nConfs < 0 )
55 goto usage;
56 break;
57 case 'P':
58 if ( globalUtilOptind >= argc )
59 {
60 Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
61 goto usage;
62 }
63 nProps = atoi(argv[globalUtilOptind]);
64 globalUtilOptind++;
65 if ( nProps < 0 )
66 goto usage;
67 break;
68 case 'v':
69 fVerbose ^= 1;
70 break;
71 case 'h':
72 goto usage;
73 default:
74 goto usage;
75 }
76 }
77 if ( pNtk == NULL )
78 {
79 Abc_Print( -1, "Empty network.\n" );
80 return 1;
81 }
82 if ( Abc_NtkIsComb(pNtk) )
83 {
84 Abc_Print( -1, "The network is combinational.\n" );
85 return 0;
86 }
87 if ( !Abc_NtkIsStrash(pNtk) )
88 {
89 Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
90 return 0;
91 }
92 if ( Abc_NtkConstrNum(pNtk) > 0 )
93 {
94 Abc_Print( -1, "Constraints are already extracted.\n" );
95 return 0;
96 }
97 if ( Abc_NtkPoNum(pNtk) > 1 && !fStruct )
98 {
99 Abc_Print( -1, "Functional constraint extraction works for single-output miters (use \"orpos\").\n" );
100 return 0;
101 }
102 // modify the current network
103 pNtkRes = Abc_NtkDarUnfold2( pNtk, nFrames, nConfs, nProps, fStruct, fOldAlgo, fVerbose );
104 if ( pNtkRes == NULL )
105 {
106 Abc_Print( 1,"Transformation has failed.\n" );
107 return 0;
108 }
109 // replace the current network
110 Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
111 return 0;
112 usage:
113 Abc_Print( -2, "usage: unfold2 [-FCP num] [-savh]\n" );
114 Abc_Print( -2, "\t unfold hidden constraints as separate outputs\n" );
115 Abc_Print( -2, "\t-C num : the max number of conflicts in SAT solving [default = %d]\n", nConfs );
116 Abc_Print( -2, "\t-P num : the max number of constraint propagations [default = %d]\n", nProps );
117 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
118 Abc_Print( -2, "\t-h : print the command usage\n");
119 return 1;
120 }
121
122
123
Abc_CommandFold2(Abc_Frame_t * pAbc,int argc,char ** argv)124 int Abc_CommandFold2( Abc_Frame_t * pAbc, int argc, char ** argv )
125 {
126 Abc_Ntk_t * pNtk, * pNtkRes;
127 int fCompl;
128 int fVerbose;
129 int c;
130 extern Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose , int);
131 pNtk = Abc_FrameReadNtk(pAbc);
132 // set defaults
133 fCompl = 0;
134 fVerbose = 0;
135 Extra_UtilGetoptReset();
136 while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF )
137 {
138 switch ( c )
139 {
140 /* case 'c': */
141 /* fCompl ^= 1; */
142 /* break; */
143 case 'v':
144 fVerbose ^= 1;
145 break;
146 case 'h':
147 goto usage;
148 default:
149 goto usage;
150 }
151 }
152 if ( pNtk == NULL )
153 {
154 Abc_Print( -1, "Empty network.\n" );
155 return 1;
156 }
157 if ( !Abc_NtkIsStrash(pNtk) )
158 {
159 Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
160 return 0;
161 }
162 if ( Abc_NtkConstrNum(pNtk) == 0 )
163 {
164 Abc_Print( 0, "The network has no constraints.\n" );
165 return 0;
166 }
167 if ( Abc_NtkIsComb(pNtk) )
168 Abc_Print( 0, "The network is combinational.\n" );
169 // modify the current network
170 pNtkRes = Abc_NtkDarFold2( pNtk, fCompl, fVerbose ,0);
171 if ( pNtkRes == NULL )
172 {
173 Abc_Print( 1,"Transformation has failed.\n" );
174 return 0;
175 }
176 // replace the current network
177 Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
178 return 0;
179 usage:
180 Abc_Print( -2, "usage: fold [-cvh]\n" );
181 Abc_Print( -2, "\t folds constraints represented as separate outputs\n" );
182 // Abc_Print( -2, "\t-c : toggle complementing constraints while folding [default = %s]\n", fCompl? "yes": "no" );
183 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
184 Abc_Print( -2, "\t-h : print the command usage\n");
185 return 1;
186 }
187