AIGER is a format for And-Inverter Graphs (AIGs).
See http://fmv.jku.at/aiger/ for details.
AIGER is used in the Hardware Model Checking Competition (HWMCC),
therefore all solvers competing in the competition have to support
the format.
The example in this directory is using super_prove as solver. Check
http://downloads.bvsrc.org/super_prove/ for the lates release. (See
https://bitbucket.org/sterin/super_prove_build for sources.)
The "demo.sh" script in this directory expects a "super_prove" executable
in the PATH. E.g. extract the release to /usr/local/libexec/super_prove
and then create a /usr/local/bin/super_prove file with the following
contents (and "chmod +x" that file):
#!/bin/bash
exec /usr/local/libexec/super_prove/bin/super_prove.sh "$@"
The "demo.sh" script also expects the "z3" SMT2 solver in the PATH for
converting the witness file generated by super_prove to VCD using
yosys-smtbmc. See https://github.com/Z3Prover/z3 for install notes.
ster' selected='selected'>master
/* * This file is part of the flashrom project. * * Copyright (C) 2009 Carl-Daniel Hailfinger * Copyright (C) 2022 secunet Security Networks AG * (Written by Thomas Heijligen <thomas.heijligen@secunet.com) * * This program is free software; you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by * the Free Software Foundation; version 2 of the License. * * This program is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. *//* * This file contains prototypes for x86 I/O Port access. */#ifndef __HWACCESS_X86_IO_H__#define __HWACCESS_X86_IO_H__ 1#include<stdint.h>/** */intrget_io_perms(void);voidOUTB(uint8_tvalue,uint16_tport);voidOUTW(uint16_tvalue,uint16_tport);voidOUTL(uint32_tvalue,uint16_tport);uint8_tINB(uint16_tport);uint16_tINW(uint16_tport);uint32_tINL(uint16_tport);#endif /* __HWACCESS_X86_IO_H__ */