Design verification is the task of establishing that a given design
meets the intended behavior. The growing complexity of verification
instances requires new methods that can provide high quality
verification coverage for large, complex designs. Probabilistic
verification complements existing simulation-based and formal
verification techniques by providing a distinct trade-off between
coverage and capacity. Probabilistic approach maps two Boolean
functions onto hash values and compare these values for
equivalence. The major drawback of probabilistic verification is the
non-zero probability of collision of hash values of two non-equivalent
functions, producing "false positive" verification results. In this
paper, we prove the existence of a perfect input assignment
which never causes collisions. We show that the equivalence of hash
values computed for a perfect input assignment implies the equivalence
of functions with 100% probability.
Boolean decomposition techniques offer a powerful alternative to traditional algebraic methods when partitioning a circuit graph in the technology independent stage of the circuit design flow. These techniques usually require to transform the circuit from a structural representation to a representation based on Binary Decision Diagrams (BDDs). It is well known that BDDs can grow exponentially in some cases, so the power of Boolean decomposition comes at the expense of an exponential increase in the size of the circuit representation. The following stages in the design flow may suffer severely from the space penalty imposed on each partitioned block. To cope with this space explosion, each block of the partitioned circuit has to be re-synthesized before further processing. The extra re-synthesis, on the other hand, may impose a prohibitive time/space penalty on the design flow.
This paper proposes an inexpensive technique to avoid re-synthesizing the BDD blocks obtained after Boolean decomposition. This technique works by
structurally partitioning the original circuit representation, according to information provided by the partitioned BDD blocks. After all the blocks have been recovered, the BDDs are not needed and can be discarded. The resulting circuit will be proportional to the original circuit representation, and not to the intermediate BDD representation.
A random Boolean network is a synchronous Boolean automaton with n
vertices. The parameters of an RBN can be tuned so that its
statistical features match the characteristics of the gene regulatory
system. The number of vertices of the RBN represents the number of
genes in the cell. The number of cycles in the RBN's state space,
called attractors, corresponds the number of different cell
types. Attractor's length corresponds to the cell cycle time.
Sensitivity of the attractors to different kind of perturbations,
modeled by changing the state of a particular vertex, associated
Boolean function, or network edge, reflects the stability of the cell
to damage, mutations and virus attacks. In order to evaluate the
attractors, their number and length have to be re-computed
repeatedly. For large RBN's, searching for attractors in the O(2<sup>n</sup>) state space is an infeasible task. Fortunately, only a subset of vertices of an RBN, called relevant vertices, determines its dynamics. The remaining vertices are redundant. In this paper, we present an algorithm for identifying redundant vertices in RBNs which allows us to reduce the search space for computing attractors from O(2
<sup>n</sup>) to Θ2<sup>√n</sup>. We also show how RBNs can be used for studying evolution.
Phylogenetic analysis is a branch of biology that establishes the
evolutionary relationships between living organisms. The goal of
phylogenetic analysis is to determine the order and approximate timing
of speciation events in the evolution of a given set of species.
Phylogenetic networks allow to represent evolutionary histories that
include events like recombination and hybridization. In this paper,
we introduce a class of phylogenetic networks called extended
galled-trees in which recombination cycles share no edge. We show
that the site consistency problem, which is NP-hard in general, can be
solved in polynomial time for this class of phylogenetic networks.
Molecular cascades introduced in provide new ways to exploit the motion of individual molecules in nanometer-scale structures. Computation is performed by purely mechanical means similarly to the toppling of a row of standing domino. A specific feature of molecular cascades is that an inverter cannot be build, because it would require that all molecules in the inverter's output untopple when the input cascade topples. This is not possible because
an untoppled state has higher energy than a toppled one. As a solution, we propose to avoid the need for inverters by representing
signals by the dual-rail convention. As a basic building block we use
a <i>molecular block</i>, which has four inputs x<sub>1</sub>,...,x<sub>4</sub> such that x<sub>3</sub> = x'<sub>1</sub>, x<sub>4</sub> = x' x<sub>2</sub>, and two outputs ƒ<sub>1</sub> = x<sub>1</sub> • x<sub>2</sub>
and ƒ<sub>2</sub> = x<sub>3</sub> + x<sub>4</sub>. If input variables are available in both complemented and non-complemented form, then any Boolean function can be implemented by a composition of such molecular blocks. We present an experimental tool which first uses a rule-based randomized search to optimize a Boolean network and then maps it into a network of interconnected molecular blocks.