Alan Mishchenko
|
be49b0fa18
|
Changes to 'pdr' to run with updated Satoko.
|
2017-09-06 08:34:58 -07:00 |
|
Alan Mishchenko
|
f06056d85d
|
Changes to 'pdr' to run with updated Satoko.
|
2017-09-06 08:34:04 -07:00 |
|
Bruno Schmitt
|
ba8112ff3a
|
Fixing bronken C++ build; Satoko internal header, solver.h, should not be used in other packages
|
2017-08-29 09:40:51 +02:00 |
|
Alan Mishchenko
|
23d36a8d56
|
Integrating Satoko into 'bmc' and 'bmc2'.
|
2017-08-16 14:20:52 +07:00 |
|
Alan Mishchenko
|
29cb71f98b
|
Integrating Satoko into pdr.
|
2017-08-16 12:08:55 +07:00 |
|
Alan Mishchenko
|
2e56f44c66
|
Compiler warnings.
|
2017-07-22 11:41:17 +07:00 |
|
Alan Mishchenko
|
b1eaf714f2
|
Experiments with SAT sweeping.
|
2017-04-11 22:12:18 -07:00 |
|
Alan Mishchenko
|
79584f5e20
|
Experiments with SAT sweeping.
|
2017-04-11 21:06:42 -07:00 |
|
Yen-Sheng Ho
|
1531dd8ec5
|
%pdra: added an option -t for disabling trace reuse
|
2017-03-31 15:34:21 -07:00 |
|
Yen-Sheng Ho
|
04bd8631e0
|
merge
|
2017-03-31 07:42:06 -07:00 |
|
Yen-Sheng Ho
|
1cb140bb11
|
%pdra: fixed bugs
|
2017-03-30 13:53:18 -07:00 |
|
Yen-Sheng Ho
|
ecf91190d6
|
added callbacks to sat solvers in pdr
|
2017-03-29 23:00:29 -07:00 |
|
Yen-Sheng Ho
|
4d47904831
|
%pdra: fixed bugs
|
2017-03-29 14:20:40 -07:00 |
|
Alan Mishchenko
|
7285f1051e
|
Experiments with multipliers.
|
2017-03-28 23:28:04 -07:00 |
|
Yen-Sheng Ho
|
758270d663
|
%pdra: refactor
|
2017-03-27 15:18:35 -07:00 |
|
Yen-Sheng Ho
|
e6098d20be
|
%pdra: added a procedure to rebuild traces
|
2017-03-27 15:10:33 -07:00 |
|
Alan Mishchenko
|
036be3a541
|
Experiments with don't-cares.
|
2017-03-26 20:32:46 -07:00 |
|
Alan Mishchenko
|
d0ea4853ec
|
Experiments with multipliers.
|
2017-03-26 14:38:04 -07:00 |
|
Alan Mishchenko
|
1ac9d2997c
|
Experiments with don't-cares.
|
2017-03-22 13:04:24 -07:00 |
|
Alan Mishchenko
|
876c2c353a
|
Integration of new SAT sweeper.
|
2017-03-11 20:54:49 -08:00 |
|
Alan Mishchenko
|
5fbe218ff8
|
Improvements to ternary simulation.
|
2017-03-09 22:57:20 -08:00 |
|
Alan Mishchenko
|
d877074d8f
|
Improvements to ternary simulation.
|
2017-03-09 22:53:47 -08:00 |
|
Yen-Sheng Ho
|
154f4b642d
|
merge
|
2017-03-03 13:46:32 -08:00 |
|
Yen-Sheng Ho
|
7eac1f5766
|
added experimental codes
|
2017-03-02 17:31:30 -08:00 |
|
Alan Mishchenko
|
ff88edd664
|
Adding alternative generalization procedure.
|
2017-03-02 13:01:32 -08:00 |
|
Alan Mishchenko
|
f419f2e812
|
Adding alternative generalization procedure.
|
2017-03-01 20:30:19 -08:00 |
|
Alan Mishchenko
|
7747d89c90
|
Adding alternative generalization procedure.
|
2017-03-01 20:29:09 -08:00 |
|
Yen-Sheng Ho
|
18b47dfbd5
|
%pdra: added an option -u for checking comb. unsat
|
2017-03-01 14:57:43 -08:00 |
|
Alan Mishchenko
|
4ec5ee410d
|
Adding dump of trivial abstraction map at the beginning in &gla -m.
|
2017-02-25 16:22:31 -08:00 |
|
Alan Mishchenko
|
80773b9522
|
Adding dump of trivial abstraction map at the beginning in &gla -m.
|
2017-02-25 09:49:31 -08:00 |
|
Yen-Sheng Ho
|
ca0bdde9b3
|
changed how pdr -t cleans up abs flops
|
2017-02-23 10:54:53 -08:00 |
|
Yen-Sheng Ho
|
d5bbf9188c
|
added %pdra -a: run with pdr -nct
|
2017-02-23 08:48:53 -08:00 |
|
Alan Mishchenko
|
53b1d46b8d
|
Remapping flops in '%pdra.
|
2017-02-21 22:20:03 -08:00 |
|
Alan Mishchenko
|
96ccd24e6e
|
Changes to Visual Studio project file to support 'pdra'.
|
2017-02-21 20:39:52 -08:00 |
|
Alan Mishchenko
|
0e9f8093c3
|
Merged in ysho/abc (pull request #59)
added a new abstraction
|
2017-02-22 04:31:10 +00:00 |
|
Yen-Sheng Ho
|
c5e9506f5d
|
small tweaks in %pdra -p
|
2017-02-20 12:58:20 -08:00 |
|
Yen-Sheng Ho
|
9f43c84501
|
added options of checking and pushing to %pdra
|
2017-02-20 12:51:04 -08:00 |
|
Alan Mishchenko
|
ac1eb60db9
|
Experiments with SAT sweeping.
|
2017-02-20 12:32:32 -08:00 |
|
Yen-Sheng Ho
|
25ecc3d429
|
fixed a tricky bug: property should not be assumed true in the last frame
|
2017-02-19 19:57:44 -08:00 |
|
Yen-Sheng Ho
|
1a66a5823a
|
working on pdr with wla
|
2017-02-19 16:09:59 -08:00 |
|
Yen-Sheng Ho
|
2d1792040a
|
working on pdr with wla
|
2017-02-19 15:57:13 -08:00 |
|
Alan Mishchenko
|
99fe7dfe29
|
Experiments with SAT sweeping.
|
2017-02-19 12:51:38 -08:00 |
|
Yen-Sheng Ho
|
2732cbc1ee
|
working on pdr with wla
|
2017-02-19 12:31:28 -08:00 |
|
Yen-Sheng Ho
|
6cf289dadd
|
working on pdr with wla
|
2017-02-19 09:55:58 -08:00 |
|
Yen-Sheng Ho
|
fc0f3b8d0d
|
working on incremental pdr
|
2017-02-18 21:22:26 -08:00 |
|
Alan Mishchenko
|
27caed8dc8
|
Experiments with SAT sweeping.
|
2017-02-18 20:20:50 -08:00 |
|
Yen-Sheng Ho
|
fdc0b471e5
|
working on incremental pdr
|
2017-02-18 14:38:08 -08:00 |
|
Alan Mishchenko
|
429f52ce15
|
Experiments with SAT sweeping.
|
2017-02-18 14:20:10 -08:00 |
|
Yen-Sheng Ho
|
b93a805129
|
copied some functions from pdr
|
2017-02-18 12:43:03 -08:00 |
|
Yen-Sheng Ho
|
91a0a0fc3b
|
copied pdr_mansolve
|
2017-02-18 10:28:16 -08:00 |
|