@Inproceedings{Sawada:1997,
title={Trace Table Based Approach for Pipelined Microprocessor Verification},
author={Sawada, Jun and Hunt, Jr., Warren A.},
booktitle={Computer Aided Verification (CAV~'97)},
series={LNCS},
volume=1254,
pages={364--375},
publisher=sv,
year=1997
}

@Book{acs,
 editor       = {M. Kaufmann and P. Manolios and J S. Moore},
 title        = "{Computer-Aided Reasoning:  {ACL2} Case Studies}",
 publisher    = "Kluwer Academic Press",
 year         = "2000"
}
 

@Inproceedings{Sawada:1999,
title={Results of the Verification of a Complex Pipelined Machine Model},
author={Sawada, Jun and Hunt, Jr., Warren A.},
booktitle={Correct Hardware Design and Verification Methods(CHARME~'99)},
year=1999,
series={LNCS},
volume=1703,
pages={313-316},
publisher=sv,
editor={Laurence Pierre and Thomas Kropf}
}

@Inproceedings{Sawada:1998,
title={Processor Verification with Precise Exceptions and Speculative Execution} ,
author={Sawada, Jun and Hunt, Jr., Warren A.},
booktitle={Computer Aided Verification (CAV~'98)},
series={LNCS},
volume=1427,
pages={135--146},
publisher=sv,
editor={Alan J. Hu and Moshe Y. Vardi},
year=1998
}

@article{Hunt:1999,
title={The {FM9801} Microprocessor Verification},
author={Hunt, Jr., Warren A. and Jun Sawada},
journal={IEEE Micro},
pages={47-55},
volume=19,
number=3,
month={May/June},
year=1999
}

@phdthesis{Sawada-theses,
author={Jun Sawada},
title={Formal Verification of an Advanced Pipelined Machine},
school={University of Texas at Austin},
month=dec,
note={Also available from {http://\-www.cs.utexas.edu/\-users/\-sawada/\-dissertation/\-diss.html}},
year=1999
}