A major challenge with the practical deployment of Internet-of-Things (IoTs) is how to develop the high-quality code needed in order to produce robust and secure IoT devices. In other domains, high-level programming languages have shown to be efficient vehicles towards this. However, the very limited compute power provided by IoT devices have made it difficult to apply the same approach to IoT devices. The Cephalopode processor is an attempt at implementing a low power hardware device directly aimed at running a high-level functional language. By integrating many resource-heavy tasks like garbage collection and arbitrary precision arithmetic into dedicated hardware, the Cephalopode processor explores the hypothesis that high-level functional languages can be used even for low-power IoT devices. This paper presents the implementation and evaluation of the Cephalopode processor. We discuss the approach taken, the compiler and the architecture of the processor. We also describe the design process and design considerations. After implementation and synthesis we compare the processor to a conventional RISC-V processor running a functional language software environment. We also compare Cephalopode with running handwritten C code on the RISC-V processor.

Domain-specific hardware design has become increasingly attractive as single-thread performance improvement has drastically slowed down. At the same time, it is clear that traditional hardware design approaches are difficult and error-prone. In this paper we describe a hardware design language, Bifröst, aimed at allowing clear, correct, and modular specification of hardware. Bifröst is tightly integrated into the Thor system, and thus a design in Bifröst can be refined in a correctness-preserving way to a realistic hardware implementation. This paper gives both syntax and semantics of the language, highlights important design decisions, and illustrates its use in several projects.

The Internet of Things (IoT) conceives a future where "things" are interconnected by means of suitable information and communication technologies. Unfortunately, recent events have demonstrated the high vulnerability of IoT. One of the main reasons for this is the use of low-level programming languages. The Octopi project is developing technologies to easily and securely program IoT devices by the use of functional high-level languages. Unfortunately, a traditional implementation of a modern functional language that runs on traditional hardware is very resource demanding. So resource demanding that few, if any, IoT devices can run them.In the Cephalopode project (which is a subproject of Octopi) we are exploring the implementation of a very low power hardware device directly aimed at running a high-level functional language. By integrating many resource-heavy tasks into dedicated hardware, we aim at creating an execution engine for IoT devices that will allow secure programming.

Finite state machines (FSMs) are at the heart of many digital circuits, in particular microprocessors such as the IoT-oriented Cephalopode processor we are implementing as part of the Octopi project.We frequently encounter two practical difficulties with FSM design: first, in the case of Mealy machines state transitions and output logic can have complex and overlapping conditions, which are difficult to maintain and comprehend if separated; and second, there is a tension between clarity and clock cycles with respect to the insertion of intermediate states.To address these in the context of the Cephalopode processor we developed the open-source tool Stately, a visual environment for designing finite state machines. States are organized spatially, individually programmed in a simple domain-specific language, and the resulting machine can be compiled to HFL code for the VossII hardware design and simulation platform.In addition to allowing the intermingling of transitions and output declarations, Stately introduces a mechanism by which chosen states can be merged during compilation. While only a modest semantic extension, it resolves several clarity-efficiency tradeoffs while retaining a clear visual interpretation. Other features include lightweight simulation for rudimentary testing, and extensive error-checking.

Symbolic trajectory evaluation (STE) is a model checking technology based on symbolic simulation over a lattice of abstract state sets. The STE algorithm operates over families of these abstractions encoded by Boolean formulas, enabling verification with many different abstraction cases in a single modelchecking run. This provides a flexible way to achieve partitioned data abstraction. It is usually called "symbolic indexing' and is widely used in memory verification, but has seen relatively limited adoption elsewhere, primarily because users typically have to create the right indexed family of abstractions manually. This work provides the first known algorithm that automatically computes these partitioned abstractions given a reference-model specification. Our experimental results show that this approach not only simplifies memory verification, but also enables handling completely different designs fully automatically.

