Verifier

[bzhang1945]

Description

Integrated the PAST program equivalence check tool into Allo, allowing for semantic verification between Allo schedules that have gone through transformations through Allo customizations.

Proposed Solutions

Imported PAST and its bindings into Allo externals, which is then used by verify.py that creates and processes schedules into their generated VHLS code to be verified by PAST.

Once the VHLS code is generated, the verifier adds pocc_pragmas to demarcate the call regions to verify on, replaces unsupported types by PAST (e.g. int_64_t -> int), identifies the live-out/output variable, prior to running the two programs through verification.

Examples

To use the verifier, we simply need two Allo schedules:
s1 = allo.customize(foo)
s2 = allo.customize(bar)

verifier = allo.verify(s1, s2) # returns either True or False

Testing

Basic testing is run on the verifier under tests/test_verify.py.

[zhangzhiru]

If the verifier returns False, do we provide meaningful information to help users identify the source of the mismatch?

[bzhang1945]

If the verifier returns False, do we provide meaningful information to help users identify the source of the mismatch?

I have added a diff highlighter that logs the differences observed between the two generated VHLS schedules if the verifier deems the two to be not equivalent. We could potentially provide more information through inspecting the IRs, but I believe not much more can be systematically logged given that all of the grunt work of semantic canonicalisation is done by PAST, and the verifier here simply passes everything along to PAST.

[chhzh123]

Thanks for submitting this PR! It mostly looks great! To enable CI testing, I think you need to change the requirement.txt file to include this dependency.
https://github.com/cornell-zhang/allo/blob/main/requirements.txt

If no direct pip installation of the past package is provided, then you need to change the CI configuration file to install it manually.
https://github.com/cornell-zhang/allo/blob/main/.github/workflows/config.yml#L35

[chhzh123]

Use the following structure, not all the users need to install past.

try:
    import past
except:
    pass

[chhzh123]

It looks great! Thanks for making the CI work