Subject: RE: [vhdl-200x] Fw: Should we merge 1164 into 1076?
From: Bailey, Stephen (SBailey@model.com)
Date: Fri Dec 19 2003 - 07:57:41 PST
I don't see this as an argument against incorporating 1164 into 1076 for the following reasons:
1. Formal verification tools today accept VHDL descriptions where the explicit logic type is std_[u]logic. If they didn't, they wouldn't be very useful. The fact that they only deal with 0 and 1 values in their proof engines does not change the fact that they do handle std_[u]logic (from a user perspective). User's are aware of the limitations of the engines in dealing with metalogic values.
2. Such formal engines can understand appropriate application of don't care handling as it is no different than short-hand expressions of truth tables (there is a bounded number of states that the don't cares expand to).
3. There are simulators today that also reduce std_ulogic down to 2 or 4 states. Some do it as an optimization technique and some do it blindly because the user states they want a 2 or 4 state simulation mode. That doesn't mean the simulators error out every time they see std_ulogic in a VHDL description. Again, the users understand the limitations imposed and accept them.
4. Gabe's comments serve as very good guidance that the incorporation of 1164 into 1076 should not result in semantics that are specified in the language that only std_ulogic can exploit. Therefore, if we were to add a capability to allow the exploitation of std_ulogic's don't care, it would be bad if it was hardcoded semantics that provided this. However, if it were provided in such a way as to allow other types to be defined and exploit the same capabilities, then it would be a good language enhancement.
(FYI, our discussions in regard to exploiting don't care have indeed been centered around the latter -- general language capabilities that could be exploited by any user-defined type. Everyone that I'm aware of in the 1076-200x effort has a very strong desire to realize general language capabilities and not one-off, non-general solutions.)
I request that the WGs be given the benefit of the doubt in that people should not oppose the incorporation of 1164 (or potentially other 1076.x) standards solely on the basis that they want to make sure that 1076 never does one-off/targeted enhancements that benefit only 1164 (or other related standard). If any such enhancement proposals are proffered, the participants in this WG and email list will have plenty of opportunity to point out the problems.
-Steve Bailey
> Dominique,
> now I get it, and I agree with you. I also admit that keeping all the
> various standards that relate to VHDL synchronized may be a
> demanding task
> for a volunteer group such as the DASC. Yet, what is worth
> doing is worth
> doing well. If the DASC finds the task too demanding then the user
> community will form or find another structure to accomplish
> what it needs.
> Let's not forget that the DASC serves the community, it is
> not a speculative
> research organization whose end products are targets EDA
> vendors must aspire
> to reach. The various 1076.x related standards enrich the
> language for
> specific application instances, but they are not generic
> enough to warrant
> their direct inclusion in the language. Specifically many
> applications of
> VHDL use both 2 and 4 value logic and very few use all nine
> values included
> in 1164. Although this fact does not diminish the
> contribution of 1164 to
> the VHDL community, or the modeling community in general, it
> is a strong
> argument against integrating 1164 into the language and
> forcing every VHDL
> tool to deal with both signal strengths and don't care conditions.
> For example, when modeling systems at a higher level of
> abstraction one
> often needs a four value logic system whose values are:
> unknown, don't care,
> false, true. Making 1164 the fundamental VHDL value system
> would get in the
> way of defining this kind of logic just as it would get in
> the way of the
> two value system used in formal analysis. Making 1164 the
> fundamental value
> system will decrease the flexibility of the language. The
> best way to keep
> the freedom to mold the language to specific needs it to keep
> it simple.
> Gabe
> ----- Original Message -----
> From: "Dominique Borrione" <Dominique.Borrione@imag.fr>
> To: "Gabe Moretti" <gmoretti@comcast.net>; "Dominique Borrione"
> <Dominique.Borrione@imag.fr>
> Cc: <vhdl-std-logic@eda.org>
> Sent: Friday, December 19, 2003 6:38 AM
> Subject: Re: Should we merge 1164 into 1076?
>
>
> > Gabe and all,
> >
> > Thank you Gabe for your message. I realize that I may have
> been a bit
> > too short,
> > and thus very obscure.
> >
> > Most current verification tools use combinations of BDD and SAT
> > solving techniques,
> > which are effective when manipulating bits, Booleans and
> vectors of those.
> > This includes both equivalence checking tools and property
> checking tools.
> > Having to deal with 9 values is a serious problem:
> > - if the 9-value logic, and all the operators truth tables, have to
> > be represented,
> > the immediate implication is that every std_ulogic signal/variable
> > must be coded using
> > 4 instead of 1 binary variable, hence a model size
> multiplied by 8**n
> > where n is the number
> > of declared inputs and signals/variables that are memorizing, and **
> > means power.
> > Needless to say, model size being already a problem in binary logic,
> > no method can cope with such a size increase.
> >
> > This is why, although most synthesized VHDL inputs use std_ulogic,
> > formal verification
> > tools consider this type as synonymous to Bit, and reason
> in binary logic.
> > Moreover, it is unclear what interpretation a formal
> verification tool
> should
> > give to metalogic values.
> >
> > I hope this clarifies my previous message.
> >
> > Dominique
> >
> > At 8:15 -0500 18/12/03, Gabe Moretti wrote:
> > >Dominique,
> > >you make a good point but some of us might need a bit of
> education to
> really
> > >appreciate what you are saying. Is there a subset of 1164 that is
> "formal
> > >verification friendly"? What is the general problem in
> 1164 that is an
> > >obstacle to formal verification? Could the issue be
> resolved by a new
> > >version of 1164? If so could the new version be backward
> compatible?
> But
> > >above all I think that we need to look for new opportunities, with
> emphasis
> > >on property checking and not equivalence checking at RTL
> and below. It
> is
> > >much harder to regain lost ground as it is to forge new
> opportunities.
> > >I think that in working toward a revision of VHDL we
> should focus on
> > >extending the system level capabilities and the
> "friendliness" of the
> > >language when used in mixed system development (software
> and mechanical
> > >development tools in particular). For example, we should
> pay attention
> to
> > >the potential of having a development environment that
> includes both VHDL
> > >and Matlab, or even VHDL and SABER. Of course
> co-existence with Verilog
> > >2001 and C should be cast in concrete. Every major VHDL vendor has
> > >co-simulation capabilities: it is beyond my logical
> ability (but well
> within
> > >my marketing reasoning) to understand why we still do not
> have a standard
> in
> > >this area!
> > >Gabe Moretti
> > >----- Original Message -----
> > >From: "Dominique Borrione" <Dominique.Borrione@imag.fr>
> > >To: "John Michael Williams" <jwill@AstraGate.net>;
> <vhdl-std-logic@eda.org>
> > >Cc: <vhdl-200x@eda.org>
> > >Sent: Thursday, December 18, 2003 2:44 AM
> > >Subject: Re: Should we merge 1164 into 1076?
> > >
> > >
> > >> Hi!
> > >>
> > >> After a long silence, I'like to jump in.
> > >>
> > >> 1164 does not make sense for many formal verification tools.
> > > > Yet, most commercial equivalence checking tools, and
> some property
> > >> checking tools,
> > >> are 1076.6 compliant, except that std_ulogic is treated as bit.
> > >> Numeric_std is treated as Numeric_bit.
> > >> Yet, I don't see that the community has any interest in
> defining a
> > >sub-VHDL for
> > >> formal verification different from the sub-VHDL for synthesis.
> > >>
> > >> Putting 1164 into 1076 would make all formal
> verification tools non
> > >compliant.
> > >> Maybe we don't care.
> > >> But maybe we do, in particular because VHDL is losing ground in
> > >> comparison with Verilog,
> > >> and we don't want to discourage tool makers from offering a VHDL
> input.
> > >>
> > >> Is there a way to express that some packages may or may not be
> supported?
> > >>
> > >> Cheers,
> > >>
> > >> Dominique
> > >>
> > >>
> > >> At 18:57 -0800 17/12/03, John Michael Williams wrote:
> > >> >Hi Peter.
> > >> >
> > >> >Two issues:
> > >> >
> > >> >1. Ease of maintenance. Putting 1164 into 1076 as an annex
> > >> > should solve this. 1076 WG --> 1164+1076 WG.
> > >> >
> > >> >2. Optionality. When I wrote "users", I meant designers, not
> > > > > tool writers. Clearly a designer, especially for
> > >> > synthesis, has the option to avoid using anything in
> > >> > TEXTIO.
> > >> >
> > >> > I wasn't more explicit because I don't view tool makers
> > >> > or standards groups as "users"; I think this idea is
> > >> > from the days when there was 1076 simulation
> > >> > and nothing else.
> > >> >
> > >> > If 1164 now is in a 1076-2002 compliant
> > >> > VHDL package, the package should work in the tool (at
> > >> > least for simulation) with no additional tool-maker
> > >> > effort.
> > >> > It shouldn't matter whether the compilation is into
> > >> > library x.1076 or library x.1164.
> > >> > In fact the annex might even allow compilation into
> > >> > either one, for backward compatibility.
> > >> >
> > >> >So, I don't see the problem for 1076 simulation users
> > >> >or tool makers. Can you think of one? Maybe I'm
> > >> >overlooking something obvious?
> > > > >
> > >> >In 1076.6, for interoperability, there may be need to
> > >> >look into it, but I don't offhand expect any problem
> > >> >with always USEing 1164 at the same time as 1076.
> > >> >
> > >> >--
> > >> > John
> > >> > jwill@AstraGate.net
> > >> > John Michael Williams
> > >> >
> > >> >Peter Ashenden wrote:
> > >> >
> > >> >>John,
> > >> >>
> > >> >>What the users chooses to use and what a comformant tool must
> implement
> > >are
> > >> >>different questions. Currently, a tool implementation must
> implement
> > >TEXTIO
> > >> >>to conform with the standard. We have no notion of
> optional parts -
> > >it's
> > >> >>all or nothing.
> > >> >>
> > >> >>It would be possible to change that and specify
> conformace sets.
> Then,
> > >we
> > >> >>might add 1164 to 1076 and make std_logic_1164 an
> optional part for
> a
> > >tool
> > >> >>to implement.
> > >> >>
> > >> >>Cheers,
> > >> >>
> > >> >>PA
> > >> >>
> > >> >>--
> > >> >>Dr. Peter J. Ashenden
> peter@ashenden.com.au
> > >> >>Ashenden Designs Pty. Ltd.
> www.ashenden.com.au
> > >> >>PO Box 640 Ph: +61
> 8 8339 7532
> > >> >>Stirling, SA 5152 Fax: +61
> 8 8339 2616
> > >> >>Australia Mobile:
> +61 414 70 9106
> > >> >>
> > >> >>
> > >> >>>-----Original Message-----
> > >> >>>From: owner-vhdl-std-logic@eda.org
> > >> >>>[mailto:owner-vhdl-std-logic@eda.org] On Behalf Of
> John Michael
> > >> >>>Williams
> > >> >>>Sent: Thursday, 18 December 2003 13:04
> > >> >>>To: vhdl-std-logic@eda.org
> > >> >>>Cc: vhdl-200x@eda.org
> > >> >>>Subject: Re: Should we merge 1164 into 1076?
> > >> >>>
> > >> >>>
> > >> >>>Hi Peter.
> > >> >>>
> > >> >>>If we included the 1164 package in 1976 as <-- 1076
> > >> >>>an annex for convenience of users, with some
> > >> >>>explanations, the maintenance
> > >> >>>would be simplified, but there still would
> > >> >>>be the choice of not using 1164.
> > >> >>>
> > >> >>>For example, there is no requirement to use
> > >> >>>TEXTIO.
> > >> >>>
> > >> >>>I don't see the stopping criterion as a problem,
> > >> >>>unless someone sees good reason to start up
> > >> >>>annexation again . . ..
> > >> >>>
> > >> >>>--
> > >> >>> John
> > >> >>> jwill@AstraGate.net
> > >> >>> John Michael Williams
> > >> >>>
> > >> >>>Peter Ashenden wrote:
> > >> >>>
> > >> >>>>Dear colleagues,
> > >> >>>>
> > >> >>>>[Disclaimer: I am speaking here as a WG member, not as DASC
> Chair.]
> > >> >>>>
> > >> >>>>From time to time, it has been suggested that we merge the
> standard
> > >> >>>>
> > >> >>>>>logic
> > >> >>>>
> > >> >>>>package definitions into the base VHDL standard document. I
> > >> >>>>would like to see if there is currently interest in
> doing so.
> > >> >>>>
> > >> >>>>The reasons for doing so are:
> > >> >>>>
> > >> >>>>(1) The standard logic types are so widely used in VHDL
> > >> >>>
> > >> >>>modeling now
> > >> >>>>that they have become an integral part of the
> language and its
> > >environment.
> > >> >>>>
> > >> >>>>(2) Maintaining the standards separately is an
> administrative and
> > >> >>>>logistical burden. In particular, ensuring that
> revisions are
> > >> >>>>synchronized is difficult. Since most of the people
> > >> >>>
> > >> >>>involved in P1164
> > >> >>>are also actively involved in P1076, they could work as a
> > >> >>>
> > >> >>>functional
> > >> >>>>team of P1076 with less overhead.
> > >> >>>>
> > >> >>>>Reasons agains are:
> > >> >>>>
> > >> >>>>(3) Adding the standard logic types to P1076 would mean all
> > >> >>>
> > >> >>>VHDL tools
> > > > >>>>would have to provide them, whereas now, a tool
> vendor could
> > >> >>>>decide not to implement them and still be compliant
> with 1076.
> > >> >>>>
> > >> >>>>(4) If you merge 1164 into 1076, do you then do 1076.2?
> > >> >>>
> > >> >>>And 1076.3?
> > >> >>>>1076.4? Where does it stop?
> > >> >>>>
> > >> >>>>Comments?
> > >> >>>>
> > >> >>>>Cheers,
> > >> >>>>
> > >> >>>>PA
> > >> >>>>
> > >> >>>>--
> > >> >>>>Dr. Peter J. Ashenden
> peter@ashenden.com.au
> > >> >>>>Ashenden Designs Pty. Ltd.
> www.ashenden.com.au
> > >> >>>>PO Box 640 Ph:
> +61 8 8339 7532
> > >> >>>>Stirling, SA 5152 Fax:
> +61 8 8339 2616
> > >> >>>>Australia
> Mobile: +61 414 70
> 9106
> > >>
> > >>
> > >> --
> > >> =========
> > >> Dominique Borrione
> > >>
> > >> Laboratoire TIMA / Tel: (+33) 4.76.57.49.82
> > >> INPG / Fax: (+33) 4.76.57.49.81
> > >> 46 Avenue Felix Viallet
> > > > 38031 Grenoble cedex / Dominique.Borrione@imag.fr
> > >> France
> > >>
> >
> >
> > --
> > =========
> > Dominique Borrione
> >
> > Laboratoire TIMA / Tel: (+33) 4.76.57.49.82
> > INPG / Fax: (+33) 4.76.57.49.81
> > 46 Avenue Felix Viallet
> > 38031 Grenoble cedex / Dominique.Borrione@imag.fr
> > France
>
>
This archive was generated by hypermail 2b28 : Fri Dec 19 2003 - 08:03:40 PST