Skip to content

Support synthesis queries referencing multiple outputs #503

@gussmith23

Description

@gussmith23

Currently, Lakeroad makes assumptions about there being exactly one output of the spec and the sketch. It asserts those outputs are equal in rosette-synthesize. However, that's not necessary; there can be multiple outputs of the expression.

#502 gets us closer to supporting this by adding an unimplemented output-ports field to rosette-synthesize.

  • Do not assume what output we use in sketches; e.g. DSP sketch should return all outputs in a map
  • Use output signal flags to populate output-ports argument of rosette-synthesize
  • Make multiple assertions in rosette-synthesize

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions