Browse Source

smtbmc error test case 1

verific_problem smtbmc_error_0
T. Meissner 6 years ago
parent
commit
e762dda316
2 changed files with 2 additions and 1 deletions
  1. +1
    -0
      vai_reg/symbiyosys.sby
  2. +1
    -1
      vai_reg/vai_reg.vhd

+ 1
- 0
vai_reg/symbiyosys.sby View File

@ -3,6 +3,7 @@ depth 30
wait on wait on
mode prove mode prove
#mode bmc #mode bmc
#mode cover
[engines] [engines]
smtbmc smtbmc


+ 1
- 1
vai_reg/vai_reg.vhd View File

@ -111,7 +111,7 @@ begin
if (DinStop_i = '1') then if (DinStop_i = '1') then
if (unsigned(a_addr) <= 7) then if (unsigned(a_addr) <= 7) then
-- Following line results in a Segmentation Fault -- Following line results in a Segmentation Fault
s_register(to_integer(unsigned(a_addr))) <= Din_i;
--s_register(to_integer(unsigned(a_addr))) <= Din_i;
-- Following line results in following error: -- Following line results in following error:
-- ERROR: Unsupported cell type $dlatchsr for cell $verific$wide_dlatchrs_8.$verific$i1$172. -- ERROR: Unsupported cell type $dlatchsr for cell $verific$wide_dlatchrs_8.$verific$i1$172.
s_register(0) <= Din_i; s_register(0) <= Din_i;


Loading…
Cancel
Save