Digital Circuits Date: Mon, 7 Feb 2000 From: Monica Nogueira To: TAG As a result of my visit and work with Michael in Lubbock on past weekends, I'm sending attached two problems: Prediction and Derivation of signal values on digital circuits. Which files are being sent? 1. circuit - contains the description of a general theory of digital circuits in A-Prolog. 2. prediction - description of the "output prediction problem". 3. derivation - description of the "input derivation problem". 4. derivation28 - descrition of a 28-gates circuit and goal for derivation problem. Our tests show that Smodels computation is feasible for both the prediction and the derivation problems. We have a simple example (included in the files) with 3-gates and a larger one with 28 gates (file derivation28). Here are the results so far: (all times in seconds) ---------------------------------------------------- | Prediction problem | Derivation problem | ---------------------------------------------------- | 3-gates | 28-gates | 3-gates | 28-gates | ---------------------------------------------------------------- 1 model | 0 | 0.79 | 0 | 6.59 | ---------------------------------------------------------------- all models | 0 | 0.79 | 0 | 12.30 | ---------------------------------------------------------------- The 28-gates derivation problem has 250 models because there are that many combinations given the delays associated with the gates, 4 input values, 10 output values and a time range of 0..5. The 0 (zero) secs time shown above is of course just an approximation. It is not possible to time more accurately the small problem (3-gates). Please let me know your questions and comments. Best regards, Monica --- File 'circuit' %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% General Theory of Digital Circuits in A-Prolog %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% %% Digital circuits consist of gates (AND, OR, NOT) %% connected by wires. Gates can possibly have propagation %% delays associated with them (no delay is expressed by zero). %% Input/output values (signals) are expressed in 3-valued %% logic (0, 1, u), where u stands for unknown. If no value %% has been applied to an input then it is said to be unknown. %% %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ % A language L for describing digital circuits will % have names for gates (g1, g2, g3, ...), gate types % (andg, org, notg), and wires (w1, w2, ...). % % is_gate(G) iff G is a gate. % % is_wire(W) iff W is a wire. % % gate(G,Y) iff gate G is of gate type Y. % To describe the geometry of the circuit (connection among % gates), we use the following relations: % output(W,G1) iff W is the output wire of gate G1. % % input(W,G2) iff W is the input wire of gate G2. % We represent a digital circuit by indicating the input and % output wires for each of its gates. To connect the output % of a gate G1 to an input of a gate G2 by a wire W, we simply % indicate that wire W is the output wire of gate G1 and also % that wire W is the input wire of gate G2. % Delays are represented by natural numbers. % No propagation delay is expressed by zero. % % delay(G,D) iff gate G has delay D. % Signals going through the circuit will be represented % by constants 0,1, u. % % We allow 3-valued logic to be used, therefore the values % of signals to be applied to input wires and to be propagated % through the gates will be 1, 0 or u. % If no value has been applied or is present on a wire then % it is said to be unknown (u). % signal(X) iff X is a signal present on the wire of a gate. signal(1). signal(0). signal(u). % These are all the relations/types required to describe % digital circuits. %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ % Since we are interested in working with digital circuits % involving propagation delays in a finite time range, % we need to represent time. In Smodels we can specify % this range as shown below. The upper bound constant % "lasttime" is defined to facilitate future references to this % limit. %const lasttime = 3. %time(0..lasttime). % next(T,T1) iff T1 is the next moment in time after time T. next(T,T1) :- time(T), time(T1), T1=T+1. %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ % Theory of digital circuits %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ % This theory describes the normal behavior of a digital circuit. % Given values of input wires at time T the theory determines % the values on other wires at all future moments of time. %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% Fluents %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ % value(Wire,Signal) - true if input or output value on Wire % is Signal. %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% Actions %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ % apply(Wire,Signal) if Signal is the value applied on Wire. %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% Effects of Acttions %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ % h(value(W,X),T) iff value X holds on wire W at time T. h(value(W,X),T) :- time(T), signal(X), is_wire(W), occurs(apply(W,X),T). %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% Static Laws for Gates Functioning %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% NOT Gate % If the input value of a NOT gate is 1 at time t and its delay % is d then its output value is 0 at time t+d. h(value(W2,0),T1) :- gate(G,notg), delay(G,D), time(T), time(T1), T1 = T+D, input(W1,G), output(W2,G), h(value(W1,1),T). % If the input value of a NOT gate is 0 at time t and its delay % is d then its output value is 1 at time t+d. h(value(W2,1),T1) :- gate(G,notg), delay(G,D), time(T), time(T1), T1 = T+D, input(W1,G), output(W2,G), h(value(W1,0),T). % If the input value of a NOT gate is u at time t and its delay % is d then its output value is u at time t+d. h(value(W2,u),T1) :- gate(G,notg), delay(G,D), time(T), time(T1), T1 = T+D, input(W1,G), output(W2,G), h(value(W1,u),T). % To represent the function of gates AND and OR, we need % some auxiliary predicates. % not_all(G,X,T) iff not all input wres of gate G % have value X at time T. not_all(G,X,T) :- time(T), is_gate(G), signal(X), signal(Y), neq(X,Y), input(W,G), h(value(W,Y),T). % all(G,X,T) iff all input wires of G have value X at time T. % Note that all input wires have a value (1,0,u) defined at % all moments of time since we have complete information % in the initial situation. all(G,X,T) :- time(T), is_gate(G), signal(X), not not_all(G,X,T). % contains(G,X,T) iff at least one input wire of G % has value X at time T. contains(G,X,T) :- time(T), signal(X), input(W,G), h(value(W,X),T). %% AND Gate % If all input wires of an AND gate have value 1 at time t % and its delay is d then its output value is 1 at time t+d. h(value(W,1),T1) :- gate(G,andg), delay(G,D), time(T), time(T1), T1 = T+D, output(W,G), all(G,1,T). % If at least one input wire of an AND gate has value 0 at time t % and its delay is d then its output value is 0 at time t+d. h(value(W,0),T1) :- gate(G,andg), delay(G,D), time(T), time(T1), T1 = T+D, output(W,G), contains(G,0,T). % If no input wires of an AND gate have value 0 and % at least one input wire has value u at time t, % and its delay is d then its output value is u at time t+d. h(value(W,u),T1) :- gate(G,andg), delay(G,D), time(T), time(T1), T1 = T+D, output(W,G), not contains(G,0,T), contains(G,u,T). %% OR Gate % If all input wires of an OR gate have value 0 at time t % and its delay is d then its output value is 0 at time t+d. h(value(W,0),T1) :- gate(G,org), delay(G,D), time(T), time(T1), T1 = T+D, output(W,G), all(G,0,T). % If at least one input wire of an OR gate has value 1 at time t % and its delay is d then its output value is 1 at time t+d. h(value(W,1),T1) :- gate(G,org), delay(G,D), time(T), time(T1), T1 = T+D, output(W,G), contains(G,1,T). % If no input wires of an OR gate have value 1, % at least one input wire has value u at time t % and its delay is d then its output value is u at time t+d. h(value(W,u),T1) :- gate(G,org), delay(G,D), time(T), time(T1), T1 = T+D, output(W,G), not contains(G,1,T), contains(G,u,T). %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% Inertia Law %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ h(value(W,X),T1) :- next(T,T1), signal(X), is_wire(W), h(value(W,X),T), not nh(value(W,X),T1). % We also need to express that there is at most one signal % present on a wire at certain moment of time. nh(value(W,X),T) :- time(T), signal(X), signal(Y), neq(X,Y), is_wire(W), h(value(W,Y),T). %% Consistency Constraint :- time(T), signal(X), is_wire(W), h(value(W,X),T), nh(value(W,X),T). % This completes our general theory of circuits. %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ --- File 'prediction' % THIS FILE CONTAINS AN A-Prolog SOLUTION TO "Output prediction problem" % for digital circuits. It should be used is conjunction with the file % "circuits" %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% Digital Circuit Problem %% "Output values prediction" %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% Here we are interested in solving the following problem: %% Given the description of a digital circuit and the values %% present at time T on the input wires of this circuit, %% we would like to be able to predict the values %% on all wires in the time interval from 0 to lasttime. %% Let's a circuit description be denoted by CD, a general theory %% of behavior of digital circuits by GT, and all input values on %% input wires of this circuit by IV. %% Definition 1: what it means for a gate to work properly? %% Given a digital circuit consisting of a gate G %% which performs function F and has propagation delay D, %% it is said to "work properly" if when inputs values I are %% applied to its input wires at time T, the output value V=F(I) %% will appear on its output wire at time T+D %% Definition 2: when is an input wire of a gate also an input wire %% for the whole circuit? %% Assume there are several gates connected such that the output %% wire of some gates is the same as the input wire of another gate. %% An input wire of a gate is said to be also an input wire for the %% whole circuit if this wire is not output wire of any gate of this %% circuit. %% Definition 3: when is an output wire of a gate also an output wire %% for the whole circuit? %% An output wire of a gate is said to be also an output wire for the %% whole circuit if this wire is not input wire of any gate of this %% circuit. %% Definition 4: when does a circuit work properly? %% Proposition: %% The theory of a digital circuit GT + CD + IV has a unique stable %% model SM and statements of the type h(value(W,X),T) belong to SM %% iff X is the value on wire W at time T in this circuit. %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% Graphical representation of digital circuit %% used in this example. %% %% ---- %% w1------| g1 |o-------w3 %% ---- | ------ %% -------| g3 |_____w5 %% -------| | %% ---- | ------ %% w2------| g2 |o-------w4 %% ---- %% %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% To achieve our goal, we need to describe the circuit and the %% initial values on its input wires. This is done in the language L %% as follows: % is_gate(G) iff G is a gate. is_gate(g1). is_gate(g2). is_gate(g3). % is_wire(W) iff W is a wire. is_wire(w1). is_wire(w2). is_wire(w3). is_wire(w4). is_wire(w5). % gate(G,Y) iff gate G is of gate type Y. gate(g1,notg). gate(g2,notg). gate(g3,andg). % delay(G,D) iff gate G has delay D. delay(g1,1). delay(g2,0). delay(g3,1). % Description of the circuit connections. input(w1,g1). output(w3,g1). input(w2,g2). output(w4,g2). input(w3,g3). input(w4,g3). output(w5,g3). % Time range is expressed as const lasttime = 4. time(0..lasttime). %% In the initial situation, if no value is applied %% to a wire then its value is u, by default. h(value(W,u),0) :- is_wire(W), not known_value(W,0). known_value(W,0) :- is_wire(W), h(value(W,1),0). known_value(W,0) :- is_wire(W), h(value(W,0),0). %% Input values are given by applying signals to wires, as %% Example1: occurs(apply(w1,0),1). occurs(apply(w2,0),0). %% Another example to try: %% occurs(apply(w1,1),1). %% occurs(apply(w2,0),3). %% occurs(apply(w1,0),4). hide input(X,Y). hide output(X,Y). hide time(X). hide is_wire(X). hide signal(X). hide delay(X,Y). hide gate(X,Y). hide next(X,Y). hide contains(X,Y,Z). hide all(X,Y,Z). hide not_all(X,Y,Z). hide nh(X,Y). hide is_gate(X). hide known_value(X,Y). --- File 'derivation' % THIS FILE CONTAINS AN A-Prolog SOLUTION TO "Input derivation problem" % for digital circuits. It should be used is conjunction with the file % "circuits" % INPUT DERIVATION PROBLEM: % Given the description of a digital circuit % with input wires W1 ... Wn and the output value V % of the circuit at time T find input values % V1 ... Vn and moments of time T1...Tn such that % application of V1...Vn to W1...Wn at times T1...Tn % causes the output value V at time T %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% Reasoning Module %% "Input values derivation problem" %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ % We introduced a language L to represent digital circuits % and a set of axioms GT to model these circuits' behavior. % This theory of digital circuits can be used together with % different reasoning modules to solve different problems. % Here is a reasoning module which finds "static" solutions % of the Input Values Derivation Problem of digital circuits. % % By "static" solution we mean a strategy in which a signal % is applied to each input wire exactly once. % This module works in the following way: %% Let's a circuit description be denoted by CD, a general %% theory of behavior of digital circuits by GT, a reasoning %% module by RM, and a goal G. % Proposition: % The theory of digital circuits CD + GT + RM + :- not G has % one or more stable models and each model SM has a set S of % statements of the type occurs(apply(W,X),T) iff % goal G is achieved in this circuit by applying at time T to % each respective wire W the value X appearing on the its % corresponding statement. % In the static case, only unique actions of applying an input % value to an input wire are allowed. This means that once an % input value is applied to an input wire W at time T then no % other values can be applied to this input wire in a future % moment of time. % For the static case only. :- time(T1),time(T2),neq(T1,T2),signal(X),signal(Y),is_wire(W), occurs(apply(W,X),T1), occurs(apply(W,Y),T2). % Note: For the dynamic case we need to remove this restriction. %% In this module we need some auxiliary predicates to define %% which wires are input wires for the whole circuit, since we %% are interested in performing actions only on these wires. % is_input_wire(W) iff W is an input wire for the whole circuit. is_input_wire(W) :- input(W,G), not is_output(W). % is_output(W) iff W is an output wire of a gate. is_output(W) :- output(W,G). % occurs(apply(W,X),T) iff action apply value X to wire W at % time T is performed. occurs(apply(W,X),T) :- time(T), signal(X), is_input_wire(W), not noccurs(apply(W,X),T), not goal(T). % noccurs(apply(W,X),T) iff action apply value X to wire W at % time T is not performed. noccurs(apply(W,X),T) :- time(T), signal(X), is_input_wire(W), not occurs(apply(W,X),T), not goal(T). % Time range is expressed as const lasttime = 5. time(0..lasttime). %% The goal is expressed by the following rule: goal(T) :- time(T), h(value(w5,1),T). % In Smodels, we indicate that we are only interested % in the stable models that achieve our goal by adding % the following constraint :- not goal(lasttime). %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% Graphical representation of digital circuit %% used in this example. %% %% ---- %% w1------| g1 |o-------w3 %% ---- | ------ %% -------| g3 |_____w5 %% -------| | %% ---- | ------ %% w2------| g2 |o-------w4 %% ---- %% %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% To achieve our goal, we need to describe the circuit and the %% goal values on its output wires. This is done in the language L %% as follows: % is_gate(G) iff G is a gate. is_gate(g1). is_gate(g2). is_gate(g3). % is_wire(W) iff W is a wire. is_wire(w1). is_wire(w2). is_wire(w3). is_wire(w4). is_wire(w5). % gate(G,Y) iff gate G is of gate type Y. gate(g1,notg). gate(g2,notg). gate(g3,andg). % delay(G,D) iff gate G has delay D. delay(g1,1). delay(g2,0). delay(g3,1). % Description of the circuit connections. input(w1,g1). output(w3,g1). input(w2,g2). output(w4,g2). input(w3,g3). input(w4,g3). output(w5,g3). %% In the initial situation, if no value is applied %% to a wire then its value is u, by default. h(value(W,u),0) :- is_wire(W), not known_value(W,0). known_value(W,0) :- is_wire(W), h(value(W,1),0). known_value(W,0) :- is_wire(W), h(value(W,0),0). %% Problem description ends here %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ hide input(X,Y). hide output(X,Y). hide time(X). hide is_wire(X). hide signal(X). hide delay(X,Y). hide gate(X,Y). hide next(X,Y). hide contains(X,Y,Z). hide all(X,Y,Z). hide not_all(X,Y,Z). hide nh(X,Y). hide is_gate(X). hide known_value(X,Y). hide is_input_wire(X). hide is_output_wire(X). hide is_output(X). hide noccurs(X,Y). hide goal(X). hide h(X,Y). --- File 'derivation28' %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% Circuit Description %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ %% This file needs to be used in conjunction with files: %% "circuit" and "derivation". %% (Important: Remove from file "derivation" the rule with %% goal(T) in the head and the definition of const lasttime %% and time range, since those are all included here.) %% The example used here is a 4-to-10 decoder. This device %% has 4 input wires and 10 output wires. It works in the %% following way: it takes a 4 lines binary number as input, %% e.g. 0111 for decimal 7, and outputs a 0 (zero) on ouput %% line 7. In the language L the circuit is represented %% as follows: % is_gate(G) iff G is a gate. is_gate(g1). is_gate(g2). is_gate(g3). is_gate(g4). is_gate(g5). is_gate(g6). is_gate(g7). is_gate(g8). is_gate(g9). is_gate(g10). is_gate(g11). is_gate(g12). is_gate(g13). is_gate(g14). is_gate(g15). is_gate(g16). is_gate(g17). is_gate(g18). is_gate(g19). is_gate(g20). is_gate(g21). is_gate(g22). is_gate(g23). is_gate(g24). is_gate(g25). is_gate(g26). is_gate(g27). is_gate(g28). % is_wire(W) iff W is a wire. is_wire(w1). is_wire(w2). is_wire(w3). is_wire(w4). is_wire(w5). is_wire(w6). is_wire(w7). is_wire(w8). is_wire(w9). is_wire(w10). is_wire(w11). is_wire(w12). is_wire(w13). is_wire(w14). is_wire(w15). is_wire(w16). is_wire(w17). is_wire(w18). is_wire(w19). is_wire(w20). is_wire(w21). is_wire(w22). % gate(G,Y) iff gate G is of gate type Y. gate(g1,notg). gate(g2,notg). gate(g3,notg). gate(g4,notg). gate(g5,notg). gate(g6,notg). gate(g7,notg). gate(g8,notg). gate(g9,notg). gate(g10,notg). gate(g11,andg). gate(g12,andg). gate(g13,andg). gate(g14,andg). gate(g15,andg). gate(g16,andg). gate(g17,andg). gate(g18,andg). gate(g19,andg). gate(g20,andg). gate(g21,notg). gate(g22,notg). gate(g23,notg). gate(g24,notg). gate(g25,notg). gate(g26,notg). gate(g27,notg). gate(g28,notg). % delay(G,D) iff gate G has delay D. delay(g1,0). delay(g2,0). delay(g3,0). delay(g4,2). delay(g5,0). delay(g6,0). delay(g7,0). delay(g8,3). delay(g9,0). delay(g10,0). delay(g11,1). delay(g12,0). delay(g13,1). delay(g14,0). delay(g15,1). delay(g16,0). delay(g17,2). delay(g18,0). delay(g19,1). delay(g20,0). delay(g21,0). delay(g22,0). delay(g23,0). delay(g24,0). delay(g25,0). delay(g26,0). delay(g27,0). delay(g28,0). % Description of the circuit connections. input(w1,g1). input(w2,g2). input(w3,g3). input(w4,g4). input(w5,g5). input(w6,g6). input(w7,g7). input(w8,g8). input(w9,g9). input(w10,g10). input(w11,g11). input(w12,g11). input(w13,g11). input(w14,g11). input(w11,g12). input(w12,g12). input(w13,g12). input(w15,g12). input(w14,g13). input(w16,g13). input(w17,g13). input(w18,g13). input(w15,g14). input(w16,g14). input(w17,g14). input(w18,g14). input(w13,g15). input(w14,g15). input(w17,g15). input(w18,g15). input(w13,g16). input(w15,g16). input(w17,g16). input(w18,g16). input(w12,g17). input(w14,g17). input(w16,g17). input(w18,g17). input(w12,g18). input(w15,g18). input(w16,g18). input(w18,g18). input(w12,g19). input(w13,g19). input(w14,g19). input(w18,g19). input(w12,g20). input(w13,g20). input(w15,g20). input(w18,g20). input(w22,g21). input(w15,g22). input(w21,g23). input(w13,g24). input(w20,g25). input(w12,g26). input(w19,g27). input(w18,g28). output(w23,g1). output(w24,g2). output(w25,g3). output(w26,g4). output(w27,g5). output(w28,g6). output(w29,g7). output(w30,g8). output(w31,g9). output(w32,g10). output(w10,g11). output(w9,g12). output(w8,g13). output(w7,g14). output(w6,g15). output(w5,g16). output(w4,g17). output(w3,g18). output(w2,g19). output(w1,g20). output(w15,g21). output(w14,g22). output(w13,g23). output(w16,g24). output(w12,g25). output(w17,g26). output(w18,g27). output(w11,g28). %% In the initial situation, if no value is applied %% to a wire then its value is u, by default. h(value(W,u),0) :- is_wire(W), not known_value(W,0). known_value(W,0) :- is_wire(W), h(value(W,1),0). known_value(W,0) :- is_wire(W), h(value(W,0),0). %% For the "derivation problem" we need to also give the goal. % Time range is expressed as const lasttime = 5. time(0..lasttime). %% The goal is expressed by the following rule: goal(T) :- time(T), h(value(w23,1),T), h(value(w24,1),T), h(value(w25,1),T), h(value(w26,1),T), h(value(w27,1),T), h(value(w28,0),T), h(value(w29,1),T), h(value(w30,1),T), h(value(w31,1),T), h(value(w32,1),T). % In Smodels, we indicate that we are only interested % in the stable models that achieve our goal by adding % the following constraint :- not goal(lasttime). %% Auxiliary predicates to control results display hide input(X,Y). hide output(X,Y). hide time(X). hide is_wire(X). hide signal(X). hide delay(X,Y). hide gate(X,Y). hide next(X,Y). hide contains(X,Y,Z). hide all(X,Y,Z). hide not_all(X,Y,Z). hide nh(X,Y). hide is_gate(X). hide known_value(X,Y). hide h(X,Y). hide is_input_wire(X). hide is_output(X). hide goal(X). hide noccurs(X,Y). ======= Date: Sun, 13 Feb 2000 From: Vladimir Lifschitz To: Monica Nogueira I asked around about the existing work on the theory of combinational circuits with gate delays, and my first impression is that there is no such theory, in spite of the practical importance of the problem. Or rather, that there had been no such theory until you came up with your formalization. Warren Hunt, an expert on the formal verification of hardware, tells me that there are "very few hardware description languages that are specified rigorously enough to permit both the verification of circuit properties and gate delays. To really prove properties about circuits described with a hardware description language requires that there is a formal definition of the hardware description language itself. Embedding a hardware description language within a logic is not necessarily an easy thing to do." The only reference he was able to give me is to a huge technical report (over 1400 pages), issued in 1994 by Computational Logic, Inc. and entitled "The FM9001 Microprocessor Proof." If it is true that a semantics of circuits with gate delays needs to be extracted from the depths of a report on the verification of a commercial microprocessor, then your simple and elegant formalization may very well turn out to be an important theoretical contribution.