Many of Mark's Publications

2015

• “Extending ACL2 with SMT Solvers”, with Yan Peng, in Proceedings of the 2015 ACL2 Workshop, Oct. 2015.
• “Integrating SMT with Theorem Proving for Analog/Mixed-Signal Circuit Verification”, with Yan Peng, in 7^th NASA Formal Methods Symposium, Apr. 2015.

2014

• “Response property checking via distributed state space exploration”, with Bradley D. Bingham, in 2014 Conference on Formal Methods in Computer Aided Design, Oct. 2014.
• “Verifying Global Start-Up for a Möbius Ring-Oscillator”, with Chao Yan and Suwen Yang, Formal Methods in System Design, vol. 45, no. 2, Oct. 2014.

2013

• “Verifying Global Convergence for a Digital Phase-Locked Loop”, with Jijie Wei, Yan Peng, and Ge Yu, in 2013 Conference on Formal Methods in Computer Aided Design, Oct. 2013.
• “Cache Prefetching and Speculation on Multi-Threaded Processors”, with Tarik Ono, in 2013 IEEE Pacific Rim Conference on Communication, Computers, and Signal Processing” Aug. 2013.
• “Distributed Explicit State Model Checking of Deadlock Freedom” with Brad Bingham, Jesse Bingham, and John Erickson, in 25^th International Conference on Computer Aided Verification, July, 2013.

2012

• “Oscillator Verification with Probability One” with Chao Yan, in 2012 Conference on Formal Methods in Computer Aided Design, Oct. 2012.
• “Modeling Energy-Time Trade-Offs in VLSI Computation”, with Brad D. Bingham, IEEE Transactions on Computers vol. 61, no. 4, Apr. 2012.

2011

• “Parameterized Verification of Deadlock Freedom in Symmetric Cache Coherence Protocols” with Brad D. Bingham and Jesse D. Bingham, in 2011 Conference on Formal Methods in Computer Aided Design, Nov. 2011.
• “On the Energy Complexity of Parallel Algorithms” with Vijay A. Korthikanti and Gul Agha, in 2011 International Conference on Parallel Processing, Sep. 2011.
• “Synchronizer Performance in Deep-Submicron Technology” with Suwen Yang and Ian W. Jones, 2011 International Symposium on Asynchronous Circuits and Systems, Apr. 2011 (Best Paper Award).

2010

• “Varactor-Based Signal Restoration for Near-Speed-of-Light Global Interconnect” with Suwen Yang, Robert Drost, Shahriar Mirabbasi, and Frank O’Mahony, in 2010 Custom Integrated Circuits Conference, Sep. 2010.
• “Formal Verification of an Arbiter Circuit” with Chao Yan and Jochen Eisinger, in 2010 Symposium on Asynchronous Circuits and Systems, May 2010.

2009

• “Synchronizer Behavior and Analysis” with Ian W. Jones and Suwen Yang, in 2009 Symposium on Asynchronous Circuits and Systems, May 2009.
• “Estimating Reliability and Throughput of Source-synchronous Wave-pipelined Interconnect” with Paul Teehan and Guy G.F. Lemieux, in 2009 Network-on-Chip Symposium, May 2009.
• “A Modular Synchronizing FIFO for NoCs” with Tarik Ono, in 2009 Network-on-Chip Symposium, May 2009.
• “Towards reliable 5Gbps wave-pipelined and 3Gbps surfing interconnect in 65nm FPGAs” with Paul Teehan and Guy G.F. Lemieux, in 2009 International Symposium on Field Programmable Gate Arrays, Feb. 2009.

2008

• “Energy Optimal Scheduling on Multiprocessors with Migration” with Brad D. Bingham, in 2008 International Symposium on Parallel and Distributed Processing with Applications, Dec. 2008.
• “Computation with Energy-Time Trade-Offs: Models, Algorithms and Lower-Bounds” with Brad D. Bingham, in 2008 International Symposium on Parallel and Distributed Processing with Applications, Dec. 2008.
• “Verifying an Arbiter Circuit” with Chao Yan, in 2008 Conference on Formal Methods in Computer Aided Design, Nov. 2008.
• “Practical Asynchronous Interconnect Network Design”, with Bradley R. Quinton and Steven J.E. Wilton, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol. 16, no. 5, 570–588, May 2008.

2007

• “An efficient linear programming solver for optimal filter synthesis”, with Jihong Ren and Chen Greif, Numerical Linear Algebra with Applications (Wiley Interscience), vol. 14, no. 9, Nov. 2007.
• “A Survey and Taxonomy of GALS Design Styles”, with Paul Teehan and Guy G.F. Lemieux, IEEE Design and Test of Computers, vol. 24 no. 5, Sep./Oct. 2007.
• “Surfing Pipelines: Theory and Implementation”, with Suwen Yang and Brian Winters, IEEE Journal of Solid State Circuits, vol. 42, no. 6, June 2007.
• “Simulating Improbable Events”, with Suwen Yang, 44th ACM/IEEE Design Automation Conference (DAC'2007) June 2007.
• “Computing Synchronizer Failure Probabilities”, with Suwen Yang, 10th Design Automation, and Test, Europe Conference (DATE'2007), Apr. 2007.
• “A Jitter Attenuating Timing Chain”, with Suwen Yang and Jihong Ren, 13th International Symposium on Asynchronous Circuits and Systems (ASYNC'2007), Mar. 2007.

2006

• “A Novel Distributed and Interleaved FIFO for Source-Synchronous Interconnect”, with Santosh Sood and Resve Saleh. 10th VLSI Design and Test Symposium (VDAT'2006), Aug. 2006.
• “A Robust Linear Program Solver for Reachability Analysis”, with Chao Yan and Marius Laza. International Conference on Mathematical Aspects of Computer and Information Sciences (MACIC'2006), July 2006.
• “System-on-Chip: Reuse and Integration”, with Resve Saleh, Steve Wilton, Shahriar Miribbasi, Alan Hu, Andre Ivanov, Partha Pande, and Christian Grecu. Proceedings of the IEEE, June 2006.
• “Surfing Interconnect”, with Jihong Ren, 12th International Symposium on Asynchronous Circuits and Systems (ASYNC'2006), Apr. 2006.

2005

• “Noise Margin Analysis for Dynamic Logic Circuits”, with Suwen Yang, IEEE/ACM International Conference on Computer Aided Design (ICCAD'2005), Nov. 2005.
• “Asynchronous IC Network Interconnect Design and Implementation Using a Standard ASIC Design Flow”, with Bradley R. Quinton and Steven J.E. Wilton. 23rd IEEE International Conference on Computer Design (ICCD'2005), Oct. 2005.
• “A Unified Optimization Framework for Equalization Filter Synthesis”, with Jihong Ren, 42nd ACM/IEEE Design Automation Conference (DAC'2005), June 2005.
• “Analysing the Robustness of Surfing Circuits”, with Suwen Yang. Workshop on Formal Verification of Analog Circuits, April 2005.
  Abstract   PDF   Postscript  
• “Energy Efficient Surfing”, with Suwen Yang, 11th International Symposium on Asynchronous Circuits and Systems (ASYNC'2005), Mar. 2005.

2004

• “A Signal Integrity Test Bed for PCB Buses”, with Jihong Ren, 22nd IEEE International Conference on Computer Design (ICCD'2005), Oct. 2005.
• “ Crosstalk Cancellation for Realistic PCB Buses”, with Jihong Ren, 14th International Workshop on Power and Timing, Modeling, Optimization and Synthesis (PATMOS'2004), Sep. 2004.

2003

• “Synthesizing Optimal Filters for Crosstalk-cancellation for High-Speed Buses”, with Jihong Ren, Proceedings of 40th ACM/IEEE Design Automation Conference (DAC'2003).
  Abstract   Bibtex   PDF   Postscript  
• “Efficient Self-Timed Interfaces for Crossing Clock Domains”, with Ajanta Chakraborty, Proceedings of 9th Int'l. Symp. on Asynchronous Circuits and Systems (ASYNC'2003, Best Paper Award).
  Abstract   Bibtex   PDF   Postscript  
• “Equalizing Filter Design for Crosstalk Cancellation”, with Jihong Ren, Proceedings of 2003 IEEE Computer Society Annual Symposium on VLSI (ISVLSI'2003).
  Abstract   Bibtex   PDF   Postscript  

2002

• “A Minimalist Source-Synchronous Interface”, with Ajanta Chakraborty, Proceedings of The 15th IEEE ASIC/SOC Conference.
  Abstract   Bibtex   PDF   Postscript  
• “A Negative Overhead, Self-Timed Pipeline”, with Brian D. Winters, Proceedings of ASYNC'2002.
  Abstract   Bibtex   PDF   Postscript  
• “An Event Spacing Experiment”, with Anthony Winstanley and Aurelien Garivier, Proceedings of ASYNC'2002.
  Abstract   Bibtex   PDF   Postscript  

2001

• “Temporal Properties of Self-Timed Rings”, with Anthony Winstanley, Proceedings of CHARME'2001.
  Abstract   Bibtex   PDF   Postscript  
• “How to Achieve Worst-Case Performance”, with Brian de Alwis, Proceedings of ASYNC'2001.
  Abstract   Bibtex   PDF   Postscript  
• “A Light-Weight Framework for Hardware Verification”, with Christoph Kern and Tarik Ono-Tesfaye Software Tools for Technology Transfer vol. 3 no. 3.
  Abstract   Bibtex   PDF   Postscript  

2000

• “Pragmatic Verification for Hybrid and Real-Time Designs”, Proceedings of 2000 American Control Conference.
  Abstract   Bibtex   Postscript  

1999

• “A Fast, ASP*, RGD Arbiter”, with Tarik Ono-Tesfaye, Proceedings of Async99.
  Abstract   Bibtex   Postscript
• “Real-Time Merging”, Proceedings of Async99.
  Abstract   Bibtex   Postscript
• “Reachability Analysis Using Polygonal Projections”, with Ian Mitchell, Proceedings of HSCC'99.
  Abstract   Bibtex   PDF Postscript
• “A Light-Weight Framework for Hardware Verification”, with Christoph Kern and Tarik Ono-Tesfaye, Proceedings of TACAS'99.
  Abstract   Bibtex   Postscript
• “Formal Verification in Hardware Design: A Survey”, with Christoph Kern, ACM Transactions on Design Automation of Electronic Systems, April 1999.
  Abstract   Bibtex   Postscript

1998

• “A Hybrid-Systems View of Discrete Computation”, Proceedings of CDC'98.
  Abstract   Bibtex   Postscript
• “Verifying a Self-Timed Divider”, with Tarik Ono-Tesfaye and Christoph Kern, Proceedings of Async98.
  Abstract   Bibtex   Postscript
• “Integrating Projections”, with Ian Mitchell, Proceedings of HSCC'98.
  Abstract   Bibtex   PDF Postscript

1997

• “A Smooth Dynamical System that Counts in Binary”, with Xuemei Huang, Proceedings of ISCAS'97.
  Abstract   Bibtex   PDF Postscript
• “Self-Timed Meshes are Faster Than Synchronous”, with Peggy B-K. Pang, Proceedings of Async97.
  Abstract   Bibtex   Postscript

1996

• “Verifying Asynchronous Data Path Circuits”, with David T. Weih, IEE Proceedings, Part E, Computers and Digital Techniques, vol. 144, no. 5, Sep. 1996.
  Abstract   Bibtex   Postscript
• “Proving Newtonian Arbiters Correct, Almost Surely”, Ian Mitchell, Proceedings of the 1996 Workshop on Designing Correct Circuits (DCC'96).
  Abstract   Bibtex   Postscript
• “Verifying Safety Properties of Differential Equations”, Proceedings of CAV'96.
  Abstract   Bibtex   PDF Postscript

1995

• “Implementing a STARI Chip”, Proceedings of ICCD'95.
  Abstract   Bibtex   Postscript

1994

• “How Fast Will the Flip Flop?”, with Peter Cahoon, Proceedings of Async94.
  Abstract   Bibtex   Postscript

1992

• “Using Synchronized Transitions for Simulation and Timing Verification”, Proceedings of DCC'92
  . Abstract   Bibtex   Postscript

1990

• “Bubbles Can Make Self-Timed Pipelines Fast”, with Ken Steiglitz, Journal of VLSI and Signal Processing, vol. 2, no. 3, Nov. 1990.
  Abstract   Bibtex