Add pono model checker

[tmeissner]

This is an attempt to add the Pono model checker.

Test with SymbiYosys is left as I don't remember how I could build all the necessary containers locally on my Mac.

[umarcor]

Thanks a lot for this so complete PR :heart:

There is a minor problem with the extension of the dockerfile. It needs to be lowercase (s/D/d/).

Test with SymbiYosys is left as I don't remember how I could build all the necessary containers locally on my Mac.

It changed since last time. However, it's in the workflow you contributed :wink: :

./.github/bin/dockerBuild -c debian-buster -d pkg:pono

The CI issues are unrelated to your changes. Something is wrong with the condition: github.event_name != 'pull_request' && github.repository == 'hdl/containers' && ${{ matrix.os }} == 'debian-buster'. The login to ghcr.io is skipped (github.event_name != 'pull_request' && github.repository == 'hdl/containers') but this one is always evaluated true...

However, when executed locally, I get the same error as https://github.com/hdl/containers/runs/2538090602?check_suite_focus=true

...
#5 129.7 update-alternatives: using /usr/lib/jvm/java-11-openjdk-amd64/bin/java to provide /usr/bin/java (java) in auto mode
#5 129.7 update-alternatives: error: error creating symbolic link '/usr/share/man/man1/java.1.gz.dpkg-tmp': 
No such file or directory
#5 129.7 dpkg: error processing package openjdk-11-jre-headless:amd64 (--configure):
#5 129.7  installed openjdk-11-jre-headless:amd64 package post-installation script subprocess returned error exit status 2
#5 129.7 dpkg: dependency problems prevent configuration of ca-certificates-java:
#5 129.7  ca-certificates-java depends on default-jre-headless | java8-runtime-headless; however:
#5 129.7   Package default-jre-headless is not installed.
#5 129.7   Package java8-runtime-headless is not installed.
#5 129.7   Package openjdk-11-jre-headless:amd64 which provides java8-runtime-headless is not configured yet.
#5 129.7
#5 129.7 dpkg: error processing package ca-certificates-java (--configure):
#5 129.7  dependency problems - leaving unconfigured
#5 129.7 Processing triggers for mime-support (3.62) ...
#5 130.1 Processing triggers for libc-bin (2.28-10) ...
#5 131.1 Processing triggers for ca-certificates (20200601~deb10u2) ...
#5 131.3 Updating certificates in /etc/ssl/certs...
#5 132.2 0 added, 0 removed; done.
#5 132.2 Running hooks in /etc/ca-certificates/update.d...
#5 132.2 done.
#5 132.5 Errors were encountered while processing:
#5 132.5  openjdk-11-jre-headless:amd64
#5 132.5  ca-certificates-java
#5 132.5 E: Sub-process /usr/bin/dpkg returned an error code (1)
#5 ERROR: executor failed running [/bin/sh -c apt-get update -qq  && DEBIAN_FRONTEND=noninteractive apt-get 
-y install --no-install-recommends     binutils     cmake     autoconf     libgmp-dev     m4     python3-toml     openjdk-11-jre-headless  && apt-get autoclean && apt-get clean && apt-get -y autoremove  && update-ca-certificates   && rm -rf /var/lib/apt/lists/*]: exit code: 100

[umarcor]

I pushed some minor fixes to this PR. The build is succesful, and the formal image was updated too. Please, when you test it, change this PR to "Ready for review", so I can merge :D.

[tmeissner]

Haha, I forgot to adopt the creating of the man1 directory from my local dockerfile copy. I've stumbled over the same error you got 😆

[tmeissner]

With the addition of the libgmpxx4ldbl package, pono seems to work now. I've tested it with SymbiYosys in bmc mode. Pono can be used with the btor engine. Currently bmc its the only supported mode.

Example for the relevant part of the sby-file:

[engines]
cover: smtbmc z3
bmc: btor pono
prove: abc pdr

In conjunction with BTOR engine it seems to be pretty fast compared to other engines/solvers like SMTBMC (z3, boolector) or abc. It depends on the design to check, but for my fifo test design I get following run times for a BMC 20 cycles deep:

Boolector: 43 sec
Pono:      2 sec
z3:        2622 sec
abc:       61 sec

Mhm, maybe there is something wrong with the BTOR engine. It seems that the checker only tests one assert. Have to dig in deeper later.

Update: pono has a parameter --prop, -p which gives the property index to check (default: 0). Symbiyosys calls the pono checker without this parameter, so only property 0 (the first in the btor-file) is checked. I haven't found a possibility to check more than one property during a run yet.

[umarcor]

Thanks!