commit 19ab493ffbd2c7e6b4a292f31ddb8cf90af3e3ff
author Cindy Chen <chencindy@google.com> Wed Oct 16 17:17:05 2019 -0700
committer cindychip <cindy.chen0316@gmail.com> Thu Oct 17 09:38:11 2019 -0700
tree 3ac9d53552efe689433c40b23b75ba767944ff10
parent 656a295ceb0f29ddf3001eef259ceccffa1ec005

[formal] Add assumption for TLUL

FPV found a countercase due to insufficient constraints. Temp convert
the assertion to assumption.

hw/formal/fpv.tcl

diff --git a/hw/formal/fpv.tcl b/hw/formal/fpv.tcl
index e0be100..924b3b5 100644
--- a/hw/formal/fpv.tcl
+++ b/hw/formal/fpv.tcl
@@ -80,6 +80,7 @@
 assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_host\w*\.legalAOpcode}
 assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_host\w*\.legalAParam}
 assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_host\w*\.sizeMatchesMask}
+assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_host\w*\.sizeGTEMask}
 assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_host\w*\.onlyOnePendingReqPerSourceID}
 assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_host\w*\.addressAlignedToSize}
 assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_host\w*\.maskMustBeContiguous}