Silver-Pi

Formally verified in-order pipelined processor circuit for the Silver ISA.

Building

Requirements:

• Poly/ML version 5.8.1 or later
• HOL4 version kananaskis-14
• Verified (System) Verilog version v3

Please run Holmake to build our HOL4 files in the silver_isa, model, and proof folders.

If you want to test the processor on hardware, please use Xilinx Vivado v2023.2 to create a project with the Verilog files in the verilog_src folder and the FPGA board PYNQ-Z1.

Contents

• silver_isa: Silver ISA specification in L3 and generated HOL4 files for the ISA.
• model: processor circuit model and related definitions, based on the verified Verilog model.
• proof: correctness proof of the pipelined circuit with respect to the Silver ISA.
• verilog_src: Verilog source code for the processor and related hardware components (e.g., a cache).
• tests: test software programs for Silver processors, generated by the verified CakeML compiler.