J. R. Burch & D. L. Dill (1994):
Automatic Verification of Pipelined Microprocessor Control.
In: D. L. Dill: Proceedings of the 6th International Conference on Computer-Aided Verification (CAV 1994),
LNCS 818.
Springer-Verlag,
pp. 68–80,
doi:10.1007/3-540-58179-0_44.
J. Cong, Y. Fan, G. Han, W. Jiang & Z. Zhang (2006):
Platform-Based Behavior-Level and System-Level Synthesis.
In: 2006 IEEE International SoC Conference.
IEEE,
pp. 199–202,
doi:10.1109/SOCC.2006.283880.
D. Gajski, N. D. Dutt, A. Wu & S. Lin (1993):
High Level Synthesis: Introduction to Chip and System Design.
Kluwer Academic Publishers.
K. Hao, S. Ray & F. Xie (2012):
Equivalence Checking for Behaviorally Synthesized Pipelines.
In: P. Groeneveld, D. Sciuto & S. Hassoun: 49th International ACM/EDAC/IEEE Design Automation Conference (DAC 2012).
ACM,
pp. 344–349,
doi:10.1145/2228360.2228423.
K. Hao, F. Xie, S. Ray & J. Yang (2010):
Optimizing Equivalence Checking for Behavioral Synthesis.
In: Design, Automation and Test in Europe (DATE 2010).
IEEE,
pp. 1500–1505.
I. Moussa and Z. Sugar and R. Suescun and A. A. Jerraya and M. Diaz-Nava and M. Pavesi and S. Crudo and L. Gazzi (1999):
Comparing RTL and Behavioral Design Methodologies in the Case of a 2M Transistors ATM Shaper,
doi:10.1145/309847.310006.
M. Kaufmann, P. Manolios & J S. Moore (2000):
Computer-Aided Reasoning: An Approach.
Kluwer Academic Publishers,
Boston, MA,
doi:10.1007/978-1-4757-3188-0.
C. Lattner & V. Adve (2004):
LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation.
In: Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO 2004),
pp. 75–84,
doi:10.1109/CGO.2004.1281665.
P. Manolios (2000):
Correctness of Pipelined Machines.
In: W. A. Hunt, Jr. & S. D. Johnson: Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design (FMCAD 2000),
LNCS 1954.
Springer-Verlag,
Austin, TX,
pp. 161–178,
doi:10.1007/3-540-40922-X_11.
J S. Moore (2011):
The Role of Human Creativity in Mechanized Verification.
In: P. Bjesse & A. Slobodová: Proceedings of the 11th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2011),
pp. 18.
D. Puri, S. Ray, K. Hao & F. Xie (2014):
Mechanical Certification of Loop Pipelining Transformations: A Preview.
In: G. Klein & R. Gamboa: 4th International Conference on Interactive Theorem Proving (ITP 2014),
LNCS 7998.
Springer.
S. Ray, K. Hao, F. Xie & J. Yang (2009):
Formal Verification for High-Assurance Behavioral Synthesis.
In: Z. Liu & A. P. Ravn: Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA 2009),
LNCS 5799.
Springer,
Macao SAR, China,
pp. 337–351,
doi:10.1007/978-3-642-04761-9_25.
J. Sawada & W. A. Hunt, Jr. (2002):
Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability.
Formal Methods in Systems Design (FMSD) 20(2),
pp. 187–222,
doi:10.1023/A:1014122630277.
J. Tristan & X. Leroy (2010):
A Simple, Verified Validator for Software Pipelining.
In: M. V. Hemenegildo & J. Palsberg: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010),
pp. 83–92,
doi:10.1145/1706299.1706311.
University of Toronto (2013):
LegUp Documentation Release 3.0.
M. N. Velev & R. E. Bryant (2005):
TLSim and EVC: A Term-level Symbolic Simulator and An Efficient Decision Procedure for the Logic of Equality with Uninterpreted functions and Memories.
International Journal on Embedded Systems,
pp. 134–149,
doi:10.1504/IJES.2005.008815.
eptcs@eptcs.org