Logic Design Verification Techniques for Liveness Checking

Abstract

A technique for verification of a logic design (embodied in a netlist) using a liveness-to-safety conversion includes assigning liveness gates for liveness properties of the netlist and assigning a single loop gate to provide a loop signal for the liveness gates. Assertion of the single loop gate is prevented when none of the liveness gates are asserted. A first state of the netlist is sampled and the sampled first state provides an initial state for a first behavioral loop for at least one of the liveness gates following the assertion of the single loop gate. The sampled first state of the first behavioral loop is compared with a later state of the first behavioral loop to determine if the sampled first state is repeated. A liveness violation is returned when the sampled first state is repeated and an associated one of the liveness gates remains asserted for a duration of the first behavioral loop.

1 . A method of verification of an integrated circuit logic design embodied in a netlist using a liveness-to-safety conversion as set forth by instructions executed by a computer system, comprising:
 assigning, by one or more instructions executed in the computer system, liveness gates for liveness properties of the netlist;   assigning, by one or more instructions executed in the computer system, a single loop gate to provide a loop signal for the liveness gates;   preventing, by one or more instructions executed in the computer system, assertion of the single loop gate when none of the liveness gates are asserted;   sampling, by one or more instructions executed in the computer system, a first state of the netlist, the sampled first state providing an initial state for a first behavioral loop for at least one of the liveness gates following the assertion of the single loop gate;   comparing, by one or more instructions executed in the computer system, the sampled first state of the first behavioral loop with a later state of the first behavioral loop to determine if the sampled first state is repeated; and   returning a liveness violation as an output of the computer system when the sampled first state is repeated and an associated one of the liveness gates remains asserted for a duration of the first behavioral loop.   
     
     
         2 . The method of  claim 1 , further comprising:
 sampling by one or more instructions executed in the computer system, responsive to a trigger, a second state of the netlist when the sampled first state has not been repeated, the sampled second state corresponding to an initial state for a second behavioral loop;   comparing, by one or more instructions executed in the computer system, the sampled second state of the second behavioral loop with a later state of the second behavioral loop to determine if the sampled second state is repeated; and   returning a liveness violation when the sampled second state is repeated and an associated one of the liveness gates remains asserted for a duration of the second behavioral loop.   
     
     
         3 . The method of  claim 2 , wherein the trigger for the sampling of the second state is based on a configurable bias to a random signal of a random gate of the netlist. 
     
     
         4 . The method of  claim 2 , wherein the trigger for the sampling of the second state is based on a time-step relative to the initial state for first behavioral loop. 
     
     
         5 . The method of  claim 2 , wherein the sampling of the second state is triggered based on a scenario encountered in the logic design. 
     
     
         6 . The method of  claim 1 , further comprising:
 checking, by one or more instructions executed in the computer system, for repetition of the first state within a specific time-range after sampling of the first state, upon a user generated coverage event, or an automatically generated coverage event.   
     
     
         7 . The method of  claim 1 , wherein the comparing, by one or more instructions executed in the computer system, the sampled first state of the first behavioral loop with a later state of the netlist to determine if the sampled first state is repeated occurs within a specific time range after the sampling of the sampled first state, or a specified coverage event. 
     
     
         8 . The method of  claim 1 , further comprising:
 detecting, by one or more instructions executed in the computer system, that a first liveness gate, included in the liveness gates, deasserted after the initial state is sampled and before the initial state is repeated; and   discontinuing, by one or more instructions executed in the computer system, the comparing along the first behavioral loop when the first liveness gate deasserted after the initial state is sampled and before the initial state is repeated.   
     
     
         9 . The method of  claim 1 , further comprising:
 assigning, by one or more instructions executed in the computer system, a constraint gate to accumulators of the netlist that track deassertion of respective ones of the liveness gates, wherein a constraint associated with the constraint gate specifies that all of the accumulators cannot flag a deassertion; and   discontinuing, by one or more instructions executed in the computer system, the comparing along the first behavioral loop when the constraint is violated.   
     
     
         10 . A method of performing liveness checking of an integrated circuit logic design embodied in a netlist as set forth by instructions executed by a computer system, comprising:
 attempting, by one or more instructions executed in the computer system, to prove that a liveness gate cannot remain asserted for a bound ‘k’ that corresponds to a number of time-steps in a first trace;   returning as an output of the computer system, when the liveness gate does not remain asserted for the bound ‘k’, an unbounded proof of correctness;   attempting by one or more instructions executed in the computer system, when the liveness gate remains asserted for the bound ‘k’, to prove that a first state of the first trace can be repeated during a second trace while the liveness gate remains asserted; and   returning as an output of the computer system, when the first state is repeated during the second trace and the liveness gate remains asserted, a concatenated trace that corresponds to an unbounded failure, the concatenated trace including the first and second traces.   
     
     
         11 . The method of  claim 10 , further comprising:
 attempting by one or more instructions executed in the computer system, when the first state is not repeated during the second trace and the liveness gate remains asserted, to prove that the liveness gate cannot remain asserted for the bound ‘k’ that corresponds to the number of time-steps in a third trace;   returning as an output of the computer system, when the liveness gate does not remain asserted for the bound ‘k’, an unbounded proof of correctness;   attempting, by one or more instructions executed in the computer system, to prove that a second state of the third trace can be repeated during a fourth trace while the liveness gate remains asserted; and   returning as an output of the computer system, when the second state is repeated during the fourth trace and the liveness gate remains asserted, a concatenated trace that corresponds to an unbounded failure, the concatenated trace including the third and fourth traces.   
     
     
         12 . The method of  claim 11 , wherein the first state corresponds to a terminal state of the first trace. 
     
     
         13 . The method of  claim 12 , wherein the second state corresponds to a terminal state of the third trace. 
     
     
         14 . The method of  claim 10 , further comprising:
 removing by one or more instructions executed in the computer system, as an initial operation, redundancy from the netlist.   
     
     
         15 . The method of  claim 11 , further comprising:
 modifying, by one or more instructions executed in the computer system, when the first state is sampled during the first trace.   
     
     
         16 . The method of  claim 15 , further comprising:
 modifying, by one or more instructions executed in the computer system, when the second state is sampled during the third trace.   
     
     
         17 . The method of  claim 10 , further comprising:
 checking by one or more instructions executed in the computer system, based on a predetermined condition, for a repeat of the first state during the first trace.   
     
     
         18 . The method of  claim 17 , wherein the predetermined condition corresponds to a specific time that is subsequent to sampling of the first state. 
     
     
         19 . The method of  claim 17 , wherein the predetermined condition corresponds to a specific event that is subsequent to sampling of the first state. 
     
     
         20 . A computer system configured to verify a logic design embodied in a netlist using a liveness-to-safety conversion, comprising:
 a memory subsystem configured to store code; and   a processor coupled to the memory subsystem, wherein the processor is configured to execute code to:
 assign liveness gates for liveness properties of the netlist; 
 assign a single loop gate to provide a loop signal for the liveness gates; 
 prevent assertion of the single loop gate when none of the liveness gates are asserted; 
 sample a first state of the netlist, the sampled first state providing an initial state for a first behavioral loop for at least one of the liveness gates following the assertion of the single loop gate; 
 compare the sampled first state of the first behavioral loop with a later state of the behavioral loop to determine if the sampled first state is repeated; and 
 return a liveness violation when the sampled first state is repeated and an associated one of the liveness gates remains asserted for a duration of the first behavioral loop.