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.