Method and apparatus for mutation coverage testing with incremental sat queries
A solution for performing incremental mutation coverage testing is disclosed. The solution can identify, for a cycle of a test, a first signal not covered during preceding cycles of the test and select, for the current cycle, a first value for the first signal. The solution can, responsive to the first value, determine whether the first signal is covered by the test in the current cycle and identify whether a first assertion not covered during the one or more preceding cycles is covered in the current cycle. The solution can remove the first signal from a list of signals if it determines that it is not covered by the test and remove the first assertion from a list of assertions if the first assertion is determined to be covered. The system can identify, for a next cycle, a second signal from the updated one or more signals for the circuit.
1 . A system to perform incremental mutation coverage testing of a circuit, the system comprising:
at least one processor coupled with memory and configured to:
identify, for a current cycle of a plurality of cycles of a test for a circuit, a first signal of one or more signals for the circuit, the first signal not covered during one or more preceding cycles of the plurality of cycles;
select, for the current cycle, a first value for the first signal;
determine, in response to the first value selected for the first signal for the circuit, whether the first signal is covered by the test in the current cycle;
identify, in response to the first value selected for the first signal for the circuit, whether a first assertion of a plurality of assertions not covered during the one or more preceding cycles is covered by the test in the current cycle;
update the one or more signals to remove the first signal from the one or more signals if the first signal is determined to be covered by the test;
update the one or more assertions to remove the first assertion from the one or more assertions if the first assertion is determined to be covered by the test; and
identify, for a next cycle following the current cycle, a second signal from the updated one or more signals for the circuit.
2 . The system of claim 1 , wherein the test is a mutation coverage test for the circuit implemented in a hardware description language (HDL) and integrated with one or more verification environment components.
3 . The system of claim 2 , wherein the assertion includes a System Verilog Assertion (SVA) corresponding to one or more cycles of a clock of the circuit.
4 . The system of claim 1 , wherein the at least one processor is configured to:
set, for the duration of the cycle, the first signal to a mutated signal value; and
determine that the first signal is covered by the test based on the mutated signal value remaining unchanged for the duration of the current cycle.
5 . The system of claim 1 , wherein the at least one processor is configured to identify that the first assertion is covered by the test based on the first assertion verifying the first signal.
6 . The system of claim 1 , wherein the at least one processor is configured to:
provide a current counter value from a plurality of counter values corresponding to the plurality of cycles, the current counter value corresponding to the current cycle; and
identify the first signal according to the current counter value.
7 . The system of claim 6 , wherein the at least one processor is configured to:
increase the current counter value to a next counter value of the plurality of counter values;
determine whether the next counter value remains below a threshold of the counter values; and
identify, responsive to the next counter value remaining below the threshold of the counter values, a second signal of the updated one or more signals to use during the next cycle of the test.
8 . The system of claim 1 , wherein the at least one processor is configured to:
select, for a next cycle following the current cycle, the first value for a second signal of the updated one or more signals;
determine, in response to the first value selected for the second signal for the circuit, whether the second signal is covered by the test in the next cycle;
identify, in response to the first value selected for the second signal for the circuit, whether a second assertion of the updated one or more assertions is covered by the test in the next cycle;
update the updated one or more signals to remove the second signal from the one or more signals if the second signal is determined to be covered by the test; and
update the updated one or more assertions to remove the second assertion from the one or more assertions if the second assertion is determined to be covered by the test.
9 . A method comprising:
determining, by at least one processor performing a current cycle of a plurality of cycles of a test for a circuit, a first signal of one or more signals for the circuit, the first signal not covered during one or more preceding cycles of the plurality of cycles;
determining, by the at least one processor for the current cycle, a first value for the first signal;
determining, by the at least one processor in response to the first value selected for the first signal for the circuit, whether the first signal is covered by the test in the current cycle;
identifying, by the at least one processor in response to the first value selected for the first signal for the circuit, whether a first assertion of a plurality of assertions not covered during the one or more preceding cycles is covered by the test in the current cycle;
updating, by the at least one processor, the one or more signals to remove the first signal from the one or more signals if the first signal is determined to be covered by the test;
updating, by the at least one processor, the one or more assertions to remove the first assertion from the one or more assertions if the first assertion is determined to be covered by the test; and
identifying, by the at least one processor for a next cycle following the current cycle, a second signal from the updated one or more signals for the circuit.
10 . The method of claim 9 , wherein the test is a mutation coverage test for the circuit implemented in a hardware description language (HDL).
11 . The method of claim 10 , wherein the assertion includes a System Verilog Assertion (SVA).
12 . The method of claim 9 , further comprising:
setting, by the at least one processor for the duration of the cycle, the first signal to a mutated signal value; and
determining, by the at least one processor, that the first signal is covered by the test based on the mutated signal value remaining unchanged for the duration of the current cycle.
13 . The method of claim 9 , further comprising:
identifying, by the at least one processor, that the first assertion is covered by the test based on the first assertion verifying the first signal.
14 . The method of claim 9 , further comprising:
providing, by the at least one processor, a current counter value from a plurality of counter values corresponding to the plurality of cycles, the current counter value corresponding to the current cycle; and
identifying, by the one or more processors, the first signal according to the current counter value.
15 . The method of claim 14 , further comprising:
incrementing, by the at least one processor, the current counter value to a next counter value of the plurality of counter values;
determining, by the at least one processor, whether the next counter value remains below a threshold of the counter values; and
identifying, by the at least one processor responsive to the next counter value remaining below the threshold of the counter values, a second signal of the updated one or more signals to use during the next cycle of the test.
16 . The method of claim 9 , further comprising:
selecting, by the at least one processor for a next cycle following the current cycle, the first value for a second signal of the updated one or more signals;
determining, by the at least one processor in response to the first value selected for the second signal for the circuit, whether the second signal is covered by the test in the next cycle;
identifying, by the at least one processor in response to the first value selected for the second signal for the circuit, whether a second assertion of the updated one or more assertions is covered by the test in the next cycle;
updating, by the at least one processor, the updated one or more signals to remove the second signal from the one or more signals if the second signal is determined to be covered by the test; and
updating, by the at least one processor, the updated one or more assertions to remove the second assertion from the one or more assertions if the second assertion is determined to be covered by the test.
17 . A non-transitory computer readable medium storing program instructions for causing at least one processor to:
identify, for a current cycle of a plurality of cycles of a test for a circuit, a first signal of one or more signals for the circuit, the first signal not covered during one or more preceding cycles of the plurality of cycles;
determine, for the current cycle, a first value for the first signal;
determine, in response to the first value selected for the first signal for the circuit, whether the first signal is covered by the test in the current cycle;
identify, in response to the first value selected for the first signal for the circuit, whether a first assertion of a plurality of assertions not covered during the one or more preceding cycles is covered by the test in the current cycle;
update the one or more signals to remove the first signal from the one or more signals if the first signal is determined to be covered by the test;
update the one or more assertions to remove the first assertion from the one or more assertions if the first assertion is determined to be covered by the test; and
identify, for a next cycle following the current cycle, a second signal from the updated one or more signals for the circuit.
18 . The non-transitory computer readable medium of claim 17 , wherein the test is a mutation coverage test for the circuit implemented in a hardware description language (HDL).
19 . The non-transitory computer readable medium of claim 18 , wherein the assertion includes a System Verilog Assertion (SVA).
20 . The non-transitory computer readable medium of claim 17 , wherein the program instructions further cause the at least one processor to:
set, for the duration of the cycle, the first signal to a mutated signal value; and
determine that the first signal is covered by the test based on the mutated signal value remaining unchanged for the duration of the current cycle.