diff --git a/vai_reg/symbiyosys.sby b/vai_reg/symbiyosys.sby index c5cca6c..67f9153 100644 --- a/vai_reg/symbiyosys.sby +++ b/vai_reg/symbiyosys.sby @@ -3,6 +3,7 @@ depth 30 wait on mode prove #mode bmc +#mode cover [engines] smtbmc diff --git a/vai_reg/vai_reg.vhd b/vai_reg/vai_reg.vhd index 41975a7..ffa71c4 100644 --- a/vai_reg/vai_reg.vhd +++ b/vai_reg/vai_reg.vhd @@ -111,7 +111,7 @@ begin if (DinStop_i = '1') then if (unsigned(a_addr) <= 7) then -- 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: -- ERROR: Unsupported cell type $dlatchsr for cell $verific$wide_dlatchrs_8.$verific$i1$172. s_register(0) <= Din_i;