Code

Add properties to verify dst and we#10

Code

Merged

fennecJ merged 7 commits intomasterfennecJ/formal_verification_RV32I:masterfrom a3012085/modified_jal_propertyfennecJ/formal_verification_RV32I:a3012085/modified_jal_propertyCopy head branch name to clipboardOct 27, 2024

+87-4

Commits

Commits on Oct 23, 2024

• Complete JAL ISA formal properties

  

  jhsy1209021

  authored and

  a3012085

  committed
  a6961fb

  Copy full SHA for a6961fb

• Use inst_valid instead of bubble

  

  jhsy1209021

  authored and

  a3012085

  committed
  335e21c

  Copy full SHA for 335e21c

• Add properties to verify rd(dst) and wen

  

  a3012085

  committed
  db9dc09

  Copy full SHA for db9dc09

• Verify all properties at once

  

  a3012085

  committed
  27a7e62

  Copy full SHA for 27a7e62

Commits on Oct 24, 2024

• Modify property name

  Show description for 2ea1072
  

  a3012085

  committed
  2ea1072

  Copy full SHA for 2ea1072

• Remove unnecessary checking in JAL property

  

  a3012085

  committed
  ae7c9fc

  Copy full SHA for ae7c9fc

Commits on Oct 27, 2024

• Simply porperty and clarify goto and intersect

  

  a3012085

  committed
  b4f8e84

  Copy full SHA for b4f8e84