berkeley-abc/abc

How to run PDR

sirandreww opened this issue · 1 comments

sirandreww commented

Description

This issue is not so much an issue, but a compilation of my findings when researching how to use abc to verify hardware models using PDR. More specifically, what commands to run to be able to verify And Inverter Graphs following the AIGER 1.9 format https://fmv.jku.at/aiger/, this is the file format that was used to run abc in the Hard-Ware Model Checking Competition (HWMCC), the most resent of which being HWMCC20.

Final Answers:

To run PDR on an AIG file called path.aig run one of the 2 following commands:

Option 1

Using ABC9 &put command:

./abc -c "&read path.aig ; &put ; fold ; pdr -v"

Option 2

Using previous ABC commands:

./abc -c "read path.aig ; logic ; undc ; strash ; zero ; fold ; pdr -v"

I assume fold2 would work for both options but I have not tried it.

Process in finding these commands:

Finding these command was not easy. I tried a few things that all turned out to produce incorrect proofs on designs that are known to be unsafe, or provide counter examples on designs that were known to be safe. These are my attempts and the results I got.

Attempt 1

./abc -c "read path.aig ; pdr -v"

This does not work because PDR does not support invariant constraints and uninitialized latches.

Attempt 2

./abc -c "read path.aig ; zero ; fold2 ; pdr -v"

This did not work because I assume zero does not handle the case of uninitialized latches.

Attempt 3

./abc -c "&read path.aig ; &st ; &put ; fold ; pdr -v"

I assumed this command would work because of #216 (comment) but &st seemed to make the command return incorrect results.

Sources:

sterin commented

Overview

PDR (and many other ABC commands) assumes the circuit it operates on is an AIG such that:

  1. All latches are initialized to zero

  2. All primary outputs (POs) are properties - a legal counterexample is one that results in one of the POs becoming 1 (i.e. reaches a bad state)

That is, newer AIGER 1.9 features such as constraints, 1-initialized latches, or nondeterministically-initialized latches are ignored. Outputs (even constraints) are treated as properties, and latches are assumed to be 0-initialized. To get a meaningful answer from PDR on an AIG that contains these features, you have to model the newer feature in the old format. In ABC this is done by running the undc, zero, and fold commands.

For example:

./abc -c ‘read picorv32_mutBX_nomem-p8.aig ; logic ; undc ; strash ; zero ; fold ; pdr’

undc

The undc command only works on logic circuits (an older ABC representation), so the logic command needs to be run prior to it to convert the AIG to a logic circuit. The zero command requires the circuit to be an AIG, so a strash command needs to run prior to it to convert the logic circuit to a structurally hashed AIG. The fold command also requires the circuit to be an AIG, but it is already an AIG at this point.

The undc command creates a single latch that is initialized to zero but is one afterwards.

init(not_is_init) := 0
next(not_is_init) := 1

And defines:

is_init := !not_is_init

This construction results in is_init being true on the first cycle and false afterwards. This is then used to model nondeterministic initialization as follows, replacing:

init(L) := nondet
next(L) := f

With a zero-initialized latch L_undc,

init(L_undc) := 0
next(L_undc) := f

And a fresh primary input (PI) PI_undc that models the non deterministic initialization. It then replaces all references to the original latch L with the following expression

L := is_init ? PI_undc : L_undc

zero

The zero command replaces each one-initialized latch

init(L) := 1
next(L) := f

With an inverted version of the latch

init(L_inv) := 0
next(L_inv) := !f

It then replaces all references to the original latch L with the following expression:

L := !L_inv

fold

The fold command "folds" the contstraints into the properties.

constraints_violated_in_current_cycle := (!C_0 || ... || !C_n )

init(constraints_violated_previously) := 0
next(constraints_violated_previously) := constraints_violated_in_current_cycle || constraints_violated_previously

constraints_violated := constraints_violated_in_current_cycle || constraints_violated_previously

It then replaces each property PI_i with

PI_fold_i := !violated && PI_i

That is, PI_fold_i can only be asserted if all constraints held up the current cycle, which is the AIGER 1.9 semantics.

Notes

  1. The names above are for ease of presentation, the actual names in ABC are different.

  2. "Replace all the references to L" means that a new circuit is constructed with the references replaced, the original circuit is not modified.