So, I just stumbled upon this. It may turn out to be useful in the months ahead. Still a long way from implementig HDMI support, but this seems to me like a good place to start more generally to understand other fast serial and packet protocols from the ground up. #fpga
@vertigo Yes, it's the same one, I just wasn't sure if it was freely *and* legally available.
@haitch For instance, my work on the SIA last night was not possible without the input from someone more experienced with formal verification than I was. I kept running into a problem where BMC would pass, but proof-by-induction repeatedly failed.
@vertigo By the way, most of the decent resources I've found available for free online are based on VHDL, and I haven't looked enough, but not a lot of above average Verilog stuff seems to be available without strings attached. But you use Verilog for Kestrel, right? So I'm feeling a bit torn because personally I'm feeling more inclined to use VHDL but it would be a mess to have a lot of duplication of efforts, and potential pitfalls eventually when linking up multi-FPGA modules.
@vertigo Still early days, but I'm pondering what's the best way to go about it. It's the sort of early decision that has a considerable impact later.
@haitch Another option might be to use something like MyHDL. It's based on Python (IIRC), and I believe it lets you output your design as either VHDL or Verilog.
I've never used it myself, but that might also be an option.
@haitch Most commercial tools allow you to freely mix Verilog and VHDL sources in a single project, since they both compile to a common netlist (analogous to LLVM or Java bytecode) representation.
You'll also find that most designs in the US are Verilog, while most in Europe are VHDL.
The issue is with the lack of VHDL support from FOSS tools. :( I don't have a problem with someone using VHDL in principle; it's just I don't know how to integrate VHDL and Verilog modules using FOSS tooling.
@vertigo Is there a published list of software dependencies you are currently using to build Kestrel?
I'll take a look at MyHDL too.
I'm taking a look at these other tools as well:
@haitch Since I'm using the formal verification features of Yosys, my dependency list is pretty steep. (Which reminds me, I need to update my website to account for that.)
Before I adopted formal verification, it's just a matter of building Verilator and Yosys, and that was everything you needed. With formal, you also need a collection of provers, which is relatively simple to build, but then *they* have dependencies, etc.
@haitch It basically took me all day to get everything compiled, since my Linux distro doesn't have packages for everything.
@vertigo I'm not going to do all that yet, but one day it will be useful in order to have reproducible and verifiable Kestrels 🙂
If I was to wear a paranoid hat, that's pretty much the last line of defence.
@haitch It was quite a bit of work to get the dependencies built. Once the deps were in place, though, Yosys compiled trivially.
That said, there has been some pay-off already. The properties I've defined for my modules have already caught subtle bugs that unit testing alone wouldn't have caught.
Though, I often ask myself if it was all worth it. I mean, unit testing gets me 80% to 90% to where I need to be. FV finds some slick edge cases, but in practice, how often will they occur?
@haitch I think it'll be well worth it for the CPU and for the video display chip. For everything else, I'm not convinced that the payoff is high enough. But, I have it now, so I might as well use it! Plus, it's another skill I'm developing, so there's that.
@vertigo So, Verilator and Yosys and whatever dependencies those bring in, that's a good start for me.
I'll see what I can do without getting carried away too much by Xilinx et all.
@vertigo This thread has been dead for seven years after some initial excitement...
@haitch Yeah. There's GHDL for simulation, but as far as I'm aware, it's not possible to intermix VHDL and Verilog sources. Also, it's just simulation; it doesn't cover synthesis. :(
@haitch Someone seems to be making some progress on a VHDL input processor for Yosys though. https://github.com/YosysHQ/yosys-plugins/tree/master/vhdl It's 3 years old though. Not sure if it's because it's functionally complete or it the authors just gave up.
@vertigo It's strange. One would think that a more tightly specified standard would have seen more comprehensive implementations by now.
@vertigo At least there is that 🙂
@vertigo If it's worth doing at all... 🙂 Like your mum said
@nonlinear @haitch Well, that'll be the test, won't it? If FV lets me build the Kestrel-3 computer without once resorting to me having to use an oscilloscope to debug what's going on inside the chip, then it'll be a success. ;)
1. I already had to use an o'scope to debug what was happening with the flash ROM chip. To be fair, this was prior to my adoption of FV; however, I don't think FV would have helped in this case anyway, so I'm willing to discard this incident as an out-lier.
Server run by the main developers of the project It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!