search

pulp-platform / pulpissimo

This is the top-level project for the PULPissimo Platform. It instantiates a PULPissimo open-source system with a PULP SoC domain, but no cluster.
Other
386 stars 167 forks source link

Formality crashes while reading in pulpissimo #38

Open dronox opened 5 years ago

dronox commented 5 years ago

Hi guys,

I tried to synthesize pulpissimo down to gate-level using Synopsys Design Compiler (I used gtech.db as target library for test purposes). The synthesis basically worked (except of course that I didn't provide memory IPs, FLL IPs, I/O cells and so on). Then I used the scripts generated by Design Compiler (default.svf and the script generated by read_file {..} -write_script formality.script) to start verification using Formality. Unfortunately, Formality crashed while reading in the RTL design.

Did you ever had that case? Or which verification tool are you using?

Thanks & Best Regards, Dustin

FrancescoConti commented 5 years ago

Hi @dronox, interesting. I am not sure whether Formality supports the same subset of SystemVerilog of DC (which is what we use for PULPissimo). Can you provide a log before the crash, and versions of DC and Formality?

dronox commented 5 years ago

Hi @FrancescoConti,

okay, I think I intermixed the behavior of Formality for the whole pulpissimo and a sub-design (I assume I tested fc_subsystem, which led to a crash - but I did not check it again). Formality does not really "crash" for pulpissimo, but it cannot load this design successfully. For pulpissimo, formality complains about a huge net which cannot be load:

Error: Net 'stream_i' width (536870916 bits) exceeds limit. (File: /local/peterson/workspace/pulp-platform/pulpissimo/ips/hwpe-stream/rtl/hwpe_stream_merge.sv Line: 27) (FMR_ELAB-270)).

Attached you'll find the complete log file for that. formality_pulpissimo.log

Versions: Formality O-2018.06-SP2 Design Compiler O-2018.06-SP2

FrancescoConti commented 5 years ago

It looks like Formality does not like the fact that hwpe_stream_merge contains a vector of interfaces (with only one interface, i.e. [0:0]) on its boundary. In fact stream_i is an interface, not a net, and it contains 32 data bits + 2 handshake bits. I am quite sure this works fine in DC as I use this construct extensively also in more complex scenarios, but perhaps Formality is confused (the fact that it identifies an interface as a "net" seems to indicate so).

Perhaps you can try to do a formal check of https://github.com/pulp-platform/hwpe-mac-engine which is signficantly smaller than the full design in terms of complexity.