Yes Marko, as you said. Strictly speaking, hardware verification (pre-silicon and post-silicon) is another world for ASIC and PLDs development. Some languages are required for validation and verification such as SystemVerilog, SystemC which are totally different perspectives of how a hardware designer thinks. As I understand, Formal verification uses model checking based on Kripke structure in order to visualize a hardware design as a mathematical model in order to analyze the transitions of discrete events. However, I've never tried formal verification just testing via testbench design. An open source toolchain for doing formal verification si *SimbiYosis * https://github.com/YosysHQ/SymbiYosys cheers, Luis Vela dsp8bit El dom, 21 feb 2021 a las 11:35, Marko Mäkelä (<msmakela_at_gmail.com>) escribió: > Sun, Feb 21, 2021 at 10:45:16AM -0600, Luis Rene Vela Garcia wrote: > >People interested in PLDs and their programming, have to understand > >that one thing is to know about this technology and HDL, and the thing > >is to go for the process of designing of a digital system and its > >veritifation. > > Nitpicking: "verification" should refer to proving that something works > correctly under all circumstances. The term "validation" is more > relaxed, somewhere between "testing" and "verification". > > I am curious: How commonly is verification part of the workflow > nowadays? About 20 years ago, I knew that Intel was heavily investing in > formal mehods, maybe prompted by the negative publicity from Pentium > bugs (FDIV giving incorrect results, and incorrect page fault handling > in LOCK XCMPCHG8B). I was under the impression that with techniques like > Binary Decision Diagrams it could be feasible to verify hardware > designs. > > When it comes to verifying software designs, I am afraid that there has > not been that much progress in the past 20 years. Some degree of > validation is practical, but verification easily suffers from state > space explosion. And I have not followed the development, on whether > there are any automated abstraction techniques. For validation, some > interesting practical techniques include fuzzing and instrumentation > (various -fsanitize implemented in Clang and GCC). Best of all, such > instrumented code can be run inside https://rr-project.org/ so that one > can replay and debug a failure exactly in the way it happened. (This is > limited to specific processor types, and tends to be completely blind to > some classes of race conditions.) > > Best regards, > > Marko > >Received on 2021-02-21 22:00:02
Archive generated by hypermail 2.3.0.