The property is of the form G(a=>C) where C=c is propositional,
or C=X^n{c} is temporal, or...

The algorithm involves several procedures.

Procedure antecedent_conditioned_slice takes a Verilog program P
and a property G(a=>C). It calls get_conditioned_slice
on the arguments. For the simple property G(a=>c) that value is returned
as the final slice. For G(a=>X^=n{c}), additional unrolling
of the conditioned slice is done for exactly n steps corresponding
to n clock ticks.

Procedure get_conditioned_slice takes a Verilog program P,
and a property G(a=>C).
It "unrolls" the program to eliminate loops and symbolically evaluates
program expressions at program nodes as it goes. When the current
annotated program copy matches the
annotation of a prior copy, the unrolling stops.

The symbolic expression of a node v is determined by the annotations
of the nodes along the (simple) paths to v. It is
is a disjunction of a conjunction of expressions for
nodes along paths leading to the node v.
The ReWrite engine for arithmetic and boolean identities attempts to determine
a simplified value of a at v: a, not(a), or else U (unknown), using
the "database" supplied by the symbolic expression for v.

Procedure get_static_slice takes a Verilog program P
and a slicing criterion based on the
variables of the antecedent a and consequent C. It essentially
performs a cone-of-influence analysis on P for those variables.
It then deletes the statements associated with irrelevant variables.
An alternative algorithm may be found in [].

Remarks:
Global Predicates. Predicates for the antecedent
such as a(x1,x2,x3) are handled through over-approximation.
A value of "don't know" for a(x1,x2,x3) is tantamount to
"might-be-true". As the unrolling proceeds,
information about variable x1 in process P1, variable x2 in process P2,
etc. is recorded, and propagates to process P3 at the next unrolling
step. If the unrolling proceeds far enough, sufficient information
may be gathered to evaluate a as true or false. Otherwise,
we overapproximate as it-might-be true.
For other global predicates or guards P(x1,x2,x3), if the predicate
is labelled "don't know" and both paths are enabled yielding
contradictory results at a node, the antecedent at that node will get
don't know as a value.