fangism / hackt

Hierarchical Asynchronous Circuit Kompiler Toolkit
http://vlsi.cornell.edu/~fang/hackt
GNU General Public License v2.0
23 stars 3 forks source link

[tool] exhaustive QDI verifier/prover "prlint" #73

Open fangism opened 8 years ago

fangism commented 8 years ago

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 commented 8 years ago

b/31603541