Remove '-ignore_unknown_cells' option from 'sat'
authorEddie Hung <eddie@fpgeh.com>
Mon, 20 Apr 2020 18:58:23 +0000 (11:58 -0700)
committerEddie Hung <eddie@fpgeh.com>
Mon, 20 Apr 2020 18:58:23 +0000 (11:58 -0700)
tests/various/dynamic_part_select.ys

index d7fa1417347517cbf773db8e566740d363b577ff..abc1daad642bc2bd8d58e2b93b302abdaebe9cc1 100644 (file)
@@ -13,7 +13,7 @@ design -copy-from gold -as gold gold
 design -copy-from gate -as gate gate
 
 miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
-sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
+sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
 
 ### Multiple blocking assingments ###
 design -reset
@@ -31,7 +31,7 @@ design -copy-from gold -as gold gold
 design -copy-from gate -as gate gate
 
 miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
-sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
+sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
  
 ### Non-blocking to the same output register ###
 design -reset
@@ -49,7 +49,7 @@ design -copy-from gold -as gold gold
 design -copy-from gate -as gate gate
 
 miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
-sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
+sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
  
 ### For-loop select, one dynamic input
 design -reset
@@ -67,7 +67,7 @@ design -copy-from gold -as gold gold
 design -copy-from gate -as gate gate
 
 miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
-sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
+sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
  
 #### Double loop (part-select, reset) ### 
 design -reset
@@ -85,7 +85,7 @@ design -copy-from gold -as gold gold
 design -copy-from gate -as gate gate
  
 miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
-sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
+sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
  
 ### Reversed part-select case ###
 design -reset
@@ -103,4 +103,4 @@ design -copy-from gold -as gold gold
 design -copy-from gate -as gate gate
  
 miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
-sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
+sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv