← Back to Patent Explorer
US5493508A Expired / Lapsed US ⏱️ 0.0 years remaining

Specification and design of complex digital systems

Assignee: LSI Corp
•
Filing: 1994-06-01
•
Granted: 1996-02-20
•
Expires: 2014-06-01
📄 Original PDF 🌐 Google Patents

Abstract

Abstract A methodology for generating structural descriptions of complex digital devices from high-level descriptions and specifications is disclosed. The methodology uses a systematic technique to map and enforce consistency of the semantics imbedded in the intent of the original, high-level descriptions. The design activity is essentially a series of transformations operating upon various levels of design representations. At each level, the intended meaning (semantics) and formal software manipulations are captured to derive a more detailed level describing hardware meeting the design goals. Important features of the methodology are: capturing the users concepts, intent, specification, descriptions, constraints and trade-offs; architectural partitioning; what-if analysis at a high level; sizing estimation; timing estimation; architectural trade-off; conceptual design with implementation estimation; and timing closure. The methodology includes using estimators, based on data gathered over a number of realized designs, for partitioning and evaluating a design prior to logic synthesis. From the structural description, a physical implementation of the device is readily realized. The methodology further includes an automated interactive, iterative technique for creating a system-level specification in a directly-executable formal specification language. This technique makes use of formal verification and feasibility analysis techniques to iteratively refine the specification prior to implementation. This iterative refinement eliminates many ambiguities and inconsistencies from the specification, and ensures that there is at least one realizable implementation of the specification. The formal verification techniques are further employed to ensure that as the design progresses, compliance with the specification is maintained, and that any specification change is reflected and accounted for, both system-wide and implementation-wide.

Inventors

  • 👤 Carlos Dangelo
  • 👤 Vijay Nagasamy

Bibliographic Details

Application Number —
Jurisdiction US
Data Source google_patents
Last Synchronized 2026-11-06 00:10
CPC Classifications
G; G06; G06F; G06F30/00; G06F30/30; G06F30/32; G06F30/33; G06F30/3323

Claims Analysis

Total Claims: 5
Claim 1
Independent Claim 145 words
An iterative, interactive method of generating a formal, directly-executable specification for a complex digital system, comprising: establishing a desired behavior for a complex digital system; creating a formal specification for the complex digital system using a formal, directly-executable specification language; and iteratively performing the steps of: a) checking for syntactical correctness of the formal specification; b) checking for logical consistency of the formal specification; c) checking for completeness of the formal specification; d) checking for correctness of the formal specification; e) comparing the desired behavior with the behavior described by the formal specification; f) determining the existence of at least one realizable implementation of the formal specification; and g) correcting any problems detected in steps a)-f) above by revising the formal specification; until the formal specification is syntactically correct, logically consistent, correct and complete, reflects the desired behavior, and has at least one realizable implementation.
Claim 2
Dependent Claim 145 words
An iterative, interactive method of generating a formal, directly-executable specification for a complex digital system, comprising: establishing a desired behavior for a complex digital system; creating a formal specification for the complex digital system using a formal, directly-executable specification language; and iteratively performing the steps of: a) checking for syntactical correctness of the formal specification; b) checking for logical consistency of the formal specification; c) checking for completeness of the formal specification; d) checking for correctness of the formal specification; e) comparing the desired behavior with the behavior described by the formal specification; f) determining the existence of at least one realizable implementation of the formal specification; and g) correcting any problems detected in steps a)-f) above by revising the formal specification; until the formal specification is syntactically correct, logically consistent, correct and complete, reflects the desired behavior, and has at least one realizable implementation.
Claim 3
Dependent Claim 34 words
A method according to claim 1, further comprising: verifying correctness of the formal specification; verifying completeness of the formal specification; and verifying the existence of at least one realizable implementation of the formal specification.
Claim 4
Dependent Claim 27 words
A method according to claim 2, wherein: the steps of verifying completeness, verifying correctness, and verifying existence of a realizable implementation are accomplished using formal proof techniques.
Claim 5
Dependent Claim 26 words
A method according to claim 3, wherein: the formal proof techniques are selected from the group consisting of symbolic simulation, mathematical theorem proving, and model checking.

References Cited (Backward Citations)

US4833619A Cited
US5146583A Cited
US5299137A Cited
US5222030A Cited
US5258919A Cited

USPTO Annuity & Maintenance Windows

Annuity Stage Window Opens Payment Deadline Surcharge Period Until Estimated Fee Status
3.5 Years (Year 4) 1999-02-19 1999-08-21 2000-02-20 $2000.00 Window Closed / Lapsed
7.5 Years (Year 8) 2003-02-19 2003-08-21 2004-02-20 $3760.00 Window Closed / Lapsed
11.5 Years (Year 12) 2007-02-19 2007-08-21 2008-02-20 $7700.00 Window Closed / Lapsed

Assigned Categories & Tags

No categories assigned to this patent yet.

Assign Category Tag