Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add Formal #18

Merged
merged 8 commits into from
Sep 22, 2024
Merged

Add Formal #18

merged 8 commits into from
Sep 22, 2024

Conversation

Clo91eaf
Copy link
Contributor

No description provided.

@Clo91eaf Clo91eaf changed the title Add Add Formal Sep 19, 2024
unlsycn
unlsycn requested changes Sep 19, 2024
View reviewed changes
templates/chisel/flake.nix Outdated Show resolved Hide resolved
@Avimitin
Copy link
Contributor

cc @sequencer for co-review

@Clo91eaf Clo91eaf force-pushed the try_formal branch 4 times, most recently from 8fc15cb to 87c425e Compare September 21, 2024 13:19
sequencer
sequencer reviewed Sep 21, 2024
View reviewed changes
templates/chisel/nix/pkgs/cds-fhs-env.nix Outdated Show resolved Hide resolved
templates/chisel/scripts/formal/FPV.tcl Outdated Show resolved Hide resolved
@sequencer
Copy link
Member

Please add documentation to readme.

@unlsycn unlsycn force-pushed the try_formal branch 3 times, most recently from 8f70a0a to 6d9dbdf Compare September 21, 2024 17:36
sequencer
sequencer reviewed Sep 22, 2024
View reviewed changes
Copy link
Member

@sequencer sequencer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There are other formal tools. Please change nix target from formal to jg-fpv?

readme.md Outdated Show resolved Hide resolved
@sequencer
Copy link
Member

sequencer commented Sep 22, 2024 •
edited
Loading

Reproduced via:

nix build '.#gcd.formal' --impure

got result:

[sequencer@biyun-highfreq-32 chisel]$ cat result/report.txt

==============================================================
    JasperGold Verification Results
==============================================================
    2021.03p002 64 bits for Linux64 3.10.0-1160.21.1.el7.x86_64
    Printed on: Saturday, Sep21, 2024 05:37:06 PM UTC
    Working Directory: /tmp/nix-build-formal.drv-0/gcd-elaborate-mlirbc-rtl


==============================================================
RESULTS
==============================================================

-------------------------------------------------------------------------------------------------------------------
       Name                                                       |    Result    |  Engine  |  Bound  |  Time
-------------------------------------------------------------------------------------------------------------------

---[ <embedded> ]--------------------------------------------------------------------------------------------------
[1]   GCDFormal.GCD_ASSUMPTION_INPUT_NOT_VALID                         temporary       ?                  0.000 s
[2]   GCDFormal.GCD_ASSUMPTION_INPUT_NOT_VALID:precondition1           covered         N             1    0.028 s
[3]   GCDFormal.GCD_ASSUMPTION_INPUT_4_6                               temporary       ?                  0.000 s
[4]   GCDFormal.GCD_ALWAYS_RESPONSE                                    proven          N      Infinite    0.001 s
[5]   GCDFormal.GCD_ALWAYS_RESPONSE:precondition1                      covered         Hp            1    0.030 s
[6]   GCDFormal.GCD_NO_DOUBLE_FIRE                                     proven          N          (12)    0.000 s
[7]   GCDFormal.GCD_NO_DOUBLE_FIRE:precondition1                       covered         Hp            1    0.030 s
[8]   GCDFormal.GCD_RESULT_IS_CORRECT                                  proven          N      Infinite    0.001 s
[9]   GCDFormal.GCD_RESULT_IS_CORRECT:precondition1                    covered         Hp            5    0.031 s
[10]  GCDFormal.GCD_COVER_BACK_PRESSURE                                covered         N             1    0.028 s

@unlsycn unlsycn merged commit f5aaa81 into master Sep 22, 2024
5 checks passed
@Clo91eaf Clo91eaf deleted the try_formal branch September 22, 2024 05:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sequencer sequencer sequencer left review comments

@unlsycn unlsycn unlsycn approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@Clo91eaf @Avimitin @sequencer @unlsycn