sifive/prockami

Kami based processor implementations and specifications

prockami's Issues

Add PMP Checks

The mem_region_read, mem_region_write, and mem_region_fetch actions must be preceded by appropriate PMP checks. Add the necessary calls to pmp_check_read, pmp_check_write, and pmp_check_execute where appropriate.

Remove Guards from Kami

Add Checks to checkForAccessFault

Revise the checkForAccessFault (rename to checkForFault) so that it returns a 2 bit vector that specifies which, if any, of the following errors occured:

• pmp error
• physical address bound
• memory device range match (is a function - make it check the range, the width and pma
  permissions and misaligned. Return 4 Bools)
• device width discrepancy
• device pma permission error
• address misaligned

Returns 2 Bools: access fault or misaligned error.

Modify the PMPAddr register generator and read actions so that they set the pmpaddr size to 32 bits when MaxXLEN is 32

TrapAction is Not Updating the mcause Register Correctly

the trapAction action is not updating the mcause register correctly. It contains a register write statement that contains a Kami Kind error - i.e. the write statement's Kind signature does not match the Kind of the register. As a result, Kami is silently ignoring this write statement.

Enhance Kami RegFile to contain starting address for hex memory file.

Revise the Test Scripts to Terminate when Test Programs Write to tohost

Change the Processor Core so that the Reg Writer Reads CSR Values Before CSR Writes Rather than the Register Reader Task

Change None for Xlen to just a list of [32;64]

Gallina let instead of Kami Let

These files use gallina let instead of Kami Let.

CompressedInsts.v
FU.v
ProcessorCore.v
Alu.v
Jump.v
Fpu.v

Rename WarlField to something else

pmp_check should be called directly with arguments about read-check/write-check/readwrite-check

LR -> pmp read passes, pmp write fails. Should LR succeed? (Ask Andrew)

Determine Behavior of Ecalls in Tests

The rv64ud-p-structural and rv64ui-p-simple tests are timing out. Both end in an ecall that results in an infinite loop. When the processor model encounters an ecall, it loops back to address 0 which then leads it to repeat these tests.

Add compressed field to the Execute Context Packet

This field will specify whether or not the current instruction is compressed.

Provide static options for disabling certain behaviors

Revise LogMaskSz Param, Xlen Name, Trunc Functions, and Xlen Param

