Overview of the witness validation flow
Correctness Witness Validation
flowchart LR
subgraph input
prog([C program])
cwit([C witness])
cir([Btor2 circuit])
strat([validation<br>strategy])
end
subgraph translation
trans[witness<br>translator]
end
bwit([Btor2<br>witness])
subgraph validation
instr[circuit<br>instrumentor]
cir2(["instrumented<br>circuit(s)"])
verifier[HW verifier]
end
subgraph output
ans(["true /<br>unknown (+ reason) /<br>error (+ reason)"])
end
prog-->trans
cwit-->trans
cir-->trans
trans-->bwit
strat-->instr
bwit-->instr
cir-->instr
instr-->cir2
strat-->verifier
cir2-->verifier
verifier-->ans
-
btor2aiger
could become a part of the circuit instrumentor, we might need to check in a pre-compiled binary - If multiple HW verifiers are specified (via
--backend_verifier <actor_def.yml>:<version>
), they will be executed sequentially (or in parallel)
Violation Witness Validation
flowchart LR
subgraph input
prog([C program])
cwit([C witness])
cir([Btor2 circuit])
end
subgraph translation
trans[witness<br>translator]
end
bwit([Btor2<br>witness])
subgraph validation
sim["HW simulator<br>(BtorSim)"]
end
subgraph output
ans(["false /<br>unknown (+ reason)/<br>error (+ reason)"])
end
prog-->trans
cwit-->trans
cir-->trans
trans-->bwit
bwit-->sim
sim-->ans
Implementation
Currently, most functionalities have been implemented. The next step is to wrap them into a standalone validator (see the "validator" blocks above).
Benchmarking
To execute them with BenchExec, we also need to write tool-info modules (template).
Edited by Po-Chun Chien