ID:276036 Top level entity of a design cannot be treated as a black-box for formal verification

CAUSE: In a Verilog Design File (.v) or VHDL Design File (.vhd), you specified a set of registers that act as RAM. When Analysis & Synthesis created the specified node as a RAM using the registers, it converted the registers into a RAM using the corresponding Altera megafunction. This memory block is a new instance that is handled as a black box by the formal verification tool. However, no such instance exists in the original design. This would result in errors in the formal verification tool. Therefore, the Quartus Prime software treated the entity that contains this block as a black box. However, the top level entity of a design cannot be treated as a black-box.

ACTION: If you want Analysis & Synthesis to use an altsyncram megafunction, but you want the formal verification tool to verify the rest of the design, replace the registers and address logic in the Verilog Design File or VHDL Design File with an explicit instantiation of an altsyncram megafunction. If the registers and address logic in an entity are treated as a black box and the entity is parameterized, you need to create a wrapper entity that does not contain parameters. If you want the RAM in the original design to function the same as the RAM implemented in the target device, and verify the design including the RAM, prevent Analysis & Synthesis from converting the registers into an altsyncram megafunction by turning off the Auto RAM Replacement logic option.