Skip to content

Provide API to run formal verification programmatically. #657

Open
@marcogelmi

Description

@marcogelmi

It would be useful to have an API that we can call to verify that two implementations are equivalent. This would be essentially the same thing that the check_ir_equivalence_main tool does.

This API would take two xls::Function* and return a StatusOr and possibly an opaque error message for debugging purposes (e.g. variable assignments, same as the command line tool).

Metadata

Metadata

Assignees

No one assigned

    Labels

    formalRelated to formal / Logical Equivalence Checkingpublic-apiRelating to the publicly exported XLS APIs

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions