Martin Povišer
|
de8620d777
|
Revert "pdr -X to write CEXes immediately"
This reverts commit e62e8ac528.
|
2024-08-12 22:53:53 +02:00 |
Martin Povišer
|
39f6fbb052
|
Revert "Fix pdr timing output"
This reverts commit c8d64b8682.
|
2024-08-12 22:53:48 +02:00 |
Martin Povišer
|
ec8419c84b
|
Revert "Improved anytime pdr"
This reverts commit 5444cf281c.
|
2024-08-12 22:53:40 +02:00 |
Jannis Harder
|
5444cf281c
|
Improved anytime pdr
(cherry picked from commit c832967200)
|
2024-08-07 15:46:44 +02:00 |
Jannis Harder
|
c8d64b8682
|
Fix pdr timing output
(cherry picked from commit acbe1b1f03)
|
2024-08-07 15:46:44 +02:00 |
Jannis Harder
|
e62e8ac528
|
pdr -X to write CEXes immediately
(cherry picked from commit f63471bdf5)
|
2024-08-07 15:46:44 +02:00 |
Alan Mishchenko
|
3fd42912ad
|
Suggested fix.
|
2024-05-16 06:24:18 -07:00 |
Alan Mishchenko
|
538ecb4515
|
Updating printouts.
|
2023-10-23 09:38:24 -07:00 |
Alan Mishchenko
|
ba64e78608
|
Changing declaration of Vec_Ptr_t sorting function to satisfy some compilers.
|
2021-09-26 11:30:54 -07:00 |
Alan Mishchenko
|
ee1bd8f0be
|
Fixing some update gcc.
|
2019-07-24 11:44:28 +07:00 |
Alan Mishchenko
|
d07608c052
|
Adding the possibility to specify file name in 'pdr'.
|
2019-04-22 12:14:31 -07:00 |
Alan Mishchenko
|
32315113ea
|
Various usability changes.
|
2018-11-18 21:03:26 -08:00 |
Alan Mishchenko
|
12908d3c25
|
Various usability changes.
|
2018-11-18 21:01:30 -08:00 |
Baruch Sterin
|
adce11979f
|
bridge relates: (1) fix netlist reader to read the latest version written by ZZ, (2) replace printf() with Abc_Print() in pdr so that it will not interfer with bridge messages
|
2017-09-15 23:28:57 -07:00 |
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
|
29cb71f98b
|
Integrating Satoko into pdr.
|
2017-08-16 12:08:55 +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
|
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 |
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
|
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 |
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 |
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 |
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 |
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 |
Yen-Sheng Ho
|
fdc0b471e5
|
working on incremental pdr
|
2017-02-18 14:38:08 -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 |
Yen-Sheng Ho
|
196b359183
|
started pdrIncr.c
|
2017-02-18 09:51:54 -08:00 |
Alan Mishchenko
|
bc010af4be
|
Promising modification of the generalization procedure in 'pdr'.
|
2017-02-17 14:10:32 -08:00 |
Alan Mishchenko
|
632ca7ed11
|
Promising alternative of CEX minimization in 'pdr'.
|
2017-02-16 13:37:46 -08:00 |