This project gives the formal specification of RISC-V ISA in Kami. In particular, it gives the semantics for RV32GC and RV64GC ISAs with User-mode, Supervisor-mode and Machine-mode instructions and the Zam extension (unaligned atomics).
Installation instructions are available in INSTALL.adoc.
The semantics are organized into two parts, the ProcKami/FuncUnits directory, and the top-level ProcKami directory.
This is a directory that contains a list of instructions that defines the RISC-V ISA, along with the semantics of these instructions, written as Kami expressions, that define how the instruction reads and updates the state of a processor such as the register files, the floating point register files, the PC, etc.
The directory is organized as the different functional units that execute a set of instructions, each, of the RISC-V ISA. Related functional units are grouped together into directories (e.g., the different functional units comprising the ALU functional units, such as the Add, Logical, Branch, DivRem, etc. are grouped into the ProcKami/FuncUnits/Alu directory).
Each functional unit is is represented by a record which contains the following fields:
- fuName
-
The name of the functional unit (for documentation purposes only)
- fuFunc
-
The function represented by the functional unit as a Kami expression (which takes some inputs, in the form of a Kami struct and produces some outputs, again in the form of a Kami struct)`
- fuInsts
-
The list of instructions that are supported by this functional unit. The fuInsts itself is a list of records where each record contains the following fields:
- instName
-
The name of the instruction (for documentation purposes only)
- extensions
-
The list of extensions that the instruction is necessary to be included in
- uniqId
-
The unique identification information for the instruction as defined by the RISC-V ISA. It contains a list of ranges (between 0 and 31) and the bit patterns in those ranges
- inputXform
-
The transformation of the generic ExecContextPkt and ContextCfgPkt into the inputs for the functional unit that executes this instruction.
-
ExecContextPkt represents the register state which the current instruction that is being executed requires to execute. It contains the following fields:
- pc
-
The PC of the instruction packet
- reg1
-
The value in the register file for the first register referenced by the instruction packet, in either the integer register file or the floating point register file, depending on the instruction
- reg2
-
The value in the register file for the second register referenced by the instruction packet, again, in either the integer register file or the floating point register file, depending on the instruction
- reg3
-
The value in the register file for the third register referenced by the instruction packet. This is needed only for the FMADD instruction and its variants, and therefore necessarily from the floating point register file
- fflags
-
The current status of the floating point flags, in order to set the new flags
- frm
-
The floating point rounding mode
- inst
-
The uncompressed 32-bit instruction represented by the current packet
- compressed?
-
Whether the instruction represented by the current packet was compressed or not
-
ContextCfgPkt represents more of the register state which the current instruction requires to execute. The difference from the ExecContextPkt is that this represents the state which changes less frequently as opposed to the state represented by the ExecContextPkt, which changes more or less after exery instruction. It contains the following fields:
- xlen
-
Specifies whether we are running the 32-bit ISA or the 64-bit ISA
- mode
-
Specifies whether we are in user mode, supervisor mode, hypervisor mode or machine mode
- extensions
-
Specifies the extensions that the machine should be supporting when executing the current instruction
- instMisalignedException?
-
Specifies whether the instruction should throw an exception when fetching an instruction not aligned to 32-bit boundaries
- memMisalignedException?
-
Specifies whether the instruction should throw an exception when performing a load, store, AMO or LR/SC on an unaligned address
- accessException?
-
Specifies whether the instruction should throw an access fault instead of misaligned fault (memory accesses resulting in misaligned faults are usually still completed by the trap handler by splitting the access into multiple aligned accesses; access faults result in system error)
-
- outputXform
-
Specifies how to transform the output of a functional unit into a processor-state update packet ExecUpdPkt, which contains the following fields:
- val1
-
The value for the first destination register, along with whether it is an updated value of an integer register or a floating point register, the PC, the floating point flags register, a memory address, a memory data (for stores and AMOs) or a CSR register.
- val2
-
Same as *val1*. This is needed when we update multiple locations, for instance the PC and an integer register in case of the JALR instruction.
- memBitMask
-
The memory mask for Store, AMO and SC operations
- mem
-
The value written to memory for Store, AMO and SC operations
- taken?
-
In case of a branch or jump instruction, tells whether the branch or jump is taken or not
- aq
-
In case of AMO or LR/SC operation, tells whether it has the acquire semantics
- rl
-
In case of AMO or LR/SC operation, tells whether it has the release semantics
- optMemXform
-
In case of memory-related instructions, specifies how the data from the memory is transformed before storing into the register file (for instance, in the case of a load byte, load half word, etc), and how the register value gets transformed before storing into the memory (in the case of a store byte, store half word, etc). This function takes a MemoryInput packet that specifies what comes out of the register file and what comes out of the memory and transforms it into a MemoryOutput packet that specifies what goes into the register file and what goes into the memory.
- MemoryInput
-
It has the following fields:
- aq:
-
In case of AMO or LR/SC operation, tells whether it has the acquire semantics
- rl:
-
In case of AMO or LR/SC operation, tells whether it has the release semantics
- reservation:
-
In case of LR/SC, specifies whether the reservation bit is set for each byte corresponding to the memory operation
- mem:
-
The value written into the memory in case of a store, AMO or SC
- reg_data:
-
The value written into the register file in case of a load, AMO or LR
- MemoryOutput
-
It has the following fields:
- aq:
-
In case of AMO or LR/SC operation, tells whether it has the acquire semantics
- rl:
-
In case of AMO or LR/SC operation, tells whether it has the release semantics
- isWr:
-
Tells whether the memory operation involves writing the memory (i.e. Store, AMO or SC)
- mask:
-
Tells which bytes will be written in case of Store, AMO or SC
- data:
-
Tells the written value in case of Store, AMO or SC
- isLrSc:
-
Tells whether the operation is LR or SC
- reservation:
-
Tells which bytes will be reserved in case of LR and which bytes' reservations have to be checked in case of SC
- tag:
-
Tells whether the value from a load is written into the integer register file or floating point register file
- reg_data:
-
Tells the value read in case of Load, AMO or LR
- instHints
-
Specifies various information about the instruction, such as whether it has a source 1 integer register, source 2 integer register, destination integer register, source 1 floating point register, source 2 floating point register, source 3 floating point register, destination floating point register, whether it is a branch, a jump to a register, a jump to an immediate value, a system call, a CSR-related instruction, a store or AMO instruction, etc.
One reason for such an organization, where each functional unit handles a set of instructions is for clarity. The other, more important reason is as follows. We want to be able to automatically analyze these functional units and generate decoders, executors, memory units, etc (see Top-level directory and files). These generated functions will be used not only in the specification in ProcKami, but also to generate complex microarchitecture implementations (such as the out-of-order processor). This makes formal verification of these complex microarchitectures easier, as they share the same generated functions (such as decoder, executor, etc) with the specification they must be proven against. For actual implementations, it is important that each functional unit handles several instructions, where the inputs and outputs for the functional units are transformed based on the instruction. This organization of separating the semantics of an instruction into a ExecContextPkt transformer to feed a functional unit, the generic functionality of the functional unit and a transformation of the output of the functional unit to an UpdateContextPkt does not overly impose any burden on the readability or the understandability of the RISC-V ISA specification, but eases the formal verification cost of implementations significantly.
These files take the tables in the ProcKami/FuncUnits directory and produce several useful functions like the decoder, reg-reader, executor, etc. These functions are all assembled in ProcessorCore.v to create a formal specification of the processor.