References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. Codasip Ltd. (2013): CodAL Architecture Description Language.
  11. T. Genet: Timbuk: A Tree Automata Library. 9118\p@ plus2\p@ minus4\p@ \z@ plus\p@ 4\p@ plus2\p@ minus2\p@ \defłeftmarginłeftmargini 2.5\p@ plus1.5\p@ minus\p@ 5\p@ plus2\p@ minus5\p@ıtemsep 2.5\p@ plus1.5\p@ minus\p@łeftmarginłeftmargini 4\p@ plus2\p@ minus2\p@ 2\p@ plus\p@ minus\p@ıtemsep http://www.irisa.fr/lande/genet/timbuk.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. 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.
  19. 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.
  20. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org