reach

package module
v0.1.3 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Aug 25, 2021 License: MIT Imports: 15 Imported by: 0

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: DOI

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

Constants

This section is empty.

Variables

This section is empty.

Functions

This section is empty.

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

Source Files

View all Source files

Directories

Path Synopsis
Package bmc provides bounded model checking support.
 Package bmc provides bounded model checking support.
cmd
Package cmd provides reach package related commands.
 Package cmd provides reach package related commands.
reach
Command reach provides a cli for binary system reachability.
 Command reach provides a cli for binary system reachability.
doc
slides/fmtabc
iic
Package iic provides an incremental inductive reachability checker.
 Package iic provides an incremental inductive reachability checker.
internal/cnf
Package cnf provides a levelled cnf for iic.
 Package cnf provides a levelled cnf for iic.
internal/lits
Package lits supports storage of and miscellaneous operations on literals for iic.
 Package lits supports storage of and miscellaneous operations on literals for iic.
internal/obs
Package obs provides support for proof obligations.
 Package obs provides support for proof obligations.
internal/queue
Packaage queue contains a basic queue of ints.
 Packaage queue contains a basic queue of ints.
Package sim provides simulation capabilities.
 Package sim provides simulation capabilities.

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.