John O'Leary
John O'Leary
Verified email at intel.com
TitleCited byYear
Formally verifying IEEE compliance of floating-point hardware
J O’Leary, X Zhao, R Gerth, CJH Seger
Intel Technology Journal 3 (1), 1-14, 1999
1521999
An industrially effective environment for formal hardware verification
CJH Seger, RB Jones, JW O'Leary, T Melham, MD Aagaard, C Barrett, ...
IEEE Transactions on Computer-Aided Design of Integrated Circuits and …, 2005
1072005
A reflective functional language for hardware design and theorem proving
J Grundy, T Melham, J O'leary
Journal of Functional Programming 16 (2), 157-196, 2006
822006
Verification of all circuits in a floating-point unit using word-level model checking
YA Chen, E Clarke, PH Ho, Y Hoskote, T Kam, M Khaira, J O'Leary, ...
International Conference on Formal Methods in Computer-Aided Design, 19-33, 1996
711996
Practical formal verification in microprocessor design
RB Jones, JW O'Leary, CJH Seger, MD Aagaard, TF Melham
IEEE design & test of computers 18 (4), 16-25, 2001
592001
Non-restoring integer square root: A case study in design by principled optimization
J O'Leary, M Leeser, J Hickey, M Aagaard
International Conference on Theorem Provers in Circuit Design, 52-71, 1994
581994
Verifying correctness of transactional memories
A Cohen, JW O'Leary, A Pnueli, MR Tuttle, LD Zuck
Formal Methods in Computer Aided Design (FMCAD'07), 37-44, 2007
522007
Synchronous elastic networks
S Krstic, J Cortadella, M Kishinevsky, J O'Leary
2006 Formal Methods in Computer Aided Design, 19-30, 2006
522006
Protocol verification using flows: An industrial experience
J O'Leary, M Talupur, MR Tuttle
2009 Formal Methods in Computer-Aided Design, 172-179, 2009
492009
Codesign of communication protocols
AS Wenban, JW O'Leary, GM Brown
Computer 26 (12), 46-52, 1993
491993
A methodology for large-scale hardware verification
MD Aagaard, RB Jones, TF Melham, JW O’leary, CJH Seger
International Conference on Formal Methods in Computer-Aided Design, 300-319, 2000
482000
Verification of a subtractive radix-2 square root algorithm and implementation
M Leeser, J O'Leary
Proceedings of ICCD'95 International Conference on Computer Design. VLSI in …, 1995
231995
Model checking transactional memory with Spin
J O'Leary, B Saha, MR Tuttle
2009 29th IEEE International Conference on Distributed Computing Systems …, 2009
202009
ATLAS: automatic term-level abstraction of RTL designs
BA Brady, RE Bryant, SA Seshia, JW O'Leary
Eighth ACM/IEEE International Conference on Formal Methods and Models for …, 2010
182010
HML: A hardware description language based on standard ML
J O'Leary, M Linderman, M Leeser, M Aagaard
Computer Hardware Description Languages and their applications, 327-334, 1993
181993
Synthesizable high level hardware descriptions: using statically typed two-level languages to guarantee verilog synthesizability
J Gillenwater, G Malecha, C Salama, AY Zhu, W Taha, J Grundy, ...
Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and …, 2008
162008
Synchronous emulation of asynchronous circuits
J O'Leary, G Brown
IEEE transactions on computer-aided design of integrated circuits and …, 1997
151997
HML: A hardware description language based on SML
J O'Leary, M Linderman, M Leeser, M Aagaard
Computer Hardware Description Languages and their Applications, IFIP …, 1993
131993
Retargeting a hardware compiler proof using protocol converters
G Brown, W Luk, J O'Leary
Proceedings of 1994 IEEE Symposium on Advanced Research in Asynchronous …, 1994
101994
Static consistency checking for Verilog wire interconnects
C Salama, G Malecha, W Taha, J Grundy, J O’Leary
Higher-Order and Symbolic Computation 24 (1-2), 81-114, 2011
92011
The system can't perform the operation now. Try again later.
Articles 1–20