what do you mean by assertion block

IFV can display the status of an assertion as ‘blocked’ if it detects any combinational loop in the signals involved in the assertion's cone-of-influence. The status ‘blocked’ indicates that the assertion could not be verified, because combinational loops exist in the design. Please follow below steps to identify and resolve the combinational loops.

Step - 1:

If you get a blocked status, first of all, please run the following command for the blocked assertion. It will let you know if indeed the assertion was blocked because of combinational loops.

formalVerifier> assertion –show <blocked_assertion_name > -verbose

For example

formalVerifier> assertion –show my_assertion –verbose
my_assertion: Block (0)
Combinational loop(s) found in the design. Use the debug command to view the nets involved in the combinational loop(s).

Step 2:

Now you would be interested in knowing which module has combinational loops and what signals are involved? In order to get this information, please run the "debug" command as suggested below.

formalverifier> debug my_assertion

Counter-example launched.
Number of combinational loop : 1
1) Net(s) in combinational loop : 2
combinational_loop.Y (File: ./test.sv)
combinational_loop.W (File: ./test.sv)

So now we know that Y, W are the signals involved. It also points out the file name where those signals are declared. We can now easily check the indicated code and remodel the HDL to remove the combinational loop.

Thanks

-Mahesh Soni

IFV can display the status of an assertion as ‘blocked’ if it detects any combinational loop in the signals involved in the assertion's cone-of-influence. The status ‘blocked’ indicates that the assertion could not be verified, because combinational loops exist in the design. Please follow below steps to identify and resolve the combinational loops.

Step - 1:

If you get a blocked status, first of all, please run the following command for the blocked assertion. It will let you know if indeed the assertion was blocked because of combinational loops.

formalVerifier> assertion –show <blocked_assertion_name > -verbose

For example

formalVerifier> assertion –show my_assertion –verbose
my_assertion: Block (0)
Combinational loop(s) found in the design. Use the debug command to view the nets involved in the combinational loop(s).

Step 2:

Now you would be interested in knowing which module has combinational loops and what signals are involved? In order to get this information, please run the "debug" command as suggested below.

formalverifier> debug my_assertion

Counter-example launched.
Number of combinational loop : 1
1) Net(s) in combinational loop : 2
combinational_loop.Y (File: ./test.sv)
combinational_loop.W (File: ./test.sv)

So now we know that Y, W are the signals involved. It also points out the file name where those signals are declared. We can now easily check the indicated code and remodel the HDL to remove the combinational loop.

Thanks

-Mahesh Soni