hackt icon indicating copy to clipboard operation
hackt copied to clipboard

[tool] exhaustive QDI verifier/prover "prlint"

Open fangism opened this issue 8 years ago • 1 comments

Would like to implement an exhaustive prover for stability/non-interference using prsim-based state exploration and coverage, and reachability analysis. The legacy tool that inspires this is "prlint." Without this, we rely on hacprsim and random timing simulation, which has been very practical to-date.

A re-implementation could leverage hierarchy and reachable state caching of subprocesses.

fangism avatar Sep 20 '16 01:09 fangism

b/31603541

fangism avatar Sep 20 '16 01:09 fangism