Zfinx SAIL status as of 18/02/2021

General RV model issues:

1. The way the model is configured is generally  lacking, this was supposed to be fixed by this PR from February https://github.com/rems-project/sail-riscv/pull/43 . This PR proposed reading all the model configuration from a YAML file, however, it looks like this got stuck last June and didn’t move since.  The lack of a general configuration method causes various issues when trying to write any extension, currently most configurations are handled using command line arguments, however, the model won’t read these arguments until it initializes many things including its  global variables. This makes it impossible to set a global variable value from the command line. Some part of the model appear to assume that the automatically generated C code variable names would stay the same upon recompilation, thus I used this trick to overwrite the correct value from the handwritten C support for the model, this is a bad solution, but it appears to be used before, and it’s the only way it can be currently done.
   
   I think the YAML configuration PR needs to be reviewed and merged ASAP, as it would affect the way all future extensions are written.
2. It appears that the model is actively managed by a single person Prashanth Mundkur, I was waiting for feedback since late November for my latest updates, and only got some feedback and help a week ago from Jessica Clarke.   I think this needs to be changed.

General SAIL Issues:

1. The documentation for SAIL is generally lacking, it often gives a single example for each keyword, and often that example has typos, or not present at all. For example in the case of forall keyword, the example provided is missing the actual source, an issue was reported here https://github.com/rems-project/sail/issues/121 on 2nd of December, no response yet.
2. Sometimes the generated C and OCAML behavior is different, for e.g when using effect keyword, an issue was reported here https://github.com/rems-project/sail/issues/122
3. SAIL error and warnings are often hard to decode, for example when using forall statements, if we use any mutable or user defined functions, Sail does not report any issue, it passes to Z3 which fails  (I know it’s not allowed, however SAIL should complain about it and it should not pass it to Z3 which would fail without any line number or any useful debug information), also when using the SAIL in the interactive mode, it ignores any include statements and it does not complain about them (I know I would need to include them in the command line input arguments, but SAIL REPL should complain about include statements if its unable to retrieve them).  

What needs to be done:

1. I was previously stuck on writing a forall statement which have its output size dependent on an input Boolean value, however I think this is now addressed here https://github.com/rems-project/sail/issues/125.    (I was planning to use this reduce the repetition  in code )
2. Code formatting, remove trailing spaces, etc as advised by Jessica in latest review on PR https://github.com/rems-project/sail-riscv/pull/75

What’s completed:

1. Implemented a command line argument to enable and disable Zfinx.
2. Changed the source and the target registers for FP ops when Zfinx is enabled.
3. Implemented register pairs handling for RV32D and exceptions required for when odd numbered register are used
4. Allowed the model to compile for when XLEN != FLEN, e.g for RV32D and fixed some issues in the source code to allow that
5. Implemented basic testing functionality based on the existing floating point tests from “riscv-tests” repo https://github.com/riscv/riscv-tests (We knew its going obsolete but it was the easiest way to check basic functionality)
6. Modified the nan boxing behavior to match Zfinx specifications
7. Changed the register names in trace when Zfinx is enabled. (Since all instructions are handled with scattered mapping statements, it’s hard to introduce any function that would handle the register name change for Zfinx unless we have an immutable global variable that tells if Zfinx is enabled, however since the model initalise and assign all global variables before parsing the input command line arguments, thus this make it impossible to assign global variable with command line arguments (https://github.com/rems-project/sail-riscv/pull/75#issuecomment-736002604) , and the only alternative as far as I am concerned is to encapsulate every mapping statement with another if statement which would result in more code duplications, which I was told to reduce)
8. Removed floating point loads, stores and moves when Zfinx is enabled .
9. Changed the behavior of mstatus.FS and mstatus.F when Zfinx is enabled

Zfinx Test Status

Waiting for standard FP tests from IIT Madras

Zfinx Toolchain/Qemu/Spike status

In progress with CAS/PLCT

Zfinx Spec Status

Waiting for opcode and consistency review