A Community of Verification Professionals

Create an Account	Home | Calendar | Downloads | FAQ | Links | Site Admin | Your Account
Login Nickname Password Security Code: Type Security Code BACKWARD Don't have an account yet? You can create one. As a registered user you have some advantages like theme manager, comments configuration and post comments with your name. Modules · Home · Downloads · FAQ · Feedback · Recommend Us · Web Links · Your Account Advertising Who's Online There are currently, 56 guest(s) and 0 member(s) that are online. You are Anonymous user. You can register for free by clicking here    Verification Guild: Forums  Forum FAQ   Search   Usergroups   Profile  Digest    Log in  Declarative vs Imperative languages          Verification Guild Forum Index -> Assertions View previous topic :: View next topic   Author Message alexg Senior Joined: Jan 07, 2004 Posts: 586 Location: Ottawa Posted: Mon Mar 22, 2004 5:35 pm    Post subject: Declarative vs Imperative languages Editor's Note: this topic was split from this topic Bernard, I agree with most part of your posting, especially about those " religious language wars". However, speaking about declarative languages, I would like to mention one important drawback of such approach. In my opinion, declarative languages are useful in two cases: 1. Low level declarations. These are design assertions such as "signal b must go high within 5 cycles after signal a" etc. 2. High level declaration. These are built on the top on already existing verification infrastructure (such as monitors) and deal with with transactions rather than with low-level signals. Example of this declaration for networking may be: "any link reqest control symbol must be followed by link responce control symbol". For both cases, we can easily write 1-line or so declaration rules, and that's why in both cases we are happy with declarative languages. For these examples, infrastructure underneath declarative layer is either not needed or already supplied by environment. Once we'll start to create infrastructure using the same declarative language (writing multiple-line assertions or so), our task will become tedious and not effective. So, in most cases declarative languages make sence when used on the top on environment, built with procedural/implementation languages. One of solutions of this problem is to add procedural/implementation layer to declarative language. That's why "verilog-flavored" modeling layer was introduced to PSL. So, now we have 2 options to use: either "Verilog-flavored PSL" or "PSL-flavored Verilog". I would choose the second option, since I see verilog as a dominant language and don't like any "flavors" of Verilog standart built-in into another language. That's why I prefer SystemVerilog approach, where declarative constructs are added to the well-known procedural/implementational language. Regards, Alexander Gnusin Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Tue Mar 23, 2004 9:20 am    Post subject: Quote: Once we'll start to create infrastructure using the same declarative language (writing multiple-line assertions or so), our task will become tedious and not effective Hi Alexander, We're in danger of straying into a debate on design technology in a verification forum, though I agree completely with your comment. What I was hinting at, however, was the concept the required functionality of the design could be declared at a higher level in a declarative language, and then a tool could build the low level implementation. That makes the user much more productive, and takes away the tedious, error prone tasks. This utopia is not quite in reach, though it is a lot closer than many people realize, for example it's already feasible to automatically generate behaviour for substantial S-o-C interface blocks, perhaps around 200-500k gates. There's still an enormous amount of work to be done, and if you asked me to guess I'd say this is still five years from mainstream use, but it's already on the horizon. That in a nutshell is why declarative languages are important, and why I'm frustrated that instead of PSL being pushed to a second and third generation, it got swamped by a short term politico marketing fight about HDL assertions. Regards Bernard Back to top tomahawkins Senior Joined: Mar 23, 2004 Posts: 29 Posted: Wed Mar 24, 2004 12:07 am    Post subject: Quote: What I was hinting at, however, was the concept the required functionality of the design could be declared at a higher level in a declarative language, and then a tool could build the low level implementation. That makes the user much more productive, and takes away the tedious, error prone tasks. I would also like to see a declarative specification language with a push-button implementation flow. But I suspect a practical language and an automated flow are not possible. I've come to realize that languages have a fundamental tradeoff between level of expression and decidability. For a specification language to be practical, it must have a high level of expression. But after a certain point it may no longer be possible to automatically synthesize a design. The expression-vs-decidability tradeoff is true of property languages. For example, CTL*, the kernel language of PSL, has a relatively low level of expression, but CTL* properties can be proved with a model checker. Higher order logic on the other hand has a much high level of expression, but in general the language lacks an automated proof. I'm also a huge fan of declarative languages -- I designed one after all. I should point out that "declarative language" and "implementation language" are not mutually exclusive. There are many declarative implementation languages. A few that come to mind are Prolog, Haskell, Mercury, and Oz. The language I created is Confluence: a declarative functional programming language for synchronous hardware design. Though it's not a perfect paradigm for every application, declarative programming has this "correct-by-construction" mentality you just don't get with imperative languages. And typically you can express more in fewer lines of code. With Confluence I've seen code reduction up to 20X then that of Verilog (usually its only 2-5X). As this is the verification guild, I should mention I recently added LTL property types to Confluence. So the same mechanics that generate hardware structures also can generate temporal properties. I haven't added properties to the back-end yet, but they will be in place shortly. BTW, the Confluence compiler is now GPL. Regards, Tom Hawkins Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Thu Mar 25, 2004 11:26 am    Post subject: Tom, To clarify your comment that PSL is based on CTL, one of the reasons Sugar was chosen as the basis for PSL was the IBM teams willingness to adapt to support both LTL and CTL. To quote from the PSL LRM Quote: PSL is an extension of the standard temporal logics LTL and CTL. A specification in the PSL Foundation Language (respectively, the PSL Optional Branching Extension) can be compiled down to a formula of pure LTL (respectively, CTL), possibly with some auxiliary HDL code, known as a satellite. The beauty of the solution is it can be used to describe virtually anything written in three of the original donations (Sugar, ForSpec & temporal 'e') and, I believe, most properties that can also be written in CBV. As far as expressiveness and push-button implementation flows are concerned, I guess I'm more optimistic than you, but time will show which of us is correct. Regards Bernard Back to top tomahawkins Senior Joined: Mar 23, 2004 Posts: 29 Posted: Fri Mar 26, 2004 9:51 am    Post subject: bdeadman wrote: To clarify your comment that PSL is based on CTL, one of the reasons Sugar was chosen as the basis for PSL was the IBM teams willingness to adapt to support both LTL and CTL. To quote from the PSL LRM Quote: PSL is an extension of the standard temporal logics LTL and CTL. A specification in the PSL Foundation Language (respectively, the PSL Optional Branching Extension) can be compiled down to a formula of pure LTL (respectively, CTL), possibly with some auxiliary HDL code, known as a satellite. I've read this in the manual. What exactly is a "satellite"? I'm not a logician, but from what I gather, there are CTL properties that can not be expressed in LTL, and vice-versa. CTL* is superset of both -- some CTL* properties are impossible in either CTL or LTL. Not surprisingly, CTL* properties require more effort to verify -- again, the trade-off between level of expression and decidability. bdeadman wrote: As far as expressiveness and push-button implementation flows are concerned, I guess I'm more optimistic than you, but time will show which of us is correct. Yes, we can certainly do much better than today. But at some point the problem becomes undecidable. For example, HOL (the Higher-Order Logic proof assistant) helps verify an implementation meets a specification. As the name implies, HOL can express properties far beyond the capabilities of either CTL*, CTL, or LTL. But the cost is the lack of full automation. (HOL is a proof "assistant", not a proof oracle). Now let's go the other way. We'll provide a specification and let HOL search for an implementation. But if implementation -> specification is undecidable, I'm willing to bet specification -> implementation is too. On the bright side -- undecidability will keep us designers and verifiers employed indefinitely. Regards, Tom Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Mon Mar 29, 2004 6:41 pm    Post subject: Tom, I'm not an expert and comment on CTL* versus CTL, but the way PSL is broken down is the Foundation Language is essentially LTL, while the Optional Branching Extensions (OBE) supports CTL. My intuitive understanding (I'm sure there are people out there ready to correct me....) is most or all of LTL can be expressed in CTL but not vice versa. Quote: I've read this in the manual. What exactly is a "satellite"? I have to admit I don't know for sure. I took this to be required to support "named endpoints" which are roughly equivalent (again, I believe!) to the satisfaction of multi-cycle events in temporal E, though I confess I don't code in this style. I'm afraid I don't agree about the mapping of specification -> implementation. It isn't yet universal, but it works in a number of important, real sized cases. A lot of work remains to be done to bring the concepts to widespread adoption but I believe it can and will happen. Regards Bernard Back to top Display posts from previous: All Posts1 Day7 Days2 Weeks1 Month3 Months6 Months1 Year Oldest FirstNewest First         Verification Guild Forum Index -> Assertions All times are GMT - 5 Hours Page 1 of 1   Jump to: Select a forum Main----------------MainEDA NewsCommunity Services Networking----------------Looking for a jobLooking for candidates Archives----------------AssertionsCoverageFormalSimulationDesignMiscellaneous Test----------------Test  You can post new topics in this forum You can reply to topics in this forum You cannot edit your posts in this forum You cannot delete your posts in this forum You cannot vote in polls in this forum Forums ©

Verification Guild © 2006 Janick Bergeron
Web site engine's code is Copyright © 2003 by PHP-Nuke. All Rights Reserved. PHP-Nuke is Free Software released under the GNU/GPL license.
Page Generation: 0.187 Seconds