CTSRD-CHERI / QuickCheckVEngine

A RISC-V TestRIG Verification Engine based on QuickCheck
BSD 2-Clause "Simplified" License
7 stars 10 forks source link

`c_flq` & `c_fsq` not in spec #53

Closed elliotb-lowrisc closed 2 months ago

elliotb-lowrisc commented 3 months ago

I can't find the c_flq and c_fsq instructions given in RV_C.hs (added here) in the RISC-V "C" extension spec (20191213). The closest I can find is FLQ and FSQ in RV128Q, but there is no mention of a compressed version.

They seem to share the same encoding as the C.LQ and C.SQ RV128C instructions that are in the spec but not yet in RV_C.hs. Shall I put a PR together to change their names from c_flq/c_fsq to c_lq/c_sq in RV_C.hs?

PeterRugg commented 3 months ago

Hmm, this is very odd. I also can't see where they would have come from, and the encoding seems to clash with the c.fld and c.fsd instructions anyway... I don't know if @gameboo has any recollection, but it was a long time ago. I'd say let's make it match our current understanding as you suggest.

gameboo commented 3 months ago

Hmmm... must be some ancient things... If they are not present in the recent spec releases, then, I am happy for these to die.

elliotb-lowrisc commented 3 months ago

Alright, I'll create a PR