一个用于操作顺序门和逆变门的python库。
py-aiger-bv的Python项目详细描述
<图>
<;figcaptiton>;pyaiger bv:操作pyaiger的扩展
顺序位矢量电路。<;/figcaption>;
<;/数字>;
目录
关于py aiger bv
这个库在
py-aiger。这是由
AIGBV
将输入、输出和锁存分组到
有序的序列(元组)。
安装
如果您只需要使用aigerbv
,您可以运行:
$ pip install py-aiger-bv
对于开发人员,请注意此项目使用 poetrypython包/依赖项 管理工具。请熟悉它,然后 运行:
$ poetry install
位向量表达式dsl
在py aiger中,当编写组合电路时, 电路dsl可能有些笨拙。对于这个常见的用例,我们有 开发了位向量表达式dsl。这个dsl实际上包括 用于有符号和无符号位向量的两个DSL。产生的所有电路 这种方式只有一个输出字。我们使用big endian编码 其中最有意义的数字是元组的第一个元素 代表这个词。对于有符号数字,使用2的补码。
importaigerbv# Create 16 bit variables.x,y=aigerbv.atom(16,'x',signed=True),aigerbv.atom(16,'y',signed=True)# bitwise ops.expr1=x&y# Bitwise and.expr2=x|y# Bitwise or.expr3=x^y# Bitwise xor.expr4=~x# Bitwise negation.# arithmeticexpr5=x+yexpr6=x-yexpr7=x<<yexpr8=x>>y# logical if unsigned, arithmetic if signed.expr9=-x# Arithmetic negation. Only defined for signed expr.expr10=abs(x)expr11=x@y# inner product of bitvectors mod 2 (+ is xor).# comparisonexpr12=x==yexpr13=x!=yexpr14=x<yexpr15=x<=yexpr16=x>yexpr17=x>=y# Atoms can be constants.expr18=x&aiger.atom(16,3)expr19=x&aiger.atom(16,0xff_12)# BitVector expressions can be concatenated.expr20=x.concat(y)# Particular bits can be indexed to create new expressions.expr21=x[1]# Single bit expressions can be repeated.expr22=x[1].repeat(10)# Switches can be implemented using ITE.test=aiger.atom(1,'test')expr23=aiger.ite(test,x,y)# x if test else y.# And you can inspect the AIGBV if needed.circ=x.aigbv# And you can inspect the AIG if needed.circ=x.aigbv.aig# And of course, you can get a BoolExpr from a single output aig.expr=aiger.UnsignedBVExpr(circ)
时序电路dsl
py aiger bv的顺序电路dsl实现了与 py aiger的时序电路dsl,但在(变量 长度)字级而不是位级。
importaigerimportaigerbvcirc=...# Create a circuit (see below).# We assume this circuit has word level# inputs: x,y, outputs: z, w, q, latches: a, bassertcirc.inputs=={'x','y'}assertcirc.outputs=={'z','w','q'}assertcirc.latches=={'a','b'}
顺序合成
circ3=circ1>>circ2
平行组合
circ3=circ1|circ2
添加反馈(插入延迟)
# Connect output y to input x with delay (initialized to True).# (Default initialization is False.)cir2=circ.feedback(inputs=['x'],outputs=['y'],initials=[True],keep_outputs=True)
重新标记
# Relabel input 'x' to 'z'.circ2=circ['i',{'x':'z'}]# Relabel output 'y' to 'w'.circ2=circ['o',{'y':'w'}]# Relabel latches 'l1' to 'l2'.circ2=circ['l',{'l1':'l2'}]
评估
# Combinatoric evaluation.circ(inputs={'x':(True,False,True),'y':(True,False)})# Sequential evaluation.circ.simulate([{'x':(True,False,True),'y':(True,False)},{'x':(False,False,True),'y':(False,False)},])# Simulation Coroutine.sim=circ.simulator()# Coroutinenext(sim)# Initializeprint(sim.send({'x':(True,False,True),'y':(True,False)}))print(sim.send({'x':(False,False,True),'y':(False,False)}))# Unrollcirc2=circ.unroll(steps=10,init=True)
aiger.aig到aiger.aigbv
# Create aigerbv.AIGERBV object from aiger.AIG object.circ=...# Some aiger.AIG objectword_circ=aigerbv.aig2aigbv(circ)# aigerbv.AIGBV object
小工具库
一般操作
# Copy outputs 'x' and 'y' to 'w1, w2' and 'z1, z2'.circ1=circ>>aigerbv.tee(wordlen=3,iomap={'x':('w1','w2'),'y':('z1','z2')})# Take 1 bit output, 'x', duplicate it 5 times, and group into# a single 5-length word output, 'y'.circ2=circ>>aigerbv.repeat(wordlen=5,input='x',output='z')# Reverse order of a word.circ3=circ>>aigerbv.reverse_gate(wordlen=5,input='x',output='z')# Sink and Source circuits (see encoding section for encoding details).## Always output binary encoding for 15. circ4=aigerbv.source(wordlen=4,value=15,name='x',signed=False)## Absorb output 'y'circ5=circ>>aigerbv.sink(wordlen=4,inputs=['y'])# Identity Gatecirc6=circ>>aigerbv.identity_gate(wordlen=3,input='x')# Combine/Concatenate wordscirc7=circ>>aigerbv.combine_gate(left_wordlen=3,left='x',right_wordlen=3,right='y',output='z')# Split wordscirc8=circ>>aigerbv.split_gate(input='x',left_wordlen=1,left='z',right_wordlen=2,right='w')# Select single index of circuit and make it a wordlen=1 output.circ9=circ>>aigerbv.index_gate(wordlen=3,idx=1,input='x',output='x1')
按位运算
aigerbv.bitwise_and(3, left='x', right='y', output='x&y')
aigerbv.bitwise_or(3, left='x', right='y', output='x|y')
aigerbv.bitwise_xor(3, left='x', right='y', output='x^y')
aigerbv.bitwise_negate(3, left='x', output='~x')
算术
aigerbv.add_gate(3, left='x', right='y', output='x+y')
aigerbv.subtract_gate_gate(3, left='x', right='y', output='x-y')
aigerbv.inc_gate(3, left='x', output='x+1')
aigerbv.dec_gate(3, left='x', output='x+1')
aigerbv.negate_gate(3, left='x', output='-x')
aigerbv.logical_right_shift(3, shift=1, input='x', output='x>>1')
aigerbv.arithmetic_right_shift(3, shift=1, input='x', output='x>>1')
aigerbv.left_shift(3, shift=1, input='x', output='x<<1')
比较
aigerbv.is_nonzero_gate(3, input='x', output='is_nonzero')
aigerbv.is_zero_gate(3, input='x', output='is_zero')
aigerbv.eq_gate(3, left='x', right='y', output='x=y')
aigerbv.ne_gate(3, left='x', right='y', output='x!=y')
aigerbv.unsigned_lt_gate(3, left='x', right='y', output='x<y')
aigerbv.unsigned_gt_gate(3, left='x', right='y', output='x>y')
aigerbv.unsigned_le_gate(3, left='x', right='y', output='x<=y')
aigerbv.unsigned_ge_gate(3, left='x', right='y', output='x>=y')
aigerbv.signed_lt_gate(3, left='x', right='y', output='x<y')
aigerbv.signed_gt_gate(3, left='x', right='y', output='x>y')
aigerbv.signed_le_gate(3, left='x', right='y', output='x<=y')
aigerbv.signed_ge_gate(3, left='x', right='y', output='x>=y')