Browse Prior Art Database

LSSD Rule Checking As a Formal Proof Mechanism

IP.com Disclosure Number: IPCOM000043557D
Original Publication Date: 1984-Sep-01
Included in the Prior Art Database: 2005-Feb-05
Document File: 3 page(s) / 16K

Publishing Venue

IBM

Related People

Horstmann, PW: AUTHOR

Abstract

Level sensitive scan design (LSSD)-type design rules can be checked by a method using formal first-order logic. By expressing a logic design as a set of interconnected functions using a program called PROLOG, the compliance of a design to a given set of design rules can be proven using a theorem prover. The logic implementation used is the PROLOG system/language published by D. H. Warren at the University of Edinburgh in 1977 as Research Reports 39 and 40 of the Department of Artificial Intelligence. The use of first-order logic instead of the more standard algorithmic approaches for LSSD rules checking has the following advantages: 1. The rules can be checked at the functional level of the design description (instead of at the logic primitive).

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 50% of the total text.

Page 1 of 3

LSSD Rule Checking As a Formal Proof Mechanism

Level sensitive scan design (LSSD)-type design rules can be checked by a method using formal first-order logic. By expressing a logic design as a set of interconnected functions using a program called PROLOG, the compliance of a design to a given set of design rules can be proven using a theorem prover. The logic implementation used is the PROLOG system/language published by D. H. Warren at the University of Edinburgh in 1977 as Research Reports 39 and 40 of the Department of Artificial Intelligence. The use of first-order logic instead of the more standard algorithmic approaches for LSSD rules checking has the following advantages: 1. The rules can be checked at the functional level of the design description (instead of at the logic primitive).

New functions are easily added to the system as additional

logic clauses and facts. 2. The rules are expressed as logic constructs

(clauses) which allow them to be readily modified

independent of the checking system. The rules can be

changed to fit the current design methodology being used. 3. Since the proof process is complete, any design which passes all of the rules has met the exact letter of

the rules' intent. In addition to the formal proof, the

information generated during the proof process is accessible

by the designer (or an interface program) and can be used to

assist in the correction of any rule violations. The actual construction of the LSSD rules checker consists of the following elements: 1. The design interconnection description expressed in terms of logic facts. These facts describe the connection

of the various functional elements of the design. Each fact

contains the node (block) name, the node's function (name),

the list of the node's successors, and the list of the

node's predecessors. 2. The functional element behavior expressed in terms of logic facts and clauses. Each function exists as a set

of PROLOG clauses which define it as a theory. Examples of

functions are AND, ADDER, MULTIPLEXER, shift register latch

(SRL), LATCH, etc. Essentially these clauses state the

expected output given a set of input values and/or the

required input values given a set of output conditions.

This bidirectional behavior is one of the attributes of

logic programming, in that once the function is logically

defined, the evaluation of that function can be either

top-down (input driven) or bottom-up (output driven). 3. Various inference (manipulatory) clauses which define the logical meaning of functions, interconnections,

signal types, etc. These clauses are required to allow the

theorem prover to traverse the design theory (description)

and function set. A simple example of this type of clause

is the CONNECT clause. Its general format is given below:

CONNECT(Node1,Node2,Control) - PROLOG definition.

1

Page 2 of 3

This clause will succeed (be true) if Node1 is connected

to Node2, if there exists a Node1 such that Node2 is its

successor, or if...