Master Thesis

Correct-by-Construction Hardware Design of A 5-Stage-Pipelined-RV32I CPU

Implementation

The Implementation of the piplined CPU follows the following steps:

1. an abstract untimed SystemC design of the base integer instruction set RV32I without interrupts is implemented as a single cycle implementation ISA.
2. based on ISA, a complete set of abstract properties is generated using the open source tool SCAM
3. these generated properties are refined while developing the hardware for the pipelined CPU in VHDL.
4. the refined properties has to be proved against the final implementation of the RTL.

Remarks

• System level design of the pipelined CPU could be found in the ESL folder.
• Assembly programs as well as instruction tests have been developed to test the CPU, as both Pipelined or single cycle implementation, on system level.

NOTE: README FILES WOULD BE ADDED ON THE 15th OF DEC 2018