The High-Speed Simulator (HSS) is a fast and flexible system for gate-level fault simulation. Originally limited to combinational logic, it is being extended to handle sequential logic. It may also prove useful as a functional simulator. The speed of HSS is obtained by converting the cycle-free portions of a circuit into optimized machine code for a general-purpose computer. This compiled code simulates the circuit's response for 16 or 32 test patterns in parallel. Faults are injected into the circuit by changing the machine instruction corresponding to the fault location. From the range of speeds seen in recent measurements, we take 240 million gates per second as a fair general estimate of the speed of 2-valued simulation running on a 3081/K computer. For 3-valued simulation, divide by 2.9. The paper discusses the merits and drawbacks of the HSS strategy. It also sketches the extensions of HSS to model sequential logic and the various applications of HSS. These include functional verification, design for testability, good machine signatures, and accurate simulation of transistor-level defects in certain CMOS technologies. Finally, there is some discussion of how the simulation requirements of future designs can be met, and of the lessons to be drawn from long-term experimentation with HSS.

Finite automata which communicate with counters or with tapes on a single letter alphabet with end mark are studied.A typical machine system s~udied here consists of a family of machines; the finite automaton part of each of the machines is ideutical; each machine has one reset counter (Mmost blank loop tape) and one non-reset counter (ahnost blank straight tape) ; the first counter counts up to a, say, and the second comets up to b.For each pair of natural numbers a, b there is a machine of the system with counters running up to a, b respectively.The system "accepts" those pairs (a, b) such that the (a, b)-nmchine eventually halts, when started in standard position.Thus the system de* fines a binary relation on natural numbers.Some solvability and unsolvability results are obtained concerning the emptiness of the set accepted by a system or the emptiness of the intersection of the sets accepted by two or more systems.Some of the theorems strengthen results of Rabin and Scott [8].It is shown for a certain class of systems that the relations defined by them are exactly the same as those definable in the elementary theory of addition of natural numbers.For another class of systems it is shown that an intersection problem is equivalent to Hilbert's tenth problem.

Ianov has defined a formal abstraction of the notion of program which represents the sequential and control properties of a program but suppresses the details of the operations. For these schemata he defines a notion corresponding to computation and defines equivalence of schemata in terms of it. He then gives a decision procedure for equivalence of schemata, and a deductive formalism for generating schemata equivalent to a given one. The present paper is intended, first as an exposition of Ianov's results and simplification of his method, and second to point out certain generalizations and extensions of it. We define a somewhat generalized version of the notion of schema, in a language similar to that used in finite automata theory, and present a simple algorithm for the equivalence problem solved by Ianov. We also point out that the same problem for an extended notion of schema, considered rather briefly by Ianov, is just the equivalence problem for finite automata, which has been solved, although the decision procedure is rather long for practical use. A simple procedure for generating all schemata equivalent to a given schema is also indicated.

This paper presents a class of plausible definitions for validity of formulas in the infinitely-many-valued extension of the Łukasiewicz predicate calculus, and shows that all of them are equivalent. This extended system is discussed in some form in [3] and [4]; the questions discussed here are raised rather briefly in the latter. We first describe the formal framework for the validity definition. The symbols to be used are the following: the connectives + and ‐, which are the strong disjunction B of [2] and negation respectively; the predicate variables Pi for i ∈ I, where I may be taken as the integers; the existential quantifiers E(J), where J⊆I, and I may be thought of as the index set on the individual variables, which however do not appear explicitly in this formulation.