# I2C target/register-control semantic benchmark
# Partially defined Boolean function for Design-from-Semantics experiments.
#
# Inputs:
#   rw        : 0=write transaction, 1=read transaction
#   reg[3:0]  : register address
#   busy      : transmit engine busy
#   rx_valid  : received write byte available
#   tx_ready  : read-data path ready (semantically irrelevant for these control strobes)
#   addr_hit  : I2C address matched this target
#   start     : valid transaction/control phase
#
# Register map:
#   0 STATUS      read
#   1 CONTROL     read/write
#   2 TXDATA      write
#   3 RXDATA      read
#   4 IRQ_STATUS  read
#   5 IRQ_MASK    read/write
#   6 IRQ_CLEAR   write
#   7 COMMAND     write/start_tx
#   8 RESET       write/soft_reset
#
# Only semantically meaningful target transactions are specified.
# Reserved registers, unmatched addresses, inactive phases, and selected
# state-dependent invalid combinations are omitted and thus unconstrained.

.i 5
.o 14
.ilb rw reg3 reg2 reg1 reg0
.ob ack nack rd_status rd_control rd_rxdata rd_irq_status rd_irq_mask wr_control wr_txdata wr_irq_mask clear_irq start_tx soft_reset consume_rx
.type fr
.p 16

# READ STATUS
10000 10100000000000
# READ CONTROL
10001 10010000000000
# READ RXDATA when rx_valid=1
10011 10001000000001
# READ IRQ_STATUS
10100 10000100000000
# READ IRQ_MASK
10101 10000010000000
# WRITE CONTROL when rx_valid=1
00001 10000001000001
# WRITE TXDATA when rx_valid=1
00010 10000000100001
# WRITE IRQ_MASK when rx_valid=1
00101 10000000010001
# WRITE IRQ_CLEAR when rx_valid=1
00110 10000000001001
# WRITE COMMAND/START_TX when busy=0 and rx_valid=1
00111 10000000000101
# WRITE RESET when rx_valid=1
01000 10000000000011
# WRITE STATUS is illegal
00000 01000000000000
# READ TXDATA is illegal
10010 01000000000000
# READ IRQ_CLEAR is illegal
10110 01000000000000
# READ COMMAND is illegal
10111 01000000000000
# READ RESET is illegal
11000 01000000000000

.e