Simulation-based Approach to Verification of Logical Descriptions with Functional Indeterminacy

A verification task of proving the equivalence of two descriptions of the same device is examined for the case, when one of the descriptions is partially defined. In this case, the verification task is reduced to checking out whether logical descriptions are equivalent on the domain of the incompletely defined one. Simulation-based approach to solving this task for different vector forms of description representations is proposed. Fast Boolean computations over Boolean and ternary vectors having big sizes underlie the offered methods.

Operating Model of Knowledge Quantum Engineering for Decision-Making in Conditions of Indeterminacy

The operating model of knowledge quantum engineering for identification and prognostic decision- making in conditions of α-indeterminacy is suggested in the article. The synthesized operating model solves three basic tasks: Аt-task to formalize tk-knowledge; Вt-task to recognize (identify) objects according to observed results; Сt-task to extrapolate (prognosticate) the observed results. Operating derivation of identification and prognostic decisions using authentic different-level algorithmic knowledge quantum (using tRAKZ-method) assumes synthesis of authentic knowledge quantum database (BtkZ) using induction operator as a system of implicative laws, and then using deduction operator according to the observed tk-knowledge and BtkZ a derivation of identification or prognostic decisions in a form of new tk-knowledge.

Using SAT for Combinational Implementation Checking

The problem of checking whether a system of incompletely specified Boolean functions is implemented by the given combinational circuit is considered. The task is reduced to testing out if two given logical descriptions are equivalent on the domain of one of them having functional indeterminacy. We present a novel SAT-based verification method that is used for testing whether the given circuit satisfies all the conditions represented by the system of incompletely specified Boolean functions.