vmurali / prockami Goto Github PK

Note:

Clean up local version and upstream it.

• Construct core names for spec cores
• Create DominatingCaps and DominatingCapsOverlap relations
• Spec cores should have non-overlapping dominating caps
• Trap core's mtdc and mtcc shouldn't overlap with any of the dominating caps
• Trap core's memory should be initialized with values in mtdc. mtdcSize should be set appropriately.
• Trap core's memory should be initialized with values in mtcc. mtccSize should be set appropriately.
• Separate SCR from Reg names.

Note:

Clean up local version and push it upstream.

Note:

Finish the proof and upstream it. Perhaps an incomplete proof can also be upstreamed if a good point is reached in the proof - explore that.

This will a) fix the compilation time, b) ensure that any instruction bit sequence is handled in one shot

• Fix RunSpec.v to use LetExpr that gets passed in registers and returns updated values instead of a general ActionT. This involves changing MemSpec.v also
• Fix RunSpec.v to push the implicitRead code inside each instruction match
• Fix IsolationSpec.v to distinguish between initial state (when registers are all in context area) and trapping state (when one process' registers are in the register file). Perhaps merge the two states by starting the process pointed to by curr
• Create unified register
• Add initial value for SCRs and CSRs