search

armleo / ArmleoCPU

ArmleoCPU - RISC-V CPU RV64GC, SMP, Linux, Doom. Work in progress to execute first instruction with new feature set
GNU General Public License v3.0
4 stars 0 forks source link

Add formal verification #47

Open armleo opened 3 years ago

ZipCPU commented 3 years ago

I look forward to reading about how this turns out.

Dan

armleo commented 3 years ago

I have a very simple formal verification, which you can see at: https://github.com/armleo/ArmleoCPU/tree/deprecated_development/testbenches/formal_divider

This was my first time using it, currently not my priority because I am planning to tape this out and really don't have time to verify everything :D.

Also thanks for your articles they are the best!

ZipCPU commented 3 years ago

Formally verifying a divider your first time out? My guess is that it didn't work out well for you, and so you got frustrated and gave up--putting the task off for later. Did I guess right?

armleo commented 3 years ago

I verified the divider and multiplier, but it took ~32 cycles and I had the following problems:

Now I realized I am dumb and should have followed my gut :)

ZipCPU commented 3 years ago

I can usually force a reset before usage with the old f_past_valid routine:

    reg f_past_valid;
    initial f_past_valid = 0;
    always @(posedge clk)
      f_past_valid <= 1;
    always @(*)
    if (!f_past_valid)
      assume(reset);

This won't help during an induction check, however. During induction you will need more assertions instead--and you can't assert the reset, unless your design reasonably wants a reset every N clocks.

As for time to tape out ... I can understand the sentiment. You are behind the learning curve. That's going to hurt any attempt at formal methods. They do take a while to learn. However, once learned, they're often a lot faster to use than the longer and longer simulations that get used instead. Just ... be careful what you intend to verify. Formal works better on the lower modules than the entire design. Yes, you can apply formal to an entire CPU--although I normally break a CPU into chunks. Likewise, formal methods don't work on multiplies or divides very well. (Sorry) They work much better on bus interfaces and pipeline handshakes.

Dan

armleo commented 3 years ago

As for time to tape out ... I can understand the sentiment. You are behind the learning curve.

Yeah pretty much, I am just too busy with other stuff in my life, so I don't have enough time for open-source.

ZipCPU commented 3 years ago

Well ... yes/no. You mentioned above that you are trying to get a job. That's the perfect time for open source. Any/all of your open source projects can be used as a port-folio that you can then use to advertise yourself to a prospective employer. Do the job you want to do as open source, and then let them evaluate the quality of your work. If they like it, they'll hire you. I'd certainly be more interested in hiring someone if 1) I could see the quality of their work product, and 2) it was as good as (or better) than the last person I had hired.

Incidentally, that's what lead me to formal methods. 1) I needed a job. 2) I was using open source as a portfolio to be hired from, and 3) having discovered one bug in my (simulation proved) open source projects I was afraid there were more. Worse, I was afraid someone reviewing one of my designs would've "seen" a bug and just never called (or never called back). Indeed, I can now look at AXI designs with a glance and often see a lot of common bugs--so this is a very real possibility to be worried about.

armleo commented 3 years ago

The problem is no matter what I do, I just won't be able to get a job. There are no Verilog/FPGA jobs in my country, and I can't leave my country because of mandatory army service. (pretty complex topic, but looks like I am stuck in here for at least 5 years). Instead, I am just doing software development, which pays enough but it's not something that I like a lot, because it's not challenging enough. Anyway, thanks for suggestions I will take a look at it once I have more time!

ZipCPU commented 3 years ago

Feel free to contact me on Freenode (or Libera.Chat) if you'd like to discuss this further. There are other options available to you.