Skip to content

Commit 5cdded3

Browse files
alanminkoalanminko
committed
Command %ufar.
1 parent 84fca2c commit 5cdded3

File tree

19 files changed

+4450
-1
lines changed

19 files changed

+4450
-1
lines changed

‎Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ MODULES := \
3636
src/misc/mem src/misc/bar src/misc/bbl src/misc/parse \
3737
src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \
3838
src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt src/opt/rar \
39-
src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd src/opt/eslim \
39+
src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd src/opt/eslim src/opt/ufar src/opt/untk src/opt/util \
4040
src/sat/bsat src/sat/xsat src/sat/satoko src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc src/sat/glucose src/sat/glucose2 src/sat/kissat src/sat/cadical \
4141
src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \
4242
src/bool/rsb src/bool/rpo \

‎src/base/main/mainInit.c‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -69,6 +69,7 @@ extern void Glucose_Init( Abc_Frame_t *pAbc );
6969
extern void Glucose_End( Abc_Frame_t * pAbc );
7070
extern void Glucose2_Init( Abc_Frame_t *pAbc );
7171
extern void Glucose2_End( Abc_Frame_t * pAbc );
72+
extern void Ufar_Init(Abc_Frame_t *pAbc);
7273

7374
static Abc_FrameInitializer_t* s_InitializerStart = NULL;
7475
static Abc_FrameInitializer_t* s_InitializerEnd = NULL;
@@ -123,6 +124,7 @@ void Abc_FrameInit( Abc_Frame_t * pAbc )
123124
Cba_Init( pAbc );
124125
Pla_Init( pAbc );
125126
Test_Init( pAbc );
127+
Ufar_Init( pAbc );
126128
Glucose_Init( pAbc );
127129
Glucose2_Init( pAbc );
128130
for( p = s_InitializerStart ; p ; p = p->next )

‎src/opt/ufar/UfarCmd.cpp‎

