Add formal verification

[armleo]

No description provided.

[ZipCPU]

I look forward to reading about how this turns out.

Dan

[armleo]

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]

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]

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

• It took too long to verify all cases. Looking back: maybe "n, n+1, n+x solver (also called something something induction solver)" might have helped me but I stopped trying.
• And I had an issue with reset, no matter what I did I couldn't force it to reset before usage. Looking back: Maybe I should have added

`ifdef FORMAL initial begin end `endif

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

[ZipCPU]

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]

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]

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]

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]

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.