Notes related to Instruction set architecture
Arm architecture, CHERI architecture, Cray architecture, ISA specification, Instruction Set Processor (ISP), MIPS architecture, PDP11 architecture, Power-PC architecture, RISC architecture, RISC-V architecture, Sparc architecture, Vector architecture, x86 architecture
Papers related to Instruction set architecture
- Detailed models of instruction set architectures: From pseudocode to formal semantics [armstrong:arw:2018]
- ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS [armstrong:popl19:2019]
- The state of Sail [armstrong:spisa:2019]
- Vector microprocessors [asanovic:phd:1998]
- Instruction set processor specifications (ISPS): The notation and its applications [barbacci:ieee:1981]
- Hardware is the new software [baumann:hotos:2017]
- The PMS and ISP descriptive systems for computer structures [bell:afips:1970]
- Computer structures: Readings and examples [bell:book:1971]
- Advanced SIMD: Extending the reach of contemporary SIMD architectures [boettcher:date:2014]
- Machine code verification of a tiny ARM hypervisor [dam:ted:2013]
- Machine code verification of a tiny ARM hypervisor [dam:trusted:2013]
- A complete formal semantics of x86-64 user-level instruction set architecture [dasgupta:pldi:2019]
- Formal specification of the x86 instruction set architecture [degenbaev:phd:2012]
- Very long instruction word architectures and the ELI-512 [fisher:isca:1983]
- Modelling the ARMv8 architecture, operationally: concurrency and ISA [flur:popl:2016]
- Mixed-size concurrency: ARM, POWER, C/C++11, and SC [flur:popl:2017]
- A HOL specification of the ARM instruction set architecture [fox:cambridge:2001]
- A trustworthy monadic formalization of the ARMv7 instruction set architecture [fox:itp:2010]
- Directions in ISA specification [fox:itp:2012]
- Improved tool support for machine-code decompilation in HOL4 [fox:itps:2015]
- Formal specification and verification of ARM6 [fox:tphols:2003]
- Abstract stobjs and their application to ISA modeling [goel:acl2:2013]
- Simulation and formal verification of x86 machine-code programs that make system calls [goel:fmcad:2014]
- Engineering a formal, executable x86 ISA simulator for software verification [goel:pcs:2017]
- Formal verification of application and system programs based on a validated x86 ISA model [goel:phd:2016]
- Using x86isa for microcode verification [goel:spisa:2019]
- An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors [gray:micro:2015]
- A retrospective on `MIPS: A microprocessor architecture' [gross:micro:2016]
- Computer architecture: A quantitative approach (Fifth edition) [hennessy:book:2011]
- Stratified synthesis: Automatically learning the x86-64 instruction set [heule:pldi:2016]
- High-level separation logic for low-level code [jensen:popl:2013]
- Examiner: Automatically locating inconsistent instructions between real devices and CPU emulators for Arm [jiang:arxiv:2021]
- Towards a formal model of the x86 ISA [kaufmann:utaustin:2012]
- Scalable vector media processors for embedded systems [kozyrakis:phd:2002]
- Subword parallelism with MAX-2 [lee:micro:1996]
- Pydgin: generating fast instruction set simulators from simple architecture descriptions with meta-tracing JIT compilers [lockhart:ispass:2015]
- RockSalt: Better, faster, stronger SFI for the x86 [morrisett:pldi:2012]
- TALx86: A realistic typed assembly language [morrisett:wcsss:1999]
- Verified LISP Implementations on ARM, x86 and PowerPC [myreen:tphols:2009]
- Polymorphic type inference for machine code [noonan:pldi:2016]
- Reduced instruction set computers [patterson:cacm:1985]
- The case for the reduced instruction set computer [patterson:sigarch:1980]
- PDP-11/45 processor handbook [pdp11:book:1973]
- MMX technology extension to the Intel architecture [peleg:micro:1996]
- End-to-end verification of ARM processors with ISA-formal [reid:cav:2016]
- Trustworthy specifications of ARM v8-A and v8-M system level architecture [reid:fmcad:2016]
- Who guards the guards? Formal validation of the ARM v8-M architecture specification [reid:oopsla:2017]
- Defining interfaces between hardware and software: Quality and performance [reid:phd:2019]
- The CRAY-1 computer system [russell:cacm:1978]
- Understanding POWER multiprocessors [sarkar:pldi:2011]
- The semantics of x86-CC multiprocessor machine code [sarkar:popl:2009]
- ARM Architecture Reference Manual (ARMv5 edition) [seal:book:2000]
- Translation validation for a verified OS kernel [sewell:pldi:2013]
- Certification of an instruction set simulator [shi:phd:2013]
- The ARM scalable vector extension [stephens:micro:2017]
- VIS speeds new media processing [tremblay:micro:1996]
- CHERI: A hybrid capability-system architecture for scalable software compartmentalization [watson:sandp:2015]