For formal verification of large-scale digital circuits, a method using satisfiability checking of logic with equality and uninterpreted functions has been proposed. This logic, however, does not consider specific properties of functions or predicates at all, e.g. associative property of addition. In order to ease this problem, we introduce "equivalence constraint" that is a set of formulas representing the properties of functions and predicates, and check the satisfiability of formulas under the constraint. In this report, we show an algorithm for checking satisfiability with equivalence constraint and also experimental results.

One important question for quantum computing is whether a computational gap exists between models that are allowed to use quantum effects and models that are not. Several types of quantum computation models have been proposed, including quantum finite automata and quantum pushdown automata (with a quantum pushdown stack). It has been shown that some quantum computation models are more powerful than their classical counterparts and others are not since quantum computation models are required to obey such restrictions as reversible state transitions. In this paper, we investigate the power of quantum pushdown automata whose stacks are assumed to be implemented as classical devices, and show that they are strictly more powerful than their classical counterparts under the perfect-soundness condition, where perfect-soundness means that an automaton never accepts a word that is not in the language. That is, we show that our model can simulate any probabilistic pushdown automata and also show that there is a non-context-free language which quantum pushdown automata with classical stack operations can recognize with perfect soundness.

A graph is said to be outerplanar if it has a planar embedding in which all vertices lie on the exterior face. For a graph G=(V, E), its spanning subgraph G =(V, E ) is called a maximal outerplanar spanning subgraph (abbreviated as mosg) if G is outerplanar and (V, E") is not outerplanar for any edge set E" such that E E"E. In this paper, we present a linear-time algorithm for finding an mosg of a given graph.

The paper is concerned with solutions to permutation layout problems such that i) no wire passes the upper area of the upper horizontal line, and ii) no wire intersects the lower horizontal line more than once. A necessary and sufficient condition for a problem to have such a solution is given. The set of all the solutions to the given problem is characterized in a graph theoretical way. A linear time algorithm is also given.

In this paper we propose an algorithm for generating maximum weight independent sets in a circle graph, that is, for putting out all maximum weight independent sets one by one without duplication. The time complexity is O(n3 + β ), where n is the number of vertices, β output size, i. e. , the sum of the cardinalities of the output sets. It is shown that the same approach can be applied for spider graphs and for circular-arc overlap graphs.

There are two approaches for formal verification of sequential designs or finite state machines: language containment checking and symbolic model checking. To verify designs of practical size, in these two approaches, designs are represented symbolically, in practice, by ordered binary decision diagrams. In the conventional algorithm for language containment checking, finite automata given as specifications are also represented symbolically. This paper proposes a new method, called partially explicit method for checking language containment. By representing states of finite automata given as specifications explicitly, this method can remove redundant computations, and as a result, provide better performance than the conventional method which uses the product machines of designs and specifications. The experimental results show that this approach is effective in checking language containment symbolically.

The class NQP was proposed as the class of problems that are solvable by non-deterministic quantum Turing machines in polynomial time. In this paper, we introduce non-deterministic quantum finite automata in which the same non-determinism as in non-deterministic quantum Turing machines is applied. We compare non-deterministic quantum finite automata with the classical counterparts, and show that (unlike the case of classical finite automata) the class of languages recognizable by non-deterministic quantum finite automata properly contains the class of all regular languages.

Suppose that there are terminals on two concentric circles Cin and Cout, with Cin inside of Cout. A set of two-terminal nets is given and the routing area is the annular region between the two circles. In this paper, we present an O(n2) time algorithm for testing whether the given net set is two-layer routable, where n is the number of nets. Applying this algorithm repeatedly, we can find, in O(n3) time, a maximal subset of nets which is two-layer routable.

Suppose that there are terminals on two concentric circles, Cin and Cout, with Cin inside of Cout. We are given a set of nets each of which consists of a terminal on Cin and a terminal on Cout. The routing area is the annular region between the two circles. In this paper, we present an O(nk-1) time algorithm for testing whether the given net set is k-layer routable without vias, where k2 and n is the number of nets.