The Forte formal verification environment for datapath-dominated hardware is described. Forte has proven to be effective in large-scale industrial trials and combines an efficient linear-time logic model-checking algorithm, namely the symbolic trajectory evaluation (STE), with lightweight theorem proving in higher-order logic. These are tightly integrated in a general-purpose functional programming language, which both allows the system to be easily customized and at the same time serves as a specification language. The design philosophy behind Forte is presented and the elements of the verification methodology that make it effective in practice are also described.

Symbolic trajectory evaluation (STE) is a lattice-based model checking technology that uses a form of symbolic simulation. It offers an alternative to 'classical' symbolic model checking that, within its domain of applicability, often is much easier to use and much less sensitive to state explosion. The limitation of STE, however, is that it can only express and verify properties over finite time intervals. In this paper, we present a generalized STE (GSTE) that extends STE style model checking to properties over infinite time intervals. We further strengthen the power of GSTE by introducing a form of backward symbolic simulation. It can be shown that these extensions together with a notion of fairness give STE the power to verify all /spl omega/-regular properties. The generalization also gives one the power to choose and adjust the level of model abstraction in a verification effort. We shall use a large-scale industrial memory design to demonstrate the strength and practicality of GSTE.

Symbolic trajectory evaluation (STE) is a lattice-based model checking technology based on a form of symbolic simulation. It offers an alternative to 'classical' symbolic model checking that, within its domain of applicability, often is much easier to use and much less sensitive to state explosion. The limitation of STE, however, is that it can only express and verify properties over finite time intervals. In this paper, we present a generalized STE (GSTE) that extends STE style model checking to properties over infinite time intervals. We further strengthen the power of GSTE by introducing a form of backward symbolic simulation. It can be shown that these extensions, together with a notion of fairness, give STE the power to verify all /spl omega/-regular properties. We use a large-scale industrial memory design to demonstrate the power and practicality of GSTE.

Contemporary microprocessors implement many iterative algorithms. For example, the front-end of a microprocessor repeatedly fetches and decodes instructions while updating internal state such as the program counter; floating-point circuits perform divide and square root computations iteratively. Iterative algorithms often have complex implementations because of performance optimizations like result speculation, re-timing and circuit redundancies. Verifying these iterative circuits against high-level specifications requires two steps: reasoning about the algorithm itself and verifying the implementation against the algorithm. In this paper we discuss the verification of four iterative circuits from Intel microprocessor designs. These verifications were performed using Forte, a custom-built verification system; we discuss the Forte features necessary for our approach. Finally, we discuss how we maintained these proofs in the face of evolving design implementations.

No abstract available.

We describe the use of parametric representations of Boolean predicates to encode data-space constraints and significantly extend the capacity of formal verification.The constraints are used to decompose verifications by sets of case splits and to restrict verifications by validity conditions.Our technique is applicable to any symbolic simulator.We illustrate our technique on state-of-the-art Intel (R) designs, without removing latches or modifying the circuits in any way.

We describe the verification of the IM: a large, complex (12,000gates and 1100 latches) circuit that detects and marks the boundariesbetween Intel architecture (IA-32) instructions. We verified agate-level model of the IM against an implementation-independentspecification of IA-32 instruction lengths. We used theorem provingto to derive 56 model-checking runs and to verify that the model-checkingruns imply that the IM meets the specification for all possiblesequences of IA-32 instructions. Our verification discoveredeight previously unknown bugs.

Floating-point circuits are notoriously difficult to design and verify. For verification, simulation barely offers adequate coverage, conventional model-checking techniques are infeasible, and theorem-proving based verification is not sufficiently mature. In this paper we present the formal verification of a radix-eight, pipelined, IEEE double-precision floating-point multiplier. The verification was carried out using a mixture of model-checking and theorem-proving techniques in the Voss hardware verification system. By combining model-checking and theorem-proving we were able to build on the strengths of both areas and achieve significant results with a reasonable amount of effort.

