Browse Source

smtbmc error test case 2

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

+ 2
- 2
vai_reg/symbiyosys.sby View File

@ -6,8 +6,8 @@ mode prove
#mode cover #mode cover
[engines] [engines]
#smtbmc
abc pdr
smtbmc
#abc pdr
[script] [script]
verific -vhdl vai_reg.vhd verific -vhdl vai_reg.vhd


+ 2
- 2
vai_reg/vai_reg.vhd View File

@ -111,10 +111,10 @@ 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;
else else
s_error <= true; s_error <= true;
end if; end if;


Loading…
Cancel
Save