FPGA Market Entry Barriers

On 28/10/2018 18:27, Theo wrote:
> HT-Lab <hans64@htminuslab.com> wrote:
..
> There aren't any tools to my knowledge that check equivalence between the
> BSV source and the RTL, but then that's a bit like checking equivalence
> between your C++ source code and your assembly output - if it fails, it's a
> compiler bug.

Yes but C++ to assembly is sequential to sequential (there are 
exceptions), I am talking about sequential to concurrent which is a 
different kettle of fish.

I suspect I don't fully understand the flow control aspect BSV adds to 
the language. However, one good reason for having a BSV to RTL 
equivalence checker is that it allows BSV to be used for DO-254/ISOxx 
type of projects. In those cases you need to prove the translation by a 
second source, using a formal tool which mathematically proves the 
sources are identical is becoming a must have for DO-254 projects.

Hans
www.ht-lab.com


> 
> Theo
> 

HT-Lab <hans64@htminuslab.com> wrote:
> On 28/10/2018 18:27, Theo wrote:
> > HT-Lab <hans64@htminuslab.com> wrote:
> ..
> > There aren't any tools to my knowledge that check equivalence between the
> > BSV source and the RTL, but then that's a bit like checking equivalence
> > between your C++ source code and your assembly output - if it fails, it's a
> > compiler bug.
> 
> Yes but C++ to assembly is sequential to sequential (there are 
> exceptions), I am talking about sequential to concurrent which is a 
> different kettle of fish.

BSV is similar - timing is explicit.  It's just that the stuff like

always @(posedge clock) begin
 if (reset) begin ... end
 if (complicated_valid_expression) begin
   ...
 end
end

is handled for you.  In other words, if you have a pipeline it'll take
exactly the number of cycles you told it, but it could starve or deadlock if
you did something wrong.  One solution to that is to write code that has a
fallback case so it'll never deadlock (eg propagate a token that's
explicitly Invalid rather than stalling waiting for the next token with
valid data).

BSV doesn't do any transformations from sequential to concurrent - if you
write sequential you get sequential (there's some handy constructs for
building state machines), if you write concurrent (the default) you get
concurrent.

> I suspect I don't fully understand the flow control aspect BSV adds to 
> the language. However, one good reason for having a BSV to RTL 
> equivalence checker is that it allows BSV to be used for DO-254/ISOxx 
> type of projects. In those cases you need to prove the translation by a 
> second source, using a formal tool which mathematically proves the 
> sources are identical is becoming a must have for DO-254 projects.

True.  There are formal tools for BSV, but they tend to approach BSV from its
underlying Haskell roots, rather than looking at the gory details of the
verilog output.    Since the compiler emits a schedule which essentially
shows its working, I suppose it could be done.

Theo

Am Sonntag, 28. Oktober 2018 12:51:11 UTC+1 schrieb Theo:
> > > 'signal x : std_logic_vector(31 downto 0)' when I could just type 

> So if I was writing in a strongly typed language rather than a disaster like
> Verilog, it would be:
> 
> Reg#(UInt#(32))

No. 
In VHDL there is a difference between A(31 downto 0), B(0 to 31) and C(32 downto 1). Your example would remove that information.
For a common bit vector that seems ridiculous overspecified, but for complex structures it is good to have that difference. 

bye Thomas

Thomas Stanka <usenet_nospam_valid@stanka-web.de> wrote:
> In VHDL there is a difference between A(31 downto 0), B(0 to 31) and C(32
> downto 1).  Your example would remove that information.  For a common bit
> vector that seems ridiculous overspecified, but for complex structures it
> is good to have that difference.

For what case would it make sense to distinguish between those, but not use
Structure.fieldname notation?

And where B(0 to 31) makes sense but reverse(B(31 downto 0)) doesn't?

(in other words, in the rare case you want something that isn't the norm,
you have to express that explicitly - rather than forcing you to express the
norm explicitly at all times)

Theo

On Wednesday, October 31, 2018 at 10:55:50 AM UTC-4, Theo wrote:
> Thomas Stanka <usenet_nospam_valid@stanka-web.de> wrote:
> > In VHDL there is a difference between A(31 downto 0), B(0 to 31) and C(32
> > downto 1).  Your example would remove that information.  For a common bit
> > vector that seems ridiculous overspecified, but for complex structures it
> > is good to have that difference.
> 
> For what case would it make sense to distinguish between those, but not use
> Structure.fieldname notation?
> 
> And where B(0 to 31) makes sense but reverse(B(31 downto 0)) doesn't?
> 
> (in other words, in the rare case you want something that isn't the norm,
> you have to express that explicitly - rather than forcing you to express the
> norm explicitly at all times)

Unfortunately I don't follow your descriptions of the BSV language enough to compare to VHDL.  The examples you show don't seem to be so much more terse than VHDL unless you are literally talking about the fact that the names of VHDL keywords are longer.  

signal foo unsigned(31 downto 0); 
foo <= bar + barfoo;

This would be what in BSV?  This is not something I've complained about ever and the issues I did mention weren't addressed by you I think. 

Is there are summary of the language somewhere to give a reasonable understanding rather than a full blown treatment of the language?  That is one strike against VHDL.  Getting up the learning curve takes some time and effort. 

Rick C. 

gnuarm.deletethisbit@gmail.com wrote:
> Unfortunately I don't follow your descriptions of the BSV language enough
> to compare to VHDL.  The examples you show don't seem to be so much more
> terse than VHDL unless you are literally talking about the fact that the
> names of VHDL keywords are longer.
> 
> signal foo unsigned(31 downto 0); 
> foo <= bar + barfoo;
> 
> This would be what in BSV?  This is not something I've complained about
> ever and the issues I did mention weren't addressed by you I think.

The direct equivalent would be:

Reg#(UInt#(32)) foo <- mkReg(99); // reset value 99

rule nameoftherule;
// happens every clock cycle if 'bar' and 'barfoo' are ready
	foo <= bar + barfoo;
endrule

but that also handles the clock and reset conditions for you as well.

My main beef with VHDL verbosity is about interfaces, and the screeds of
code that end up being written to connect a thing inside a module to the
outside of the module, with a 1:1 correspondence between wires.  You end up
declaring all the wires three times - once as the definition of the
interface of the parent module, once of the definition of the interface in
the child module, and once inside the module when you want to connect A to
B.  VHDL does support interfaces (where you just define the bundle of wires
only once), but I don't see that in codebases.  Does it lack tools support?

> Is there are summary of the language somewhere to give a reasonable
> understanding rather than a full blown treatment of the language?  That is
> one strike against VHDL.  Getting up the learning curve takes some time
> and effort.

The BSV By Example book is quite good:
http://csg.csail.mit.edu/6.S078/6_S078_2012_www/resources/bsv_by_example.pdf

There's also a toy BSV compiler here that I haven't played with:
https://www.cl.cam.ac.uk/~djg11/wwwhpr/toy-bluespec-compiler.html
(it seems to be a DSL in F#, so not something you can directly feed .bsv
files)

Theo

On 31/10/2018 19:27, Theo wrote:
> gnuarm.deletethisbit@gmail.com wrote:
..
Hi Theo,

> the child module, and once inside the module when you want to connect A to
> B.  VHDL does support interfaces (where you just define the bundle of wires
> only once), but I don't see that in codebases.  Does it lack tools support?

Interfaces are not yet supported but they are coming with VHDL2018, see 
section 6.5 of the draft VHDL2018 LRM:

http://www.eda-twiki.org/twiki/pub/P1076/PrivateDocuments/P1076-2018.pdf

Unfortunately as all VHDL designers will know we won't see EDA vendors 
adopting VHDL2018 any time soon.

Regards,
Hans
www.ht-lab.com

> 
>> Is there are summary of the language somewhere to give a reasonable
>> understanding rather than a full blown treatment of the language?  That is
>> one strike against VHDL.  Getting up the learning curve takes some time
>> and effort.
> 
> The BSV By Example book is quite good:
> http://csg.csail.mit.edu/6.S078/6_S078_2012_www/resources/bsv_by_example.pdf
> 
> There's also a toy BSV compiler here that I haven't played with:
> https://www.cl.cam.ac.uk/~djg11/wwwhpr/toy-bluespec-compiler.html
> (it seems to be a DSL in F#, so not something you can directly feed .bsv
> files)
> 
> Theo
> 

On Thursday, November 1, 2018 at 4:06:04 AM UTC-4, HT-Lab wrote:
> On 31/10/2018 19:27, Theo wrote:
> > gnuarm.deletethisbit@gmail.com wrote:
> ..
> Hi Theo,
> 
> > the child module, and once inside the module when you want to connect A to
> > B.  VHDL does support interfaces (where you just define the bundle of wires
> > only once), but I don't see that in codebases.  Does it lack tools support?
> 
> Interfaces are not yet supported but they are coming with VHDL2018, see 
> section 6.5 of the draft VHDL2018 LRM:
> 
> http://www.eda-twiki.org/twiki/pub/P1076/PrivateDocuments/P1076-2018.pdf
> 
> Unfortunately as all VHDL designers will know we won't see EDA vendors 
> adopting VHDL2018 any time soon.

Maybe by 2028. 

Rick C.