Formal hardware verification based on symbolic trajectory evaluation shows considerable promise in verifying medium to large scale VLSI designs with a high degree of automation. However, in order to verify today's designs, a method for composing partial verification results is needed. This paper presents a theory of composition for symbolic trajectory evaluation and shows how implementing this theory using a specialized theorem prover is very attractive. Symbolic trajectory evaluation is used to prove low level properties of a circuit, and these properties are combined using the prover. Providing a powerful and flexible interface to a coherent system (with automatic assistance in parts) reduces the load on the human verifier. This hybrid approach, coupled with powerful and simple data representation, increases the range of circuits which can be verified using trajectory evaluation. The paper concludes with two examples. One example is the complete verification of a 64 b multiplier which takes approximately 15 minutes on a SPARC 10 machine.>

Given two models of a circuit, Q and Q', we say that Q' as a refinement of Q if every possible behavior of Q' is allowed by Q. We present a unified framework for verifying refinement using both model-checking and symbolic trajectory evaluation techniques. In this framework, the refinement conditions are derived and verified automatically. To demonstrate this approach, we present a design for a synchronizer circuit used in a high-speed synchronous design.>

A novel approach to formal hardware verification results from the combination of symbolic trajectory evaluation and interactive theorem-pmviug.From symbolic trajectory evaluation we inherit a high degree of automation and accurate models of circuit behavionr and timing.From interactive theorempmving we gain access to powerful mathematical tools such as induction and abstraction.We have prototype a hybrid tool and used this tool to obtain verification results that could not be easily obtained with previously published techniques.

Symbolic trajectory evaluation is a new approach to formal hardware verification combining the circuit modeling capabilities of symbolic logic simulation with some of the analytic methods found in temporal logic model checkers.We have created such an evaluator by extending the symbolic switch-level simulator COSMOS.This program gains added efficiency by exploiting the ability of COSMOS to evaluate circuit operation over a ternary logic model, where the third value X represents an unknown logic value.This program can formally verify systems containing complex featurea such as switch-level models, detailed timing, and pipelining.

In order to detect potential timing problems caused by small deviations of the internal delays in a VLSI circuit, a delay model is proposed in which the sizes of the delays are bounded by lower and upper bounds. He then introduces a race model, called the extended bounded delay (XBD) model, is presented, which can be used to predict the behavior of a circuit when the circuit is started in a stable state and some inputs change. The XBD race model is continuous and computationally intractable. A description is also given of an efficient algorithm, called the ternary bounded delay (TBD) algorithm, and it is shown that the results of this algorithm exactly summarize the behavior of the network according to the XBD race model. The author has implemented the TBD algorithm in the COSMOS switch-level simulator, and early results show that the overhead is small compared with standard unit delay simulation.>

A unified framework is developed for the study of asynchronous circuits of both gate and MOS type. A basic network model consisting of a directed graph and a set of vertex excitation functions is introduced. A race analysis model, using three values (0, 1, and x), is developed for studying state transitions in the network. It is shown that the results obtained using this model are equivalent to those using ternary simulation. It is also proved that the set of state variables can be reduced to a minimum size set of feedback variables, and the analysis still yields both the correct state transitions and output hazard information. Finally, it is shown how the general results above are applicable to both gate and MOS circuits.

Ternary simulation techniques provide efficient methods for the analysis of the behavior of VLSI circuits. However, the results of ternary simulation have not been completely characterized. In this paper we prove a somewhat modified version of the Brzozowski-Yoeli conjecture (stated in 1976) that the results of the ternary simulation of a gate network N correspond to the results of the binary race analysis of Ñ in the ``multiple-winner'' model, where Ñ is the network N in which a delay has been inserted in each wire.

A robust storage structure is intended to provide the ability to detect and possibly correct damage to the structure. One possible source of damage is the partial completion of an update operation, due to a "crash" of the program or system performing the update. Since adding redundancy to a structure increases the number of fields which must be changed, it is not clear whether adding redundancy will help or hinder crash recovery. This paper examines some of the general principles of using robust storage structures for crash recovery. It also describes a particular class of linked list structures which can be made arbitrarily robust, and which are all suitable for crash recovery.