Today, circuits are used in various safety-critical systems, therefore yielding a high demand for reliable systems. Consequently, a lot of research is conducted to improve the testability of designs by increasing the test coverage or reducing the required test time. In this context, provable computational bounds are crucial to ensure fast test pattern generation. Previous works proved polynomial test set generation for Binary Decision Diagram (BDD) circuits. Later, the testability of Kronecker Functional Decision Diagrams (KFDDs) was assessed, as KFDDs can exponentially reduce the required logic. However, the test set generation for KFDD circuits generally requires exponential resources. In this paper, we present a technique to derive circuits from KFDDs, for which a complete test set under the Cellular Fault Model (CFM), as well as the Stuck-At Fault Model (SAFM), can be generated within polynomial resources. The derived circuit is linear in size regarding the KFDD size, and in contrast to previously derived KFDD circuits, no redundant faults can occur, yielding fully testable circuits under CFM and SAFM. In our evaluation, the complete test set generation was up to 50 times faster than the previous exponential method, clearly showcasing the advantages of our polynomial approach.

Trust in electronic devices is dependent on their safe and reliable behavior. An integral part is the correct design of the hardware. While classically simulation-based approaches have been applied, only through formal proof techniques complete correctness can be guaranteed. The core of these formal approaches, and responsible for time and space complexity, is the choice of the underlying data structure to represent the functional behavior. A significant class of data structures are graph-based function representations, like BDDs, KFDDs or *BMDs. These have shown excellent properties – provability in polynomial time and space – for some function classes, e.g., adders. Experimental studies have validated these properties, and formal proofs can guarantee this behavior. Unfortunately, these properties often cannot be generalized to varying function classes. One reason is that graph-based representations are usually tailored for either bit-level or word-level functions. However, designing hybrid data structures that can represent both types in parallel might allow formal proofs for even larger functional classes.In this paper, we demonstrate how to design these hybrid data structures, overcoming limitations of current formal verification approaches. We introduce a generalized concept on decompositions and graph-based function representations based on Kronecker matrices with an extended element space and dimension. It is shown how these extensions allow the representation of hybrid function classes, paving the way for more trust in electronic devices.

To ensure the functional correctness of digital circuits, formal verification methods have been established, where the circuits are proven to implement the correct function. Several methods exist for the execution of the verification process. However, the verification process can have an exponential time or space complexity, causing the verification to fail. While exponen-tial in general, recently it has been proven that the verification complexity of several circuits is polynomially bounded. In this paper, we prove the polynomial verifiability of several state-of-the-art approximate adders using BDDs. These approx-imate adders include handcrafted approximate adders, which consist of several subadders, as well as automatically generated approximate adders, where regular adders can be arbitrarily altered by removing gates and changing the type of gates. Thus, this paper provides insight into the possible methods for the design of approximate adders, such that the approximate adders remain polynomially verifiable. Here, we give upper bounds for the BDD sizes during the verification process, as well as for the time and space complexity. The upper bounds for the BDD sizes are then experimentally evaluated.