Paper Info
Title
Automatic Correctness Proof of the Implementation of Synchronous Sequential Circuits Using an Algebraic Approach
Abstract
In this paper, we propose a technique for proving the correctness of the implementations of synchronous sequential circuits automatically, where the specifications of synchronous sequential circuits are described in an algebraic language ASL, which we have designed, and the specifications are described in a restricted style. For a given abstract level's specification, we refine the specification into a synchronous sequential circuit step by step in our framework, and prove the correctness of the refinement at each design step. Using our hardware design support system, to prove the correctness of a design step, we have only to give the system some invariant assertions and theorems for primitive functions. Once they are given, the system automatically generates the logical expressions from the invariant assertions and so on, whose truth guarantees the correctness of the design step, and tries to prove those truth using a decision procedure for the prenex normal form Presburger sentences bounded by only universal quantifiers. Using the system, we have proved the correctness of the implementation of a GCD circuit, the Tamarack microprocessor, a sorting circuit and so on, in a few days. The system has determined the truth of each logical expression within a minute.
Year
DOI
Venue
1994
10.1007/3-540-59047-1_48
TPCD
Keywords
Field
DocType
synchronous sequential,automatic correctness proof,algebraic approach,sequential circuits,normal form
Sequential logic,Expression (mathematics),Computer science,Correctness,Prenex normal form,State diagram,Arithmetic,Theoretical computer science,Sorting,Invariant (mathematics),Bounded function
Conference
ISBN
Citations 
PageRank 
3-540-59047-1
4
0.65
References 
Authors
7
4
Name
Order
Citations
PageRank
Junji Kitamichi16410.32
Sumio Morioka249345.23
Teruo Higashino31086119.60
kenichi taniguchi425635.56