Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Constraints on Existential Parameters #450

Open
UnsignedByte opened this issue Aug 28, 2024 · 1 comment
Open

Constraints on Existential Parameters #450

UnsignedByte opened this issue Aug 28, 2024 · 1 comment
Labels
C: language Component: the Filament language S: needs triage Status: Needs some more thinking before being actionable

Comments

@UnsignedByte
Copy link
Collaborator

One of the current limitations of existential parameters is the inability to describe relationships between two components' existential parameters. Currently in the type system (smt solver) we already represent (non-opaque) existential parameters as a result of a function on input parameters. Therefore, we could theoretically provide this information in existential parameter constraints.

For example, one of the cases where this issue pops up is when using floating point addition or negation.

We have something like the following:

comp FAdd[E, M]<'G:1>(
  X: ['G, 'G+1] W,
  Y: ['G, 'G+1] W,
) -> (
  R: ['G+L, 'G+L+1] W,
) with {
  some W where W == E + M + 1;
  some L where L >= 0;
} { ... }

comp FSub[E, M]<'G:1>(
  X: ['G, 'G+1] W,
  Y: ['G, 'G+1] W,
) -> (
  R: ['G+L, 'G+L+1] W,
) with {
  some W where W == E + M + 1;
  some L where L >= 0;
} { ... }

where subtraction has the same latency of an addition, only adding an inverter on Ys sign bit.

I propose being able to rewrite FSub's constraints on L as follows:

comp FSub[E, M]<'G:1>(
  X: ['G, 'G+1] W,
  Y: ['G, 'G+1] W,
) -> (
  R: ['G+L, 'G+L+1] W,
) with {
  some W where W == E + M + 1;
  some L where L == FAdd[E, M]::L;
} { ... }

Which will then allow us to place additions and subtractions in parallel without having to add assumptions or unused registers.

@UnsignedByte UnsignedByte added S: needs triage Status: Needs some more thinking before being actionable C: language Component: the Filament language labels Aug 28, 2024
@rachitnigam
Copy link
Member

Is this issue the same as #406?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
C: language Component: the Filament language S: needs triage Status: Needs some more thinking before being actionable
Projects
None yet
Development

No branches or pull requests

2 participants