A kind of online edge-coloring problems on bipartite graphs is considered. The input is a graph (typically with no edges) and a sequence of operations (edge addition and edge deletion) under the restriction that at any time the graph is bipartite and degree-bounded by k, where k is a prescribed integer. At the time of edge addition, the added edge can be irrevocably assigned a color or be left uncolored. No other coloring or color alteration is allowed. The problem is to assign colors as many times as possible using k colors. Two algorithms are presented: one with competitiveness coefficient 1/4 against oblivious adversaries, and one with competitiveness coefficient between 1/4 and 1/2 with the cost of requiring more random bits than the former algorithm, also against oblivious adversaries.

This paper deals with formal verification of high-level designs, in particular, symbolic comparison of register-transfer-level descriptions and behavioral descriptions. We use state machines extended by quantifier-free first-order logic with equality, as models of those descriptions. We cannot adopt the classical notion of equivalence for state machines, because the signals in the corresponding outputs of such two descriptions do not change in the same way. This paper defines a new notion of consistency based on signal-transitions of the corresponding outputs, and proposes an algorithm for checking consistency of those descriptions, up to a limited number of steps from initial states. As an example of high-level designs, we take a simple hardware/software codesign. A C program for digital signal processing called PARCOR filter was compared with its corresponding design given as a register-transfer-level description, which is composed of a VLIW architecture and assembly code. Since this example terminates within approximately 4500 steps, symbolic exploration of a finite number of steps is sufficient to verify the descriptions. Our prototype verifier succeeded in the verification of this example in 31 minutes.

A binary moment diagram, which was proposed for arithmetic circuit verification, is a directed acyclic graph representing a function from binary-vectors to integers (f : {0,1}n Z). A multiplicative binary moment diagram is an extension of a binary moment diagram with edge weights attached. A multiplicative binary moment diagram can represent addition, multiplication and many other functions with polynomial numbers of vertices. Lower bounds for division, however, had not been investigated. In this paper, we show an exponential lower bound on the number of vertices of a multiplicative binary moment diagram representing a quotient function or a remainder function.

In this paper is given a necessary and sufficient condition for a permutation layout problem to have a wiring pattern such that no wire passes the upper area of the upper horizontal line, no wire intersects the lower horizontal line more than once, and between-pins congestion is not more than k, where the portion of the lower horizontal line which is placed to the left (resp., right) of the leftmost (resp., rightmost) terminal is considered to be a between-pins spacing. A linear time algorithm is given for the case k1, based on a graph theoretical representation of the condition.

Let G = (A, B, E) be a bipartite graph with bipartition (A:B) of vertex set and edge set E. For each vertex v, Γ(v) denotes the set of adjacent vertices to v. G is said to be t-convex on the vertex set A if there is a tree and a one-to-one correspondence between vertices in A and edges of the tree such that for each vertex b B the edges of the tree corresponding to vertices in Γ(b) form a path on the tree. G is doubly t-convex if it is convex both on vertex set A and on B. In this paper, we show that, the class of doubly t-convex graphs is exactly the class of bipartite circle graphs.

Let H=(V(H),E(H)) be a directed graph with distinguished vertices s and t. An st-path in H is a simple directed path starting from s and ending at t. Let (H) be defined as { SS is the set of vertices on an st-path in H (s and t are excluded)}. For an undirected graph G=(V(G),E(G)) with V(G) V(H)- { s,t }, if the family of maximal independent sets of G coincides with (H), we call H an MIS-diagram for G. In this paper, we provide a necessary and sufficient condition for a directed graph to be an MIS-diagram for an undirected graph. We also show that an undirected graph G has an MIS-diagram iff G is a cocomparability graph. Based on the proof of the latter result, we can construct an efficient algorithm for generating all maximal independent sets of a cocomparability graph.

In this paper we present polynomial time algorithms for the following three problems on a Hamilton graph with a prescribed Hamilton circuit: (1) Given a Hamilton graph G with a prescribed Hamilton circuit, find a maximal planar Hamilton subgraph of G, (2) Given a Hamilton graph G and a planar Hamilton subgraph H of G, find a maximal planar Hamilton subgraph of G that contains H, and (3) Given an edge-weighted Hamilton graph G=(V, E), find a planar Hamilton subgraph G=(V, E) of G such that the addition of an edge e E-Edestroys the planarity, unless we delete an edge from Ehaving no less weight than e. The time complexities of the algorithms are O(n+m), O(m3/2) and O(m5/3), respectively, where n(resp., m) is the number of vertices (resp., edges) of the Hamilton graph. These algorithms are applicable to the Topological Via Minimization problem.