ppc/cross (tooling date Sun Jan 22 02:23:23 GMT 2012)

This family corresponds to litmus tests involving pairs exercising typical Power scenarios. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms, as soon as the model is Power. It involves several diy cycles instead of one.

Name

SC

CAV'11

TSO (all delay/cyc)

TSO (1 delay/cyc)

TSO (opt delay/cyc)

Expected (TSO)

PSO (all delay/cyc)

PSO (1 delay/cyc)

PSO (opt delay/cyc)

Expected (PSO)

RMO (all delay/cyc)

RMO (1 delay/cyc)

RMO (opt delay/cyc)

Expected (RMO)

Power (all delay/cyc)

Power (1 delay/cyc)

Power (opt delay/cyc)

Expected (Power)