@inproceedings(AagaardCHARME03, author = {M. D. Aagaard}, year = {2003}, title = {A Hazards-Based Correctness Statement for Pipelined Circuits}, booktitle = {Proc. of {CHARME}'03}, series = {LNCS}, volume = {2860}, publisher = {Springer}, pages = {66--80}, doi = {10.1007/978-3-540-39724-3_8}, ) @inproceedings(HolikVMCAI13, author = {P. A. Abdulla and F. Haziza. and L. Holik}, year = {2013}, title = {All for the Price of Few (Parameterized Verification through View Abstraction)}, booktitle = {Proc. of {VMCAI}'13}, series = {LNCS}, volume = {7737}, publisher = {Springer}, pages = {476--495}, doi = {10.1007/s10009-015-0406-x}, ) @inproceedings(bouajjani:antichain, author = {A. Bouajjani and P. Habermehl and L. Holi\'k and T. Touili and T. Vojnar}, year = {2008}, title = {{Antichain-Based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata}}, booktitle = {Proc. of CIAA'08}, series = {LNCS~5148}, publisher = {Springer}, doi = {10.1007/978-3-540-70844-5_7}, ) @inproceedings(VojnarCAV04, author = {A. Bouajjani and P. Habermehl and T. Vojnar}, year = {2004}, title = {Abstract Regular Model Checking}, booktitle = {Proc. of {CAV}'04}, series = {LNCS}, volume = {3114}, publisher = {Springer}, pages = {197--202}, doi = {10.1007/978-3-540-30579-8_19}, ) @inproceedings(BurchCAV94, author = {J. R. Burch and D. L. Dill}, year = {1994}, title = {Automatic Verification of Pipelined Microprocessor Control}, booktitle = {Proc. of {CAV}'94}, series = {LNCS}, volume = {818}, publisher = {Springer}, pages = {68--80}, doi = {10.1007/3-540-58179-0_44}, ) @inproceedings(MTV12, author = {L. Charvat and A. Smrcka and T. Vojnar}, year = {2012}, title = {Automatic Formal Correspondence Checking of {ISA} and {RTL} Microprocessor Description}, booktitle = {Proc. of {MTV}'12}, publisher = {{IEEE}}, pages = {6--12}, doi = {10.1109/mtv.2012.19}, ) @inproceedings(MTV14, author = {L. Charvat and A. Smrcka and T. Vojnar}, year = {2014}, title = {Using Formal Verification of Parameterized Systems in {RAW} Hazard Analysis in Microprocessors}, booktitle = {Proc. of {MTV}'14}, publisher = {{IEEE}}, pages = {83--89}, doi = {10.1109/mtv.2014.21}, ) @inproceedings(EUROCAST15, author = {L. Charv\'{a}t and Smr\v{c}ka, A. and T. Vojnar}, year = {2015}, title = {Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems}, booktitle = {Proc. of {EUROCAST}'15}, series = {LNCS}, volume = {9520}, publisher = {Springer}, pages = {605--614}, doi = {10.1007/978-3-319-27340-2_75}, ) @inproceedings(ClarkeVMCAI06, author = {E. Clarke and M. Talupur and H. Veith}, year = {2006}, title = {Environment abstraction for parameterized verification}, booktitle = {Proc. of {VMCAI}'06}, series = {LNCS}, volume = {3855}, publisher = {Springer}, pages = {126--141}, doi = {10.1007/11609773_9}, ) @manual(Codal, organization = {Codasip Ltd.}, year = {2013}, title = {CodAL Architecture Description Language}, ) @misc(timbuk, author = {T. Genet}, title = {{Timbuk: A Tree Automata Library}}, note = {{\relax\fontsize {9}{11}\selectfont\abovedisplayskip 8\p@ plus2\p@ minus4\p@ \abovedisplayshortskip\z@ plus\p@ \belowdisplayshortskip4\p@ plus2\p@ minus2\p@ \def\leftmargin \leftmargini\parsep 2.5\p@ plus1.5\p@ minus\p@ \topsep5\p@ plus2\p@ minus5\p@ \itemsep2.5\p@ plus1.5\p@ minus\p@ {\leftmargin\leftmargini \topsep4\p@ plus2\p@ minus2\p@ \parsep2\p@ plus\p@ minus\p@ \itemsep\parsep }\belowdisplayskip\abovedisplayskip http://www.irisa.fr/lande/genet/timbuk}}, ) @inproceedings(XieDATE14, author = {K. Hao and S. Ray and F. Xie}, year = {2014}, title = {Equivalence Checking for Function Pipelining in Behavioral Synthesis}, booktitle = {Proc. of {DATE}'14}, publisher = {{IEEE}}, pages = {1--6}, doi = {10.7873/date.2014.163}, ) @inproceedings(DillFMCAD96, author = {R. B. Jones and C. H. Seger and D. L. Dill}, year = {1996}, title = {Self-Consistency Checking}, booktitle = {Proc. of {FMCAD}'96}, series = {LNCS}, volume = {1166}, publisher = {Springer}, pages = {159--171}, doi = {10.1007/bfb0031806}, ) @inproceedings(PixleyDATE09Hector, author = {A. Koelbl and R. Jacoby and H. Jain and C. Pixley}, year = {2009}, title = {Solver Technology for System-level to {RTL} Equivalence Checking}, booktitle = {Proc. of {DATE}'09}, publisher = {{IEEE}}, pages = {196--201}, doi = {10.1109/date.2009.5090657}, ) @inproceedings(BeyerFMCAD10, author = {U. Kuhne and S. Beyer and J. Bormann and J. Barstow}, year = {2010}, title = {Automated Formal Verification of Processors Based on Architectural Models}, booktitle = {Proc. of {FMCAD}'10}, publisher = {{IEEE}}, pages = {129--136}, ) @inproceedings(MishraDATE02, author = {P. Mishra and H. Tomiyama and N. Dutt and A. Nicolau}, year = {2002}, title = {Automatic Verification of In-Order Execution in Microprocessors with Fragmented Pipelines and Multicycle Functional Units}, booktitle = {Proc. of {DATE}'02}, publisher = {{IEEE}}, pages = {36--43}, doi = {10.1109/date.2002.998247}, ) @inproceedings(DeMoura08Z3, author = {L. De Moura and N. Bjorner}, year = {2008}, title = {Z3: An Efficient {SMT} Solver}, booktitle = {Proc. of {TACAS}'08}, series = {LNCS}, volume = {4963}, publisher = {Springer}, pages = {337--340}, doi = {10.1007/978-3-540-78800-3_24}, ) @inproceedings(NamjoshiVMCAI07, author = {K. S. Namjoshi}, year = {2007}, title = {Symmetry and completeness in the analysis of parameterized systems}, booktitle = {Proc. of {VMCAI}'07}, series = {LNCS}, volume = {4349}, publisher = {Springer}, pages = {299--313}, doi = {10.1007/978-3-540-69738-1_22}, ) @book(Patternson12Book, author = {D. A. Patterson and J. L. Hennessy}, year = {2012}, title = {Computer Organization and Design: The Hardware / Software Interface}, edition = {fourth}, publisher = {Morgan Kaufmann}, address = {Boston}, doi = {10.1016/c2013-0-08305-3}, ) @inproceedings(VelevICCAD11, author = {M. N. Velev and P. Gao}, year = {2011}, title = {Automatic Formal Verification of Multithreaded Pipelined Microprocessors}, booktitle = {Proc. of {ICCAD}'11}, publisher = {{IEEE}}, pages = {679--686}, doi = {10.1109/iccad.2011.6105403}, )