Skip to content

fcof: c[gs]ethigh cross refinements #75

Open
@nwf

Description

@nwf

cheriot_instr_csethigh_cross1 and cheriot_instr_cgethigh_cross1 involve cross-products of capability {exponent, top, bottom, correction factor} and address population count. These are, mm, let's say interesting quantities, and so doubtless the correct things to consider, but will give rise to similarly interestingly shaped impossible subsets of the cross-product.

For example, it is not possible for...

  • a capability with T and B both all-zeros to be anything other than correction factor vector 3'b000 (with a_mid >= B, at that) or 3'b100 (3'b111 is ruled out because a_mid cannot be smaller than all zeros).

    • all-ones T and B, on the other hand, permit more variance in a_mid: it can be >= B (by being equal), or can be <, but only if the exponent is non-zero.
  • an address with fewer than 9 bits set (cp_cd_address bins valid[24] through valid[32]) to have its a_mid field be anything other than less than an all-ones B field, or greater-or-equal-to an all-zeros B field.

I'm sure there're many more such constraints. Help?

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions