[Formal][PropertyAnnotation] Annotating IOG-based invariants#855

Merged

Basmet0 merged 34 commits into

EPFL-LAP:mainfrom

Basmet0:invariant5

May 14, 2026

Commits on Apr 13, 2026

algorithm for finding IOGs
Bas Niekel
committed

Commits on Apr 16, 2026

annotating invariant 6: Consecutive tokens within an IOG must have an active fork in between
Bas Niekel
committed
invariant now works for any slot within an operation (rather than just the first slot)
Bas Niekel
committed
small cleanup of IOG generation code with better naming
Bas Niekel
committed
extraction of IOG finding into separate file
Bas Niekel
committed
fixed IOG path code to support multiple possible paths
Bas Niekel
committed

Commits on Apr 17, 2026

handle pipeline slots as well as normal slots in invariant 6
Bas Niekel
committed

Commits on Apr 22, 2026

added some more explaining comments for the IOG finding algorithm
Bas Niekel
committed

Commits on Apr 25, 2026

start of IOG-single-token invariant:
Bas Niekel
committed
getAllSlotsOfOperation properly handles load's hidden slot in MC
Bas Niekel
committed
slot of terminating sink is annotatable
Bas Niekel
committed
change testbench generator to work with IOG single-token invariant
Bas Niekel
committed

Commits on Apr 29, 2026

Merge branch 'main' into invariant5
Bas Niekel
committed
change testbench to:
Bas Niekel
committed
set default testbench to not use dead buffers
Bas Niekel
committed
format
Bas Niekel
committed

Commits on Apr 30, 2026

change types.mlir unit test
Bas Niekel
committed
attempt fix types.mlir
Bas Niekel
committed

Commits on May 6, 2026

more comments
Bas Niekel
committed
fixed an issue that made smv module arguments mismatch
Bas Niekel
committed
Merge branch 'main' into invariant5
Bas Niekel
committed
replace template with ValueRange
Bas Niekel
committed

Commits on May 8, 2026

Commits on May 9, 2026

flow expresssions now handle dead buffer op
Bas Niekel
committed
resolved merge-conflicts
Bas Niekel
committed
Merge branch 'main' into invariant5
Bas Niekel
committed
more logical TokenCountNamer which does not need special smv definitions
Bas Niekel
committed
formatting
Bas Niekel
committed

Commits on May 11, 2026

Merge branch 'main' into invariant5
Bas Niekel
committed
comments
Bas Niekel
committed

Commits on May 12, 2026

small fixes for clarity
Bas Niekel
committed