arminbiere/aiger

AIGER And-Inverter-Graph Library

aiger's Issues

aigsim latch behavior

Consider the following aiger circuit system.aag:

aag 2 0 1 2 1
2 1
2
4
4 2 2
o0 latch
o1 and

Running ./aigsim system.aag -r 4 yields:

0  10 1
1  11 1
1  11 1
1  11 1
Trace is a witness for: { b0 b1 }

I would have expected that both outputs o0 and o1 are the same in each step. In particular, I would have expected that the output o0 is 0 in the first step. Is this the intended behavior of a latch or is this a bug of the aigsim tool?

Is there any way to take a random input?

aiger_read_literal: the situation end of file was ignored under the if-case <expected_followed_by == '\n'>

In aiger.c, the function aiger_read_literal reads literals one by one.
Under the if-case <expected_followed_by == '\n'>, when the input in the format of files, there can be no '\n' but only EOF identifier at the end of the file. Maybe the code should be modified (in ** **):

 if (expected_followed_by == '\n')
    {
      if (reader->ch != '\n' **&& reader->ch != EOF**)
	return aiger_error_usu (private,
		 "line %u: expected new line after %s %u",
		 reader->lineno_at_last_token_start, context, res);
}

Transforming some outputs into latches

Hi Armin,

Do you see an easy way of using/chaining the current binaries to transform some of the outputs of an aiger file into latches? It's an easy program, but just wanted to check with you before reinventing the wheel.

Cheers,
Guillermo

smvtoaig not working

I am not able to convert *.smv files.