Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • Jun 05 09:20
    dependabot[bot] labeled #482
  • Jun 05 09:20
    dependabot[bot] labeled #482
  • Jun 05 09:20
    dependabot[bot] opened #482
  • Jun 05 09:20

    dependabot[bot] on npm_and_yarn

    Bump ws from 6.2.1 to 6.2.2 in … (compare)

  • May 27 13:10
    dependabot[bot] labeled #481
  • May 27 13:10
    dependabot[bot] labeled #481
  • May 27 13:10
    dependabot[bot] opened #481
  • May 27 13:10

    dependabot[bot] on npm_and_yarn

    Bump dns-packet from 1.3.1 to 1… (compare)

  • May 25 07:46
    dependabot[bot] labeled #480
  • May 25 07:46
    dependabot[bot] labeled #480
  • May 25 07:46
    dependabot[bot] opened #480
  • May 25 07:46

    dependabot[bot] on npm_and_yarn

    Bump browserslist from 4.16.3 t… (compare)

  • May 12 01:11
    dependabot[bot] labeled #479
  • May 12 01:11
    dependabot[bot] labeled #479
  • May 12 01:11
    dependabot[bot] opened #479
  • May 12 01:11

    dependabot[bot] on npm_and_yarn

    Bump postcss from 8.2.7 to 8.2.… (compare)

  • May 10 07:17
    dependabot[bot] labeled #478
  • May 10 07:17
    dependabot[bot] labeled #478
  • May 10 07:17
    dependabot[bot] opened #478
  • May 10 07:17

    dependabot[bot] on npm_and_yarn

    Bump hosted-git-info from 2.7.1… (compare)

Taichi Ishitani
@taichi-ishitani
These are basic tests so some bit field types may not be tested enough.
Dan Gisselquist
@ZipCPU
taichi-ishitani: Okay, so ... here's why I'm interested: I've taken an interest in formally verifying AXI and AXI-lite components. When I find an open source component, I like to formally verify it to see if I can find any faults with it.
So, I pulled your design into SymbiYosys to see if I might find some faults.
However, my own perspective is quite biased. I tend to have an unfailing belief in formal methods, and also a strong prejudice against simulation based methods. This is based on my own experience which (sadly) is much too limited.
So ... I figured I'd ask you to see your thoughts on whether or not you felt your design was working, before revealing any of the bugs I've found using formal methods.
:D
Taichi Ishitani
@taichi-ishitani
I've tested my axi4 lite bridge with simple sequence only and have not yet tested it with stressful access sequences.
Therefore, I'm not sure whether or not the bridge module always works well.
Dan Gisselquist
@ZipCPU
That's fair enough.
Have you tried using SymbiYosys at all?
Taichi Ishitani
@taichi-ishitani
so your trial by using formal methods increases quality of my axi4 lite bridge module :)

Have you tried using SymbiYosys at all?

no I have not yet. What kind of tool?

Dan Gisselquist
@ZipCPU
SymbiYosys uses Yosys to convert a Verilog design into a formal property description, suitable for a formal solver to work with.
If you add your design to a set of AXI-lite properties, such as those found here: https://github.com/ZipCPU/wb2axip/blob/master/bench/formal/faxil_slave.v
You can then check whether or not your design meets the criteria for being a valid AXI4-lite slave.
I use SymbiYosys quite regularly with just about all of my designs, and certainly with any design that will ever touch a bus of any type.
It gives me a strong confidence that my designs work.
Taichi Ishitani
@taichi-ishitani
To verify converted formal properties, we need to use formal verification tool (VC formal, jasper)?
Dan Gisselquist
@ZipCPU
No. Yices works just fine, as does Boolector.
I'm using yices so far for my tests. Everything I've done at this point has all been open source.
Taichi Ishitani
@taichi-ishitani
Thanks for the information. Sounds good!
Dan Gisselquist
@ZipCPU
taichi-ishitani: Here are two traces, showing how well your design works (when it works): https://imgur.com/a/09SG0je
That said, this is ... one of the most complex AXI-lite designs I've examined so far. It seems kind of strange, though, for a protocol which is (supposed to be) a lite version of AXI, or for that matter something that should be as simple as a basic register controller.
Taichi Ishitani
@taichi-ishitani

one of the most complex AXI-lite designs I've examined so far.

This module has a state machine to control request ready and response valid so you think so.
Generated modules may be connected with other modules cascadingly and so, in some case, it will take multiple cycles to get read data.
Therefore, I've implement the bridge module that way.

Dan Gisselquist
@ZipCPU
Here are the files I used when running SymbiYosys: https://gist.github.com/ZipCPU/05c2182cd833a243709db537b7953821
You'll still need the AXI-lite slave property set, but after that you should have everything you need to repeat my experiments with your design.
The AXI-slave property set is posted, just not in the same place. You can find that here: https://github.com/ZipCPU/wb2axip/blob/master/bench/formal/faxil_slave.v
Taichi Ishitani
@taichi-ishitani
connect my generated module and your formal AXI driver then I can verify my design by using SymbiYosys tool. Correct?
Dan Gisselquist
@ZipCPU
The design I just shared on gist.github.com does exactly that
Taichi Ishitani
@taichi-ishitani
Thanks. I understand. I will try to use SymbYosis tool.
Dan Gisselquist
@ZipCPU
taichi-ishitani: Still haven't tried formal methods?
Dan Gisselquist
@ZipCPU
taichi-ishitani: Here's a trace SymbiYosys is giving me. https://imgur.com/CAyxr3h This would crash Xilinx's (new) AXI Smartconnect interconnect.
Taichi Ishitani
@taichi-ishitani
I have not yet tried. New project for work is just started so I'm very busy.
Dan Gisselquist
@ZipCPU
Ok
Taichi Ishitani
@taichi-ishitani

https://github.com/rggen/rggen-verilog-rtl/blob/700657593c90e34db4f02f2ffc26664bb8939749/rggen_axi4lite_adapter.v#L215
This is handshake logic for write/read response.

  • w_bus_valid will be asserted when r_response_valid eq 0
  • r_response_valid will be de-asserted when response handshake is completed

Therefore, waveform which you show is strange.

Dan Gisselquist
@ZipCPU
taichi-ishitani: Okay, found the issue. I had the core configured for a synchronous reset.
Dan Gisselquist
@ZipCPU
:/
My apologies.
Taichi Ishitani
@taichi-ishitani
No problem :)
tgingold
@tgingold
3/ is the way to go. The needed information is already extracted. I will to do it.
I am not sure what do you mean by 'translate aggregates'. But yes, it is chain of choices.
Olof Kindgren
@olofk
Don't miss the next edition of FOSSi Dial-Up tomorrow https://www.fossi-foundation.org/dial-up/
hkalbasi
@hkalbasi:mozilla.org
[m]
Hi, why rocket chip and boom isn't on the librecore directory of cores?
Dan Gisselquist
@ZipCPU
The librecore registry of cores is (generally) generated by the core authors.
hkalbasi
@hkalbasi:mozilla.org
[m]
So can someone add them or it is against the rules of librecore?
Dan Gisselquist
@ZipCPU
Don't know. Let's see if someone else here does.
Jonathan Balkind
@Jbalkind
projects are listed under a username, not just the project name
so it might be a little strange for it to be randomperson/rocket or randomperson/boom
but I don't recall if there was any structural limitation against doing so