M. D. Aagaard (2003):
A Hazards-Based Correctness Statement for Pipelined Circuits.
In: Proc. of CHARME'03,
LNCS 2860.
Springer,
pp. 66–80,
doi:10.1007/978-3-540-39724-3_8.
P. A. Abdulla, F. Haziza. & L. Holik (2013):
All for the Price of Few (Parameterized Verification through View Abstraction).
In: Proc. of VMCAI'13,
LNCS 7737.
Springer,
pp. 476–495,
doi:10.1007/s10009-015-0406-x.
A. Bouajjani, P. Habermehl, L. Holi\'k, T. Touili & T. Vojnar (2008):
Antichain-Based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata.
In: Proc. of CIAA'08,
LNCS 5148.
Springer,
doi:10.1007/978-3-540-70844-5_7.
A. Bouajjani, P. Habermehl & T. Vojnar (2004):
Abstract Regular Model Checking.
In: Proc. of CAV'04,
LNCS 3114.
Springer,
pp. 197–202,
doi:10.1007/978-3-540-30579-8_19.
J. R. Burch & D. L. Dill (1994):
Automatic Verification of Pipelined Microprocessor Control.
In: Proc. of CAV'94,
LNCS 818.
Springer,
pp. 68–80,
doi:10.1007/3-540-58179-0_44.
L. Charvat, A. Smrcka & T. Vojnar (2012):
Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description.
In: Proc. of MTV'12.
IEEE,
pp. 6–12,
doi:10.1109/mtv.2012.19.
L. Charvat, A. Smrcka & T. Vojnar (2014):
Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors.
In: Proc. of MTV'14.
IEEE,
pp. 83–89,
doi:10.1109/mtv.2014.21.
L. Charvát, A. Smrčka & T. Vojnar (2015):
Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems.
In: Proc. of EUROCAST'15,
LNCS 9520.
Springer,
pp. 605–614,
doi:10.1007/978-3-319-27340-2_75.
E. Clarke, M. Talupur & H. Veith (2006):
Environment abstraction for parameterized verification.
In: Proc. of VMCAI'06,
LNCS 3855.
Springer,
pp. 126–141,
doi:10.1007/11609773_9.
K. Hao, S. Ray & F. Xie (2014):
Equivalence Checking for Function Pipelining in Behavioral Synthesis.
In: Proc. of DATE'14.
IEEE,
pp. 1–6,
doi:10.7873/date.2014.163.
R. B. Jones, C. H. Seger & D. L. Dill (1996):
Self-Consistency Checking.
In: Proc. of FMCAD'96,
LNCS 1166.
Springer,
pp. 159–171,
doi:10.1007/bfb0031806.
A. Koelbl, R. Jacoby, H. Jain & C. Pixley (2009):
Solver Technology for System-level to RTL Equivalence Checking.
In: Proc. of DATE'09.
IEEE,
pp. 196–201,
doi:10.1109/date.2009.5090657.
U. Kuhne, S. Beyer, J. Bormann & J. Barstow (2010):
Automated Formal Verification of Processors Based on Architectural Models.
In: Proc. of FMCAD'10.
IEEE,
pp. 129–136.
P. Mishra, H. Tomiyama, N. Dutt & A. Nicolau (2002):
Automatic Verification of In-Order Execution in Microprocessors with Fragmented Pipelines and Multicycle Functional Units.
In: Proc. of DATE'02.
IEEE,
pp. 36–43,
doi:10.1109/date.2002.998247.
L. De Moura & N. Bjorner (2008):
Z3: An Efficient SMT Solver.
In: Proc. of TACAS'08,
LNCS 4963.
Springer,
pp. 337–340,
doi:10.1007/978-3-540-78800-3_24.
K. S. Namjoshi (2007):
Symmetry and completeness in the analysis of parameterized systems.
In: Proc. of VMCAI'07,
LNCS 4349.
Springer,
pp. 299–313,
doi:10.1007/978-3-540-69738-1_22.
D. A. Patterson & J. L. Hennessy (2012):
Computer Organization and Design: The Hardware / Software Interface,
fourth edition.
Morgan Kaufmann,
Boston,
doi:10.1016/c2013-0-08305-3.
M. N. Velev & P. Gao (2011):
Automatic Formal Verification of Multithreaded Pipelined Microprocessors.
In: Proc. of ICCAD'11.
IEEE,
pp. 679–686,
doi:10.1109/iccad.2011.6105403.