|
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
C. L. Berman. Circuit width, register allocation, and reduced function graphs. Research Report RC 14129, Mathematical Sciences Dept., IBM T. J. Watson Research Center, 1988.
|
| |
2
|
C. L. Berman. Ordered binary decision diagrams and circuit structure. In ICCD, 1989.
|
| |
3
|
C. L. Berman, 1990. Personal Communication.
|
 |
4
|
Karl S. Brace , Richard L. Rudell , Randal E. Bryant, Efficient implementation of a BDD package, Proceedings of the 27th ACM/IEEE conference on Design automation, p.40-45, June 24-27, 1990, Orlando, Florida, United States
[doi> 10.1145/123186.123222]
|
| |
5
|
F. Brglez and H. Fujiwara. A neutral netlist of 10 combinational benchmark circuits and a target translator in FORTRAN. In ISGAS, 1985.
|
| |
6
|
|
| |
7
|
|
| |
8
|
E. Cerny and C. Mauras. Tautology checking using cross-controllability and cross-observability. In ICCAD, 1990.
|
| |
9
|
L. Claesen, editor. Proceedings o} the IMEC-IFIP International Workshop on Applied Formal Methods For Correct VLSI Design, Nov. 1989.
|
| |
10
|
A. L. Fisher and R. E. Bryant. Performance of COS- MOS on the IFIP workshop benchmarks. In Claesen {9}.
|
| |
11
|
|
| |
12
|
M. Fujita, H. Fujisawa, and N. Kawato. Evaluation and improvements of boolean comparison method based on binary decision diagrams. In ICCAD, 1988.
|
| |
13
|
M. Fujita, Y. Matsunaga, and H. Fujisawa. On the application of binary decision diagrams to formal hardware design. In Claesen {9}.
|
| |
14
|
D. Goldberg. Computer Arithmetic. Appendix A in {15}, 1990.
|
| |
15
|
|
| |
16
|
D. E. Long, 1990. Personal Communication.
|
| |
17
|
J. C. Madre. Benchmarks for tautology checking: Experimental results. In Claesen {9}.
|
| |
18
|
S. Malik, A. R. Wang, R. K. Brayton, and A. Sangiovanni-Vincentelli. Logic verification using binary decision diagrams in a logic synthesis environment. In ICCAD, 1988.
|
| |
19
|
S. Minato, N. Ishiura, and S. Yajima. Fast tautology checking using shared binary decision diagrams: Benchmark results. In Claesen {9}.
|
| |
20
|
J. A. Rees, N. I. Adams, and J. R. Meehan. The T Manual. Yale University, 4th edition, 1984.
|
| |
21
|
H. Simonis. Formal verification of multipliers. In Clae-
|
CITED BY 14
|
|
|
|
|
|
|
|
Gianpiero Cabodi , Paolo Camurati , Stefano Quer, Auxiliary variables for extending symbolic traversal techniques to data paths, Proceedings of the 31st annual conference on Design automation, p.289-293, June 06-10, 1994, San Diego, California, United States
|
|
|
Kiyoharu Hamaguchi , Akihito Morita , Shuzo Yajima, Efficient construction of binary moment diagrams for verifying arithmetic circuits, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.78-82, November 05-09, 1995, San Jose, California, United States
|
|
|
|
|
|
|
|
|
Woohyuk Lee , Abelardo Pardo , Jae-Young Jang , Gary Hachtel , Fabio Somenzi, Tearing based automatic abstraction for CTL model checking, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.76-81, November 10-14, 1996, San Jose, California, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|