IEEE Transactions on Computers · 1992 · 126 citations · 8 references
EngineeringComputer EngineeringComputer ScienceFormal MethodsLogicReal-time SystemsBoolean AlgebraDeductive VerificationDigital Logic DesignLogic SynthesisReal-time Systems DesignTemporal LogicBoolean FunctionsConstraintsFormal ReasoningFunctional ConstraintsInterval Temporal LogicTemporal Logic SpecificationTemporal Logic Verification
The authors propose a general synthesis method for efficiently implementing any family of Boolean functions over a set of variables, as a self-timed logic module. Interval temporal logic is used to express the constraints that are formulated for the self-timed logic module. A method is provided for proving the correct behavior of the designed circuit, by showing that it obeys all the functional constraints. The resulting circuit is compared with alternative proposed self-timed methodologies. This approach is shown to require less gates than other methods. The proposed method is appropriate for automatic synthesis of self-timed systems. A formal proof of correctness is provided.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>
8
Leslie Lamport · IFIP Congress · 1983 · 445 citations
The correctness problem in computer science
Mathematics and Computers in Simulation · 1983 · 355 citations
A Temporal Logic for Multilevel Reasoning about Hardware
Moszkowski · Computer · 1985 · 329 citations