• Change MaxXlen and Max_Xlen to Xlen
• Change the order of the AddrSz and LogMaskSz parameters in StdLibKami.RegMapper.
• Update the CSR Interface functions to use the new AddrSz and LogMaskSz argument order.
• Define ContextWidth as log2_up numContexts in StdLibKami and update the CSR Interface definitions accordingly.
• Replace the Decoder Pkt argument to Commit with a Bool indicating whether or not the decoded instruction was compressed or not.
• Replace the Extensions Pkt with a Bool indicating whether or not XLEN = 32 or 64 bits (where appropriate).
• Draft a function unsafeTruncLsb : forall n m : nat, Bit n -> Bit m, where n >= m.
• Draft a function extendMsbWithFunc : forall f (n m : nat), Bit n -> Bit m, where n <= m.
• Draft notations: xlen_trunc : forall n : nat, Bool @# ty -> ..., xlen_zero_extend, xlen_sign_extend, flen_trunc, flen_one_extend.
• Change every truncate from Rlen to the type required in InputXform to use unsafeTruncLsb and change every extend from the type in OutputXform to Rlen using one of the above functions.
• Revise Processor.v so that the currently enabled extensions (#extensions) are passed to the decoder rather than the list of supported extensions, i.e. line 159 of FU.v
  (decoderWithException (func_units _) (CompInstDb _) ($$ supportedExts) (mode _)
• remove code that truncates to 32 bits using the Xlen/2 method and use the xlen_trunc function instead.

Add xlen Parameter to runElf and runTests Task

CSR fields bug

Currently different views have different types for registers, and nobody is checking if the reads are correct. Here's the proposed solution:

• Each CSR group has a single CSRField that contains:
  Record CSRField
  := {
  csrFieldName : string;
  csrFieldKind : Kind;
  csrFieldIsValid
  : FieldUpd @# ty ->
  csrFieldKind @# ty ->
  csrFieldKind @# ty ->
  Bool @# ty;
  csrFieldXform
  : FieldUpd @# ty ->
  csrFieldKind @# ty ->
  csrFieldKind @# ty ->
  csrFieldKind @# ty
  }.
  Let the Kami struct formed from a list of above fields be called csrKind.
  (Note that there's no "csrFieldDefaultValue").
  It also has a csrAddr, list csrViews and csrAccess.
• Each csrView contains two simple transformations csrKind -> CsrValue and CsrValue -> csrKind, where CsrValue is of Xlen length. If the dynamic size of the view is x bits, while CsrValue is Bit y, you simply unpack \compose ZeroExtendTruncLsb to transform a CsrValue into csrKind. But, the Alternative way requires you to perform the right transformation from csrKind to CsrValue. For instance, if the csrKind holds an address, you want to sign-extend that to form the CsrValue. If it holds something other than an address, perhaps, you want to zero-extend. So this is determined on a case-by-case basis.

Automatic register generation from memory device table

Revise FU.v so that Each Component is Stored in a Separate File Task

Revise the CSR Interface so that it supports input transformers

The RISC-V spec requires us to designate certain register fields as WARL (write any - read legal) fields. When an invalid value is written to these fields, the processor does not throw an exception. However, the value returned on subsequent writes must be a legal value. Unfortunately, the spec allows implementations to chose any legal value to return. Extend the CSR interface so that every CSR entry has an associated valid predicate and an input transform function.
The valid predicate function's type is as follows:

Definition WarlStateField k := STRUCT {
"csrValueToWrite" :: k;
"pc" :: VAddr;
"compressed?" :: Bool }

Definition FieldUpd k := STRUCT {
"warlStateField" :: WarlStateField k;
"config" :: ConfigCtxtPkt
}

k ## ty
-> FieldUpd k ## ty
-> Bool ## ty

The function that computes the new value to be written is as follows:

k ## ty
-> FieldUpd k ## ty
-> k ## ty

Initially, we will use a last "legal value" policy. Modify the CSR interface to use these functions when writing CSR values.

Change CSR Mask Application

The current version of the ZiCSR functional unit applies the masks to CSR values in its input transform functions and passes the resulting CSR value to the Register Writer. Murali asked me to change the CSR interface so that the RegMapper.locationReadWrite function accepts a mask value and applies the mask value to write values. This will move the mask application to StdLibKami.RegMapper. Revise ZiCSR so that it passes two values to its context update packet - the register value to store in the CSR and the mask value to apply, rather than just the masked result.

Make access and dirty bit behavior in page table customizable

PAddrSz and Xlen are separate parameters

Generate a list of Misa Field Registers from a list of Supported Extensions and Use the Extended Module Notation to Add Registers to the Processor Module

Params handler issues

1. Simple filter if a wrong a wrong extension is passed - ignore the extension and proceed gracefully
2. Get rid of dependencies, or automatically add dependencies
3. Get rid of most auxiliary definitions and inline if necessary

Support Dynamic Extensions

Remove compressed field from context config packet

Revise the Fetch Unit to Support PMP Exception Handling

The rv64mi-p-access test issues an invalid jump instruction (at address 10c) that appears to be intended to raise a PMP access exception. Currently, the fetch unit does not raise exceptions. Revise the Fetch unit so that it raises access exceptions and add the PMP registers. Comply with the following:

"Attempting to fetch an instruction from a PMP region that does not have execute permissions raises a fetch access exception..." and latter "If no PMP entry mathces an M-mode access, the access succeed. If no PMP entry matches an S-mode or U-mode access, but at least one PMP entry is implemented, the access fails." (edited)
Finally "Failed accesses generate a load, store, or instruction access exception."

Declare PMP registers as one list of registers

Revise the "isvalid" predicate for the C extension field CSR register

The C extension field CSR register's isvalid predicate should reject write requests when the current PC is not aligned to a 32 bit boundary.

SignExtend instead of ZeroExtend by default

Xlen and Flen sized registers must be sign extended to Rlen

pmp failure, device failure, physical address overflow results in access fault

Implement the EBreak Instruction

Use Hypervisor prefixes "h" instead of reserved WARL fields

Automatic register generation from CSR table

Make instMisalignedException memMisalignedException and accessException either gallina parameters or part of extension

    "instMisalignedException?" :: Bool ;
    "memMisalignedException?"  :: Bool ;
    "accessException?"         :: Bool

Remove the mode field from the decoder packet

Modify Definitions so that Misa Field Names are Derived from the First Letter of Extension Names

Remove Magic Numbers Where Reasonable

Apply a transformation to the Instruction Entries table that filters Xlens

The transformation should filter the xlens fields so that they only contain those values less than or equal to max xlen.

Extend the module notation to support lists of registers

Revise the way that the `ContextCfgPkt` is generated so that it contains all and only the stable values

• Remove "mode" field from DecoderPkt
• Add "compressed?" field into ExecContextPkt
• ContextCfgPkt should contain "xlen", "mode" and "extensions"
• There should be an ActionT producing ContextCfgPkt, by reading appropriate CSR registers (directly, not through the CSR-read interface). "xlen" should be filled by using either mxl, hxl, sxl, uxl depending on the mode CSR
• ContextCfgPkt should be an input to createInputXform

Change the type signature for pt_walker

The page table walker currently returns a Maybe PAddr type. Change the type signature so that the pt_walker returns a PktWithException PAddr type and modify pt_walker so that it throws the correct access and page fault exceptions when errors occur.

Correct the Kind Error in Writes to the "mpp" and "spp" Registers

The trapAction function contains a write to the "mpp" and "spp" registers. These registers have different Kami kinds, but both are written to by the same Kami statement. The kind signature associated with this statement matches the Kind of the "mpp" register. Consequently, this statement has a kind error when writing to the "spp" register. Modify the trapAction function so that it writes the kind signature is correct by adding a width parameter to the trapAction function and setting it correctly in the calling function (commit).

Change the Processor Core so that the Reg Writer Reads CSR Values Before CSR Writes Rather than the Register Reader Task

Add Supervisor and User Mode CSRs Task

Change PMP check in Page Table Walk - it should raise Access Exception

Filter xlens in decode_match_xlen

filter xlens in decode_match_xlen so that the list is only those values less than Xlen.