Add APB samples

docs/examples/amba/apb2sram.fl

@@ -0,0 +1,170 @@
+module apb2sram (apb: APB, sram: ! SRAMBus) {
+    fsm {
+
+        fork {
+            apb.read(addr, data);
+            sram.read(addr, data);
+        }
+
+        fork {
+            apb.write(addr, data);
+            sram.write(addr, data);
+        }
+    }
+}
+
+struct APB {
+    addr    :   int32;
+    rdata   : ! int32;
+    wdata   :   int32;
+    en      :   int1;
+    strb    :   int4;
+    ready   : ! int1;
+    write   :   int1;
+    sel     :   int1;
+}
+
+struct SRAM {
+    addr    :   int32;
+    rdata   : ! int32;
+    wdata   :   int32;
+    wen     :   int;
+}
+
+trans read (addr : int32, data : int32) on APB {
+    self.sel = 1;
+    self.en = 0;
+    self.write = 0;
+    self.addr = addr;
+    addr = self.addr;
+    clk;
+    self.en = 1;
+    self.ready = 1;
+    self.rdata = data;
+    while !self.ready { clk; }
+    data = self.rdata;
+    clk;
+}
+
+trans write (addr : int32, data : int32) on APB {
+    self.sel = 1;
+    self.en = 0;
+    self.write = 1;
+    self.wdata = data;
+    self.addr = addr;
+    self.strb = 15;
+    addr = self.addr;
+    data = self.wdata;
+    clk;
+    self.en = 1;
+    self.ready = 1;
+    while !self.ready { clk; }
+    clk;
+}
+
+# "Formal" description
+trans read (addr: int32, data: int32) on APB {
+    nop { clk; }
+    property self.sel == 1;
+    property self.en == 0;
+    property self.write == 0;
+    property self.addr == addr;
+    clk;
+    property self.en == 1;
+    nop { clk; }
+    property self.ready == 1;
+    property self.rdata == data;
+    clk;
+    release;
+}
+
+trans write (addr: int32, data: int32) on APB {
+    nop { clk; }
+    property self.sel == 1;
+    property self.en == 0;
+    property self.write == 1;
+    property self.addr == addr;
+    property self.wdata == data;
+    clk;
+    property self.en == 1;
+    nop { clk; }
+    property self.ready == 1;
+    clk;
+    release;
+}
+
+trans read (addr : int32, data : int32) on SRAM {
+    self.addr = addr;
+    addr = self.addr;
+    self.we = 0;
+    clk;
+    self.data = rdata;
+    data = self.rdata;
+}
+
+trans write (addr : int32, data : int32) on SRAM {
+    self.addr = addr;
+    addr = self.addr;
+    self.we = 1;
+    self.wdata = data;
+    data = self.wdata;
+    clk;
+}
+
+struct Reg<T> {
+    value: T,
+}
+
+tran set (value: const T) on Reg<T> {
+    let tmp = value;
+    clk;
+    self.value = tmp;
+}
+
+tran get (value: T) on Reg<T> {
+    value = self.value;
+}
+
+module MyMagicSRAM (bus: in SRAM) {
+    let words: [Reg<int32>; 1024];
+
+    fsm {
+        INITIAL: {
+            let addr;
+            let data;
+            with bus.read(addr, data) {
+                let tmp = addr;
+                clk;
+                data = words[tmp];
+            }
+            with bus.write(addr, data) {
+                let tmpA = addr;
+                let tmpD = data;
+                clk;
+                words[tmpA] = tmpD;
+            }
+            with epsilon { clk; }
+        }
+    }
+}
+
+# READ
+Req (Master):
+
+self.addr = addr;
+self.we = 0;
+clk;
+data = self.rdata;
+
+1. Assignments to outputs
+2. Reads from inputs
+
+Resp (Slave):
+
+addr = self.addr;
+self.we = 0;
+clk;
+data = self.rdata;
+
+1. Assignment to inputs
+2.

docs/examples/amba/apb_a.txt

