From a110290e8026a50100e778e730ab1435a5a58182 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20K=C3=B6fferlein?= Date: Sun, 11 Nov 2018 19:59:58 +0100 Subject: [PATCH] Updated Deep Verification Base (markdown) --- Deep-Verification-Base.md | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/Deep-Verification-Base.md b/Deep-Verification-Base.md index 6992d03..9cc11d2 100644 --- a/Deep-Verification-Base.md +++ b/Deep-Verification-Base.md @@ -56,7 +56,33 @@ Deep mode can basically be combined with tiling. In this case, the tiles form hi ## The hierarchical engine -... +The hierarchical engine can be based on a guiding shape/intruder approach. + +Consider a simple boolean operation - for example a NOT operation. In this case there is a subject shape from the first layer and zero or many intruder shapes per subject shape. The intruder shapes come from the second layer. Knowing all intruders for each subject shape allows implementing the NOT operation by simply subtracting the intruders from the subject. This operation is local: only intruders within a limited distance - in this less than zero, i.e. overlapping - will participate and the output of the operation is fully defined from the inputs (subject shape, intruders). + +The hierarchical approach only needs to identify intruders for each subject shape in a hierarchical fashion. For each subject shape inside a cell, intruders can originate from: + + * shapes from the current cell (shape-shape interactions) + * outside the tree of the current cell - i.e. siblings of the current cell (cell context interactions) + * child cells (bottom-up interactions) + +Taking these three interactions into account renders the following algorithm: + + * We start from the top cell. There is no context because there are no siblings of the top cell. + * Collect all shape-shape interactions between subject and intruder layer + * Collect shape-child cell interactions where the shapes come from the subject layer and the intruders from the child cells + * From the collected intruders per local shape compute the output and keep it in stock for the current cell + * For each child cell instance detect intruders by looking at + * Overlapping child cells adding intruders to the subject shapes of another instance + * Local intruder shapes adding intruders to subject shapes of an instance + * The intruder shapes for one instance form the cell context + * Treat each instance recursively by additionally taking the context into account: the context will add intruder shapes when considering subject shapes and instances inside this cell + * To harvest the benefit of the hierarchical approach we can skip each child cell if it has been handled before with identical context + +A further step involves recombination of the various context-dependent outputs of an operation into a part common to all cells and context-specific parts. The latter need to be placed into the parent cells where the context was derived from. + +This is a brief description of the idea. +