CPU verification

[Google Scholar]

Notes: ISA specification

ISA specification, Symbolic trajectory evaluation

  • A framework for microprocessor correctness statements [aagaard:charme:2001]
  • A methodology for large-scale hardware verification [aagaard:fmcad:2000]
  • Testing the FM9001 microprocessor [albin:cli:1995]
  • An approach to systems verification [bevier:jar:1989]
  • Putting it all together - Formal verification of the VAMP [beyer:ijsttt:2006]
  • Formal verification of pipelined Y86-64 microprocessors with UCLID5 [bryant:cmu:2018]
  • Automatic verification of pipelined microprocessor control [burch:cav:1994]
  • Formal verification of the ARM6 micro-architecture [fox:ucam:2002]
  • End-to-end formal verification of a RISC-V processor extended with capability pointers [gao:fmcad:2021]
  • Balancing automation and control for formal verification of microprocessors [goel:cav:2021]
  • Verifying x86 instruction implementations [goel:cpp:2020]
  • Using x86isa for microcode verification [goel:spisa:2019]
  • Symbolic simulation of the JEM1 microprocessor [greve:fmcad:1998]
  • Simplifying design and verification for structural hazards and datapaths in pipelined circuits [higgins:hldvt:2004]
  • Synthesizing formal models of hardware from RTL for efficient verification of memory model implementations [hsiao:micro:2021]
  • Instruction-level abstraction (ILA): A uniform specification for system-on-chip (SoC) verification [huang:todaes:2019]
  • Microprocessor design verification [hunt:jar:1989]
  • FM8501: A verified microprocessor [hunt:lncs:1994]
  • Verifying the FM9801 microarchitecture [hunt:micro:1999]
  • Microarchitecture verification by compositional model checking [jhala:cav:2001]
  • Replacing testing with formal verification in Intel Core i7 processor execution engine validation [kaivola:cav:2009]
  • Symbolic trajectory evaluation: The primary validation vehicle for next generation Intel processor graphics FPU [kirankumar:fmcad:2012]
  • Automated pipeline design [kroening:dac:2001]
  • Proving the correctness of pipelined micro-architectures [kroening:itg:2000]
  • Automated formal verification of processors based on architectural models [kuhne:fmcad:2010]
  • Deductive verification of advanced out-of-order microprocessors [lahiri:cav:2003]
  • Experience with term level modeling and verification of the M* CORE microprocessor core [lahiri:hldvt:2001]
  • COATCheck: Verifying memory ordering at the hardware-OS interface [lustig:asplos:2016]
  • RTLcheck: Verifying the memory consistency of RTL designs [manerkar:micro:2017]
  • Verification of an implementation of Tomasulo's algorithm by compositional model checking [mcmillan:cav:1998]
  • Axiomatic hardware-software contracts for security [mosier:isca:2022]
  • End-to-end verification of ARM processors with ISA-formal [reid:cav:2016]
  • Defining interfaces between hardware and software: Quality and performance [reid:phd:2019]
  • Formal verification by symbolic evaluation of partially-ordered trajectories [segar:fmsd:1995]
  • A flexible formal verification framework for industrial scale validation [slobodova:memocode:2011]
  • Automatic refinement checking of pipelines with out-of-order execution [srinivasan:ieeetoc:2010]
  • Processor memory system verification using DOGReL: a language for specifying end-to-end properties [stewart:difts:2014]
  • Formal verification of superscalar microprocessors with multicycle functional units, exception, and branch prediction [velev:dac:2000]
  • Opening Pandora's box: A systematic study of new ways microarchitecture can leak private data [vicarte:isca:2021]
  • Formal modeling and verification of microprocessors [windley:ieeetoc:1995]
  • Integrating memory consistency models with instruction-level abstraction for heterogeneous system-on-chip verification [zhang:fmcad:2018]