Lines changed: 336 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,336 @@
1+
/*
2+
* UifCmd.cpp
3+
*
4+
* Created on: Aug 25, 2015
5+
* Author: Yen-Sheng Ho
6+
*/
7+
8+
#include "base/wlc/wlc.h"
9+
#include "opt/ufar/UfarCmd.h"
10+
#include "opt/ufar/UfarMgr.h"
11+
#include "opt/untk/NtkNtk.h"
12+
#include "opt/util/util.h"
13+
14+
#include <iostream>
15+
#include <iomanip>
16+
#include <climits>
17+
#include <regex>
18+
19+
using namespace std;
20+
21+
static UFAR::UfarManager ufar_manager;
22+
23+
static int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv );
24+
static int Abc_CommandAnalyzeCex( Abc_Frame_t * pAbc, int argc, char ** argv );
25+
static int Abc_CommandCreateAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv );
26+
static int Abc_CommandCreateMiter( Abc_Frame_t * pAbc, int argc, char ** argv );
27+
static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv );
28+
29+
static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc ) { return (Wlc_Ntk_t *)pAbc->pAbcWlc; }
30+
static inline void Wlc_AbcFreeNtk( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc)); }
31+
static inline void Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ) { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk; }
32+
33+
34+
void Ufar_Init(Abc_Frame_t *pAbc)
35+
{
36+
//Cmd_CommandAdd( pAbc, "Word level Prove", "%%test", Abc_CommandTest, 0 );
37+
//Cmd_CommandAdd( pAbc, "Word level Prove", "%%cex", Abc_CommandAnalyzeCex, 0 );
38+
//Cmd_CommandAdd( pAbc, "Word level Prove", "%%abs", Abc_CommandCreateAbstraction, 0 );
39+
Cmd_CommandAdd( pAbc, "Word level", "%ufar", Abc_CommandProveUsingUif, 0 );
40+
//Cmd_CommandAdd( pAbc, "Word level Prove", "%%miter", Abc_CommandCreateMiter, 0 );
41+
}
42+
43+
static int Abc_CommandCreateMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
44+
{
45+
Wlc_Ntk_t * pNew = UFAR::CreateMiter(Wlc_AbcGetNtk(pAbc), 0);
46+
Wlc_AbcUpdateNtk(pAbc, pNew);
47+
return 0;
48+
}
49+
50+
static int Abc_CommandCreateAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
51+
{
52+
Wlc_Ntk_t * pNew = ufar_manager.BuildCurrentAbstraction();
53+
Wlc_AbcUpdateNtk(pAbc, pNew);
54+
return 0;
55+
}
56+
57+
static int Abc_CommandAnalyzeCex( Abc_Frame_t * pAbc, int argc, char ** argv )
58+
{
59+
if ( pAbc->pCex == NULL )
60+
{
61+
cout << "There is no CEX.\n";
62+
return 0;
63+
}
64+
65+
// ufar_manager.GetOperatorsInCex(pAbc->pCex);
66+
ufar_manager.FindUifPairsUsingCex(pAbc->pCex);
67+
68+
return 0;
69+
}
70+
71+
static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv )
72+
{
73+
if (Wlc_AbcGetNtk(pAbc) == NULL) {
74+
cout << "There is no current design.\n";
75+
return 0;
76+
}
77+
78+
OptMgr opt_mgr(argv[0]);
79+
opt_mgr.AddOpt("--norm", ufar_manager.params.fNorm ? "yes" : "no", "", "toggle using data type normalization");
80+
opt_mgr.AddOpt("--adder", "no", "", "toggle including adders");
81+
opt_mgr.AddOpt("--cexmin", ufar_manager.params.fCexMin ? "yes" : "no", "", "toggle using CEX minimization");
82+
opt_mgr.AddOpt("--sim", "none", "str", "use simulation and specify its setting");
83+
opt_mgr.AddOpt("-v", to_string(ufar_manager.params.iVerbosity), "num", "specify verbosity level");
84+
opt_mgr.AddOpt("--seq", to_string(ufar_manager.params.nSeqLookBack), "num", "specify the number of look-back frames (0 = no sequential UIF)");
85+
opt_mgr.AddOpt("--profile", "no", "", "dump time distribution");
86+
opt_mgr.AddOpt("--pba_uif", ufar_manager.params.fPbaUif ? "yes" : "no", "", "toggle using proof-based refinement for UIF pairs");
87+
opt_mgr.AddOpt("--lazysim", ufar_manager.params.fLazySim ? "yes" : "no", "", "toggle applying UIF pairs based on simulation");
88+
opt_mgr.AddOpt("--pbasim", ufar_manager.params.fPbaSim ? "yes" : "no", "", "toggle combining pba and sim");
89+
opt_mgr.AddOpt("--pbacex", ufar_manager.params.fPbaCex ? "yes" : "no", "", "toggle combining pba and cex");
90+
opt_mgr.AddOpt("--satmin", ufar_manager.params.fSatMin ? "yes" : "no", "", "toggle using sat-min in pba");
91+
opt_mgr.AddOpt("--cbawb", ufar_manager.params.fCbaWb ? "yes" : "no", "", "toggle using cex-based refinement for white boxing");
92+
opt_mgr.AddOpt("--grey", ufar_manager.params.fGrey ? "yes" : "no", "", "toggle using grey-box constraints");
93+
opt_mgr.AddOpt("--grey2", to_string(ufar_manager.params.nGrey), "float", "specify the greyness threshold");
94+
opt_mgr.AddOpt("--dump", "none", "str", "specify file name");
95+
opt_mgr.AddOpt("--dump-abs", "none", "str", "specify file name");
96+
opt_mgr.AddOpt("--par", "none", "str", "use parallel solvers");
97+
opt_mgr.AddOpt("--dump_states", "none", "str", "specify the name for the states file");
98+
opt_mgr.AddOpt("--read_states", "none", "str", "specify the name for the states file");
99+
opt_mgr.AddOpt("--sp", ufar_manager.params.fSuper_prove ? "yes" : "no", "", "toggle using super_prove");
100+
opt_mgr.AddOpt("--simp", ufar_manager.params.fSimple ? "yes" : "no", "", "toggle using simple (prove)");
101+
opt_mgr.AddOpt("--syn", ufar_manager.params.fSyn ? "yes" : "no", "", "toggle using simple synthesis");
102+
opt_mgr.AddOpt("--pth", ufar_manager.params.fPthread ? "yes" : "no", "", "toggle using pthreads");
103+
opt_mgr.AddOpt("--onewb", to_string(ufar_manager.params.iOneWb), "int", "specify the mode for one-white-boxing");
104+
opt_mgr.AddOpt("--timeout", to_string(ufar_manager.params.nTimeout), "num", "specify the timeout (sec)");
105+
opt_mgr.AddOpt("--exp", to_string(ufar_manager.params.iExp), "int", "specify the exp mode");
106+
opt_mgr.AddOpt("--miter", "yes", "", "toggle mitering the problem");
107+
opt_mgr.AddOpt("--under", "-1", "num", "try under-approximation with the given size");
108+
if(!opt_mgr.Parse(argc, argv)) {
109+
opt_mgr.PrintUsage();
110+
cout << "\n This command was developed by Yen-Sheng Ho at UC Berkeley in 2015.\n";
111+
cout << " https://people.eecs.berkeley.edu/~alanmi/publications/2016/fmcad16_uif.pdf \n";
112+
return 0;
113+
}
114+
115+
if(opt_mgr["--norm"])
116+
ufar_manager.params.fNorm ^= 1;
117+
if(opt_mgr["--cexmin"])
118+
ufar_manager.params.fCexMin ^= 1;
119+
if(opt_mgr["--pba_uif"])
120+
ufar_manager.params.fPbaUif ^= 1;
121+
if(opt_mgr["--pbasim"])
122+
ufar_manager.params.fPbaSim ^= 1;
123+
if(opt_mgr["--pbacex"])
124+
ufar_manager.params.fPbaCex ^= 1;
125+
if(opt_mgr["--satmin"])
126+
ufar_manager.params.fSatMin ^= 1;
127+
if(opt_mgr["--cbawb"])
128+
ufar_manager.params.fCbaWb ^= 1;
129+
if(opt_mgr["--grey"])
130+
ufar_manager.params.fGrey ^= 1;
131+
if(opt_mgr["--grey2"])
132+
ufar_manager.params.nGrey = stof(opt_mgr.GetOptVal("--grey2"));
133+
if(opt_mgr["--sp"])
134+
ufar_manager.params.fSuper_prove ^= 1;
135+
if(opt_mgr["--simp"])
136+
ufar_manager.params.fSimple ^= 1;
137+
if(opt_mgr["--syn"])
138+
ufar_manager.params.fSyn ^= 1;
139+
if(opt_mgr["--pth"])
140+
ufar_manager.params.fPthread ^= 1;
141+
if(opt_mgr["--onewb"])
142+
ufar_manager.params.iOneWb = stoi(opt_mgr.GetOptVal("--onewb"));
143+
if(opt_mgr["--exp"])
144+
ufar_manager.params.iExp = stoi(opt_mgr.GetOptVal("--exp"));
145+
if(opt_mgr["--par"])
146+
ufar_manager.params.parSetting = opt_mgr.GetOptVal("--par");
147+
if(opt_mgr["--sim"])
148+
ufar_manager.params.simSetting = opt_mgr.GetOptVal("--sim");
149+
if(opt_mgr["--dump_states"]) {
150+
smatch sub_match;
151+
string option = opt_mgr.GetOptVal("--dump_states");
152+
if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
153+
ufar_manager.params.fileStatesOut = sub_match[1].str();
154+
else
155+
ufar_manager.params.fileStatesOut = opt_mgr.GetOptVal("--dump_states");
156+
}
157+
if(opt_mgr["--read_states"])
158+
ufar_manager.params.fileStatesIn = opt_mgr.GetOptVal("--read_states");
159+
if(opt_mgr["--lazysim"])
160+
ufar_manager.params.fLazySim ^= 1;
161+
if(opt_mgr["-v"])
162+
ufar_manager.params.iVerbosity = stoi(opt_mgr.GetOptVal("-v"));
163+
if(opt_mgr["--timeout"])
164+
ufar_manager.params.nTimeout = stoi(opt_mgr.GetOptVal("--timeout"));
165+
if(opt_mgr["--seq"])
166+
ufar_manager.params.nSeqLookBack = stoi(opt_mgr.GetOptVal("--seq"));
167+
if(opt_mgr["--dump-abs"]) {
168+
smatch sub_match;
169+
string option = opt_mgr.GetOptVal("--dump-abs");
170+
if(regex_search(option, sub_match, regex(R"(/?(\w+)\.v$)")))
171+
ufar_manager.params.fileAbs = sub_match[1].str();
172+
else
173+
ufar_manager.params.fileAbs = opt_mgr.GetOptVal("--dump");
174+
}
175+
if(opt_mgr["--dump"]) {
176+
smatch sub_match;
177+
string option = opt_mgr.GetOptVal("--dump");
178+
if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
179+
ufar_manager.params.fileName = sub_match[1].str();
180+
else
181+
ufar_manager.params.fileName = opt_mgr.GetOptVal("--dump");
182+
}
183+
184+
// ufar_manager.DumpParams();
185+
LogT::prefix = "UIF_PROVE";
186+
187+
set<unsigned> set_op_types;
188+
set_op_types.insert(WLC_OBJ_ARI_MULTI);
189+
if (opt_mgr["--adder"])
190+
set_op_types.insert(WLC_OBJ_ARI_ADD);
191+
if (!UFAR::HasOperator(Wlc_AbcGetNtk(pAbc), set_op_types)) {
192+
cout << "There is no operator for UIF.\n";
193+
return 0;
194+
}
195+
196+
Wlc_Ntk_t * pNew = NULL;
197+
timeval t1, t2;
198+
gettimeofday(&t1, NULL);
199+
200+
if (!opt_mgr["--miter"]) {
201+
if (Wlc_NtkPoNum(Wlc_AbcGetNtk(pAbc)) != 2) {
202+
cout << "The current design doesn't have dual outputs.\n";
203+
return 0;
204+
}
205+
pNew = UFAR::CreateMiter(Wlc_AbcGetNtk(pAbc), 0);
206+
Wlc_AbcUpdateNtk(pAbc, pNew);
207+
}
208+
209+
if (ufar_manager.params.fNorm) {
210+
pNew = UFAR::NormalizeDataTypes(Wlc_AbcGetNtk(pAbc), set_op_types, true);
211+
Wlc_AbcUpdateNtk(pAbc, pNew);
212+
}
213+
214+
if (opt_mgr["--under"]) {
215+
pNew = UFAR::MakeUnderApprox(Wlc_AbcGetNtk(pAbc), stoi(opt_mgr.GetOptVal("--under")));
216+
Wlc_AbcUpdateNtk(pAbc, pNew);
217+
pNew = UFAR::MakeUnderApprox2(Wlc_AbcGetNtk(pAbc), set_op_types, stoi(opt_mgr.GetOptVal("--under")));
218+
Wlc_AbcUpdateNtk(pAbc, pNew);
219+
Wlc_WriteVer(Wlc_AbcGetNtk(pAbc), "UND.v", 0, 0);
220+
}
221+
222+
Gia_Man_t * pGia = UFAR::BitBlast(Wlc_AbcGetNtk(pAbc));
223+
Gia_ManPrintStats( pGia, NULL );
224+
Gia_ManStop( pGia );
225+
226+
ufar_manager.Initialize(Wlc_AbcGetNtk(pAbc), set_op_types);
227+
228+
int ret = ufar_manager.PerformUIFProve(t1);
229+
if (ret == 1) {
230+
LOG(0) << "Proved by UIF (UNSAT).";
231+
} else if (ret == 0) {
232+
LOG(0) << "Falsified by UIF (SAT).";
233+
} else {
234+
LOG(0) << "Undecided by UIF.";
235+
}
236+
237+
gettimeofday(&t2, NULL);
238+
unsigned tTotal = elapsed_time_usec(t1, t2);
239+
if(opt_mgr["--profile"]) {
240+
auto log_profile = [&](const string& str, abctime t) {
241+
LOG(1) << str << " time = " << fixed << setprecision(4) << setw(8) << (double)t/1000000 << " sec [" << setw(7) << (double)t/tTotal*100 << "%]";
242+
};
243+
log_profile("BLSolver ", ufar_manager.profile.tBLSolver);
244+
log_profile("UifRefine ", ufar_manager.profile.tUifRefine);
245+
log_profile("WbRefine ", ufar_manager.profile.tWbRefine);
246+
log_profile("UifSim ", ufar_manager.profile.tUifSim);
247+
log_profile("GbRefine ", ufar_manager.profile.tGbRefine);
248+
}
249+
250+
LOG(0) << "Time = " << setprecision(5) << ((double) (tTotal) / 1000000) << " sec";
251+
252+
return 0;
253+
}
254+
255+
static int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
256+
{
257+
LogT::prefix = "TEST::";
258+
OptMgr opt_mgr(argv[0]);
259+
opt_mgr.AddOpt("--ntk", "none", "str", "specify the file name (*.aig) for the input network");
260+
opt_mgr.AddOpt("--adder", "no", "", "toggle including adders");
261+
if(!opt_mgr.Parse(argc, argv)) {
262+
opt_mgr.PrintUsage();
263+
return 0;
264+
}
265+
set<unsigned> set_op_types;
266+
set_op_types.insert(WLC_OBJ_ARI_MULTI);
267+
if(opt_mgr["--adder"]) {
268+
set_op_types.insert(WLC_OBJ_ARI_ADD);
269+
}
270+
Wlc_Ntk_t * pNew = UFAR::AddConstFlops(Wlc_AbcGetNtk(pAbc), set_op_types);
271+
Wlc_AbcUpdateNtk(pAbc, pNew);
272+
return 0;
273+
274+
#if 0
275+
opt_mgr.AddOpt("--ntk", "none", "str", "specify the file name (*.aig) for the input network");
276+
opt_mgr.AddOpt("--inv", "none", "str", "specify the file name (*.pla) for the invariant");
277+
if(!opt_mgr.Parse(argc, argv)) {
278+
opt_mgr.PrintUsage();
279+
return 0;
280+
}
281+
282+
string nameNtk = opt_mgr.GetOptVal("--ntk");
283+
string nameInv = opt_mgr.GetOptVal("--inv");
284+
UFAR::TestInvariant(nameNtk, nameInv);
285+
#endif
286+
#if 0
287+
set<unsigned> set_op_types;
288+
set_op_types.insert(WLC_OBJ_ARI_MULTI);
289+
290+
OptMgr opt_mgr(argv[0]);
291+
opt_mgr.AddOpt("--cube", "no", "", "toggle using cubes for interpolants");
292+
if(!opt_mgr.Parse(argc, argv)) {
293+
opt_mgr.PrintUsage();
294+
return 0;
295+
}
296+
297+
UFAR::TestITP(Wlc_AbcGetNtk(pAbc), set_op_types, opt_mgr["--cube"]);
298+
#endif
299+
#if 0
300+
if ( Wlc_AbcGetNtk(pAbc) == NULL ) {
301+
cout << "There is no current design.\n";
302+
return 0;
303+
}
304+
305+
if (Wlc_NtkPoNum(Wlc_AbcGetNtk(pAbc)) != 2) {
306+
cout << "The current design doesn't have dual outputs.\n";
307+
return 0;
308+
}
309+
310+
set<unsigned> set_op_types;
311+
set_op_types.insert(WLC_OBJ_ARI_MULTI);
312+
if (!UFAR::HasOperator(Wlc_AbcGetNtk(pAbc), set_op_types)) {
313+
cout << "There is no operator for UIF.\n";
314+
return 0;
315+
}
316+
317+
Wlc_Ntk_t * pNew = NULL;
318+
319+
pNew = UFAR::CreateMiter(Wlc_AbcGetNtk(pAbc), 0);
320+
Wlc_AbcUpdateNtk(pAbc, pNew);
321+
322+
pNew = UFAR::NormalizeDataTypes(Wlc_AbcGetNtk(pAbc), set_op_types, true);
323+
Wlc_AbcUpdateNtk(pAbc, pNew);
324+
325+
ufar_manager.Initialize(Wlc_AbcGetNtk(pAbc), set_op_types);
326+
ufar_manager.DumpMgrInfo();
327+
328+
pNew = ufar_manager.BuildCurrentAbstraction();
329+
Wlc_AbcUpdateNtk(pAbc, pNew);
330+
331+
332+
return 0;
333+
#endif
334+
}
335+
336+

‎src/opt/ufar/UfarCmd.h‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
/*
2+
* UifCmd.h
3+
*
4+
* Created on: Aug 25, 2015
5+
* Author: Yen-Sheng Ho
6+
*/
7+
8+
#ifndef SRC_EXT2_UIF_UIFCMD_H_
9+
#define SRC_EXT2_UIF_UIFCMD_H_
10+
11+
#include "base/main/mainInt.h"
12+
13+
#ifdef __cplusplus
14+
extern "C" {
15+
#endif
16+
17+
void Ufar_Init(Abc_Frame_t *pAbc);
18+
19+
#ifdef __cplusplus
20+
}
21+
#endif
22+
23+
#endif /* SRC_EXT2_UIF_UIFCMD_H_ */

0 commit comments

Comments
 (0)