proxy.golang.org : github.com/irifrance/reach
Package reach contains finite state symbolic reachability libraries and tools. All reachability checking in this package and its subpackages uses a sequential circuit in the form of http://godoc.org/github.com/irifrance/gini/logic#S to represent a transition relation between state variables. State variables are latches in `S`. The set of initial states is defined by the initial values of latches in `S` and the bad states are defined by a literal in `S`. The root package, reach, is centered around a few data structures to to aid in coordinating checkers. `Output`, which is the output of a checker from analyzing a logic.S and a, or some, bad states. `Result`, which is the result of analysing a single reachability query with one set of bad states represented by a z.Lit in a logic.S. `Primer` which can find `x'` given `x` for latches and properties. `Trace`, which is a trace of a sequential logic system. These are concepts related to coordination of checkers. Various checkers are found in the subpackages of reach.
Registry
-
Source
- Documentation
- JSON
- codemeta.json
purl: pkg:golang/github.com/irifrance/reach
License: MIT
Latest release: about 4 years ago
First release: almost 7 years ago
Namespace: github.com/irifrance
Last synced: about 5 hours ago