reach

README

⊧ Reach -- A Finite State Reachability Tool

Reach is a symbolic finite state reachability checker. One could also say that Reach is a safety model checker.

Install

Reach is written in Go and requires Go to build/install from source. To install Go, please see the installation webpage.

Then all one needs to do is run

go install github.com/go-air/reach/...@latest

This will also get and build our only dependency (gini) apart from Go itself.

Please have a look at our releases for the project status. If you would like to have binary distributions, please let us know by the issue tracker.

Background

As a software tool, Reach works on transition systems either in gini/logic form (for library use) or in aiger format (for cli use) which specify sequential synchronous circuits with Boolean/binary state, functions, and I/O.

Mathematically, often enough we think of these things as transition systems (x,I,T,B) where

1. x is a set of binary variables.
2. I(x) is a set of initial states.
3. T(x,x') is a transition relation over pairs of states.
4. B(x) is a set of bad states (e.g. the complement of a safety property).

I, T, and B above are formulas, so the size of the state space is 2**|x|.

The reachability problem is to find if there is a sequence of states such that the first one satisfies I(x), the last one satisfies B(x), and every adjacent pair in the sequence satisfies T(x,x').

This problem is PSPACE complete. This means the class of problems represented by possible inputs to Reach are considered intractable (but atleast decidable), more so than the easiest intractable complexity class (NP-complete).

Documentation

The doc directory contains some high level documentation. Godoc is available for library reference.

Usage

⎣ ⇨ reach
Reach is a finite state reachability tool for binary systems.

usage: reach [gopts] <command> [args]

available commands:
	iic	iic is an incremental inductive checker.
	bmc	bmc performs SAT based bounded model checking.
	sim	sim simulates aiger.
	ck	ck checks traces and inductive invariants.
	stim	stim outputs an aiger stimulus from an output directory.
	aag	aag outputs an ascii aiger of the Reach internal aig.
	aig	aig outputs an binary aiger of the Reach internal aig.
	info	info provides summary information about an aiger or output.

global options:
  -cpuprof string
    	file to output cpu profile

For help on a command, try "reach <cmd> -h".

Performance

We've developed Reach initially with tip and hwmcc benchmarks. Reach can solve a lot of these problems quickly and is fairly robust in terms of different kinds of inputs. Reach also uses some unique technology, making it reasonable to try out on inputs for which other methods (smv, abc, etc) have problems. Its proof engine is much faster than baseline IC3, but it is still behind ABC/PDR on many problems.

Citing Reach

DOI based citations and downloads:

BibTeX:

@misc{scott_cotton_2019_2554423,
  author       = {Scott  Cotton},
  title        = {go-air/reach: Tenu},
  month        = jan,
  year         = 2019,
  doi          = {10.5281/zenodo.2554423},
  url          = {https://doi.org/10.5281/zenodo.2554423}
}

Documentation

Overview

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/go-air/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.

1. `Output`, which is the output of a checker from analyzing a logic.S and a, or some, bad states.

2. `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.

3. `Primer` which can find `x'` given `x` for latches and properties.

4. `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.

Index

• type Output
  • func MakeOutput(g, dir string) (*Output, error)
  • func OpenOutput(d string) (*Output, error)
  • func (o *Output) Aiger() (*aiger.T, error)
  • func (o *Output) AigerPath() string
  • func (o *Output) AppendResult(bads ...*Result)
  • func (o *Output) Invariant(dst inter.Adder, i int) error
  • func (o *Output) InvariantPath(i int) string
  • func (o *Output) IsVerifiable(i int) bool
  • func (o *Output) Remove() error
  • func (o *Output) ResultPath(i int) string
  • func (o *Output) Results() []*Result
  • func (o *Output) RootDir() string
  • func (o *Output) Store() error
  • func (o *Output) Trace(i int) (*Trace, error)
  • func (o *Output) TracePath(i int) string
  • func (o *Output) TryVerify(dur time.Duration) []error
  • func (o *Output) TryVerifyResult(i int, dur time.Duration) []error
  • func (o *Output) Verify() []error
  • func (o *Output) VerifyResult(i int) []error
• type Primer
  • func NewPrimer(t *logic.S, ps ...z.Lit) *Primer
  • func (p *Primer) Prime(m z.Lit) z.Lit
• type Result
  • func (b *Result) Add(m z.Lit)
  • func (b *Result) FormatStatus() string
  • func (b *Result) IsReachable() bool
  • func (b *Result) IsSolved() bool
  • func (b *Result) IsUnreachable() bool
  • func (b *Result) SetReachable(t *Trace)
  • func (b *Result) SetUnreachable()
  • func (b *Result) String() string
• type Trace
  • func DecodeTrace(r io.Reader) (*Trace, error)
  • func NewTrace(s *logic.S, ws ...z.Lit) *Trace
  • func NewTraceBmc(u *logic.Roll, model inter.Model, ws ...z.Lit) (*Trace, []error)
  • func NewTraceLen(s *logic.S, sLen int, ws ...z.Lit) *Trace
  • func (t *Trace) Append(vs []bool)
  • func (t *Trace) Encode(w io.Writer) error
  • func (t *Trace) EncodeAigerStim(dst io.Writer) (int, error)
  • func (t *Trace) InputVal(i, depth int) bool
  • func (t *Trace) LatchVal(i, depth int) bool
  • func (t *Trace) Len() int
  • func (t *Trace) Verify(s *logic.S) []error
  • func (t *Trace) WatchVal(i, depth int) bool

Types

type Output

type Output struct {
	// contains filtered or unexported fields
}

Output encapsulates the output of the reach command checking subcommands.

func MakeOutput

func MakeOutput(g, dir string) (*Output, error)

MakeOutput creates an output object backed by directory root dir and binary aiger file with path g.

MakeOutput tries to create dir/basename(g) as a directory where basename(g) is the filename of g (not the full path) with the extension removed.

MakeOutput then tries to symlink g into the dir above. If all that goes well, MakeOutput returns an output object and a nil error. Otherwise, MakeOutput returns a nil Output and a non-nil error.

func OpenOutput

func OpenOutput(d string) (*Output, error)

OpenOutput tries to open an output as created by MakeOutput.

func (*Output) Aiger

func (o *Output) Aiger() (*aiger.T, error)

Aiger tries to return the aiger for this problem

func (*Output) AigerPath

func (o *Output) AigerPath() string

AigerPath gives the path to the linked aiger.

func (*Output) AppendResult

func (o *Output) AppendResult(bads ...*Result)

AppendResult lets a checker append bad state information to the output.

func (*Output) Invariant

func (o *Output) Invariant(dst inter.Adder, i int) error

Invariant places the invariant associated with bad state i in dst.

func (*Output) InvariantPath

func (o *Output) InvariantPath(i int) string

InvariantPath gives the path to the invariant associated with bad state i.

func (*Output) IsVerifiable

func (o *Output) IsVerifiable(i int) bool

IsVerifiable returns whether or not the `i`th bad states formula has either

1. a trace and is reachable; or
2. an invariant is unreachable

IsVerifiable checks the existence of files by os.Stat to accomplish this.

func (*Output) Remove

func (o *Output) Remove() error

Remove tries to remove the output info, which is a recursive directory removal. It returns non-nil error if this directory removal fails. Once remove has been called, Store will fail.

func (*Output) ResultPath

func (o *Output) ResultPath(i int) string

ResultPath gives the path associated with storing Result meta-data, in json and parseable by json.Unmarshall.

func (*Output) Results

func (o *Output) Results() []*Result

Results returns the bad states for which `o` contains result information.

func (*Output) RootDir

func (o *Output) RootDir() string

RootDir gives the root of the output directory.

func (*Output) Store

func (o *Output) Store() error

Store attempts to store `o`, including any traces or invariants found in it's bad states. Store returns a non-nil error if there is a problem doing this.

func (*Output) Trace

func (o *Output) Trace(i int) (*Trace, error)

Trace tries to parse and return the trace associated with `i`th bad state info. Trace does not cache.

func (*Output) TracePath

func (o *Output) TracePath(i int) string

TracePath gives the path to trace associated with bad state i.

func (*Output) TryVerify

func (o *Output) TryVerify(dur time.Duration) []error

TryVerify tries to verify all traces and invariants given to `o`, each within `dur` time.

func (*Output) TryVerifyResult

func (o *Output) TryVerifyResult(i int, dur time.Duration) []error

TryVerifyResult

func (*Output) Verify

func (o *Output) Verify() []error

Verify verifies all traces and invariants given to `o`, returning a slice of errors if there are any, and nil otherwise.

Verify is time limited to 1 second. Since Verify requires sat calls for invariant verification, one possibgle error is ErrTimeout. Use TryVerify to specify a different time limit.

func (*Output) VerifyResult

func (o *Output) VerifyResult(i int) []error

VerifyResult verifies the results associated with Result at index i in the backing Result slice.

It should only be called when the corresponding bad has either an invariant or trace associated with it.

type Primer

type Primer struct {
	// contains filtered or unexported fields
}

Primer takes literals in a logic.S and returns the corresponding literal with latches replaced with their next states.

func NewPrimer

func NewPrimer(t *logic.S, ps ...z.Lit) *Primer

NewPrimer creates a new primer for a sequential system in type *logic.S for the latches in `t` and the properties specified in `ps`.

NewPrimer may, and usually does, add nodes `t`.

func (*Primer) Prime

func (p *Primer) Prime(m z.Lit) z.Lit

Prime finds the primed version of a literal `m` in the transition system `trans` passed to NewPrimer. `m` should have been present in `trans` when NewPrimer was called. If this is not the case, Prime may panic or otherwise have undefined behavior.

type Result

type Result struct {
	M         z.Lit         // the defining literal in the associated logic.S
	Status    int           // 1=reachable -1=unreachable 0=unknown
	Depth     int           // The depth of the analysis (= length of trace or depth of unreachability)
	Dur       time.Duration // If a timeout was specified, then its duration.
	Trace     *Trace        `json:"-"` // A trace (optional even if Reachable is true)
	Invariant []z.Lit       `json:"-"` // invariant in cnf.
}

Result holds info about bad states.

func (*Result) Add

func (b *Result) Add(m z.Lit)

Add is for storing an invarant proving unreachability in memory. It is optional.

func (*Result) FormatStatus

func (b *Result) FormatStatus() string

FormatStatus returns

func (*Result) IsReachable

func (b *Result) IsReachable() bool

IsReachable returns if a bad state is known to be reachable.

func (*Result) IsSolved

func (b *Result) IsSolved() bool

IsSolved returns whether or not the result represents a solution of a bad state.

func (*Result) IsUnreachable

func (b *Result) IsUnreachable() bool

IsUnreachable returns whether `b` is known to be unreachable.

func (*Result) SetReachable

func (b *Result) SetReachable(t *Trace)

SetReachable makes b known to be reachable. The trace `t` is optional and will be recorded.

func (*Result) SetUnreachable

func (b *Result) SetUnreachable()

SetUnreachable makes `b` known to be unreachable.

func (*Result) String

func (b *Result) String() string

type Trace

type Trace struct {
	Inputs  []z.Lit
	Latches []z.Lit
	Watches []z.Lit
	// contains filtered or unexported fields
}

Trace holds data for a trace of a sequential circuit as defined by `github.com/go-air/gini/logic.S`, giving values to the latches, inputs, and an optional list of watched literals.

func DecodeTrace

func DecodeTrace(r io.Reader) (*Trace, error)

DecodeTrace tries to read a trace as written by Encode. DecodeTrace returns a non-nil error if there is an io or formatting error.

func NewTrace

func NewTrace(s *logic.S, ws ...z.Lit) *Trace

NewTrace creates a new trace of length 0 containing all the inputs and latches of `s` and the specified watches `ws`.

func NewTraceBmc

func NewTraceBmc(u *logic.Roll, model inter.Model, ws ...z.Lit) (*Trace, []error)

NewTraceBmc creates a new trace given an unroller `u` and a model for the combinational circuit `u.C`.

Since the unroller only contains cone of influence portion of a sequential circuit, the undefined values are taken by simulation. The model is checked to be coherent with the simulation. A non-nil error is returned iff there is incoherence.

func NewTraceLen

func NewTraceLen(s *logic.S, sLen int, ws ...z.Lit) *Trace

NewTraceLen creates a new trace of length 0 containing all the inputs and latches of `s` and the specified watches `ws` from the first `sLen` nodes of `s`.

If `s` was created at one time suitable for making a trace, and had len `n==s.Len()` at this time, and later new latches or gates or inputs were defined in `s`, then the circuit `s` when it had len `n` may be used for constructing a new trace, specifying sLen as `n`.

func (*Trace) Append

func (t *Trace) Append(vs []bool)

Append adds a new step to the trace.

`vs` should be the truth values associated with an evaluation of a circuit with corresponding input, latch, and watch literals. If `s` is such a circuit, then `len(vs) == s.Len()` and `vs` contains truth values for all gates in the circuit indexed by variable, as in `github.com/go-air/gini/logic.C.Eval`

func (*Trace) Encode

func (t *Trace) Encode(w io.Writer) error

Encode writes a trace in a mostly binary format with some readable header info.

func (*Trace) EncodeAigerStim

func (t *Trace) EncodeAigerStim(dst io.Writer) (int, error)

EncodeAigerStim encodes a 'stimulus', which for an aiger file is just the sequence of inputs (since all initial values are assumed to be '0' in an aiger file.

EncodeAigerStim returns the number of bytes written to dst and any error which occured in the process of encoding writing to dst.

func (*Trace) InputVal

func (t *Trace) InputVal(i, depth int) bool

InputVal returns the truth value for input with index i at depth `depth`.

func (*Trace) LatchVal

func (t *Trace) LatchVal(i, depth int) bool

LatchVal returns the truth value for latch with index i at depth `depth`.

func (*Trace) Len

func (t *Trace) Len() int

Len returns the number of states in the trace.

func (*Trace) Verify

func (t *Trace) Verify(s *logic.S) []error

Verify verifies that the trace is coherent with simulation under `s` and that the simulation leads to every literal in t.Watches being true at some point.

Verify returns a non nil error describing a latch or watch in a bad state in the trace with respect to s iff there is such a latch or watch.

Verify may panic if the trace is not dimensioned according to `s`. Namely, if the latches in `t` are not latches in `s`, or likewise inputs. For watches in `t`, the corresponding literals should exist in `s`.

func (*Trace) WatchVal

func (t *Trace) WatchVal(i, depth int) bool

WatchVal returns the truth value for the variable underlying the watched literal with index i at depth `depth`.