Better testing infrastructure for sequential logic

[bgamari]

Currently writing testbench code in CLaSH is rather painful. For instance, I recently tried testing an AXI interface. AXI, like many protocols, uses a valid/ready handshake for transmission. This means that for my testbench to send a message to the device-under-test I need to wait for an acknowledgement, which may take a number of cycles. In Verilog I would usually write non-synthesizeable testbench like,

initial begin
  forever begin
    // place request on bus
    req_addr = 32'h42; req_valid = 1;
    // wait until acknowledgement
    @(posedge clk && resp_ready) 
    // place next request...

However, using CLaSH's simulate function I am forced to know the precise number of cycles I will need to wait. While this is an understandable consequence of the structure of the Signal type, it is nevertheless a rather bad regression from Verilog.

[bgamari]

Just to supply some inspiration, here is an example of the test bench that I would like to be able to write,

-- | A test plan for a component accepting inputs of type @i@ and outputs of type @o@
data TestM clk i o a 

-- | Feed the DUT an input, return the output that it produces.
tick :: i -> TestM clk i o o

-- | Feed the DUT the given input until it produces an output that satisfies
-- the given predicate.
tickUntil :: i -> (o -> Bool) -> TestM clk i o o

-- | A simple assertion
assert :: Bool -> String -> TestM clk i o ()

testIt :: TestM System (AxiIn 13 32) (AxiOut 13 32) ()
testIt = do
    tick defAxiIn  -- feed the DUT with an input
    tickUntil
        (defAxiIn & axiReadIn %~
               ( (arvalid .~ True)
               . (arid .~ TransId 1)
               . (araddr .~ 32)
               . (arlen  .~ 0)
               . (arsize .~ BurstSize 4)
               . (arburst .~ BurstIncr)))
        (view $ axiReadOut . arready)
    o <- tickUntil defAxiIn (view $ axiReadOut . rvalid)
    assertEqual "Data" 10 (o ^. axiReadOut . rdata)

Unfortunately, it's not at all clear how to implement such an interface in a safe way. You can approximate the desired semantics with some clever knot tying, but it's hard to preserve the property that tick gives you the output from cycle n on the nth invocation.

[christiaanb]

How about something like this?

data Test i o = Tick i | TickUntil i (o -> Bool) 

testMachineS plan curOutput = case plan of
  [] -> error "finished"
  Tick _:rest -> rest
  TickUntil _ f:rest -> if f curOutput then rest else plan

testMachineO plan = case plan of
  [] -> error "finished"
  Tick i:_ -> i
  TickUntil i _:_ -> i

testIt
  :: (Signal domain i -> Signal domain o)
  -- ^ Function to test
  -> [Test i o]
  -- ^ Plan
  -> [o]
testIt dut plan = sample o
  where
    o   = dut inp
    inp = moore testMachineS testMachineO plan o

[bgamari]

I'm quite fond of the idea of a monadic interface, at least in principle. Here is my attempt: https://git.smart-cactus.org/ben/clash-play/blob/master/TestM.hs.