spent several hours writing this: https://libre-riscv.org/HDL_workflow/ please do review, add anything missing or make corrections. bartek and team, the document now contains development dependencies and links to install procedures, which will help you get set up for the formal proof tutorial. l.