• Input_format_for_model_checkingChisel
  • Book:  Chisel-Book
  • Slides:  Chisel Book Chapter1-7  Chisel Book Chapter8-10  Chisel_Book Chapter12
  • Test code:  Chap2
• FIRRTL (A Hardware Intermediate Representation and Compiler Framework)
  • Github: https://github.com/chipsalliance/firrtl
  • Slides: BTRO2_Input format for model checking
  • Paper: Unlocking Design Reuse with Hardware Compiler Frameworks
  • Slides: HCF_chap3-4

时序性质形式化验证

• Verilog/SystemVerilog Assertion
  • Book:  SVA_The Power Of Assertions In SystemVerilog_2015
  • Slides: SVA_Introduction2    SVA_Introduction3    SVA_Introduction4
• 已有的部分SVA拓展到Chisel的工作
  • Paper:  Dynamic Verification Library for Chisel

指令集一致性验证

• CPU/RISC-V指令集介绍
  • Book:  RISC-V_Reader-Chinese
  • Book:  The RISC-V Instruction Set Manual Volume I Unprivileged ISA
  • Book:  The RISC-V Instruction Set Manual Volume II Privileged Architecture
  • Slides:  RISCV相关知识调研  RISCV特权级指令
• 指令集规范
  • Paper:  Isla_Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models_CAV2021
  • Paper:  ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS_POPL2019
  • Slides:  ISA语义规范_POPL2019