VerilRocq: A Rocq-embedded framework to verify Verilog modules

Directory Content

• src: Core framework and case study
  • Lib: General-purpose libraries used in the framework
  • Lang: Formal syntax and semantics of Verilog
• dep: External dependencies
  • coqutil: Various data structures and utility lemmas, from https://github.com/mit-plv/coqutil

Build

make