A Mathematical Model for the Verification of Systolic Networks