@@ -0,0 +1,40 @@
+module MyMagicSRAM (
+	input  logic        clk,
+	input  logic        rst_n,
+	input  logic [31:0] bus_addr,
+	output logic [31:0] bus_rdata,
+	input  logic [31:0] bus_wdata,
+	input  logic        bus_wen
+);
+
+
+
+endmodule
+
+
+/*
+INITIAL:
+	-- bus.read  --> INITIAL (A)
+	-- bus.write --> INITIAL (B)
+
+INITIAL:
+	self.addr = addr;  (A)
+    addr = self.addr;  (A)
+    self.we = 0;       (A)
+    -> A2;             (A)
+A2:
+    self.data = rdata; (A)
+    data = self.rdata; (A)
+    -> INITIAL;        (A)
+
+INITIAL:
+    self.addr = addr;  (B)
+    addr = self.addr;  (B)
+    self.we = 1;       (B)
+    self.wdata = data; (B)
+    data = self.wdata; (B)
+	-> B2;             (B)
+B2:
+	-> INITIAL;        (B)
+
+*/

docs/examples/amba/apb_b.txt

@@ -0,0 +1,47 @@
+module MyMagicSRAM (
+	input  logic        clk,
+	input  logic        rst_n,
+	input  logic [31:0] bus_addr,
+	output logic [31:0] bus_rdata,
+	input  logic [31:0] bus_wdata,
+	input  logic        bus_wen
+);
+
+
+
+endmodule
+
+
+/*
+INITIAL:
+	-- bus.read  --> INITIAL (A)
+	-- bus.write --> INITIAL (B)
+
+---------------------------
+
+INITIAL:
+	self.addr = addrA;    (A)
+    addrA = self.addr;    (A)
+	let tmpA = addrA;     (A)
+    self.we = 0;          (A)
+    ---
+    dataA = words[tmpA];  (A)
+    self.rdata = dataA;   (A)
+    dataA = self.rdata;   (A)
+    -> INITIAL;           (A)
+
+---------------------------
+
+INITIAL:
+    self.addr = addrB;    (B)
+    addrB = self.addr;    (B)
+    let tmpAB = addrB;    (B)
+    self.we = 1;          (B)
+    self.wdata = dataB;   (B)
+    dataB = self.wdata;   (B)
+    let tmpDB = dataB;    (B)
+    ---
+    words[tmpAB] = tmpDB; (B)
+	-> INITIAL;           (B)
+
+*/

docs/examples/amba/apb_c.txt

@@ -0,0 +1,79 @@
+read_master {
+	sel <= 1;
+	en <= 0;
+	write <= 0;
+	addr <= @ADDR;
+	clk;
+	en <= 1;
+	while !ready { clk; }
+	let @DATA = rdata;
+	clk;
+	// sel  <= 0;
+	// en   <= 0;
+	// addr <= X;
+}
+
+write_master {
+	sel <= 1;
+	en <= 0;
+	write <= 1;
+	addr <= @ADDR;
+	wdata <= @DATA;
+	clk;
+	en <= 1;
+	while !ready { clk; }
+	clk;
+	// sel  <= 0;
+	// en   <= 0;
+	// addr <= X;
+}
+
+read_slave {
+	while sel != 1 && en != 0 && write != 0 { clk; }
+	let @ADDR = addr;
+	clk;
+	assert(en == 1);
+	ready <= 1;
+	rdata <= @DATA;
+	clk;
+	// ready <= 0;
+	// rdata <= X;
+}
+
+write_slave {
+	while sel != 1 && en != 0 && write != 1 { clk; }
+	let @ADDR = addr;
+	let @DATA = wdata;
+	clk;
+	assert(en == 1);
+	ready <= 1;
+	clk;
+	// ready <= 0;
+}
+
+rw_slave {
+	while sel != 1 && en != 0 { clk; }
+	let @ADDR = addr;
+	if write == 0 {}
+	if write == 1 {
+		let @DATA = wdata;
+	}
+	clk;
+	assert(en == 1);
+	ready <= 1;
+	if write == 0 {
+		rdata <= @DATA;
+	}
+	if write == 1 {}
+	clk;
+	// ready <= 0;
+	// rdata <= X;
+}
+
+read_monitor {
+	while sel != 1 && en != 0 && write != 0 { clk; }
+	clk;
+	assert(en == 1);
+	while !ready { clk; }
+	clk;
+}