Skip to content

ci(formal): read the props file with -formal - #2272

Merged
gHashTag merged 1 commit into
masterfrom
ci/formal-props-formal-flag
Aug 19, 2026
Merged

ci(formal): read the props file with -formal#2272
gHashTag merged 1 commit into
masterfrom
ci/formal-props-formal-flag

Conversation

@gHashTag

Copy link
Copy Markdown
Owner

Closes #2271. Refs #2265. One flag, exact-error negative control both directions. docs/NOW.md updated.

🤖 Generated with Claude Code

The layer-5 flag fix covered only the DUT read line; CI yosys read the
props plain and resolved 'assert' as a task name (rc=16) while the local
proof had flagged both reads. Negative control: the flagless read
reproduces the exact CI error locally; with -formal the chain proves
Status PASSED. All three .sby updated, including the blocked uart one.

Closes #2271.
@gHashTag
gHashTag enabled auto-merge (squash) August 19, 2026 23:56
@github-actions

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-08-19 23:56:27 UTC

Summary

Status Count
Total Open PRs 25
PRs with Failing Checks 10
PRs with All Checks Green 15
READY 7
FAILING 10
PENDING 0

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=375b2f88cc2f != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

@github-actions

Copy link
Copy Markdown
Contributor

📓 NotebookLM Notebook linked to this PR

This notebook contains session context, decisions, and artifacts for this work.

@gHashTag
gHashTag merged commit 24d81bd into master Aug 19, 2026
19 of 21 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

formal .sby read the props file without -formal — 'assert' resolved as a task name

1 participant