verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
75 stars 21 forks source link

V1 Hashing algorithms #179

Open stp59 opened 4 years ago

stp59 commented 4 years ago

Hashing algorithms currently implemented:

Hashing algorithms currently unimplemented:

hackedy commented 4 years ago

This is highly unscientific since some of these tests are probably PSA tests or otherwise unsupported, but:

% find ~/dev/petr4 -name '*.p4' | xargs grep '\<HashAlgorithm\.' | sed -E 's/.*HashAlgorithm.([a-z_0-9]+).*/\1/' | sort | uniq -c | sort -g
   9 lookup3
  12 crc32
  25 identity
  32 crc16
 177 csum16
hackedy commented 4 years ago

Oh, oops, that's a bad command line and not counting what I thought it was counting.

hackedy commented 4 years ago

In reality it's more like this. And I checked and only 5 of the tests using csum16 actually have STF files for us to run.

   2 lookup3
   4 crc32
  13 identity
  14 crc16
  49 csum16
stp59 commented 4 years ago

Update: the implementation of v1model currently supports identity, random, csum16, and crc16. crc16 is currently buggy, causing one test case to fail. most of the tests use csum16, which is working correctly.

hackedy commented 4 years ago

Moving the 1 crc16 test to unsupported.