In order to enhance the readability and to simplify the verification of temporal logic programs in the XYZ system,we propose a structured temporal logic language called XYZ/SE,based on XYZ/BE which is the basis language of the XYZ system.A set of proof rules are given and proved to be sound and adequate for proving the partial correctness of XYZ/SE programs in a compositional way.Moreover,we show that every XYZ/BE program can be transformed into an equivalent XYZ/SE program.So we have developed a general co…

A formal technique for incorporating two specification paradigms is presented,in which an algebraic specifi- cation is implemented by a set of abstract procedures specified in pre- and post-condition style.The link be- tween the two level specifications is provided via a translation from terms of algebraic specifications into tempo- ral logic formulae representing abstract programs.In terms of translation,a criterion for an abstract implementation satisfying its specification is given,which allows one to ch…

Data Flow Diagram(DFD)has been widely used in Software Engineering as means of require- ment analysis and system specification.However,one defect of DFD approach remains untackled: the lack of formal semantics has brought about a lot of problems.In this paper,we model Data Flow Diagram as networks of concurrent processes.With the use of temporal logic language XYZ/E,the formal basis of the semantic specification of DFD can be ensured,and the system prop- erties sach as safety and liveness can be easily char…

A new explanation of quaternary Q gate expression in Post algebra is given in this paper by using transmission function theory proposed in [1] and the quaternary ECL Q gate circuit is de- signed.The SPICE2 simulation to this circuit has confirmed that it has desired logical function and is totally compatible with various quaternary ECL circuits proposed before.

This paper presents a functional language for the unambiguous description of digital circuits,a me- thod and algorithms to obtain a standard-cell layout,and a comparative evaluation of the developed func- tional standard-cell placement technique.The presented placement scheme is different from traditional methods because the complete layout geometry is specified and constructed automatically from a function- al description.The construction relies on a translation that combines the simplicity of standard-cel…

This paper proposes an approach to synthesize functional programs of Backus FP system from input/output instances.Based on a theory of orthogonal expansion of programs,the task of program synthesis is expressed in program equations,and fulfilled by solving them according to the knowledge about the equivalence between programs.Some general knowledge of solving program equations with a number of examples are given in the paper.

To use reasoning knowledge accurately and efficiently,many reasoning methods have been proposed. However,the differences in form among the methods may obstruct the systematical analysis and harmonious integration of them.In this paper,a common reasoning model JUM(Judgement Model)is introduced. According to JUM,a common knowledge representation form is abstracted from different reasoning methods and its limitation is reduced.We also propose an algorithm for transforming one type of JUMs into another.In some ...

Nondeterminism of PROLOG execution requires that a block of control information or a choice point for each procedure call be stored when there are other candidate clauses to be used.When the currently selected clause fails,the bindings made by the clause must be undone and the stored choice point is reactivated,and then another clause of the candidate ones is chosen to run on it. Storing and reactivating choice points and undoing account for the great overhead are required to control PROLOG execution,which …

It is known that critical path test generation method is not a complete algorithm for combinational circuits with reconvergent-fanout.In order to make it a complete algorithm,we put forward a reconvergent-fanout- oriented technique,the principal critical path algorithm,propagating the critical value back to primary inputs along a single path,the principal critical path,and allowing multiple path sensitization if needed.Relationship among test patterns is also discussed to accelerate test generation.

Sequential diagnosis is a very useful strategy for system-level fault identification because of its lower cost of hardware.In this paper,the characterization of sequentially t-diagnosable system is given,and a tmiversal algorithm to seek faulty units in the system is developed.

In this paper,a fast algorithm for polygon operations is introduced.The intersection validation testing method is described.

Existing global microcode compaction approaches have all assumed a target architecture that has microoperation conflicts and data dependencies as the two fundamental compaction constraints.However, new practical micromachine features demand that the timing constraint be introduced into the traditional compaction model to guarantee compaction correctness.This paper starts by an analysis on the nature of timing constraints,then modifies the roles for microoperation motions,presents an algorithm,TST,based on T…

A lambda system with algebraic operators,lambda-plus system,is introduced.After giving the definitions of the system,we present a sufficient condition for formulating a model of the system. Finally,a model of such system is constructed.